基于BAN逻辑的协议分析往往容易忽略密码协议潜在的“重放攻击”漏洞,为解决这一问题,对BAN逻辑分析的新消息判断法则逻辑公设作了一点改进.从而降低了BAN逻辑分析的误导性.

Due to the rapid growth of the Internet applications, varied cryptographic protocols, including thses complex protocols with many roles and many cryptographic primitives, have been widely used to achieved various secure requirements in the distributed system. In the large distributed network environment, due to the maximum number of participants involved and the complexcity of run conditions of the protocol, the security characterzation and analysis for protocols is very difficult and complicated. In this paper, we introduce a new algebra system called Cryptographic Protocol Algebra(CPA) that characterizes the algebraic properties of messages involved in the protocol with multiple cryptographic operations. Based on CPA, we propose a new formal model for general cryptographic protocols. And we specify run conditions and security properties of cryptographic protocols in the unbounded network environment by building a formal language. Based on our model, we characterize a coordinated attack mode to protocols, and discuss reduction techniques for the protocol security analysis. Finally we briefly describe a new automatic analysis process for cryptographic protocols.