一种分析和设计安全协议的新逻辑

摘要

安全协议是一种面向应用层的协议，它为通信的实体打上包装，穿上盔甲，防止攻击者对敏感数据进行窃取，保证通信内容的完整性。不同的应用需求对安全协议的设计也提出了新的要求，如组通信、匿名通信、安全多方计算、不可抵赖的签名、盲签名、群盲签名和数字现金等安全技术都要依靠安全协议来实现，所以安全协议的安全性显得特别重要。 随着信息技术的发展，信息安全成为人们普遍关心的话题。人们已经逐渐习惯于在网上进行办公、交流，在网上进行着各种商品的交易，因此网络安全问题是当今的一个研究热点。怎样在不安全的环境中进行秘密通信?这个问题主要通过安全协议来解决，所以安全协议是网络安全成败的关键所在。 本文在分析了安全协议分析的现状和安全协议设计的现状的基础上，提出了一种可以用来分析和设计安全协议的新逻辑，并结合串空间模型来证明了新逻辑的正确性。最后以几个比较有代表性的例子来说明新逻辑的具体应用。具体来说，本文取得了下面一些成果： (1)给出了新逻辑的构成，包括新逻辑的符号、新逻辑的推理规则和新逻辑的合成规则。其中推理规则是用来分析安全协议的，主要看安全协议能否达到最终目标，而合成规则是用来对安全协议进行设计的。 (2)给出了新逻辑的语义。串空间模型是安全协议分析的一种重要工具，它具有良好的语义，但其分析过程难度较大。新逻辑分析安全协议的过程比较容易操作，但逻辑本身的语义不是很清晰。本文把新逻辑和串空间模型结合起来，给出了新逻辑的串空间语义，从而证明了新逻辑的正确性。 (3)运用新逻辑来分析安全协议。用新逻辑的推理规则结合安全协议执行的初始条件以及安全协议执行的步骤，分析安全协议是否能达到目标，如果不能，那说明安全协议是存在缺陷或者漏洞的。 (4)运用新逻辑来设计安全协议。从安全协议的目标出发，运用合成规则可以把安全协议要达到的目标分成许多子目标，然后分别考察各个子目标，直到各个子目标都满足为止。最后综合设计的整个过程给出安全协议的形式化描述。 (5)新逻辑将安全协议的分析和设计过程纳入一个框架中进行，消除了用不同的方法来分析和设计安全协议可能导致的不一致性。 (6)简化了分析和设计过程中的对初始条件和安全协议目标分别进行形式化的过程。如果用不同的方法来分析和设计安全协议，需要对安全协议运行的初始条件和安全协议目标形式化两次。而在新逻辑中，对初始条件和安全协议目标的形式化过程只需要做一次，从而提高了工作效率。 安全协议是信息安全和网络安全的核心所在。在某种意义上说，只要解决了安全协议的安全性问题，那么信息安全和网络安全的问题就容易解决得多。本文致力于解决安全协议的安全性问题，虽然取得了一些成果，但仍然存在一些不足，比如新提出来的逻辑不具有完备性。在安全协议消息比较多的情况下，如果用计算机来自动实现安全协议的分析和设计，容易产生组合爆炸。

目录

文摘

英文文摘

西南交通大学学位论文版权使用授权书及西南交通大学学位论文创新性声明

第1章绪论

第2章基础知识

第3章分析和设计安全协议的新逻辑

第4章分析和设计安全协议的新逻辑的语义

第5章分析和设计安全协议的新逻辑的应用

结论

致谢

参考文献

攻读博士学位期间发表的论文及科研成果