信息网络安全

信息网络安全 ›› 2015, Vol. 15 ›› Issue (7): 71-76.doi: 10.3969/j.issn.1671-1122.2015.07.011

• • 上一篇    下一篇

基于形式化分析工具的认证协议安全性研究

段然, 徐乃阳, 胡爱群()   

  1. 东南大学信息科学与工程学院,江苏南京210096
  • 收稿日期:2015-05-20 出版日期:2015-07-01 发布日期:2015-07-28
  • 作者简介:

    作者简介： 段然（1992-）,男,山西,硕士研究生,主要研究方向：信息安全;徐乃阳（1991-）,男,安徽,硕士研究生,主要研究方向：信息安全;胡爱群（1964-）,男,江苏,教授,博士,主要研究方向：通信与无线网络安全。

  • 基金资助:
    国家重点基础研究发展计划（973计划）[2013CB338003]

Research on Authentication Protocol Security Based on Formal Verification Tool

Ran DUAN, Nai-yang XU, Ai-qun HU()   

  1. School of Information and Engineering, Southeast University, Nanjing Jiangsu 210096, China
  • Received:2015-05-20 Online:2015-07-01 Published:2015-07-28

RichHTML

1

PDF (PC)

165

摘要：

随着互联网业务的高速发展,计算机网络已成为信息交流的主要手段。在网络带来便利的同时,也带来了隐私信息泄露的问题。为保障信息安全,人们投入大量的人力物力,其中认证协议的安全性是重点研究的内容之一。形式化分析方法是辅助协议设计、弥补协议安全漏洞的有效手段,大致分成模型检测方法、定理证明方法和信仰逻辑方法。AVISPA工具融合了模型检测等形式化分析方法,而SPAN工具将AVISPA的功能形象化、本地化,表现为信息序列图表的形式。文章选用SPAN工具分析了SSL协议和Kerberos协议的安全性。分析表明,SSL协议易遭受证书伪造、篡改攻击,而Kerberos协议使用的对称密钥体系存在安全性不足的问题。根据分析结果,改进SSL协议,促使用户不完全信任SSL证书,且入侵者无法获取用于加密证书的公钥;改进Kerberos协议,用公钥密码体系取代对称密钥,这样能够在一个密钥被破解时保障其他密钥的安全。

关键词: 认证协议, 安全性, SPAN, SSL协议, Kerberos协议

Abstract:

With the rapid development of the Internet services, the computer network has been the main approach to interchange of information. The Internet 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.

Key words: authentication protocol, security, SPAN, SSL protocol, Kerberos protocol

中图分类号: