Kerberos5协议的形式化分析综述  

Survey on Formal Analysis of Kerberos 5

作　　者：赵倩倩[1] 李舟军[1] 周倜[2] 

机构地区：[1]北京航空航天大学计算机学院,北京100083 [2]国防科技大学计算机学院,长沙410073

出　　处：《计算机科学》2009年第5期21-26,共6页Computer Science

基　　金：国家自然科学基金(60473057,90604007,60703075,90718017);高等学校博士学科专项科研基金资助课题(20070006055)的支持

摘　　要：网络认证协议Kerberos5提供三方认证机制,允许客户在单次登录的前提下实现对多个网络应用服务器的身份认证,目前该协议已得到广泛应用。FreeBSD,Linux服务器以及微软公司的Windows系列均采用该协议提供网络安全认证,因而该协议自身的安全性引起人们的广泛关注。由于该协议采用时间戳机制,同时涉及4个参与方,协议的复杂度较高,如何对其安全性进行全面的形式化分析与验证,一直是安全协议分析领域的研究热点与难点。目前国际上对其验证的方法主要分为两类,分别是基于符号模型的验证方法和基于计算模型的验证方法。全面系统地介绍和分析了目前国际上对该协议的形式化验证工作,在此基础上简要介绍作者目前的研究工作。Network Authentication Protocol Kerberos 5 provides us with a third-party authentication mechanism. The protocol was designed to allow a client to repeatedly authenticate herself to multiple network servers based on a single login. Nowadays this protocol has been widely used in Windows serials as well as FreeBSD and Linux system for network authentication. As a result, the security properties of it attract great attention. Since the protocol adopts timestamp and involves four participants, how to formally analyze and verify its security comes to be a hot and hard research point. Many methods were carried out internationally, which can be divided into two main approaches., one based the symbolic model and another based on the computational model. This paper introduced and analyzed typical formally work on analyses of Kerberos 5 over the world across-the-board and systematically, finally showed out our current research effort.

关 键 词：KERBEROS 5 形式化分析 认证性 保密性 

分 类 号：TP309[自动化与计算机技术—计算机系统结构] TN915.04[自动化与计算机技术—计算机科学与技术]