Yahalom协议及其变体的时序缺陷分析与改进

研究Yahalom协议及其变体,发现该系列协议存在的时序缺陷,给出一种利用此缺陷攻击Yahalom协议及其变体的方法。尽管Yahalom协议历经几次修改,且被证明不存在密钥泄露问题,但Yahalom协议及其变体仍然存在以前没有被关注过的时序缺陷。该文从时序角度对Yahalom-Paulson协议进行改进。改进后的协议保持了原协议的安全性,同时能抵御原来因时序缺陷所引起的攻击。     

Yahalom协议的安全性分析及其改进方法

对Yahalom协议的安全性进行了较详细的分析,发现Yahalom协议遭受攻击的主要原因是协议中交换的消息无定长、消息的相似性及对称性;在网络或通信中,存在着执行流程(消息)的交错,即流程不是按设计者设想的串行顺序执行的.在这些情况下系统就存在很大的安全漏洞,极易遭受并行或重放攻击.文中提出了一种完全基于可信任第三方的改进方法,从而避免了此类并行或重放攻击.     

Yahalom协议的安全性分析及其改进方法

对Yahalom协议的安全性进行了较详细的分析,发现Yahalom协议遭受攻击的主要原因是协议中交换的消息无定长、消息的相似性及对称性;在网络或通信中,存在着执行流程(消息)的交错,即流程不是按设计者设想的串行顺序执行的。在这些情况下系统就存在很大的安全漏洞,极易遭受并行或重放攻击。文中提出了一种完全基于可信任第三方的改进方法,从而避免了此类并行或重放攻击。     

数据独立技术在CSP协议模型中的设计与实现

在研究Roscoe数据独立技术的基础上,引入新的进程扩展CSP协议模型,并以Yahalom协议为例给出了完整的协议模型。随后对扩展的协议模型进行形式化描述。最后使用脚本语言CSPM对其进行编写,完成验证。     

基于串空间模型安全协议形式化分析方法的研究

从串空间模型理论人手,提出了三种典型的串空间形式化方法(基于极小元理论的串空间方法、基于理想与诚实理论的串空间方法、基于认证测试理论的串空间方法),并对每一种方法的证明步骤及优缺点进行了分析.在此基础上,应用提出的串空间方法对Yahalom协议的秘密性和认证性进行了分析.分析结果表明利用不同方法的优点,能更好地保证安全协议形式化分析的准确性.     

Yahalom协议的串空间模型及分析

作为一种用来分析密码协议的最具代表性的定理证明技术，串行空间理论已被成功地用来分析许多典型的密码协议。其理论中的理想和诚实两个概念的提出更是大大简化了一类密码协议的证明步骤．首次利用串空间理论从机密性和鉴别两个方面对Gavin Lowe提出的Yahalom协议的改进版进行了分析．分析结果证明该协议是安全的．     

基于串空间模型安全协议形式化分析方法的研究

从串空间模型理论人手,提出了三种典型的串空间形式化方法（基于极小元理论的串空间方法、基于理想与诚实理论的串空间方法、基于认证测试理论的串空间方法）,并对每一种方法的证明步骤及优缺点进行了分析。在此基础上,应用提出的串空间方法对Yahalom协议的秘密性和认证性进行了分析。分析结果表明利用不同方法的优点,能更好地保证安全协议形式化分析的准确性。     

标准模型下可证安全的加密密钥协商协议

密钥加密协议的目的是利用安全性低的口令协商安全性高的密钥,进而利用密钥对以后的通信进行加密或身份认证,从而实现安全通信.现有的密钥加密协议大多缺乏安全证明,或者仅在Random Oracle模型下证明了协议的安全性.与Random Oracle模型下的协议相比,标准模型下可证安全的EKE(encrypted key exchange)协议虽然不需要Random Oracle假设,但它们都对参与方的计算能力要求较高,协议规则也更为复杂.从David P. Jablon在"Extended Password Key Exchange Protocols Immune to Dictionary Attacks"一文中提出的协议出发,通过引入服务端的公钥,并利用ElGamal加密和伪随机函数集,将一个Random Oracle模型下可证安全的EKE协议改进为一个标准模型下可证安全的EKE协议,并证明了改进后的协议仍然是安全的.与原始协议相比,改进后的协议只需要DDH(decisional Diffie-Hellman)假设,而不需要理想加密和Random Oracle假设;与其他标准模型下可证安全的协议相比,改进后的协议不需要CCA2(chosen ciphertext attack-2)安全的加密方案,从而不仅可以减少指数计算的次数,而且具有协议规则简单的优点.相对于KOY协议,改进后的协议将指数运算次数降低了73%;相对于Jiang Shao-Quan等人在"Password Based Key Exchange with Mutual Authentication"一文中提出的协议,改进后的协议将指数运算次数降低了55%.     

第三代短波网多址接入协议的研究与改进

为了解决短波资源有限问题,对短波网络MAC协议进行了研究.针对在短波可利用信道有限时,第三代短波网络MAC协议不能有效解决冲突的问题,提出了一种根据网络节点的重要程度设置不同接入概率的协议改进方法.分析了第三代短波网络多址接入协议,通过仿真研究了该"时隙CSMA"协议产生冲突的原因,然后针对该问题提出了一种有效解决冲突的改进方法.最后,建立了冲突产生的教学模型,在理论上证明了所提出方法的正确性,仿真分析表明了改进方法在解决冲突问题时具有良好的效果.     

