安全协议中的互模拟等价性验证

摘要

随着信息服务和商业活动等越来越多地出现在开放的通讯网络上，用以保证上述服务的网络安全协议的可靠性成为备受人们关注的焦点。然而，由于外部面临恶劣的网络环境和内部缺乏系统化设计验证方法，网络安全协议变得非常脆弱和容易出错。 形式化的方法为验证和分析安全协议提供了有效的途径。它用形式化的语言抽象出复杂的密文通讯协议，并借助于高级的推理或证明系统实现协议的分析验证。建立在进程演算基础之上的互模拟等价性验证的方法，由于具有能确切地刻画协议运行的代数语义模型(Spi演算)和十分有效的等价性验证方法而成为近年来研究的热点。然后，Spi演算模型中还存在某些不足，更重要的是基于原有的互模拟关系的方法仅限于人工完成，不能实现自动验证。 我们的工作是针对上述不足之处展开的，目标是扩充Spi演算语言，在此基础上建立新型的互模拟等价关系，并实现该关系的自动证明，从而设计出安全协议互模拟等价性自动验证工具。主要研究内容和创新之处在于以下三点： 1)扩充Spi演算语言，为密文通讯协议建立了新型Spi演算模型。扩充Spi演算语法，建立了公钥密码操作原语，使之能表示所有密钥体制的安全协议；修改了Spi演算中并发语义，限制了原先通道可以传递的机制，使之能描述协议中通讯主体跟其环境直接交互，从而可以更确切地刻画现实中的安全协议； 2)在新Spi演算里设计了符号操作语义和符号互模拟。我们的符号操作语义使输入进程仅接收环境中有意义的带符号的消息项，这样就很好地解决了输入进程可能产生的无穷分支问题。定义的符号Reefed互模拟确保了两个进程只需要执行有限次的迁移动作，就可以判断出它们是否互模拟； 3)建立并证明了符号Reefed互模拟与原具体互模拟之间的可靠性关系，从而可以设计安全协议的互模拟等价性验证工具。 基于这项工作，可以实现安全协议的互模拟等价关系的自动验证，我们相信这对于应用在软件和集成电路中的自动检测也有很大的启发作用。本文最后做出了全文总结，并对本领域未来的研究提出了新的展望。

目录

文摘

英文文摘

第一章引言

第二章形式化研究的主要方法

第三章Spi演算下的互模拟分析方法

第四章互模拟等价的自动验证

第五章本文总结和展望

致谢

参考文献

发表的论文

原创性声明及关于学位论文使用授权的声明