摘要： 在分析了物联网通信节点使用的David数字图书馆通信协议运行的基础上,指出了此协议存在阅读器非法扫描标签和协议主体没有会话密钥的安全隐患,提出了解决安全隐患的方案。采用通信顺序进程(CSP)的形式化分析方法对提出的方案进行了建模分析,对复杂环境下的攻击者和各协议主体建立了CSP进程。在实验中,攻击者在Dolev_Yao模型下对新的协议方案模型进行攻击,最后没有发现攻击点。实验结果表明,该协议方案能有效解决David数字图书馆协议的安全隐患,保证了协议主体的相互认证性以及会话密钥的安全性,证明了模型的可行性。
| [1] 赵志军,沈强,唐晖,等．物联网架构和智能信息处理理论与关键技术[J].计算机科学,2011,38(8):1-8 [2] 国务院办公厅．国务院关于推进物联网有序健康发展的指导意见.http://www.gov.cn/zwgk/2013-02/17/content_2333141.htm 2013．国发〔2013〕7号 [3] 谢鸿波．安全协议形式化分析方法的关键技术研究[D].成都:电子科技大学,2011 [4] 赵自强．基于串空间模型的形式化方法的扩展与应用[D].成都:成都理工大学,2011 [5] Armstrong P,Goldsmith M,Lowe G,et al．Recent developments in FDR[C]∥Computer Aided Verification．Springer,2012 [6] Shaikh S A,Bush V J,Schneider S A．Specifying authentication using signal events in CSP[J].Computers & Security,2009,28(5):310-324 [7] 卿斯汉．认证协议两种形式化分析方法的比较[J].软件学报,2003,14(12):2028-2036 [8] 周永彬,冯登国．RFID安全协议的设计与分析[J].计算机学报,2006(4):4581-4589 [9] 胡游君．RFID安全协议形式化分析研究及DRAP协议的建立与实现[D].秦皇岛:燕山大学,2007 [10] 丁振华,李锦涛,冯波．基于Hash函数的RFID安全认证协议研究[J].计算机研究与发展,2009,46(4):583-592 [11] 伍新华,唐翠婷．一种基于Hash的RFID双向认证协议[J].武汉理工大学学报:交通科学与工程版,2011,35(3):571-574 [12] 周晔．基于Hash链的RFID双向认证协议研究[D].成都:西南交通大学,2012 [13] Ryan S A,Schneider S,et al．安全协议的建模与分析:CSP方式[M]．张玉清,莫燕,吴建耀,译.北京:机械工业出版社,2005:30-53 [14] Palikareva H,Ouaknine J,Roscoe A W．SAT-solving in CSPtrace refinement[J].Science of Computer Programming,2012,77(10/11):1178-1197 [15] 薛锐,冯登国．安全协议的形式化分析技术与方法[J].计算机学报,2006(1):1-20 [16] Molnar D,Wagner D．Privacy and security in library RFID:issues,practices,and architectures[C]∥Proceedings of the 11th ACM conference on computer and communications security,2004．Washington,DC,USA:ACM.2004:210-219 [17] 唐郑熠,李祥．Dolev-Yao攻击者模型的形式化描述[J].计算机工程与科学,2010,32(8):36-38+45 [18] 张忠,徐秋亮．物联网环境下UC安全的组证明RFID协议[J].计算机学报,2011(7):1188-1194 [19] Roscoe A,Smyth T,Nguyen L．Model checking cryptographic protocols subject to combinatorial attack.http://www．cs．ox．ac．uk/files/4157/guess．pdf,2012 [20] 任伟,宋军,叶敏,等．物联网自治安全适配层模型以及T2ToI中T2T匿名认证协议[J].计算机研究与发展,2011(S2):320-325 |
| No related articles found! |
|
||
首页