基于计算模型的安全协议验证软件Crypto Verif研究

CryptoVerif:A Prover Based on Computional Model for Security Protocol

目前,对安全协议的自动化证明分为两类:基于符号模型的和基于计算模型的。介绍了基于计算模型的协议证明软件CryptoVerif,介绍了其原理和可证明的安全属性,并使用其证明了一个协议的安全性;最后,指出其不足,为以后的软件改进指出了方向。

Now,mechanized provers to security protocol are divided in two classes：one base on the symbolic model and another based on computional model.This paper introduces and analyzes CryptoVerif based on the computional model,analyzes the principal and security properties to be proved by it,and uses it to prove the secrecy of a small protocol;in the end,tell the shortcome of the prover,show out the direction for study.