论文部分内容阅读
ＢＡＮ作为对认证协议形式化分析的逻辑，在获得巨大的声望的同时也受到诸多抨击。如对秘密性要求的形式化表示，以及将协议格式改写为ＢＡＮ可分为格式时的困难。其中一个例子就是对Ｎｅｓｓｅｔｔ协议的分析。为解决这些问题，ＷｅｎＢｏ Ｍａｏ，ＣｏｌｉｎＢＯｙｄ于１９９３年提出了一个新的逻辑（ＭＢ９３）。该文将介绍这两个逻辑，并构造一个简单协议来指出ＭＢ９３逻辑在分析Ｎｅｓｓｅｔｔ协议及类似公钥体制的认证协议时