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

针对物联网通信协议安全性不足和使用非形式化方法进行分析时容易出现错误的问题,提出了一种物联网安全通信协议,建立了协议主体模型和攻击者模型,采用通信顺序进程CSP的形式化方法对协议模型进行了分析。该通信协议对传送的信息进行加密,采用的加密方式是散列函数结合异或运算。协议主体进行了相互认证,认证服务器为协议主体通信分配了会话密钥,解决了读写器非法扫描和信息安全传送的问题。利用故障发散改进检测器（FDR）对该协议模型CSP进程进行了检测,结果表明：该协议主体进行了相互认证,会话密钥是安全的,所提出的物联网通信协议是安全可靠的,CSP方法用于分析协议的安全性是可行的。

Formal Analysis of Security Protocol in Internet of Things

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.