选择认可动态逻辑

本文提出了一种用于分析网络安全协议的形式化逻辑——选择认可动态逻辑。该逻辑重视通信实体间的明文信息,通过对通信实体之间交换信息的状态的演绎,刻划了通信各方对信息的获取以及由此产生的攻击行为。预共享密钥交换协议是IPSec中IKE的验证模式之一,本文利用选择认可动态逻辑对该协议进行了演绎,剖析了其认证过程和密钥生成的关键所在,随后对该协议的局限性和野蛮模式下的特点进行了评估。