一种自动密码协议分析方法

密码协议是构建网络安全环境、保护信息系统安全的重要手段之一,然而分析其固有缺陷和揭示入侵攻击行为,却是一件非常困难的事情。文中通过综合基于逻辑和模型检测的密码协议分析方法,提出了一种基于目标提取和消息模式匹配的自动密码协议分析方法,并以Needham-Schroeder(NS)公钥协议为例,进行了具体分析。     

密码协议的符号模型检测及分析

对密码协议模型检测的方法作了理论上的研究,并用SMV检测工具给出了一个实际分析的例子。结果表明,利用符号模型检测方法分析并发现密码协议重放攻击的漏洞是一种行之有效的方法。     

网络管理中一种互认证密码协议的安全性分析

基于串空间模型的极小元和理想理论,对网络管理中的一种互认证密码协议进行保密性和认证性分析,通过分析发现该协议存在冗余部分,并提出相应的改进方案;同时在协议的认证性设计方面,指出基于非对称密码系统和对称密码系统的认证协议的区别。     

RFID分布式密钥阵列认证协议的安全性分析

RFID技术已广泛地应用在诸如访问控制、支付系统、票务系统以及供应链管理等领域,但同时安全和隐私问题变得越来越严重。安全认证协议的设计与完善对于保护信息安全和用户隐私变得更加重要。2011年H.Ning等人提出分布式可扩展密钥阵列认证协议（KAAP）,该协议采用分布式密钥阵列架构、访问列表机制和动态随机数机制来抵御系统外部攻击和内部假冒攻击。针对KAAP建立两种有效的攻击模型,在此基础上分析得出该认证协议不能有效地抵御来自外部的重放攻击和拒绝服务攻击。KAAP安全性存在漏洞,不能达到设计的预期目标。     

Symmetric authentication in a simulatable Dolev–Yao-style cryptographic library

Tool-supported proofs of security protocols typically rely on abstractions from real cryptography by term algebras, so-called Dolev–Yao models. However, until recently it was not known whether a Dolev–Yao model could be implemented with real cryptography in a provably secure way under active attacks. For public-key encryption and signatures, this was recently shown, if one accepts a few additions to a typical Dolev–Yao model such as an operation that returns the length of a term.Here we extend this Dolev–Yao-style model, its realization, and the security proof to include a first symmetric primitive message authentication. This adds a major complication: we must deal with the exchange of secret keys. For symmetric authentication, we can allow this at any time, before or after the keys are first used for authentication, while working only with standard cryptographic assumptions.     

一种双向一次性口令身份认证方案的设计

提出了一种基于单向散列函数的双向一次性口令身份认证方案(OTPAP),该方案克服了通常的一次性口令方案的弱点,可以用在网络环境下,实现通信双方的互相认证,防止重放攻击和冒充攻击。方案实现简单,执行效率高,可用于电子商务过程中的身份认证,以增强应用系统的安全性。     

一种基于不可复制功能的RFID认证协议的安全性分析

