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

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

作　　者：吴名欢[1] 程小辉[1] 

机构地区：[1]桂林理工大学信息科学与工程学院桂林541004

出　　处：《计算机科学》2014年第1期225-229,270,共6页Computer Science

基　　金：国家自然基金项目(61262075);广西高等学校重大科研项目(20120120012);广西教育厅项目(201010LX192)资助

摘　　要：在分析了物联网通信节点使用的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.

关 键 词：物联网 形式化分析 David数字图书馆协议 通信顺序进程 

分 类 号：TP393.04[自动化与计算机技术—计算机应用技术]