论文部分内容阅读
本文主要针对时态认知逻辑的模型检测问题进行了初步研究，研究成果体现在如下几方面：(1)论文首先对安全协议验证的形式化方法进行了概括和总结。并讨论了今后安全协议验证的一些研究方向。安全协议验证的形式化方法主要包括模型检测、定理证明、petri网方法、pi演算方法、csp(CommunicatingSequentialProcesses)方法和串空间方法等。从基本原理、方法及工具到在安全协议验证的应用等方面比较详细的讨论了计算机专家们在形式化方法方面所做的工作。(2)在SMV(SymbolicModelVerification)等模型检测工具的基础上，根据知识的语义和集合理论，提出了多智体系统时态认知逻辑模型检测方法。使SMV等模型检测工具的功能从时态逻辑扩展到时态认知逻辑。而时态认知逻辑己被广泛应用于分布式系统和协议的规范描述。本文也以TMN(MTatebayashi，NMatsuzaki，DBNewman)协议为例，探讨了该算法在安全协议验证方面的应用。(3)根据自动机理论和知识的语义，提出了“Onthefly”模型检测时态认知规范的算法，该算法在模型检测带有知识算子的时态规范时，往往只需产生系统的小部分状态空间，就能找到一个反例，从而实现“Onthefly”模型检测时态认知规范，且算法的时间复杂性是多项式时间的。算法也以TMN协议为例，探讨了该算法在安全协议验证方面的应用。(4)通过协议行为结构的定义，及对行为和行为结构的分析，提出了一种新的密码协议秘密性的验证算法，该算法的时间复杂度是多项式时间的。算法也以TMN协议为例，探讨了该算法在安全协议验证方面的应用。算法在普通微机上(CPU为1.8GHz,RAM为256MB)验证TMN协议和NS协议的秘密性只需不到1秒的时间。