基于CSP物联网通信协议的建模与形式化分析研究

摘要

针对物联网通信协议安全性不足和使用非形式化方法对协议的安全性进行分析时容易出现错误的问题,通过分析物联网感知层协议中的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能有效地分析通信协议的安全性。

目录

封面

声明

中文摘要

英文摘要

目录

第1章 绪 论

1.1研究的背景与意义

1.2协议安全性形式化分析方法现状

1.3研究内容及工作重点

1.4研究的标准

1.5论文组织结构

第2章 CSP相关理论与应用

2.1基本的操作符号

2.2 CSP的相关定理

2.3 Casper/FDR基础语法

2.4 Casper/FDR应用实例

第3章 物联网通信安全协议安全性研究

3.1物联网协议的相关安全特性

3.2 Hash-lock协议分析

3.3随机Hash-lock协议分析

3.4 David数字图书馆协议分析

3.5实验及分析

第4章 双向认证协议DDL2P的提出与分析

4.1双向认证协议DDL2P提出环境

4.2 DDL2P协议方案

4.3 DDL2P协议的CSP进程模型

4.4 DDL2P协议的攻击者CSP进程模型

第5章 实验与分析

5.1实验装置-故障发散改进检测器FDR2

5.2实验验证

5.3同条件下的不同协议实验比较

5.4实验结果讨论

第6章 总结与展望

6.1总结

6.2展望

致谢

参考文献

申请学位期间获奖情况及发表的学术论文