论文部分内容阅读
为了增强通讯网络安全性,研究者致力于通讯协议的形式化分析与验证。Abdelmajid在Kerberos协议中添加用户物理位置作为新的认证因素得到改进协议,并用改进BAN逻辑说明改进协议的安全性。针对添加用户物理位置这一因素进一步完善后的协议Kerberos*,结合可识别性和管辖性构造一种新的管辖规则,运用改进GNY逻辑对协议Kerberos*进行安全性分析。分析结果表明,协议Kerberos*是安全的,运用改进GNY逻辑证明过程比改进BAN逻辑更详细、更严谨,此方法可运用于其它类似协议形式化分析。
In order to enhance the security of communication networks, researchers are committed to the formal analysis and verification of communication protocols. Abdelmajid improved protocol by adding user physical location as a new authentication factor in the Kerberos protocol and improved protocol security with improved BAN logic. Aiming at the Kerberos *, which is a further factor of adding physical location of users, a new jurisdictional rule is constructed based on identifiability and jurisdiction, and the security of protocol Kerberos * is analyzed by using improved GNY logic. The analysis results show that the protocol Kerberos * is secure. The application of improved GNY logic proves that the BAN logic is more detailed and rigorous than other methods. This method can be applied to formal analysis of other similar protocols.