无线认证协议Linear MAKEP的模型检验

模型检验是一种自动化程度很高的形式化分析技术。用有限状态机对无线认证协议Linear MAKEP建模,并对该协议的认证性用CTL公式进行形式化描述,将得到的模型和公式输入模型检验工具SMV进行检验。对检验结果进行分析发现：在Linear MAKEP协议中,入侵者可以冒充服务器与客户进行通信,不满足认证性。给出了协议的一种改进,使其满足认证性。     

无线传感器网络的认证协议分析

通过对现有无线传感器网络的认证协议进行比较和分析,总结了各协议的优点及存在问题,根据目前对传感器节点软硬件性能研究的进展,探讨了无线传感器网络安全认证协议研究的进一步发展方向.     

无线传感网身份认证协议研究

无线传感器网络由功耗、处理能力、通信能力及存储容量均有限的节点组成,传感器节点易遭受物理攻击及资源的有限的特点,均为节点安全性带来了严重威胁.因此,文章指出针对无线传感网安全问题,除了要有轻量级的密码算法之外,还需要高效的密钥分配和管理机制.为了解决内存有限性和安全性之间的平衡问题,目前已经有许多密钥建立技术,但是,学术领域中对于哪种方案最有效仍有争议.文章对各种常见的身份认证协议进行了比较和分析.     

基于SMV的安全协议模型检验

SMV是一个基于线性时态逻辑的符号化模型检验工具。本文利用SMV对Needham-Schroeder公钥协议的简化版本进行了验证,发现了利用消息重放进行的攻击。     

基于PKI的通用无线认证协议研究

基于PKI的WTLS协议涉及复杂的证书操作,需耗费较大的通信和计算开销,且缺乏对服务器证书的有效性检查.引入可信证书验证代理(TCVP)和证书有效性凭据(CVT)等概念,由TCVP为无线通信节点(WN)生成短时有效的CVT,WN通过交换CVT来完成证书的有效性检查和公钥交换.基于此,提出了一种通用无线认证协议(GWAP).在GWAP框架下,采用ECC算法设计了一种具体的无线安全认证协议,并进行了效率分析.结果表明,该协议在确保安全的前提下降低了通信开销.     

无线传感器网络用户认证协议研究进展

无线传感器网络(WSN,wireless sensor network)用户认证技术是传感器网络验证用户的合法性以避免网络数据信息泄露的有效手段之一,同时,用户也需验证传感器网络的合法性,避免获得错误或虚假数据信息。由于WSN节点能量、通信和计算能力等资源受限,且通常部署在敌对或无人值守的区域,因此传统用户认证协议并不完全适用于WSN。从WSN认证协议的安全攻击入手,给出其安全需求及理论基础,归纳总结了设计流程,针对其安全性分析,描述了安全攻击模型,并综述了形式化分析验证工具AVISPA体系结构和HLPSL语言构成。评述了当前的各种WSN用户认证协议,建议了未来研究方向,这些研究工作将有助于WSN用户认证协议的设计、分析与优化。     

抽象状态机下认证协议新的语义模型

为了简洁而正确的表达一个密码协议，选择一个具有比较自然语义的模型是十分必要的。不仅如此，一个恰当的模型须便于安全性质的分析，因此，具有一定的表达能力是十分必要的。为了探讨适合的方法和工具，人们使用各种各样的形式化工具来表达、分析密码协议的安全性。目前主要的方法包括逻辑的方法，如BAN逻辑，SVO等；基于模型检测的方法，如FDR工具，基于定理证明的和代数方法等等。各种方法都具有自己的优势和缺陷。探讨不同的方法和工具对于密码协议的描述和分析具有重要的意义。并可借此发现和发明好的模型和方法。     

一个无线Hand-Off认证协议的分析与改进

通过分析文献[1]中Wang提出的一个匿名移动无线认证方案中的Hand-Off认证协议,发现了其存在安全漏洞,无法抵抗中间人发起的重放攻击,针对该协议存在的安全漏洞对原协议进行了改进,改进后的协议可以安全的实现用户与机站之间的身份认证,并可以有效地抵抗中间人发起的重放攻击。     

NTRUSign无线认证和密钥协商协议

NTRU是一个快速、低开销的公钥体制,适合在资源受限的应用中使用。NTRUSign是基于NTRU的数字签名算法。基于NTRUSign算法,给出了一个无线认证和密钥协商协议。该协议的安全性基于有限时间内在大维数格计算最短向量的困难性。协议包括三个阶段:用户注册阶段、服务器注册阶段、认证阶段和密钥协商阶段。通过安全性分析和协议性能分析对比,表明该协议是一个安全性和效率比占优的协议。     

