论文部分内容阅读
导师苏开乐教授近年来新提出了基于本地会话的安全协议验证逻辑LLS(Logic of Local Sessions)。LLS逻辑基于安全协议的证明，它可以验证复杂协议的相关安全属性和处理多层认知规范，并且还实现了协议的完全自动化验证。本文通过扩展LLS逻辑，使其可以验证基于Dime-HelImaJl的密钥协商协议的相关安全规范。
本文的主要工作包括：
1．对LLS逻辑进行了扩展：(1)增加了密钥协商原子公式；(2)增加了一组密钥协商公理，并对新增加的公理进行了证明；(3)扩充了LLS逻辑最核心的(n，1)-Secrecy公理。
2．应用扩展后的LLS逻辑分析了一个有代表性的基于Dime-Hellman的密钥协商协议——STS协议。根据分析结果，我们给出了STS协议可以达到的安全目标，发现了STS协议存在的一个可能攻击，并提出了修改意见。