Computationally sound mechanized proofs for Diffie-Hellman key exchange protocols

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 publi...

Full description

Bibliographic Details
Main Authors: FENG Chao, ZHANG Quan, TANG Chao-jing
Format: Article
Language:zho
Published: Editorial Department of Journal on Communications 2011-01-01
Series:Tongxin xuebao
Subjects:
Online Access:http://www.joconline.com.cn/thesisDetails?columnId=74420087&Fpath=home&index=0