基于进程演算的安全协议形式化研究

代理获取

页面导航

目录
摘要
著录项
相似文献
相关主题

摘要

随着网络技术的应用逐步渗透到许多关键部门，以及电子商务的兴起与广泛应用，信息安全已变得日益重要。安全协议是信息安全的基础，但其正确性和安全性却不容乐观，已有的安全协议往往被证实并不如设计所期望的那样安全．即使不考虑与实现相关的协议缺陷和密码系统被成功破译的可能性，复杂的网络环境还是使得攻击者可利用安全协议自身的缺陷来实施各种各样的攻击．因此，安全协议是否能达到它所要求的安全目标是非常关键的问题。对安全协议的分析和验证是保证所设计的协议满足其安全性的重要技术手段，而借助形式化的方法或工具分析安全协议是非常必要而且行之有效的．安全协议的形式化分析已有二十多年的历史，已逐渐成为安全协议研究的热点。近十几年来，世界各国学者对其进行了广泛和深入的研究，尤其是美国和欧洲的一些国家在这一关键领域投入了大量的研究经赞和力址．同时，安全协议设计和分析也引起了国内研究人员的高度重视．虽然安全协议形式化研究领域取得了可喜的成果，但尚有诸多问题亟待解决，譬如，如何精确刻画安全协议，如何扩充现在已经成热的理论或方法去研究更多的安全性质，如何使安全性质在统一的框架下进行分析和验证等等。安全协议是一个典型的并发分布式系统，而进程演算是一个强有力的并发分布式系统建模工具，具有强大的描述能力和严格的语义，能够精确刻画安全协议中各个参与者之间的交互行为．利用进程演算对安全协议进行分析和验证时，既可以借鉴其作为代数模型的基本验证理论与方法，又可以使用其作为抽象程序设计语言的程序分析方法．然而，由于进程演算固有的缺乏数据结构支持的特点，难以建模主体拥有的知识以及知识推理，以至于只能分析很少的安全性质,另一方面，基于知识和信念的逻辑推理方法可以为协议消息和主体建模，但是缺乏推导主体行为的机制．而且，协议的理想化过程过于依赖分析者的直觉，其困难常常导致分析结论的错误．所以，我们将进程演算和知识推理二者实现优势互补，以进程演算为基础，嵌入消息知识推理系统，为安全协议建模和分析．本文的主要成果和创新如下： 1．本文详细探讨了安全协议形式化分析的各种方法，尤其是基于进程演算的各种分析手段，并做了两个实例研究：一是在对spi演算进行适当扩展的基础上分析了 Kerberos协议的认证性，二是以Applied π-演算为基础分析了iKP协议的认证性和匿名性。 2．以进程演算为基础，结合协议主体知识的逻辑推理以弥补进程演算固有的缺乏数据结构支持的特点，建立一个适合于安全协议形式化分析的一般模型GSPM,它可以精确刻画安全协议，在统一的框架下形式化描述和验证各种安全性质．GSPM 中的进程演算部分描述了协议参与主体的演化行为，逻辑部分使用了一系列推理规则推理主体的知识．嵌入的知识推理系统具有可扩展性，可以加入新的推理规则更深入地分析安全协议．此外，GSPM不为攻击者行为单独建模，既最大化了攻击者能力，又简化了协议的分析过程。 3．以GSPM为基础分析验证安全性质 (a)基于GSPM，定义了一步可达关系和多步可达关系两个概念，利用可达关系概念形式化地描述了安全协议的保密性，并以TMN协议为例作了实例研究． (b)在给出了GSPM的LTS操作语义的基础上，形式化地定义了安全协议的认证性，并以NSPK协议为例作了实例研究． (c)基于GSPM的变体GSPM，采用博弈思想形式化地定义了公平交换协议的非否认性和公平性，并以一种认证邮件机制-MD机制为例作了实例研究． (d)对其它安全性质的形式化描述进行了讨论． 4．在GSPM的变体GSPM+的基础上提出了一个环境敏感的抽象互模拟等价关系，形式化地定义了保密性和认证性，并做了简单的实例分析． 5．引入了符号化技术解决GSPM中等待输入消息时导致的无限分叉问题．在等待输入一个匹配项时，将环境能产生的消息项分成有限类，产生有限个替换，选择某个替换进行迁移，并把替换记录在迁移过程中，非常技巧性地将迁移过程中可能产生的无穷分叉变成了有限分叉．我们分别在以GSPM为基础的可达关系、LTS 和博弈语义中引入符号化技术，并以实例分析作了说明．符号化技术的采用为我们正在开发的自动验证工具奠定了基础．

著录项

作者
顾永跟;
展开▼
作者单位

上海交通大学;

展开▼
授予单位上海交通大学;
学科计算机软件与理论
授予学位博士
导师姓名傅育熙;
年度 2005
页码
总页数
原文格式 PDF
正文语种中文
中图分类 TP393.08;
关键词
安全协议; 形式化方法; 安全性质; 进程演算; 符号化技术;

相似文献

中文文献
外文文献
专利

1. 基于进程演算和知识推理的安全协议形式化分析 [J] . 顾永跟 ,傅育熙 . 计算机研究与发展 . 2006,第005期
2. 基于类pi演算的电子支付协议安全性形式化研究 [J] . 顾永跟 ,李国强 ,王国钧 . 计算机应用研究 . 2006,第003期
3. 基于Spi演算的Kerberos认证协议形式化研究 [J] . 李国强 ,顾永跟 ,傅育熙 . 计算机科学 . 2004,第011期
4. 基于强化学习的安全协议形式化验证优化研究 [J] . 杨锦翔 ,熊焰 ,黄文超 . 计算机工程 . 2021,第012期
5. 基于串空间的安全协议形式化分析研究 [J] . 姚萌萌 ,唐黎 ,凌永兴 . 信息网络安全 . 2020,第002期
6. 基于进程演算的安全协议形式化分析 [C] . 顾永跟 ,傅育熙 ,朱涵 . 2005年全国理论计算机科学学术年会 . 2005
7. 基于进程演算的安全协议形式化研究 [A] . 李国强 . 2005

基于进程演算的安全协议形式化研究

目录

摘要

著录项

相似文献

相关主题

期刊订阅