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

摘要：

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

关键词：认证协议、安全性、SPAN、SSL协议、Kerberos协议

分类号：TP309(计算技术、计算机技术)

资助基金：国家重点基础研究发展计划973计划2013CB338003

在线出版日期：2016-03-24（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：71-76