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

摘要

Openflow是目前使用最为广泛的SDN通信协议,由于其协议规范还在不断完善,因此存在一定的安全隐患,对Openflow协议及其相关应用的安全分析也越来越受到重视.Mynah协议是在Openflow协议的基础上实现的安全认证协议.对Mynah协议的保密性和认证性进行分析,基于符号模型,利用应用PI演算对Mynah协议进行形式化建模,并使用安全协议分析工具Proverif进行自动化分析.结果表明,Mynah协议并不具备保密性和认证性,为此,给出了Mynah协议中不具备保密性和认证性的解决办法.%Openflow is the most popular sdn protocol and widely used till now,as the protocol is still in the process of completing so that it has protential safety hazards and more attention has been paid on the issue.Mynah is a security protocol based on openflow and in this paper we analyse the pravicy and authentication of the protocol based on symbolic model,formalized with the Applied PI calculus in the symbolic model and use automatic tool ProVerif to analyse automatically.The results indicate that the Mynah protocol is lack of privacy and authentication.Finally the solutions for the problem of no privacy and authentication in Mynah protocol are presented.