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

摘要

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