【摘要】 BAN作为对认证协议形式化分析的逻辑，在获得巨大的声望的同时也受到诸多抨击。如对秘密性要求的形式化表示，以及将协议格式改写为BAN逻辑可分析格式时的困难。其中一个例子就是对Nessett协议的分析。为解决这些问题，WenBoMao，ColinBoyd于1993年提出了一个新的逻辑（MB93）。该文将介绍这两个逻辑，并构造一个简单协议来指出MB93逻辑在分析Nessett协议及类似公钥体制的认证协议时也是有缺陷的，随后提出了一种改进MB93的方法。更多还原

【Abstract】 BAN is one of logics that were designed to analyze authentication protocols formally. BANhas got a big fame for its success and its share of critique, such as the lack of secret requirement and the dificulty for rewriting protocols in the form which BAN can work on. One sample is the analysis of NessettProtocol. To deal with those problems, Wenbo Mao and Colin Boyd have published a new logic (MB93).We will introduce those two logics, and will construct a simple protocol to show that MB93 still can not analyze Nessett protocols and such public－key protocols correctly. And we present one way to improve MB93.更多还原