当今,物联网技术发展迅速,人们对物联网的研究也在逐渐深入,随着时间的推移,物联网技术会得到越来越多的实际应用。伴随着物联网相关硬件、软件的开发和研究,很多问题也逐渐凸显出来,如何确保物联网通讯主体间的信息安全问题显得尤为重要。然而,通过安全协议实现物联网的安全通信问题逐渐成为研究热点。论文结合当前物联网安全问题的研究现状,针对物联网的通信特点,提出一种可抵御已知明文攻击的物联网安全协议模型,实现了在信息交互过程中的身份认证、密钥分发、数据加密等问题。通过Casper+FDR工具对论文提出的安全协议进行建模和形式化分析,证明该协议的安全性;通过与其他物联网安全协议的对比和对网络通信开销的期望值计算,分析协议的性能;通过Socket仿真实现协议的交互过程,说明协议的可用性。期间所做主要研究如下:1)通过查阅文献,对物联网的安全问题和物联网安全协议的研究现状进行细致了解,并总结其中存在的问题。2)通过分析目前较为公认的物联网体系结构概念,得出物联网通信的特点和安全特性,并且通过对原有物联网安全协议的分析,提出一种可抵御已知明文攻击的物联网安全协议模型。3)该物联网安全协议模型分为密钥协商和实体通信两个阶段,可以根据实际需求设定会话密钥协商的周期,提高通信效率。4)通过Casper语法规范对协议进行建模,将完成Casper语法建模的安全协议伪码进行编译,生成CSP描述,再通过模型监测工具FDR对安全协议的CSP描述进行形式化分析。5)通过安全协议的形式化分析结果,分析安全协议所存在的不足,完善该安全协议模型,并重新建模,引入“大随机数”这一概念对协议进行修改,使其可以抵御已知明文攻击或穷举攻击。6)结合物联网通信环境,将论文提出的安全协议模型与以往提出的物联网安全协议进行对比,分析协议的性能;利用socket编程,完成协议通信的仿真过程,验证协议的可用性。7)总结研究过程中所存在的问题和不足之处,对下一步的研究方向做出规划。通过论文所做的研究中可以发现,这种“可抵御已知明文攻击的物联网安全协议模型”的特点有:①在密钥的分配过程中引入“大随机干扰数”这一概念,使其可抵御已知明文攻击;②可以根据通信需求定期更新会话密钥,确保密钥的新鲜性;③在消息的完整性确认和身份认证的过程中,引入“哈希函数”和“时间戳”,从而提高了通信效率、减少了网络信息负载量、确保了身份认证的时效性。针对该协议的形式化分析和性能分析表明,该协议可以保证物联网通信环境下的安全性需求,并且其网络开销、存储复杂度、计算复杂度都相对较小。