基于Spi演算的SSL3.0安全协议仿真分析

安全协议中的错误和漏洞很难完全由人工来发现，借助形式化方法对其进行分析可以保证安全协议的正确件和完整性。目前安全协议的形式化分析和验证已成为网络安全的研究热点，其中基于Spi演算的模型验证方法足当前的一个重要研究领域。文章介绍了SSL3．0安全协议的握手过程和Spi演算的基本概念，包括基于spi演算认证性的验证方法。存此基础上，基于spi演算形式化地建立了SSL3．0安全协议的仿真模型，给出了分析SSL3．0安全协议的详细过程，最终验证了SSL3．0安令协议的认证性。仿真分析的结果表明，Spi演算能够为安全协议的分析和验证提供可靠和有效的支持。     

基于Spi演算的安全协议验证

在安全协议的各种验证方法中,进程代数方法依托完善的进程演算理论得到了很好的应用.Spi演算在PI演算的基础上扩充了密码操作原语来刻画安全协议,并使用测试等价验证安全属性.讨论了利用Spi演算进行验证的过程,并对经典NSSK协议进行分析.     

利用CCS的协议描述与验证技术的研究

本文讨论的ＣＣＳ在协议描述与验证方面的应用技术和两个案例分析表明，通讯系统演算ＣＣＳ在协议描述、协议验证等方面有巨大应用潜力。     

一种基于π t演算的安全协议建模方法

安全协议模型是安全协议分析与验证的基础,现有的建模方法中存在着一些缺点,如:建模复杂、重用性差等.为此提出了一种类型化的π演算:πt演算,并给出了相应类型推理规则和求值规则,πt演算的安全性也得到了证明.πt演算可以对安全协议、协议攻击者进行形式化建模.基于πt演算的安全协议模型及其建模过程使用NRL协议为例做出了说明.同时给出了攻击者模型,并证明了基于πt演算的安全协议攻击者模型与D-Y攻击者模型在行动能力上是一致的.这保证了基于πt演算的安全协议模型的验证结果的正确性.基于πt演算的建模方法能在协议数据语义、协议参与者知识方面实现细致的描述.与同类方法相比,该方法可提供多种分析支持,具有更好的易用性、重用性.分析表明,该方法可以在建模中发现一定的安全协议漏洞.     

基于扩展Spi演算的IKEv2协议形式化分析与改进

安全性是新一代密钥交换协议的关键,而Spi演算是研究协议安全性的一种形式化方法,文中采用Spi演算研究了IKEv2协议的安全属性。针对Spi演算不能形式化定义Diffie-Hellman密钥交换和密钥生成的问题,扩展了Spi演算的语法和语义。基于扩展的Spi演算形式化分析了IKEv2协议,分析结果表明协议满足认证性和私密性,但不能保护相对重要的发起方身份。针对IKEv2协议的不足,提出了一种基于Weil对签名算法的改进方案。改进后的协议解决了发起方身份保护问题,具有更好的安全性。     

泛函程序设计语言实现中的图归约演算

本文叙述了在Ｖｏｎ Ｎｅｕｍａｎｎ机器上实现基于λ演算，ＳＫＩ演算的泛函程序设计语言所采用的图归约演算。ＳＫＩ－Ｇ演算是ＳＫＩ演算的图形表示，是基于图形的形式归约系统，面向机器实现，是实现高阶，引用透明，归约语义，全惰性泛函程序设计语言的主要技术基础。     

基于Spi演算的Kerberos认证协议形式化研究

网络安全已成为世人关注的问题，安全协议的形式化验证显得越来越重要，基于Spi演算的验证是一种很好的模型检测方法。我们介绍了Spi演算并扩展了两个基本原语，描述和验证Kerberos协议的认证性，同时指出了该协议的不足之处，最后分析了基于Spi演算的形式化研究的今后发展方向。     

基于类pi演算的电子支付协议安全性形式化研究*

设计一个满足安全需求的协议非常困难,并且极易出错,因此利用形式化方法来检验安全协议引起了人们极大的关注。使用了类pi演算来验证电子支付协议的认证性和匿名性。     

基于进程演算和知识推理的安全协议形式化分析

安全协议的形式化分析是当前安全协议研究的热点,如何扩充现在已经成熟的理论和方法去研究更多的安全性质,使同一系统中各种安全性质在统一的框架下进行分析和验证是一个亟待解决的问题.进程演算是一强有力的并发系统建模工具,而结合知识推理可以弥补进程演算固有的缺乏数据结构支持的特点,以此提出了一个安全协议形式化分析的一般模型.基于此模型,形式化地定义了一些安全性质,给出了一个实例研究,并指出了进一步完善此模型的研究方向.     

C2P:基于Pi演算的协议C代码形式化抽象方法和工具

