中文摘要：

为了增强通讯网络安全性，研究者致力于通讯协议的形式化分析与验证。 Abdelmajid 在 Kerberos 协议中添加用户物理位置作为新的认证因素得到改进协议，并用改进 BAN 逻辑说明改进协议的安全性。针对添加用户物理位置这一因素进一步完善后的协议 Kerberos ＊，结合可识别性和管辖性构造一种新的管辖规则，运用改进 GNY 逻辑对协议 Ker-beros ＊进行安全性分析。分析结果表明，协议 Kerberos ＊是安全的，运用改进 GNY 逻辑证明过程比改进 BAN 逻辑更详细、更严谨，此方法可运用于其它类似协议形式化分析。

英文摘要：

In order to enhance the communication network security ,security specialists devote themselves to formal a-nalysis and verification of the communication protocols .Abdelmajid adds the user＇s physical location as a new factor in the Kerberos protocol is applied to obtain improved protocol .In the meantime ,he utilizes the modified BAN logic to illustrate the safety of the improved protocol .To the further improved protocol Kerberos ＊ which adds the user＇s physical location ,the modified GNY logic is applied to analyze the security of Kerberos ＊ protocol by combining identifiability with jurisdiction to construct a new jurisdiction rules .Analysis results show that Kerberos ＊ protocol is secure ,and modified GNY logic proofs are more detail and more rigorous than modified BAN logic .The method can be applied to the formal analysis of the similar protocols .