A computationally observational equivalence model for the Diffe-Hellman key agreement primitive was pro-posed and the soundness of the model was proved.Compared with prior works

this model can extend the power of the mechanized prover CryptoVerif directly.When applying the model to proving the public-key Kerberos

the deficiency of the adversary’s capability was uncovered and an enhanced model for the adversary was presented.The model was vali-dated by verifying the public-key Kerberos in Diffie-Hellman mode with CryptoVerif automatically.Being different from current approaches

the verification procedure is both automatic and computationally sound.