形式化方法为安全协议分析提供了理论工具,但经过形式化验证过的协议标准在转换为具体程序实现时可能无法满足相应的安全属性.为此,提出了一种检测安全协议代码语义逻辑错误的形式化验证方法.通过将协议C源码自动化抽象为Pi演算模型,基于Pi演算模型对协议安全属性形式化验证.最后,给出了方案转换的正确性证明,并通过对Kerberos协议实例代码验证表明方法的有效性.根据该方案实现了自动化模型抽象工具C2P与成熟的协议验证工具ProVerif结合,能够为协议开发者或测试人员检测代码中的语义逻辑错误提供帮助.     

基于Spi演算的SSL3.0协议安全性分析

对标准Spi演算的语法及语义进行了合理扩展,并利用扩展后的Spi演算对大型复杂协议SSL V3.0的安全性进行了形式化分析,得出了与其他分析方法相同的结论。     

基于逻辑编程的EKE协议分析

基于逻辑编程规则及Spi演算提出了一种验证密码协议安全性的新方法，利用该方法可以对密码协议的安全性质以程序化的方式进行验证。通过对EKE协议进行的分析，不但证明了协议已知的漏洞，而且发现了针对EKE协议的一个新的攻击——并行会话攻击。很好地验证了该新方法对密码协议的分析能力。     

基于Spi演算的密码协议的控制流分析

基于Spi演算和控制流分析，提出了一个密码协议的新分析方法。随后利用该方法对Beller-Chang-Yacobi MSR协议进行了分析，通过证明该协议已知的漏洞，说明该方法是正确的，并通过更深入的研究和分析，证明了该协议在并行会话攻击下是不安全的，基于此对该协议进一步改进，改进后的协议是安全的。     

基于图元的事件图生成算法

与单轮运行情形不同，多轮并发运行的密码协议存在更为复杂的安全性问题。并发运行密码协议的形式化分析对象包括密码协议的多轮并发运行和多个密码协议的并发运行两种情形，且二者具有统一的形式化模型。基于扩展的串空间模型和Spi演算理论，提出用于并发运行密码协议安全属性验证的事件图模型。图元是事件图的构造单元，它满足消息事件之间的通信关系和前驱关系约束以及消息语句的新鲜性约束。定义消息事件之间、图元之间以及消息事件和图元之间的前缀、组合和选择运算，并给出事件图生成算法。     

一种基于扩展Spi演算的类型系统

主要探讨了使用非形式化的原理和形式化的规则来获得密码协议安全属性的方法。这些原理和规则基于传统的等级和信息流的思想，通过将其扩展后用来处理密码协议中的并发进程。提出的规则是基于Spi演算扩展语法的一种类型规则。通过这些规则可以向用户担保．如果协议通过了类型检测，则该协议没有泄漏任何秘密的消息。     

A Calculus for Cryptographic Protocols: The Spi Calculus

We introduce the spi calculus, an extension of the pi calculus designed for describing and analyzing cryptographic protocols. We show how to use the spi calculus, particularly for studying authentication protocols. The pi calculus (without extension) suffices for some abstract protocols; the spi calculus enables us to consider cryptographic issues in more detail. We represent protocols as processes in the spi calculus and state their security properties in terms of coarse-grained notions of protocol equivalence.     

基于概率多项式时间进程的安全协议分析

针对Spi演算在安全协议分析中存在的局限性，通过引入概率多项式时间进程，提出一个分析安全协议的新方法。该方法是对Spi演算的改进，在该方法中攻击者是概率多项式时间进程，协议的安全性用概率可观察等价性表示。通过对一个基于ElGamal加密和Diffie-Hellman的密钥交换协议分析，证明了该方法的可行性和有效性。     

新的域间身份认证协议及其形式化验证

Internet上不同的安全域间要实现信息资源的安全访问首先需要认证.目前常用的认证协议是Kerberos协议,但在网络环境下,该协议无法对真实的客户端进行认证.因此,给出了新的域间身份认证协议以及相应的"现时"产生方案,并利用改进的Spi演算对所设计的认证协议进行了分析,证明了该协议的安全性,能够有效地解决网间的信息安全传输.     

基于可达关系的安全协议保密性分析

借助形式化的方法或工具分析安全协议是非常必要而且行之有效的.进程演算具有强大的描述能力和严格的语义,能够精确刻画安全协议中各个参与者之间的交互行为.作者以进程演算为基础,嵌入消息推理系统以弥补进程演算固有的缺乏数据结构支持的特点,尝试地提出了一个基于可达关系的安全协议保密性分析模型.基于此模型,形式化地描述了安全协议的保密性,证明了一定限制条件下的可判定性.并且以TMN协议为例,给出了该模型的实例研究.