移动微支付协议Payword的改进与形式化分析

针对移动微支付协议Payword不满足不可否认性的问题,提出了改进的移动微支付协议Payword。相比Payowrd,改进的Payword具有更好的安全性和公平性。为验证改进的移动微支付协议Payword能否满足不可否认性,对SVO逻辑进行扩展,并运用扩展后的SVO逻辑对改进的Payword微支付协议进行形式化分析。分析结果表明,改进后的微支付协议满足不可否认性。     

非否认协议中认证保密性的设计与形式化分析

探讨了非否认协议的保密性认证目标,用攻击的方法验证了A(0)协议在认证保密性方面的不足;对其消息格式和会话密钥建立后确认方式做了修改,提出了NA(0)协议;进一步运用SVO逻辑对NA(0)协议进行了形式化的分析,验证了NA(0)协议满足主体身份的认证性和会话密钥的保密性.     

电子邮件协议的非否认性形式化分析

非否认性是考量电子商务协议的重要方面。SVO逻辑以其简洁的特点在协议的安全性验证方面被广泛应用。本文通过对SVO逻辑分析推理规则进行扩展,将其运用到对电子商务协议的非否认性的验证上,对CMP1进行了形式化分析。形式化分析的结果表明CMP1满足非否认性。     

轻量级移动支付协议LMPP的安全性分析与改进

无线网络以及各种智能设备的兴起,使得移动支付越来越重要,因此必须采用安全的轻量级移动支付协议（Lightweight Mobile Payment Protocol,LMPP）来保障移动支付的顺利进行。针对资源有限的移动设备及环境受限的支付场景,选取以移动运营商（Mobile Network Operator,MNO）为价值链的轻量级的隐私保护移动支付协议为研究对象。采用SVO逻辑形式化分析协议,证明协议不满足公平性。并对LMPP协议其他安全属性进行分析,针对协议不满足公平性的部分做出改进。同时运用SPIN模型检测工具进行检测,验证结果表明,改进后的协议满足公平性。     

基于扩展SVO逻辑的身份认证协议在军事通信中的应用

军事通信中,移动终端的身份认证是一个重要的问题,为了降低通信中移动端的计算量,移动设备的身份认证协议采用哈希函数代替签名机制进行身份认证.而形式化分析的SVO逻辑方法没有适用于哈希函数进行身份认证的逻辑语法,本文采用扩展SVO逻辑方法,实现一个基于扩展SVO逻辑方法的移动通信中可相互认证的实体认证协议,协议经过验证证明有较好的可适用性.     

基于改进语义SVO逻辑的二维认证协议分析

一种基于二维几何距离的实体认证协议无需在非安全信道当中传送密钥,使得认证的过程更加安全与便捷,然而该协议的正确性与安全性并未得到严格论证。考虑该实体认证协议的特点,采用改进语义的SVO逻辑对其进行合理性描述,并对其运行过程进行形式化的具体分析,发现该协议在认证过程中存在着双方认证不确定的缺陷。针对此缺陷提出了一种修正方案,以确保认证协议的正确性,并且通过改进语义SVO逻辑的形式化分析证明了该改进认证协议的安全性。     

Netbill协议原子性的符号模型检验分析

电子商务协议的安全性和原子性是电子商务研究者和使用者广泛关心的问题,采取一定的方法对协议进行分析检验是协议开发过程中一个必要环节。论文在对Netbill协议及其原子性进行形式化描述的基础上,基于符号模型检验器(SMV)从钱原子性和商品原子性两个角度对Netbill协议进行了分析和检验,从而表明了用SMV对电子商务协议分析和验证的可行性。     

基于攻击者行为能力的SVO协议分析

SVO原逻辑不适用于证明基于证书的认证与密钥交换协议安全性问题。为此,提出2个SVO逻辑相关公理,对证书真实性与会话密钥安全性进行判断及验证,并结合Dolev-Yao安全模型,从攻击者行为能力的角度评估密码协议的安全性。经分析证明Mangipudi协议未能提供前向安全且存在假冒攻击的安全缺陷,因此给出一个在Dolev-Yao安全模型下可证明安全的解决方案。     

改进的可证安全的相互认证及密钥协商方法

提出一种新的用于移动通信的相互认证和密钥协商方法——NMAKAP。NMAKAP采用基于阿贝尔群的模幂运算和散列函数进行身份认证,取代了传统公钥密码算法和数字签名方案,降低了协议的计算开销和实现成本。在SVO逻辑系统证明下,NMAKAP协议是安全的。SVO逻辑是安全协议形式化分析的一种重要方法,文章扩展了SVO逻辑分析散列函数的逻辑语法。SVO逻辑方法的认证目标被发现存在中间人攻击,为此提出了新的认证目标,并分析了新目标的安全性。分析了一种可用于移动通信的认证协议——MAKEP。MAKEP协议通过预计算,大大降低了移动设备的计算量,但被认为存在Hijacking攻击。分析表明针对原MAKEP协议的Hijacking攻击并不成立,但该协议被发现存在未知共享密钥攻击,为此提出了改进意见。     

不可否认协议时限性的形式化分析

虽然SVO逻辑由于其简单性在对不可否认协议的形式化分析中得到了广泛的应用,但它在时间描述能力上的不足使得它无法分析不可否认协议的时限性.通过向SVO逻辑添加一种简单的时间表达和分析方法扩展了SVO逻辑,并使用扩展后的逻辑对Zhou和Gollmann于1996年提出的一个公平不可否认协议及其一个改进协议进行了分析.分析结果表明,原协议不具有时限性,而改进协议具有时限性,因此也说明了扩展后的新逻辑能够分析不可否认协议的时限性.另外,新逻辑还能用来分析一般密码协议中的时间相关性质.     

