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

CryptoVerif:A Prover Based on Computional Model for Security Protocol

作　　者：李林[1] 

机构地区：[1]中南民族大学计算机学院,湖北武汉430074

出　　处：《软件导刊》2011年第4期140-142,共3页Software Guide

摘　　要：目前,对安全协议的自动化证明分为两类:基于符号模型的和基于计算模型的。介绍了基于计算模型的协议证明软件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.

关 键 词：安全协议 计算模型 CryptoVerif 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]