基于CSP的物联网David数字图书馆协议的改进与形式化分析

On CSP Improvements to David's Digital Library Protocol and Formal Analysis in Internet of Things

在分析了物联网通信节点使用的David数字图书馆通信协议运行的基础上,指出了此协议存在阅读器非法扫描标签和协议主体没有会话密钥的安全隐患,提出了解决安全隐患的方案。采用通信顺序进程(CSP)的形式化分析方法对提出的方案进行了建模分析,对复杂环境下的攻击者和各协议主体建立了CSP进程。在实验中,攻击者在Dolev_Yao模型下对新的协议方案模型进行攻击,最后没有发现攻击点。实验结果表明,该协议方案能有效解决David数字图书馆协议的安全隐患,保证了协议主体的相互认证性以及会话密钥的安全性,证明了模型的可行性。

This paper analysed David＇s digital library protocol used in the Internet of Things,and pointed out the secu- rity risks of this protocol. Aiming at the security risks was put forward, this protocol, the way to solve the security risks was put-forward. Using the formal analysis method, the communicating sequential processes （CSP）, role of protocol and the attackers were modeled. In the experiments, the new protocol is attacked under Dolev_Yao model by a attacker, but no attacks is finally founded. The experimental results show that the algorithm can effectively solve the security risks of this David＇s digital library protocol. Mutual authentication protocol role, as well as the security of the session key, and the feasibility of the model are proved.