论文部分内容阅读
BAN作为对认证协议形式化分析的逻辑,在获得巨大的声望的同时也受到诸多抨击。如对秘密性要求的形式化表示,以及将协议格式改写为BAN可分为格式时的困难。其中一个例子就是对Nessett协议的分析。为解决这些问题,WenBo Mao,ColinBOyd于1993年提出了一个新的逻辑(MB93)。该文将介绍这两个逻辑,并构造一个简单协议来指出MB93逻辑在分析Nessett协议及类似公钥体制的认证协议时