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

目前,对物联网的研究越来越深入,物联网在未来社会的发展和应用越来越广泛,随着各种物联网硬件和应用软件开发和研究,物联网的安全问题也凸显出来,如何对物联网的通信主体进行身份认证,如何对数据进行保密安全的传输,这是一个迫切需要研究和解决的应用需求。安全协议在通信主体的身份认证、密钥的分配和数字签名等方面发挥着重要作用,但是,安全协议的安全性设计、分析和证明长期以来一直是信息安全研究的重点和难点问题,随着攻击的新手段和新技术不断涌现,安全协议的设计,分析和证明也在不断的接收新的挑战。本文在当前比较公认的物联网概念和体系结构基础上,针对物联网传感网络的安全协议的形式化设计,分析和证明展开研究,主要工作为：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协议进行定理证明,对模型的无穷状态空间进行推理,解决模型验证所不能完成状态空间爆炸问题；总之,本文提出对安全协议的形式化设计、分析和证明较之于传统的非形式化设计和分析,具有较强的数学理论基础,可以保证在攻击者模型所具备的攻击条件下安全协议的可靠性,保密性和数据一致性。