论文部分内容阅读
针对物联网通信协议安全性不足和使用非形式化方法对协议的安全性进行分析时容易出现错误的问题,通过分析物联网感知层协议中的Hash-lock协议、随机Hash-lock协议、David数字图书馆协议,发现这些协议存在阅读器非法扫描标签和协议主体没有会话密钥的安全隐患问题。为了解决这两个安全问题研究了增强物联网通信协议安全性方法,该方法使用了适合此特征的异或运算和具有单向性质的哈希函数进行加密处理,采用形式化的分析方法对其安全性进行分析验证。 物联网感知层设备有计算能力有限、存储能力有限和供电能力有限的特点,DDL2P通信协议使用了适合此特征的异或运算和具有单向性质的哈希函数进行加密处理。在DDL2P协议运行之前,除了在服务器中注册标签的ID和共享密钥外,增加了注册标签阅读器的ID值和共享的密钥k,在协议中增加了对Tag阅读器进行认证;同时对新鲜值进行加密传送;服务器在它们进行认证的同时,产生一个会话密钥并通过加密方式传送给Tag阅读器和Tag标签,这样在后续的通信中便可以使用会话密钥进行加密传送。解决了Hash-lock协议、随机Hash-lock协议、David数字图书馆协议没有对读写器进行认证,以及以明文方式传送消息的安全缺陷,由此解决了读写器非法扫描和信息安全传送的问题。 对通信顺序进程CSP形式化分析理论进行了研究。研究了CSP的数理基础进程代数、迹的概念、相关的定理和符号。对设计的协议,先使用CSP理论对协议进行分析建模,然后把其转化成一个CSP系统,把协议主体建模成CSP进程,把协议的通信过程建模成通信事件,同时使用CSP描述协议系统的安全特性。最后使用故障发散改进检测器FDR模型检测器检测该协议的安全属性是否与协议的安全性说明相符合。 实验结果表明DDL2P协议保证了协议主体的相互认证性以及会话密钥的安全性,达到了安全协议的安全性要求,解决了协议Hash-lock协议、随机Hash-lock协议、David数字图书馆协议的安全缺陷,同时也表明形式化方法CSP能有效地分析通信协议的安全性。