kerberos5协议的形式化分析综述

网络认证协议kerberos5提供三方认证机制，允许客户在单次登录的前提下实现对多个网络应用服务器的身份认证，目前该协议已得到广泛应用。freebsd，linux服务器以及微软公司的windows系列均采用该协议提供网络安全认证，因而该协议自身的安全性引起人们的广泛关注。由于该协议采用时间戳机制，同时涉及4个参与方，协议的复杂度较高，如何对其安全性进行全面的形式化分析与验证，一直是安全协议分析领域的研究热点与难点。目前国际上对其验证的方法主要分为两类，分别是基于符号模型的验证方法和基于计算模型的验证方法。