SaaS模式下新型认证方案的设计与分析

针对软件即服务(SaaS)应用系统下认证协议的应用及安全性问题,提出一种新型认证方案。通过加密用户口令,将散列结果传输到网络上,只有服务器私钥才能解密,从而实现客户端及服务器双向认证一次性口令技术,提高认证系统的安全性。采用SVO逻辑对该协议进行形式化分析,结果验证了其安全性。     

基于双线性对的WSN密钥协商和认证协议

无线传感器网络(WSN)节点在电源、计算能力和内存容量等方面存在局限性,且面临的安全威胁更复杂。为此,提出一种适用于类LEACH路由的WSN密钥协商和认证协议。通过引入当前轮数,实现节点间的双向身份认证,以抵御选择性转发、Sybil和Hello泛洪等常见攻击。利用ID和双线性对原理生成节点间的动态会话密钥,从而减少节点间的交互步骤,降低能耗。SVO逻辑推理和性能分析结果表明,该协议同时满足安全性要求和WSN的特殊应用要求。     

模态逻辑与带变量串空间相结合的协议分析

在传统的串空间基础上引入带变量的串空间模型,对于未确定的消息项或其子项用变量表示,允许变量出现在消息项及其演算中,协议由参与协议运行的不同主体的带变量的串组成。以协议运行的迹语义为模型,提出了一个用于推理协议主体的各种行为的模态逻辑系统,给出了该逻辑的语法、公理及推理规则。基本的模态公式 表示主体A完成动作P, 是相应的结果,通过主体行为的各种组合并绑定相应逻辑公式,最终推断安全协议的秘密性和可鉴别性。用该方法分析Helsinki协议,能发现其中的安全漏洞Horng-Hsu攻击。     

适用于无线体域网的动态口令认证协议

无线体域网中传输的是与生命高度相关的敏感数据，身份认证是信息安全保护的第一道防线。现有的基于人体生物信息的身份认证方案存在信息难提取、偶然性大和误差性大的问题，基于传统密码学的认证方案需较大计算资源和能量消耗，并不适用于无线体域网环境。为此，在动态口令和非对称加密机制基础上，提出一种适用于无线体域网的动态口令双向认证轻量协议，并对其进行形式化分析。通过理论证明、SVO逻辑推理及SPIN模型检测得出：该协议满足双向认证，且能够抵御重放攻击、伪装攻击、拒绝服务器攻击和口令离线攻击，具有较高安全性。     

一种网络间可信连接协议

为了解决深化“互联网+先进制造业”进程中网络可信互连问题，引入了可信连接架构（trusted connect architecture，简称TCA）技术.基于TCA技术思想，针对网络间可信认证需求，设计了一种支持网络间互连的可信连接协议（TCA-SNI）.引入了网络间双向认证过程，给出了TCA-SNI协议的交互过程；使用扩展的SVO逻辑系统对协议进行逻辑推理，证明该协议是安全可靠的；使用Dolev-Yao攻击者模型对协议进行攻击测试，实验结果表明，协议的安全目标均已达成，证明该协议可以抵御真实网络中的攻击.     

普适环境下的一种跨域认证机制

由于普适计算的高度移动性,通信的双方经常位于不同的区域,为了保证服务的合法访问以及消息的安全传输,需要进行跨域认证以及安全会话密钥建立。提出了一种新的跨域认证与密钥建立协议,该协议采用生物加密技术省去了证书管理的负担,合理设计了通信双方及其各自服务器之间的交互,完成了跨域双向认证,并采用签密技术为通信双方派生密钥。对协议进行了安全及性能的分析,并用经典的SVO逻辑证明了其正确性。     

一种新型的非否认协议

在克服一种非否认协议草案的缺陷的基础上,提出一种新的非否认协议.新的协议可以在不安 全和不可靠的信道上工作,并能对付各种欺骗行为.此外,还对SVO逻辑进行扩充,引进一些新 的概念和方法,并用扩展后的SVO逻辑分析与证明新的非否认协议.     

Analysis of Authentication Protocols in Agent-Based Systems Using Labeled Tableaux

The study of multiagent systems (MASs) focuses on systems in which many intelligent agents interact with each other using communication protocols. For example, an authentication protocol is used to verify and authorize agents acting on behalf of users to protect restricted data and information. After authentication, two agents should be entitled to believe that they are communicating with each other and not with intruders. For specifying and reasoning about the security properties of authentication protocols, many researchers have proposed the use of belief logics. Since authentication protocols are designed to operate in dynamic environments, it is important to model the evolution of authentication systems through time in a systematic way. We advocate the systematic combinations of logics of beliefs and time for modeling and reasoning about evolving agent beliefs in MASs. In particular, we use a temporal belief logic called TML$^{+}$ for establishing trust theories for authentication systems and also propose a labeled tableau system for this logic. To illustrate the capabilities of TML$^{+}$, we present trust theories for several well-known authentication protocols, namely, the Lowe modified wide-mouthed frog protocol, the amended Needham–Schroeder symmetric key protocol, and Kerberos. We also show how to verify certain security properties of those protocols. With the logic TML$^{+}$ and its associated modal tableaux, we are able to reason about and verify authentication systems operating in dynamic environments.