基于事件逻辑的改进Needham-Schroeder协议安全性证明  

Security authentication of the modified Needham-Schroeder protocol based on logic of event

作　　者：刘欣倩 肖美华[1] 程道雷 梅映天 李伟[1] 

机构地区：[1]华东交通大学软件学院,江西南昌330013

出　　处：《计算机工程与科学》2015年第10期1850-1855,共6页Computer Engineering & Science

基　　金：国家自然科学基金资助项目(61163005);计算机软件新技术国家重点实验室开放课题资助项目(KFKT2012B18);江西省自然科学基金资助项目(20132BAB201033);江西省高校科技落地计划资助项目(KJLD13038);江西省对外科技合作技术资助项目(20151BDH80005);华东交通大学研究生创新计划资助项目(YC2014-X007)

摘　　要：安全协议是现代网络安全的基础,密码协议的安全性证明是一个挑战性的问题。事件逻辑是一种描述分布式系统中状态迁移的形式化方法,用于刻画安全协议的形式化描述,是定理证明的基础。用事件序语言、事件类和一个表示随机数、密钥、签名和密文的原子类,给出身份认证协议可以被形式化定义和强认证性证明理论。利用该理论对增加时间戳的Needham-Schroeder协议安全性进行证明,证明改进的Needham-Schroeder协议是安全的。此理论适用于类似复杂协议形式化分析与验证。Security protocols are the foundation of modern secure networked systems. Proving the security properties of cryptographic protocols is a challenge. Logic of event is a formal method for describing the state migration of a distributed system, which formally describes security protocols, and which is the basis of theorem proving. Using the language of event orderings, event classes, and a type of atoms representing random numbers, keys,signatures, and ciphertexts, we present a theory in which authentication protocols can be formally defined and strong authentication properties proven. The improved Needham-Schroeder protocol with time stamp, is proved to be of good security by our theory. The thoery can also be applied to formal analysis and verification of similar security protocols.

关 键 词：事件逻辑 改进的Needham-Schroeder协议 形式化方法 强认证性理论 

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