关键词:
安全协议
形式化方法
事件逻辑理论
ECC-based RFID双向认证协议
摘要:
射频识别技术(RFID)是物联网(Io T)的重要组成部分,提高RFID系统的安全性是亟需解决的问题。而保障通信系统的安全性与系统所使用的安全协议息息相关,如果安全协议的安全属性没有得到严格的证明,则增加了网络通信中的风险。形式化方法是分析与验证安全协议最强有力的手段之一。事件逻辑理论(Logic of Events Theory,Lo ET)作为一种分布式系统安全性描述的形式化方法,提供了对安全协议基本原语的形式化规范,并通过对协议的强认证性质进行证明,进而验证协议的安全属性。
本文通过对事件逻辑理论的创新性扩展,成功将其应用于基于ECC的RFID这一类协议的形式化分析与验证中,使扩展后的事件逻辑理论适用于带有复杂加密算法协议的安全性分析。本文的主要研究内容如下:
1.详细介绍事件逻辑基本理论,给出事件逻辑基本定义,包括基本建模理论,公理系统以及协议的形式化描述。引入扩充谓词Fresh和First Send以及相应的推理规则,增强其在协议分析中的实用性,特别是在处理消息的新鲜性和识别发送事件的首发性方面,有助于确保协议证明过程中事件类和基本序列的一致性,同时提高了事件排序的能力并降低了协议分析的复杂度。
2.将事件逻辑与其他形式化方法进行比较,分析事件逻辑对于其他方法的优势与不足。对事件逻辑理论进行扩展,提出三个新事件类Compute、Retrieve、Generate并给出相应的定义。根据新的事件类,扩展因果公理,定义新的因果关系。对其他相关公理及规则进行扩展,使得扩展后的事件逻辑理论能够分析带有复杂加密算法的协议。建立机密性系统,引入归纳机密规则,扩展Lo ET所能证明的安全属性范畴。
3.利用扩展后的事件逻辑理论,深入形式化分析一个ECC-based RFID双向认证协议。首先对ECC会话密钥的生成过程进行形式化抽象描述,定义协议进程和基本序列用于描述协议,对协议所需满足的强认证属性进行了严格的形式化定义,通过理论推导,证明协议在合理假设下满足双向强认证性质,表明扩展的事件逻辑理论可以证明ECC-based RFID这一类带有复杂加密算法协议的安全属性,扩展了事件逻辑理论的使用范围。