基于时序逻辑的加密协议分析  

Analyzing Encryption Protocols Based on Temporal Logic

作　　者：肖德琴[1] 周权[2] 张焕国[3] 刘才兴[4] 

机构地区：[1]中国科学院研究生院信息安全国家重点实验室,北京100080 [2]广州大学理学院数学系信息安全研究所,广州510405 [3]武汉大学计算机学院软件工程国家重点实验室,武汉430072 [4]华南农业大学理学院计算机系,广州510642

出　　处：《计算机学报》2002年第10期1083-1089,共7页Chinese Journal of Computers

基　　金：国家自然科学基金 ( 199310 10 ;6 6 9730 34);中国科学院研究生院信息安全国家重点实验室课题资助

摘　　要：形式化方法由于其精炼、简洁和无二义性 ,逐步成为分析加密协议的一条可靠和准确的途径 ,但是加密协议的形式化分析研究目前还不够深入 ,至今仍没有统一的加密协议验证体系 .针对这一现状 ,该文从加密协议可能面临的最强大的攻击着手 ,提出了一种基于时序逻辑的加密协议描述方法 ,在该模型下 ,对协议行为、入侵者行为、安全需求等特性的描述均用时序逻辑公式表达 ,从而利用现有的统一的时序逻辑框架分析密码协议的性质 .特别地 ,作者描述和检测了一个系统入侵者不能用任何代数和逻辑的办法获得消息的实例 .通过对比 ,作者认为该方法具有形式化程度较高的特点 .In order to develope a unified theory to verify encryption protocols. This paper provided a way to describe encryption protocols based on temporal logic from the main weakness and threats to encryption protocols. The protocol's actions,the intruder's actions and correctness requirements can be specified using temporal formulas under this model. All this analysis is specified according to standard safety properties,for which standard temporal logic proof techniques apply. In particular, authors model an encryption protocol where the intruder cannot obtain plaintexts by any logical or algebraic techniques. Comparing with relevant ones, it is a better formal way to describe encryption protocols. This scheme can be used widely,not only in analyzing traditional cryptosystem's,but also in describing public key cryptosystem's. In addition,it can also analyze other characteristics,such as the characteristics of fault-tolerance and no key to be reused.

关 键 词：时序逻辑 加密协议分析 形式化方法 密码学 单钥加密系统 

分 类 号：TN918.1[电子电信—通信与信息系统]