基于应用Pi演算的WTLS握手协议建模与分析

针对WTLS握手协议中的特殊密码原语,用等值理论定义了椭圆曲线DH密钥交换原语,用可信机构颁发数字证书的方式定义了数字证书原语。并在密码原语定义的基础上建立了WTLS握手协议的形式化模型,最后用Pro Verif工具分析了协议的秘密性和认证性。结果表明WTLS握手协议满足其安全性说明。

一种改进的IKEv2协议及其形式化验证

针对IKEv2协议在系统开销和发起方身份保护方面的不足,提出了一种改进协议的方案。新的协议采用基于超椭圆曲线的W eil对技术进行数字签名认证,并且首先认证响应方身份。通过该方案,改进后的协议降低了系统开销,实现了对发起方身份的主动保护。最后,基于应用pi演算的方法对协议进行了建模,并定义和分析了协议的安全属性。结果表明,改进后的协议具有更好的安全性和实用性。

密钥交换协议前向安全性的自动化分析

会话密钥的安全影响了整个通信网络的安全,前向安全性是密钥交换协议中保证会话密钥安全的一种特殊的安全属性。首先扩展了应用PI演算,增加了阶段进程语法描述协议的前向安全性;然后提出了一个基于一阶定理证明器Pro Verif的前向安全性自动化分析方法;最后运用这种方法分析了两种典型的密钥交换协议,STS协议和MTI协议的前向安全性,分析结果表明该方法简单可靠。

基于ProVerif的安全协议形式化分析与验证

形式化方法是分析与验证安全协议属性的强有力的工具。在对一阶定理证明器ProVerif深入研究的基础上,对简化的Needham-Schroeder认证协议进行了形式化分析。

基于符号模型的Mynah协议安全性自动化分析

Openflow是目前使用最为广泛的SDN通信协议,由于其协议规范还在不断完善,因此存在一定的安全隐患,对Openflow协议及其相关应用的安全分析也越来越受到重视。Mynah协议是在Openflow协议的基础上实现的安全认证协议。对Mynah协议的保密性和认证性进行分析,基于符号模型,利用应用PI演算对Mynah协议进行形式化建模,并使用安全协议分析工具Proverif进行自动化分析。结果表明,Mynah协议并不具备保密性和认证性,为此,给出了Mynah协议中不具备保密性和认证性的解决办法。