【摘要】 本文利用由Ｗｉｌｌ Ｍａｒｒｅｒｏ，Ｅｄｍｕｎｄ Ｃｌａｒｋｅ 及Ｓｏｍｅｓｈ Ｊｈａ 提出的认证协议的检测模型，对改进的ＴＮＭ［１］ 协议进行检测，给出了如何将ＴＭＮ 协议模型化，并利用该模型对其进行检测，找出了用ＣＳＰ 模型没能找到的两个新的攻击方法，最后给出了ＴＭＮ协议的改进形式更多还原

【Abstract】 In this paper,we use a model checker for authentication protocol,due to Marrero,Edmund,and Jha,to detect errors in the improved TMN protocol [1] .We show how to model the TMN protocol,by the MCJ mode,which is used to test if the intrude can successfully attack the protocol,and find out two kind of new flaws which were not found by the CSP method.Finally,we give an improved TMN protocol.更多还原