A formalisation for the PGP protocol has been written as an MCRL2 model by Wytse Oortwijn from the VerCors team. You can find it here.