基于不可复制功能(PUF)的射频识别(RFID)认证协议是近年来的研究热点。2011年,Bassil等在ITST国际会议上提出了一种新的基于PUF的RFID认证协议(BASSIL R, EL-BEAINO W, KAYSSI A, et al. A PUF-based ultra-lightweight mutual-authentication RFID protocol [C]// 2011 International Conference on Internet Technology and Secured Transactions. Piscataway: IEEE, 2011: 495-499)。分析了该认证协议的安全性,通过假设敌手参与协议,指出其不能抵抗密钥泄露攻击、跟踪攻击,也不能抵抗阅读器冒充攻击以及同步破坏攻击;同时描述了这些攻击的细节,并给出了它们的成功概率和计算复杂度。     

Needham-Schroeder 协议的认证测试方法形式化分析

在安全协议的形式化分析方法中,串空间模型和基于串空间模型的认证测试方法是比较常用的验证方法。针对Needham- Schroeder协议存在中间人攻击的缺陷,提出对协议的改进并采用认证测试方法,验证了改进的协议可以满足协议的安全目标。     

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

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

基于认证测试方法的EAP-AKA协议分析

EAP-AKA(Extensible Authentication Protocol-Authentication and Key Agreement)是WLAN的认证和密钥分配协议;认证测试是一种以串空间理论为基础的安全协议分析验证方法。运用认证测试方法对EAP-AKA协议的双向身份认证过程进行了分析证明,结果说明EAP-AKA能够保证移动终端和认证服务器之间的双向认证。     

可信网络接入认证协议的设计与分析

随着对TNC应用和研究的不断深入,其架构自身的安全性问题也逐渐成为人们所关注的焦点。在分析了TNC架构存在局限性的基础上,提出了一种新的基于TNC规范的网络接入认证协议,在服务器端和客户端安全协商会话密钥的前提下实现了通信双方的双向身份认证和双向平台认证,在提高认证效率的同时使得整个认证过程更为安全可靠。最后,对协议进行了安全性分析,并给出了协议的安全性验证过程,分析结果表明该接入认证协议能够达到预期的安全目标。     

基于ID变化的RFID安全协议

提出了一种基于ID变化的RFID安全协议,由于使用单向Hash函数,从而使数据存储机制很好地解决了阅读器和标签数据不同步的问题,有效地防止了非法读取、位置跟踪、窃听、伪装哄骗、重放等攻击。分析表明,该方法具有前向安全,效率高,安全性好等特点,适用于标签数目较多的情况。     

基于矩阵理论的RFID认证协议设计及BAN逻辑分析

针对目前提出的射频识别(RFID)认证协议大多不能抵抗重放攻击和数据篡改攻击的问题,提出了一种能抵抗这些攻击的低成本安全协议--基于矩阵的安全协议(MSP)。该协议基于矩阵理论的矩阵乘法和伪随机数生成器(PRNG),实现所需门电路不超过1000,满足低成本的要求。与基于同等算法的已有协议分析得出MSP大大降低了标签存储量和计算复杂度。最后,经BAN逻辑分析证明MSP实现了安全认证。因此,MSP非常适用于RFID环境。     

密码协议验证中的Petri网方法

如何验证密码协议的安全性是一个复杂的问题,只有形式化的验证方法才能证明密码协议的绝对正确.利用Petri网给出了一种用于密码协议验证的形式化方法.在合理假设的基础上,区分合法用户与攻击者在执行协议时的前提条件,列出执行协议后的结果,在此基础上建立了攻击者的Petri网模型.最后,用这种方法对NSPK协议进行了验证,证明了最初的NSPK协议中存在一个安全问题,而改进的NSPK协议则消除了这个问题.证明了这种方法的有效性.     

A simple framework for real-time cryptographic protocol analysis with compositional proof rules

A real-time process algebra, enhanced with specific constructs for handling cryptographic primitives, is proposed to model cryptographic protocols in a simple way. We show that some security properties, such as authentication and secrecy, can be re-formulated in this timed setting. Moreover, we show that they can be seen as suitable instances of a general information flow-like scheme, called timed generalized non-deducibility on compositions (tGNDC), parametric w.r.t. the observational semantics of interest. We show that, when considering timed trace semantics, there exists a most powerful hostile environment (or enemy) that can try to compromise the protocol. Moreover, we present a couple of compositionality results for tGNDC, one of which is time dependent, and show their usefulness by means of a case study.     

RV-TEE: secure cryptographic protocol execution based on runtime verification

Journal of Computer Virology and Hacking Techniques - Analytical security of cryptographic protocols does not immediately translate to operational security due to incorrect implementation and...     

Security analysis and enhancements of an improved authentication for session initiation protocol with provable security

Very recently, Tu et al. proposed an authentication scheme for session initiation protocol using smart card to overcome the security flaws of Zhang et al.’s protocol. They claimed that their protocol is secure against known security attacks. However, in this paper, we indicate that Tu et al.’s protocol is insecure against impersonation attack. We show that an adversary can easily masquerade as a legal server to fool users. As a remedy, we also improve Tu et al.’s protocol without imposing extra computation cost. To show the security of our protocol, we prove its security in the random oracle model.     

基于数字签名认证的IKE协议安全性分析及改进

IKE协议的复杂性使得其存在一些安全漏洞。简要介绍基于数字签名认证方式的IKE协议工作机制之后,分析了IKE协议容易遭受的两种中间人攻击,针对中间人攻击导致用户身份泄漏的安全缺陷,提出两种改进方案并给出改进前后定量的性能分析。     

RFID超轻量级认证协议RCIA形式化分析与改进

无线射频识别（RFID）是物联网中的一种非接触式的自动识别技术,被广泛运用于构建物物互联的RFID系统。RCIA是一种超轻量级RFID双向认证协议,提供高安全性并声称能抵御去同步攻击。形式化方法是安全协议分析的有力手段。运用模型检测工具SPIN对RCIA协议的认证性及一致性进行验证,结果表明RCIA协议存在去同步攻击漏洞。针对此漏洞,提出基于密钥同步机制的修补方案,对RCIA协议进行了改进。对改进后的协议进行形式化分析与验证,结果表明改进后的RCIA协议具有更高的安全性。提出的协议抽象建模方法对此类超轻量级RFID双向认证协议形式化分析具有重要借鉴意义;提出的基于密钥同步机制的漏洞修补方案,被证明能有效抵御去同步漏洞,可适用于此类超轻量级RFID双向认证协议的设计和分析。     

Analysing a stream authentication protocol using model checking

In this paper, we consider how one can analyse a stream authentication protocol using model checking techniques. In particular, we will be focusing on the Timed Efficient Stream Loss-tolerant Authentication Protocol, TESLA. This protocol differs from the standard class of authentication protocols previously analysed using model checking techniques in the following interesting way: an unbounded stream of messages is broadcast by a sender, making use of an unbounded stream of keys; the authentication of the n-th message in the stream is achieved on receipt of the n+1-th message. We show that, despite the infinite nature of the protocol, it is possible to build a finite model that correctly captures its behaviour.