安全协议的形式化验证技术研究

对安全协议形式化验证方法所应用的技术进行了研究，总结了当前安全协议的各种形式化验证方法的特点，指出今后一段时期内安全协议形式化验证技术的研究方向．     

基于π-演算的安全协议描述与验证

π-演算是以进程间移动通信为研究重点的并发理论，本文扼要叙述π-演算的基本概念，论述了如何用π-演算描述和验证安全协议，具体以Station-to-Station协议的一个不完全版本为例进行了分析，发现并在π-演算的工具MWB中证实了协议中存在的一个攻击，分析受到攻击的原因并给出了协议的改进版本．     

网络协议描述和验证技术的分析与比较

随着计算机网络与分布式系统的发展，通信协议的设计和实现的复杂性的增加导致了协议程技术的出现．讨论协议形式描述与验证技术的目的与方法，重点介绍了基于FMS、通信演算系统以及Petri网协议验证技术的特点及其优点．     

一种新的电子邮件协议及其形式化分析

在安全协议的形式化分析方法中,串空间模型和基于串空间模型的协议认证分析方法是比较常用的验证方法.分析了DKNRP协议存在一定的缺陷,并提出一种新的电子邮件协议,基于扩展的串空间模型采用认证测试方法,验证了新协议可以满足其安全目标.     

基于扩展的认证测试的改进迂回路由协议的安全分析

RFC3775文档中,迂回路由协议被用来保护从移动节点到通信节点的绑定更新．由于迂回路由协议存在诸多的安全漏洞,提出了一种改进的迂回路由协议,并用扩展的认证测试安全协议形式化方法分析了这种改进的迂回路由协议的安全性．分析结果显示,该协议的发起者和响应者能相互验证身份．     

IP Sec下安全关联协商的实现环境

IP Sec是IP协议层的安全体系结构，是构筑虚拟专网(Virtual Private Networks，VPNs)的基本规范；它是通过安全关联(Seeurity Association，SA)的约定和协商来实现对通信实体间通信过程的保护．目前，在该领域中尚有诸如IP Sec下安全关联的协商机制等问题有待进一步探讨．首先分析IP Sec安全关联及其协商的实现条件和相应的保护环境，即ISAKMP SA，然后讨论在IKE协议中协商ISAKMP SA过程存在的安全关联载荷认证缺陷，并以主模式下预共享密钥方式交换过程为例，针对该缺陷对IKE协议交换过程中验证参数的计算提出了改进方案．     

NetBill协议的形式化描述及分析

通过对安全协议验证的形式化需求分析,论证了形式化描述和分析是描述电子商务协议并验证它们属性的有效方法.介绍了一个扩展的BAN逻辑,基于这个逻辑对一种电子交易协议NetBill协议进行形式化描述,并在有入侵的情况下对该协议所期望的属性(安全、原子、隐私)进行了正确的分析,证明了该协议在有入侵者的情况下能够满足安全、原子和隐私等要求.     

一个基于模态逻辑的安全协议度量方法

为将量化分析方法引入安全协议分析中,以模态逻辑方法为基础定义了协议度量方法,并形式化地给出度量协议内容对协议安全目标满足度的参数和方法,同时在此基础上,进一步地给出了对安全协议冗余进行度量及化简的方法。应用该方法对实例协议进行分析,直接描述各协议内容的贡献度,显示冗余内容对目标实现的无效作用,从而可以安全化简。量化分析在安全协议形式化分析中的应用是本方法的主要特点,它具有模态逻辑方法的优点及缺陷。     

面向命题投影时序逻辑的安全协议模型检测

针对无条件安全通信协议,特别是Russian Cards协议的安全性验证问题,提出基于命题投影时序逻辑(PPTL)的模型检测方法.根据协议构造规则建立了Russian Cards协议的ProMeLa模型;利用chop算子将多个交互事件进行顺序复合,以表达协议所期望的通信序列;由projection算子定义了协议在该序列上的安全性质,再将该性质转为Never Claim语法结构并连同协议模型作为模型检测器SPIN的输入,以完成验证工作.验证结果表明,由协议规则构造的Russian Cards通信协议是安全可靠的,该方法也适用于一般的无条件安全通信协议的验证.     

无线网络认证密钥交换协议L-MAKEP的改进

L-MAKEP协议是一种适用于非对等的无线网络的高效的密钥交换协议,该协议具有执行简单且计算复杂度低的优点。分析对比三种攻击方法,表明协议不能抵抗伪造和欺骗攻击,并指出安全问题在于其中的异或运算和公钥身份信息性验证的缺失。因此,在Yang-Chen方案的基础上采用身份密码系统,以身份信息作为用户的公钥,并在等式验证公式中引入公钥身份信息,从而实现双方的身份信息验证。同时增加了哈希确认来对弱客户端进行确认。协议的分析表明,改进协议能够正确执行,同时其安全性得到提高。     

支持身份隐藏的EAP-PSK协议改进

