摘要
随着互联网业务的高速发展,计算机网络已成为信息交流的主要手段。在网络带来便利的同时,也带来了隐私信息泄露的问题。为保障信息安全,人们投入大量的人力物力,其中认证协议的安全性是重点研究的内容之一。形式化分析方法是辅助协议设计、弥补协议安全漏洞的有效手段,大致分成模型检测方法、定理证明方法和信仰逻辑方法。AVISPA工具融合了模型检测等形式化分析方法,而SPAN工具将AVISPA的功能形象化、本地化,表现为信息序列图表的形式。文章选用SPAN工具分析了SSL协议和Kerberos协议的安全性。分析表明,SSL协议易遭受证书伪造、篡改攻击,而Kerberos协议使用的对称密钥体系存在安全性不足的问题。根据分析结果,改进SSL协议,促使用户不完全信任SSL证书,且入侵者无法获取用于加密证书的公钥;改进Kerberos协议,用公钥密码体系取代对称密钥,这样能够在一个密钥被破解时保障其他密钥的安全。
With the rapid development of the Internet services, the computer network has been the main approach to interchange of information. The lnternet brings convenience to people, while also brings about privacy leakage and further more monetary loss. People devotes to themselves to protect information security in which authentication protocol is in major. Formal analysis assists protocol- design and covers the bug of protocol security. Formal analysis includes model checking, theorem proving and belief logic. AVISPA includes model checking and some else formal analysis, and also can be automatic. SPAN makes the function of AVISPA vivid and localization which is described as Message Sequence Charts. Choose SPAN to analyze SSL protocol and Kerberos protocol. It turns out that SSL protocol tends to suffer from falsify certification and the public key system isn＇t secure on Kerberos protocol. To improve SSL protocol, make users not believe in SSL certification and provide the intruder from fetching public-key for encrypting certification; to improve Kerberos protocol, public- key replacing symmetric-key keeps other keys safe even if the intruder crack one key.
出处
《信息网络安全》
2015年第7期71-76,共6页
Netinfo Security
基金
国家重点基础研究发展计划(973计划)[2013CB338003]