新的域间身份认证协议及其形式化验证

Internet上不同的安全域间要实现信息资源的安全访问首先需要认证.目前常用的认证协议是Kerberos协议,但在网络环境下,该协议无法对真实的客户端进行认证.因此,给出了新的域间身份认证协议以及相应的"现时"产生方案,并利用改进的Spi演算对所设计的认证协议进行了分析,证明了该协议的安全性,能够有效地解决网间的信息安全传输.     

Mutual authentications to parties with QR-code applications in mobile systems

User authentication over the Internet has long been an issue for Internet service providers and users. A good authentication protocol must provide high security and mutual authentication on both sides. In addition, it must balance security and usability, which has been shown in the literature to be a difficult problem. To solve this problem, we propose a novel mutual authentication protocol with high security and usability. The proposed protocol was developed for quick response code, a type of two-dimensional barcode that can be photographed and quickly decoded by smartphones. We implemented a prototype using the proposed mutual authentication protocol and demonstrated how the prototype improves usability in a mobile communication system. We also used the Gong–Needham–Yahalom logic with several well-known attack models to analyze the security of the proposed protocol, and we obtained satisfactory results. We expect that using the proposed protocol, Internet service providers will be able to provide a mutual authentication mechanism with high security and usability.     

Study on Strand Space Model Theory

The growing interest in the application of formal methods of cryptographic pro-tocol analysis has led to the development of a number of different ways for analyzing protocol. In this paper, it is strictly proved that if for any strand, there exists at least one bundle containing it, then an entity authentication protocol is secure in strand space model (SSM) with some small extensions. Unfortunately, the results of attack scenario demonstrate that this protocol and the Yahalom protocol and its modification are de facto insecure. By analyzing the reasons of failure of formal inference in strand space model, some deficiencies in original SSM are pointed out. In orderto break through these limitations of analytic capability of SSM, the generalized strand space model(GSSM) induced by some protocol is proposed. In this model, some new classes of strands, oracle strands, high order oracle strands etc., are developed, and some notions are formalized strictly in GSSM, such as protocol attacks, valid protocol run and successful protocol run. GSSM can then be used to further analyze the entity authentication protocol. This analysis sheds light on why this protocol would be vulnerable while it illustrates that GSSM not only can prove security protocol correct, but also can be efficiently used to construct protocol attacks. It is also pointed out that using other protocol to attack some given protocol is essentially the same as the case of using the most of protocol itself.     

Reachability results for timed automata with unbounded data structures

Systems of Data Management Timed Automata (SDMTAs) are networks of communicating timed automata with structures to store messages and functions to manipulate them. We prove the decidability of the reachability problem for a subclass of SDMTAs which assumes an unbounded knowledge, and we analyze the expressiveness of the model and the considered subclass. In particular, while SDMTAs can simulate a Turing machine, and hence the reachability problem is in general undecidable, the subclass for which reachability is decidable, when endowed with a concept of recognized language, accepts languages that are not regular. As an application, we model and analyze a variation of the Yahalom protocol.     

Kaman协议的形式化验证

Kaman协议是移动Ad Hoc网络安全认证机制,然而,协议设计者未对该协议的安全性作严格的形式化分析。协议复合逻辑PCL是验证协议安全属性的形式化方法,PCL逻辑能够简化协议安全分析过程。本文在协议复合逻辑PCL中描述Kaman协议并分析Kaman协议的安全属性,证明Kaman协议能够实现其安全目标。     

移动通信中可证安全的双向认证密钥协商协议

在基于无线网络的分布式环境中,带认证的密钥协商协议对通信双方是否能够建立安全的会话至关重要.同时,协议的可证安全也逐步得到重视.在借鉴以往无线通信密钥建立协议的基础上,提出了一个可相互认证的密钥协商协议MAKAP(mutual authenticated key agreement protocol),并在Bellare和Rogaway的模型下证明了它的安全性,同时分析了其计算代价.与以往许多协议相比,MAKAP协议不仅在安全证明上有较明显的优势,而且其计算量也不大,有较高的实用性.     

基于网络编码的可信网络连接改进模型与协议设计

可信网络连接(TNC)模型用于保证网络接入的安全,随着TNC模型研究和应用的不断深入,TNC架构自身的安全性问题显得非常重要.本文首先对传统TNC的模型和工作流程进行分析,指出由于下层传输协议的安全措施缺失,传统TNC模型存在安全隐患.然后,针对该隐患,设计基于网络编码的可信网络连接模型(NCBTNC)和协议,在不降低...     

Ad hoc网络安全路由协议SRP的分析与改进

安全性是决定Adhoc网络能否得到充分利用的一个关键所在。由于不依赖固定基础设施,Adhoc网络的安全体系结构面临新的挑战,其中路由协议的安全问题是一个很重要的问题。首先介绍了安全路由协议SRP的设计思想并分析了其存在的安全漏洞问题,然后针对其漏洞问题提出一种改进的安全路由协议ESRP,并进行模拟分析。