论文部分内容阅读
通过对安全协议验证的形式化需求分析,论证了形式化描述和分析是描述电子商务协议并验证它们属性的有效方法.介绍了一个扩展的BAN逻辑,基于这个逻辑对一种电子交易协议--NetBill协议进行形式化描述,并在有入侵的情况下对该协议所期望的属性(安全、原子、隐私)进行了正确的分析,证明了该协议在有入侵者的情况下能够满足安全、原子和隐私等要求.