关键词: 密码协议, 形式化分析, 定理证明, 模型检测, 前推

Abstract: In the highly informative society, cryptographic protocols are necessary techniques to ensure the security of many applications in networks. As flaws of cryptographic protocols will bring serious security problems to the cyberspace application, and even cause the immeasurable loss, formal analysis of the cryptographic protocols become an important issue. Formal analysis method is the most reliable and effective method, in which theorem proving method and the model checking method to be widely used as formal analysis method with proving. In these methods, analysts have to enumerate the security properties at first, and then prove or check whether the cryptographic protocol satisfies these security properties. However, if not all the security properties have been enumerated before formal analysis, some flaws will be missing. As an alternative way, formal analysis method with reasoning for cryptographic protocols do not need to enumerate security properties but perform forward reasoning to find out flaws. This paper presents a concrete formal analysis method with reasoning. We formalize cryptographic protocols and intruder’s behaviors according to the features of cryptographic protocols, then perform forward reasoning with the results of formalization. At last, we find out flaws by analyzing the result of forward reasoning.