【摘要】 在分布式系统中,客户向对方证实自己的身份以及建立会话密钥已是非常重要,密码协议的实施就是达到这种目的的有效方法。但密码协议的设计容易出错。本文给出了一种密码协议分析和检测模型,该模型对密码协议的描述简单而且直观。在此模型中,协议被描述成状态变换系统,通过对系统状态的检测,能够发现协议中存在的泄漏。最后,给出了如何将改进的TMN协议模型化,并找出了一种新的攻击,同时,给出了TMN协议的进一步改进。更多还原

【Abstract】 In secuer distributed systems it is essential that principals could prove their identities to each other and establish a session key. Cryptographic protocols are used to ensure authentication and related purposes,but the design of authentication cryptographic protocols is error prone. In this paper, we develop a way of verifying these protocol using model checking, in which the description of protocol is very simple and intuiive. By modeling protocol as a system of states ranslation, and examining all possible states, model checking has found some flaws in some well know protocols. Finally, we show how to use the model checking to detect errors in improved TMN protocol, and find and unknown attack on this protocol. We also propose a further improved TMN protocol.更多还原