分布式网络环境下密码协议形式模型和安全性

Formal Model and Security Analysis for Cryptographic Protocols in the Distributed Network Environment

随着互联网的应用和发展,各种类型的安全协议,包括具有多个角色、多种密码运算的复杂密码协议,已广泛应用于分布式系统中解决各种安全需求.在大规模分布式网络环境下,参与协议运行的主体是大数量的甚至是动态的,密码协议运行环境极为复杂,这使得密码协议的安全性描述和分析变得非常复杂.引入了一个新的代数系统刻画具有多种密码运算的消息代数,并提出了一个新的密码协议模型,描述了无边界网络中的攻击模式,通过建立形式语言规范了无边界网络环境下密码协议的运行环境和安全性质 该协议模型描述了一种“协同攻击”模式,并讨论了密码协议的安全性分析约简技术,给出一个新的安全自动分析过程的简要描述.

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.