基于符号模型的Mynah协议安全性自动化分析

摘要

Openflow是目前使用最为广泛的SDN通信协议,由于其协议规范还在不断完善,因此存在一定的安全隐患,对Openflow协议及其相关应用的安全分析也越来越受到重视。Mynah协议是在Openflow协议的基础上实现的安全认证协议。对Mynah协议的保密性和认证性进行分析,基于符号模型,利用应用PI演算对Mynah协议进行形式化建模,并使用安全协议分析工具Proverif进行自动化分析。结果表明,Mynah协议并不具备保密性和认证性,为此,给出了Mynah协议中不具备保密性和认证性的解决办法。