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

安全协议是现代网络安全的基础,密码协议的安全性证明是一个挑战性的问题。事件逻辑是一种描述分布式系统中状态迁移的形式化方法,用于刻画安全协议的形式化描述,是定理证明的基础。用事件序语言、事件类和一个表示随机数、密钥、签名和密文的原子类,给出身份认证协议可以被形式化定义和强认证性证明理论。利用该理论对增加时间戳的Needham-Schroeder协议安全性进行证明,证明改进的Needham-Schroeder协议是安全的。此理论适用于类似复杂协议形式化分析与验证。

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

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.