sal框架下的安全协议分析技术研究

sal是一种新的结合模型检验和定理证明技术的分析框架。它使用一种过渡性的中间语言将不同验证工具统一在其框架之中，以便保证安全协议的验证不会顾此失彼。本文对基于sal框架下的安全协议分析技术进行了研究，介绍了sal中间语言描述安全协议的方法，包括消息项中协议主体、入侵者、现时值、公私密钥、对称密钥、加密、解密、dh问题等的描述，协议规则与性质的描述，给出了在sal下刻画入侵者模型和建立通信模型的一般方法，并以经典的nspk协议为例，找到了一个已知的认证性攻击。