RFID安全协议形式化模型研究

Only the formal method can discover flaws comprehensively and prove security of radio frequency identification (RFID) security protocols. There exist many mature formal models for security protocols, but they all can not accurately describe RFID security protocols. This project focuses on the formal model for designing and analyzing RFID security protocols in the Internet of Things. Firstly, the model for RFID communications and the model for the adversary capabilities are put forward in the Internet of Things. Secondly, both the framework of strand space which belongs to symbol theory and the framework of universally composable security which belongs to computation theory are improved keeping in mind the special characteristics of RFID system, so that they can accurately describe RFID security protocols. Finally, the RSSUC model for RFID security protocols is provided which integrates the strand space theory and the universal composability theory under the environment of RFID system. The new model absorbs merits of the strand space model and the universal composability model perfectly, which can provide complete and systemic support theory for designing and analyzing efficient and reliable RFID security protocols in the Internet of Things.

采用形式化方法才能全面、客观地分析射频识别（RFID）安全协议，但是现有成熟的安全协议形式化模型不能准确地描述RFID系统安全协议。本项目主要研究适用于物联网环境下RFID系统安全协议设计与分析的形式化模型。通过分析物联网环境下RFID系统的环境特征,建立RFID系统的通信模型以及RFID协议攻击者的能力模型。进而针对RFID系统环境，分别对符号理论类的串空间框架和计算理论类的通用可组合安全框架进行改进和扩展，使其能够准确描述RFID安全协议。在RFID系统环境下，融合串空间模型和通用可组合模型两种理论，各取所长，提出RFID安全协议形式化模型——RSSUC模型。该模型很好地综合了串空间模型和通用可组合模型的优点，可以为高效、可靠的物联网环境下RFID安全协议的设计和分析提供比较完整和系统的理论支持。

本项目主要研究适用于物联网环境下RFID系统安全协议设计与分析的形式化模型。借鉴串空间框架和通用可组合（UC）安全框架对安全协议的建模思想，融合串空间模型和UC模型两种理论，为高效、可靠的RFID安全协议设计和分析提供比较完整和系统的理论支持。研究成果是：（1）通过分析物联网环境下RFID系统的环境特征,建立RFID系统的通信模型以及RFID协议攻击者的能力模型。（2）针对RFID系统环境，分别对符号理论类的串空间框架和计算理论类的通用可组合安全框架进行改进和扩展，使其能够准确描述RFID安全协议。（3）建立了串空间框架下的RFID安全协议和UC框架下的RFID安全协议的对应关系。（4）在RFID系统环境下，融合串空间模型和通用可组合模型两种理论，各取所长，提出RFID安全协议形式化设计和分析的新模型。