基于Strand空间模型的安全协议分析方法研究

摘要

该文通过对基于Strand空间模型的安全协议分析方法的研究,提出了用于提高安全协议分析效率的改进的状态空间简化技术.在协议分析过程中,将一般的状态空间简化技术与剪枝定理相结合,不但删除了协议运行的冗余状态,而且删除了协议运行的不可达状态,从而有效地简化了状态空间,大大减少了协议分析的工作量.也就是说,在协议分析过程中,令入侵者总是截获诚实主体发送的消息,并以该消息丰富其知识集合,以便增强其攻击能力;同时,入侵者总是等待诚实主体没有消息发送的时候才重发或伪造消息给协议主体,从而使入侵者每次发送消息前,其知识集合都尽可能完备,以便形成最有效的攻击.以上两种简化技术的应用删除了协议运行的大量冗余状态,并且不会遗漏导致攻击的状态.为了删除协议运行的不可达状态,在协议分析时,可根据协议特点,设计适用于该协议的剪枝定理.对于协议分析中的每个状态,首先以剪枝定理判断该状态的可达性,再确定是否需要对该状态进行进一步扩展.剪枝定理的应用删除了协议运行的不可达状态,进一步简化了状态空间.在Strand空间模型的基础上,通过在安全协议分析算法的设计中选择合理的状态结构记录协议的运行情况,使该改进的状态空间简化技术易于实现.即通过使入侵者知识集合尽量完备,并且随着其知识的增加,删除其中的冗余信息,有利于入侵者生成攻击时所需要的消息;通过优先绑定发送消息的节点,并使入侵者总是截获诚实主体发送的消息,有效删除了协议分析中的冗余状态,并将诚实主体发送的消息用于丰富入侵者知识集合,从而增强了入侵者的能力;通过在状态转换前检查状态的可达性,删除了协议分析中的不可达状态以及以这些状态为根的状态转换子树.作为利用该技术简化安全协议分析的实例,在对Needhan-Schroeder-Lowe协议的分析过程中,以认证定理作为剪枝定理,将其与一般的简化技术相结合,简化了该协议的分析过程.并且根据该设计思想,通过VB下的程序设计,实现了对Needhan-Schroeder协议的认证性质分析.总之,在Strand空间模型的基础上,在协议的认证性质分析过程中,通过将状态空间简化技术与剪枝定理相结合,减少了协议分析的工作量,提高了协议分析的效率,达到了预期的设计目标.

目录

文摘

英文文摘

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

1引言

1.1安全协议形式化分析方法的研究现状

1.2安全协议形式化分析方法研究的发展趋势

1.3基于Strand空间模型的安全协议分析方法研究的意义

2 Strand空间模型

2.1消息项

2.2 Strand、Strand空间和Bundle

2.2.1 Strand和Strand空间

2.2.2 Bundle

2.3利用Strand进行协议说明

2.4入侵者模型

3认证检验

3.1可入侵密钥和安全密钥

3.2输出检验与输入检验

3.3认证检验

3.3.1利用输出检验的认证检验

3.3.2利用输入检验的认证检验

3.4认证检验证明协议的正确性

4状态空间简化技术在安全协议分析中的应用

4.1状态空间简化技术

4.1.1一般的状态空间简化技术

4.1.2不可达定理

4.2状态空间简化技术应用说明

5基于Strand空间模型实现安全协议认证性质分析

5.1目标和节点绑定

5.2状态结构

5.3模型检查算法

5.3.1后继状态转换算法

5.3.2更新入侵者知识集合

5.3.3生成可接受项的集合

5.4安全协议认证性质分析

5.4.1用于认证协议分析的剪枝定理

5.4.2 Needham-Schroeder-Lowe协议

5.4.3 Needham-Schroeder仂议

6结束语

参考文献

致 谢

攻读硕士学位期间发表的学术论文目录

学位论文评阅及答辩情况表