摘要

近年来,人们在运用BAN逻辑进行形式化分析时,发现非形式化的理想化步骤是其致命缺陷,导致目前BAN逻辑的研究进展迟缓。有鉴于此,人们开始考虑采用另外一些形式化逻辑分析方法对协议的安全性进行分析。文章介绍了一种新的Nonmonotomic逻辑(简称N逻辑)的协议形式化分析方法,并运用此方法分析SSL3.0握手协议,对分析结果进行总结,提出协议的缺陷和逻辑本身需要进一步完善的地方。

  • 单位
    中国防卫科技学院