论文部分内容阅读
行为时序逻辑（TLA）是LeslieLamport于20世纪90年代提出的一种新的逻辑，运用这种逻辑对软件或协议系统进行建模，在一定程度上减少了由于状态空间爆炸带来的压力，它能在一种语言中同时表达模型程序与系统属性。文中首先介绍了行为时序逻辑的语法和语义，然后以EKE协议为例，用基于行为时序逻辑语言TLA＋对EKE协议进行了建模分析，用TLA建模并用行为时序逻辑语言TLA＋进行协议的描述，最后用TLC检测工具进行分析，发现存在中间人的重放攻击漏洞。