论文部分内容阅读
BAN逻辑和BAN类逻辑是验证安全协议简单易用的逻辑方法。基于BAN类逻辑的自动验证构架,以拥有和信仰为基础,通过使用自动分析和验证技术,解决了BAN类逻辑的理想化过程的非形式化和初始假设集合的非形式化问题,并自动的验证安全协议是否达到预期的目标。分析结果表明,该构架在一定程度上解决了BAN类逻辑的过分依赖经验和手工证明的缺陷。