关键词: 密码协议, 逻辑分析, 重放攻击

Abstract:

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.

Key words: cryptographic protocol, formal method, information security, algebra system