物联网传感网络安全协议形式化研究

【作者】 李俊霖；

【导师】 周华；

【作者基本信息】 云南大学 ， 系统分析与集成， 2011， 博士

【摘要】 目前,对物联网的研究越来越深入,物联网在未来社会的发展和应用越来越广泛,随着各种物联网硬件和应用软件开发和研究,物联网的安全问题也凸显出来,如何对物联网的通信主体进行身份认证,如何对数据进行保密安全的传输,这是一个迫切需要研究和解决的应用需求。安全协议在通信主体的身份认证、密钥的分配和数字签名等方面发挥着重要作用,但是,安全协议的安全性设计、分析和证明长期以来一直是信息安全研究的重点和难点问题,随着攻击的新手段和新技术不断涌现,安全协议的设计,分析和证明也在不断的接收新的挑战。本文在当前比较公认的物联网概念和体系结构基础上,针对物联网传感网络的安全协议的形式化设计,分析和证明展开研究,主要工作为：1、通过分析当前比较公认的物联网概念和体系结构,对物联网体系结构与传统的网络体系结构作了分析比较,得出物联网传感网络的特点和安全属性；2、根据物联网传感网络的特点和安全属性,提出针对物联网传感网络攻击者的模型：3、根据物联网传感网络的特点和安全属性,提出一种基于无线网络的物联网传感网络SNIT(The Sensing Network of the Internet of Things)模型；4、针对SNIT模型,对通信主体进行抽象,提出一种基于协议元的形式化设计方法,该方法首先对协议元进行选择和设计,并对其进行基于UM击模型下的SK安全属性进行证明；5、针对SNIT模型提出一种SNIT协议,该协议根据发起通讯请求的通信主体的不同SNIT办议又分为SNIT_C, SNIT_S_三个协议,并对三个协议进行形式化描述和攻击者建模；6、采用CSP对SNIT协议进行形式化分析和模型验证；7、采用串空间理论对SNIT协议进行定理证明,对模型的无穷状态空间进行推理,解决模型验证所不能完成状态空间爆炸问题；总之,本文提出对安全协议的形式化设计、分析和证明较之于传统的非形式化设计和分析,具有较强的数学理论基础,可以保证在攻击者模型所具备的攻击条件下安全协议的可靠性,保密性和数据一致性。更多还原

【Abstract】 Presently, the study of Internet of Things (IOT) is more and more deeper, the development and application of IOT more and more wider in the future social. The security problem of IOT come out as the Development and Research of various IOT hardware and application software, So how to implement the identification authentication of the IOT communications principal and how to transport data ensure secret and security is an application requirement that sorely need to be studied and resolved.Security protocol is playing an important part in the identification authentication of communications principal, key distribution and digital signature and so on. But, the security design, analysis and prove have long been the important and difficulty problem to security protocols with the emerging of new attack means and technic constantly, so it is facing new challenges.This thesis base on the concept and architecture of IOT.that is the official acceptance carrying on an investigation into the formalization design and verification of the security protocols that transport in IOT sensor network. The main research content and contributions of this thesis are below:1. With the concept and architecture of IOT that is the official acceptance, contrasting and analyzing the architecture of IOT with the traditional.network architecture,educe the characteristics and security properties of IOT sensor network.2. According to the characteristics and security properties of IOT sensor network, put forward a model to deal with attacker of Internet of Things sensor network.3.According to the characteristics and security properties of Internet of Things sensor network, put forward a SNIT (The Sensing Network of the Internet of Things) model of IOT sensor network base on Wireless Network。4. For the SNIT model, giving an abstract of communications principal, educe a formal design method that base on protocol metadata. The method first choose and design protocol metadata, and then certificate the security properties that base on UM attach model;5.Educing a kind of SNIT protocol that is classified according to the agent which initiates communications request:SNIT_C, SNIT_M and SNIT_Sto, for SNIT model.6. Formal analysis,model checking and verification for SNIT Protocols by CSP.7.Adopt theorem proving for SNIT protocol by strand space theory, reasoning infinity state space of the model, solving the space explosion problem that model checking can not be.In summation, this thesis educe formalization design, analysis and certificate for security protocol that has a great of mathematics technical and can ensure its reliability, confidentiality and data consistency under the condition of attractor model has the ability to attack compare to traditional un-formalization design and analysis.更多还原