符号化模型检测网络安全协议

摘  要

简要回顾了形式化方法的发展历程,阐述了形式化分析的定义、方法、重要性及主要研究内容,讨论了形式规约语言与方法,以及演绎证明和模型检测等形式化验证方法。
密码协议安全性的分析是网络安全的1个难题,运用形式化方法对密码协议进行分析1直是该领域的研究热点；本文以1个实例阐述运用模型检测工具ＳＭＶ对ＴＭＮ密码协议进行形式分析,在建立1个有限状态系统模型和刻画ＴＭＮ密码协议安全性质的基础上,发现了1些新的攻击。
着重分析了模型检测技术和逻辑推证技术的优点和不足,并在此基础上提出了1种混合形式化技术的说明,该技术可提供更为完全的安全协议形式化分析。
关键字：形式化分析；SMV模型；模型检测；逻辑推证；混合分析技术。

Abstract

  This paper presents the definition and importance of formal methods after simply looking back on the history of formal methods, and provides an overview of formal methods. Discusses specification languages (methods) and verification methods that include deductive proving and model checking.
It is a hard problem in area of computer network security to analyze cryptographic protocols. Using formal methods to analyze cryptographic protocols remains the key issue in this field. In this paper, a methodology is presented by using a model checker of formal methods, SMV, to analyze the TMN cryptographic protocol. After building a finite state system of the protocol and describing the security property of the protocol, SMV is used to discover some new attacks upon TMN cryptographic protocol.
The advantages and disadvantages of model checking technology and logic reasoning technology is analyzed, Based on it, the author gives a specification of new mixed technology of the two technologies which can provide a more complete formal analysis of security protocols. （转载自科教范文网http://fw.nseac.com）
Key words：  formal analysis; SMV; model checking; logic reasoning technology; mixed formal analysis technology.

注释：不含源代码