一种基于形式化验证的物联网协议安全性自动分析方法与系统

摘要

本发明公开了基于形式化验证的物联网协议安全性自动分析方法与系统，其中方法包括：基于物联网协议状态机构建协议需满足的安全属性，对物联网协议和其需满足的安全属性自动实现形式化描述，应用两种攻击场景对攻击者能力进行建模,基于动态优先策略实现形式化验证。本发明的基于形式化验证的物联网协议安全性自动分析方法能高效地将MQTT、CoAP和AMQP协议部署在多个物联网平台上的协议状态机转换为形式化语言，并进行自动化、系统性的安全分析。