物联网安全协议攻击者模型形式化构建研究

Research of formal establish security protocol attacker model in communicating sequential processes

在Dolev-Yao攻击者模型基础上,利用通信顺序进程(Communicating Sequential Processes,CSP)对物联网安全协议攻击者能力进行形式化构建,并用实例分析了攻击者模型的攻击行为.可以检验出给定的物联网安全协议崩溃的假设条件和原因,为下一步物联网安全协议自动化设计、分析和验证研究奠定理论基础.

This paper focused on formal establishment of the Internet of things security protocol attacker ability using communicating sequential processes(CSP),and used a case of the Internet of things security protocol to analyze the attacker's aggression,which was based on the current researches of Dolev-Yao attacker model.The process of attack can test the collapse reasons of the protocol,and laid the formal security foundations for automatic analysis of security protocol.