一种多项式时间复杂度的密码协议秘密性验证方法

密码协议的秘密性验证是网络安全领域的一个难题,本文在提出协议行为结构的基础上,通过对协议行为及其结构的分析,提出了一种新的密码协议的秘密性验证算法,该算法的时间复杂度是多项式时间的,从而简化了秘密性验证过程,文中最后,作为实例,给出了TMN密码协议的秘密性验证。     

基于面向对象时间Petri网的密码协议分析

利用面向对象技术和时间Petri网的优点,提出一种基于面向对象时间Petri网的密码协议分析方法。该方法可以降低建模复杂性和计算复杂性,提高建模效率,实现时间Petri网的高度模块化,能更好地适应密码协议分析过程中的重组和扩充。实例分析结果证明了该方法的有效性。     

密码协议验证中的Petri网方法

如何验证密码协议的安全性是一个复杂的问题,只有形式化的验证方法才能证明密码协议的绝对正确.利用Petri网给出了一种用于密码协议验证的形式化方法.在合理假设的基础上,区分合法用户与攻击者在执行协议时的前提条件,列出执行协议后的结果,在此基础上建立了攻击者的Petri网模型.最后,用这种方法对NSPK协议进行了验证,证明了最初的NSPK协议中存在一个安全问题,而改进的NSPK协议则消除了这个问题.证明了这种方法的有效性.     

基于有色Petri网的一种密码协议的描述和分析

Petri网作为一种数学工具,已被广泛应用于过程的描述、分析和验证。文章使用有色Petri网对文献[1]中提到的一种密码协议进行描述和分析,发现并验证该协议的安全缺陷。     

基于时延Petri网的密码协议分析及性能评估

形式化分析方法由于其精炼、简洁和无二义性逐步成为分析密码协议的一条可靠和准确的途径，但是密码协议的形式化分析研究目前还不够深入，针对这一现状，该文提出用时延Petri网来表示和分析密码协议。该模型不但能够反映协议的静态和动态的特性，而且能够对密码协议进行时间、空间上的性能评估。作为实例，文章对MSR无线协议作了详细的形式分析和性能评估。最后，与其它形式化分析密码协议的方法作了比较。     

基于Petri网的安全电子交易协议描述与分析

对密码协议模型进行了分析，引入时延Petri网分析工具，建立了一种新的安全电子交易协议的形式描述工具。利用该分析工具对安全电子交易协议中的支付部分进行了形式描述，并分析了它的安全等问题。     

基于Petri网的密码协议形式化建模

密码协议是安全共享网络资源的机制和规范,是构建网络安全环境的基石,其安全性对整个网络环境的安全起着至关重要的作用。提出了采用Colored Petri Nets(CPN,着色Petri网)分析密码协议的新方法。采用新方法对TMN协议的多次并发会话通信进行形式化建模,模型依据会话配置和会话顺序进行功能单元划分,采用on-the-fly方法生成攻击路径。采用状态空间搜索技术,发现了该协议的多次并发会话不安全状态,并获得了新的攻击模式。     

一种兼顾协议正确性验证和性能评估的Petri网方法

基于Petri网的协议形式化分析方法由于其精炼、简洁和无二义性逐步成为分析协议的一条可靠和准确的途径,但是协议的形式化分析目前研究还不够深入,协议分析的两个重点内容正确性验证和性能评估所需要的模型不同,一种模型只能解决一方面的工作。为了有效地解决这一问题,文中提出了一种用原型Petri网作为协议验证模型的思路和方法,在不改变原型Petri网结构的基础上对变迁赋予发生时延,解决了协议的性能评估问题。本文还给出了协议验证内容与Petri网分析方法的对应关系,并对0-1停止等待协议进行了详细的分析,最后把0-1停止等待协议的原型Petri网模型转化为时延Petri网,对协议的性能进行了评估。     

改进型有色Petri网的安全协议分析

利用有色Petri网分析安全协议时存在空间爆炸问题,对此提出了构建入侵者成功攻击安全协议所需知识集RI与入侵者可以获得的知识集KI,并定义入侵成功函数的改进型有色Petri网。利用改进型有色Petri网对具体的Helsinki协议和TMN协议进行了分析。实验表明,该方法能大大简化带有入侵者的Petri网模型的构造过程,有效缓解了Petri网在分析安全协议时的空间爆炸问题。     

一种新的基于有色Petri网的安全协议建模方法

密码协议安全性的分析是网络安全的一个难题，运用形式化方法对密码协议进行分析一直是该领域的研究热点。本文提出了一种新的基于有色Petri网的安全协议建模方法，并以TMN密码协议为例，说明了这一方法的建模过程。     

一种基于Petri网的安全协议验证方法

安全协议是实现网络安全的关键,如何验证安全协议的安全性是一个非常重要的工作。论文提出一种基于着色Petri网的安全协议形式化描述与安全验证方法,此方法建立在逆向状态分析和着色petri网可达性矩阵的基础之上,并采用具体协议来验证该方法的有效性。     

设计密码协议的若干原则与方法

传统的密码协议设计主要考虑理想环境下运行的安全性。为了设计实用安全的密码协议,首先对理想环境下密码协议中存在的主要攻击进行研究和总结,提出四条协议设计原则,以避免常见的设计缺陷;然后通过对消息完整性的研究,提出一种协议转换算法,可将理想环境下安全的密码协议转换为现实环境下安全的密码协议,并证明算法的安全性。该转换算法的提出,有助于设计在现实环境下运行安全的密码协议。     

有色Petri网的一种密码协议建模分析

密码协议是任何安全系统的基础,对它的设计越来越受到广大用户的关注.本文详细论述了文献[1]提到的一种密码协议,并使用有色Petri网对该协议建模分析,说明该设计的正确性.     

TMN密码协议的SMV分析

密码协议安全性的分析是网络安全的一个难题，运用形式方法对密码协议进行分析一直是该领域的研究热点。运用模型检测工具SMV对TMN密码协议进行了形式分析。在建立一个有限状态系统模型和刻画TMN密码协议安全性质的基础上，使用SMV对TMN密码协议进行了安全分析。分析结果表明TMN密码协议存在一些未被发现的新攻击。     

Algebra model and security analysis for cryptographic protocols

With the rapid growth of the Internet and the World Wide Web a large number of cryptographic protocols have been deployed in distributed systems for various application requirements, and security problems of distributed systems have become very important issues. There are some natural problems: does the protocol have the right properties as dictated by the requirements of the system? Is it still secure that multiple secure cryptographic protocols are concurrently executed? How shall we analy…     

基于CCS的加密协议分析

加密协议的分析需要形式化的方法和工具.该文定义了加密协议描述语言PEP (principals+environment=protocol),并说明对于一类加密协议,其PEP描述可以转化为有穷的基本CCS进程,由此可以在基于CCS的CWB(concurrency workbench)工具中分析加密协议的性质.此方法的优点在于隐式地刻画攻击者的行为,试图通过模型检查(model checking)发现协议潜在的安全漏洞,找到攻击协议的途径.