物联网中安全通信协议的形式化分析  

Formal Analysis of Security Protocol in Internet of Things

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

机构地区：[1]桂林理工大学广西矿冶与环境科学实验中心,广西桂林541004 [2]桂林理工大学信息科学与工程学院,广西桂林541004

出　　处：《桂林理工大学学报》2013年第2期333-338,共6页Journal of Guilin University of Technology

基　　金：国家自然科学基金项目(61262075);广西高校重大科研项目(201201ZD012);广西矿冶与环境科学实验中心资助项目(KH2011YB006)

摘　　要：针对物联网通信协议安全性不足和使用非形式化方法进行分析时容易出现错误的问题,提出了一种物联网安全通信协议,建立了协议主体模型和攻击者模型,采用通信顺序进程CSP的形式化方法对协议模型进行了分析。该通信协议对传送的信息进行加密,采用的加密方式是散列函数结合异或运算。协议主体进行了相互认证,认证服务器为协议主体通信分配了会话密钥,解决了读写器非法扫描和信息安全传送的问题。利用故障发散改进检测器(FDR)对该协议模型CSP进程进行了检测,结果表明:该协议主体进行了相互认证,会话密钥是安全的,所提出的物联网通信协议是安全可靠的,CSP方法用于分析协议的安全性是可行的。For the security of Internet of Things and the mistakes in non-formal method analysis,the secure communication protocol of the Internet of Things is presented.The master model and the attacker model of the protocol are established.Formal analysis method of CSP is used to analyse the protocol.The protocol message is encrypted by the method which is constructed by the combination of Hash function and XOR.The master of each protocol is mutually certified.When certified,the session key is assigned to the master of the protocol and then the problem that reader illegall scanning and the security of information transmission would be solved.The investigations of the experiment,which is conducted by FDR to detect the CSP of the model,shows that the mutual authentication and the session key of the master of the protocol are safe.The formal method based on the CSP could analyse the security of the protocol effectively.The proposed communication protocol of the Internet of Things is safe and reliable,and the security of the CSP formal analysis method is feasible.

关 键 词：物联网 形式化分析 安全协议 通信顺序进程 

分 类 号：TP309.2[自动化与计算机技术—计算机系统结构]