鉴于身份隐藏这一安全新需求,在分析EAP-PSK协议的基础上,剖析EAP-SIM和EAP-TTLS认证身份保密的特点,提出一种支持身份隐藏机制的EAP-PSK改进方案,并在复杂性上与EAP-TTLS进行了比较.结果表明,新协议具有安全、简单、可行、与原协议兼容的优点,有一定的实用价值.     

一种新的安全协议设计方法

已有的安全协议往往被证实并不如它们的设计者所期望的那样安全,如何设计才能确保协议的安全性是目前研究的难点之一.通过介绍目前安全协议设计的主要思路和方法,说明了PDS系统的主要内容和方法,推导出了ISO-9798-3协议.     

RFID认证协议的安全性分析

针对RFID认证协议本身的安全性问题,分析了最近提出的几个协议的优缺点,给出了它们在一些安全特性上的比较,结果表明它们在某些方面都存在一些安全漏洞。通过对协议研究和分析,表明目前提出某些认证协议没有达到RFID系统的安全需求。只有通过更加有效的方法,才能设计出完全可靠、安全和高效的安全协议。     

一种改进的RC（3,7）安全协议

针对在无条件安全通信中,现有的俄罗斯纸牌协议在3个游戏者和7张纸牌的情况下（RC（3,7）协议）显著存在通信信息冗余的问题,提出一种消息构造算法和一组发送规则.首先计算最小信息集合,然后给出通信数据,最后通信方发送基于最小信息集的消息,这样就形成了一种改进的RC（3,7）协议.通过形式化推理的方式证明了新算法的有效性,在此基础上证明了新协议的有效性.为通信各方建立了博弈模型,并对模型的2种可能模式进行匹配,通过这种方式证明了该协议的安全性.结果表明：与原始协议比较,改进的RC（3,7）协议应用于身份认证具有更加安全、更少信息冗余等特点.     

基于攻击者的“角色冒充”的协议验证方法

网络的普及使得网络安全问题日益重要 ,协议的安全性和密码算法的安全性是网络数据安全的两个最基本的概念。介绍了几种具有代表性的安全协议的形式化验证工具 ,并提供了用 JAVA语言实现的基于攻击者和秘密的安全协议验证算法。提出了身份验证协议必须交换秘密的概念 ,还为协议的形式化验证过程设计了框架。实现的验证工具是证伪的     

基于SMV的安全协议建模及类型缺陷攻击发现

在分析安全协议模型的基础上,探讨了基于SMV工具的安全协议的建模及发现类型缺陷攻击的方法,对Otway-Rees协议的建模和分析表明,该方法对于发现类型缺陷攻击是有效的.     

eCK模型的安全性分析

认证密钥协商协议应该尽可能多地具备良好的安全性质以满足实际的需求。作为最近提出的一种设计和分析两方认证密钥协商协议的形式化方法,eCK模型正受到越来越多的关注,而其所能提供的确切安全保证值得深入探究。由此,对eCK模型定义和有关认证密钥协商协议基本良好安全性质之间的关系进行了详细分析。结论表明在eCK模型下可证明安全的认证密钥协商协议具备大多数基本的良好安全性质。据此总结了eCK模型的优势和不足。     

Enhancement in Ad hoc on Demand Distance Vector （AODV） Routing Protocol Security

IntroductionAs mobile ad hoc networks edge closer toward wide-spread deployment ,security issues have become a centralconcern and are increasingly i mportant . Due to thedecentralized nature of ad-hoc networks , securityrequirements are different from those of traditionalnetworks . Problems are caused for example by the weakphysical protection of the network nodes , the inherentinsecurity of the wireless communication channel , themobility of the nodes and their li mited processor andbattery r…     

基于SWIM卡公钥认证的二阶段握手加密套接层协议

根据普通智能手机移动接入时端端加密的安全需求，提出了一个基于SWIM卡公钥认证的二阶段握手加密套接层（SSL）改进协议．在握手的第1阶段，该协议由SWIM卡完成终端与网关之间基于公钥证书的身份认证，并产生、分发密钥材料．利用第1阶段的认证结果替代标准SSL握手协议的认证部分，利用第1阶段产生的共享密钥、随机数按照标准SSL密钥生成方法生成移动通信双方的会话密钥、初始化向量，进而完成第2阶段的握手SSL改进协议．所提协议的安全性通过了BAN的逻辑推理、证明，其适用性分析结果表明，在端端安全性、通信带宽效率变化、密码运算量和移动终端普适性等方面，它要比无线应用协议更适于移动应用的安全性需要，在相同的实验环境下，移动终端安全接入的时间也从3．5S缩短到1．5S．     

无线传感器网络中的一种安全高效的路由协议

针对无线传感器网络中部分路由协议在设计时对安全性考虑不够的问题，本文提出一种安全高效的路由协议-STEEN协议。该协议是在TEEN（Threshold sensitive Energy Efficient sensor Network protocol）路由协议的基础上，以增强路由安全性同时兼顾网络的能量消耗为目标而设计的。该协议通过预置密钥和采用随机密钥对密钥管理的方法，解决了节点间的认证和安全通信的问题，增强了网络的安全性。通过安全性分析可以看到，该安全路由协议可防御多种针对网络层的攻击。