适用于无线Mesh网络的双向认证和密钥交换协议

在无线Mesh网络(WMN)通信模式下,认证和密钥交换对于其计费统计与安全连接起着十分重要的作用。在终端用户与Mesh路由器之间快速建立安全连接对于减少网络整体时延有着重要的帮助。MAKEP协议是为解决低功耗终端与高性能服务器之间的快速认证与密钥交换而提出的,但在非频繁加密业务连接下,认证协议的效率大大降低。针对WMN模式下的业务连接需求,提出了改进的MMAKEP协议,在降低业务连接时延的同时也提供了前向保密性。     

身份认证协议的模型检测分析

提出一个直观、易用的模型来模拟和验证身份认证协议，并给出基于Spin(模型检测工具）的实现，它不仅可以模拟多对参与者同时进行会话，而且还有效缩减了状态空间，从而避免了以前文献中提到的状态爆炸现象，同时该文用Needham-Schroeder公钥协议和TMN协议来说明如何应用该模型。     

802.11i双向认证协议的模型检查

确保安全协议的正确性对于保证Internet上安全敏感的业务非常重要。采用形式化方法建模和验证安全协议可以检测到传统测试手段难以发现的错误。模型检查作为形式化验证方法的一种,有着自动化和提供反例等诸多优点。使用模型检查工具SPIN对802.11i双向认证协议EAP-TLS进行验证,提取出包含协议设计重要细节的形式化模型,对协议安全属性采用线性时态逻辑抽象,并验证协议模型是否满足安全属性。提出了一种使用PROMELA建模认证协议的方法。     

一种移动支付协议的模型检验分析

给出了移动支付协议的一种有限状态机建模方法,该方法在传统支付协议的基础上充分考察了移动环境中移动装置和无线网络的特点,所建立的模型具有全面、准确、直观、简洁的特点。以一个典型的移动支付协议KSL为例,对该协议进行有限状态机建模,并通过模型检验工具对其公平性进行了分析验证,指出了其缺陷并进行了改进,从而表明了方法的有效性。该方法具有一定的通用性,以其为基础,可对其他类型的移动电子商务协议进行模型检验分析。     

无线网络中身份认证协议选择方法

无线网络中通常存在多种身份认证协议可供选择,如何选择一个能够满足用户个性化需求的协议是个尚未解决的问题.从用户的角度出发,针对无线网络的特点,在综合考虑了用户最为关心的几个要素,如协议的安全性、能量消耗、认证时间以及用户偏好的基础上,提出了解决方案.将能量消耗定义为用户发送、接收消息能量消耗以及交互过程中密码操作所涉及的能量消耗之和.其中,密码操作包括Hash算法、RSA密钥交换、数字签名以及对称加解密算法.实验部分对EAP-PEAP,EAP-TLS,EAP-TTLS-MD5和EAP-TTLS-MSCHAPV2这4种最为常用的协议进行比较,结果表明不管用户如何设置权值,EAP-TTLS/MSCHAPV2和EAP-TTLS/MD5总是优于EAP-PEAP,EAP-TLS. 该方案通过考虑用户对身份认证协议的安全性以及性能方面的要求,按照用户的个性化需求进行了协议方案的选择.     

Model Checking Data Consistency for Cache Coherence Protocols

A method for automatic verification of cache coherence protocols is presented, in which cache coherence protocols are modeled as concurrent value-passing processes, and control and data consistency requirement are described as formulas in first-orderμ-calculus. A model checker is employed to check if the protocol under investigation satisfies the required properties. Using this method a data consistency error has been revealed in a well-known cache coherence protocol. The error has been corrected, and the revised protocol has been shown free from data consistency error for any data domain size, by appealing to data independence technique.     

Model Checking Russian Cards

We implement a specific protocol for bit exchange among card-playing agents in three different state-of-the-art epistemic model checkers and compare the results.     

基于IBE的无线网络身份认证模型研究

传统的基于PKI无线网络身份认证方案效率较低、适用性较差。基于IBE的身份认证方案无需通过颁发数字证书来绑定用户身份和公钥,可以提高认证效率。针对IBE的这个特点,就IBE在无线网络身份认证中的应用问题开展研究,在此基础上设计了基于IBE的无线网络认证模型和相关协议,并分析协议的效率和安全性。