在一个分布式的网络环境中，人们通过安全协议实现安全共享网络资源的需求，因此安全协议的安全性逐渐成为网络安全的关键。传统的安全协议分析技术包括传统的基于推理结构性方法，基于攻击结构性方法以及基于证明结构性方法三大类。 Petri网原本是用于并行系统分析的工具，但随着关注安全协议的学者不断实践，使用Petri网方法实现对安全协议的分析验证已经初露端倪。继[ALMU03]对STS协议的成功分析之后，[GULO05l和[DRES05]也分别成功地对3GPPAKA协议和SAP无线协议进行分析，其中[GULO05]的工作是本文的重点内容。 BAN逻辑是基于推理结构性方法的经典，但是它本身具有一定的缺陷，尤其是对重放攻击的检测能力十分弱。3GPPAKA协议设计者使用BAN逻辑进行分析，声称协议的安全目标已经达到[3GTS33]。然而，本文使用Petri网的分析将会得到不同的结果。 一个认证协议可以看成在其执行过程中通信实体信仰不断变化的过程，因此对一个认证协议的分析可视为对主体信仰的评估。KG逻辑正是基于信仰变化的逻辑。本文将使用KG逻辑对设计者的BAN逻辑分析工作进行改进，得到与Petri网一致的结果。