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

安全协议在网络信息安全中扮演着重要角色,但保证安全协议的正确是一个很困难的问题。现在,许多形式化方法都被用来分析安全协议,本文中我们研究各种方法的基本思想、它的优缺点、发展趋势以及方法之间的关系。最后,说明安全协议形式化分析的困难所在。

密码协议形式化分析方法研究

项目背景 南京邮电大学计算机系于2001年起,就对密码协议形式化分析方法研究课题向国家有关部门提出了申请.该课题先后得到了国家自然科学基金(60173037和70271050)、江苏省自然科学基金和江苏省自然科学基金预研项目(BK200421 8)、江苏省高技术研究计划(BG2004004)、国家高科技项目八六三(2004AA775053)、江苏省计算机信息处理技术重点实验室基金(kjs03061和kjs04)资助.该文对当前密码协议的主要形式化分析方法进行了总结和概述,依据其不足或缺陷提出了一些改进的思路,并探讨了密码协议形式化分析方法今后的发展趋势.

一种改进的基于认证测试的形式化分析方法

近年来,认证测试定理得到了改进,并应用于各种安全协议的分析。但是这些改进定理在应用范围和准确性方面存在一定的缺陷。针对这些缺陷,文章提出了一种改进的输入测试定理及加密测试定理,并给出了改进定理的证明。通过分析认证测试中常规节点的判定、证明过程中的错误、参数一致性证明过程中的不准确性和错误,指出了认证测试在使用过程中的缺陷。基于这些缺陷,文章提出了一种改进的基于认证测试的形式化分析方法——递归测试,并通过该方法证明了BAN-Yahalom协议。分析结果表明,该方法扩大了认证测试使用范围,且可以有效地、准确地分析安全协议。

安全协议的形式化分析方法初探

安全协议是网络安全的重要因素,但是它并不完善,我们需要用形式化的方法去分析它是否具有相应的安全属性。本文主要分析了三类典型的安全协议形式化分析方法,研究这些方法的基本思想和优缺点,并提出了形式化分析方法中存在的问题及可行的解决办法。

安全协议形式化分析方法综述之一:基于推理结构性方法

本文给出了基于推理结构性安全协议形式化分析方法的一个全面综述,分析了此类方法中的各种逻辑系统的优势与不足。

安全协议形式化分析方法综述之二——基于攻击结构性方法

本文给出了现行的基于攻击结构性方法的分类,分析了各类工具的特点。

Casper/FDR和串空间在物联网通信协议中的形式化分析

通过应用实例研究了如何用Casper/FDR和串空间两种分析方法对通信协议进行形式化分析:用Casper/FDR对协议的有穷状态进行穷举验证,当发现协议漏洞时会自动给出攻击的迹,但是此方法会产生状态爆炸的问题;串空间方法正好可以解决状态爆炸问题,用串空间对协议的各种状态进行证明,但是如果发现了协议漏洞,该方法不能给出攻击者的迹。

一种颜色Petri网的电子商务协议分析方法

针对现有颜色Petri网方法未能分析时限性的缺点,提出一种基于颜色Petri网的电子商务协议分析方法,用于分析可追究性、公平性和时限性三个重要安全属性.针对时限性建立了表示主体是否成功接收消息的状态颜色集和主体自定义的时间颜色集,并充分考虑时限性对公平性的影响,更加有效地分析公平性.文中以KZG协议为例,建立了KZG的分层颜色Petri网模型,利用CPN Tools工具对该模型仿真运行,并通过状态空间和查询函数分析了协议的性质,证明了本方法的有效性.

统一的安全属性形式化描述方法的研究

安全属性的基于特定分析方法和限于特定属性的形式化描述严重影响了安全协议形式化分析方法的有效性和适用性。为解决这个问题,本文提出了一种统一的形式化描述方法,即通过属性动作之间的匹配关系来表达协议的安全属性。用这种方法详细分析了认证属性、保密属性以及公平性属性的形式化表达。通过比较分析,该方法与其他方法相比,具有准确、简洁和扩展性强的特点,在总体上优于其他方法。

基于形式化分析法的情报应用模式研究

网络信息环境下大数据的兴起为情报学领域带来新机遇和新挑战,该文简述了情报与情报分析的概念,指出情报分析员面临的现实挑战,对情报分析法的特点优势进行了概述,归纳了形式化情报分析法的5种应用模式,为弥补情报界在分析技术方面的不足提供了借鉴,帮助分析人员克服思维误区,为明智决策、任务成功提供更优化的情报支持。

协议主体密钥在测试组件构造上的性质分析

针对认证测试理论在测试组件构造方面缺少具体形式化构造规则的不足,根据协议主体在认证测试中的角色特点,以及包含惟一源发消息的消息组件在认证测试中的作用和性质,对消息组件进行分类和定义并提出认证测试模型的概念,基于认证测试模型给出协议主体密钥在测试组件构造上的性质命题,同时运用认证测试基础理论对命题进行正确性证明,从而确定测试组件构造的形式化规则。

基于串空间理论的kerberos协议的安全性分析

运用串空间这一前沿的安全协议形式化分析方法,对kerberos协议的安全性进行了分析,得出了协议满足认证性和机密性的结论,并给出了一种新的kerberos协议的形式化证明方法,扩展了串空间理论在实用协议分析方面的应用。

基于形式化分析法的情报模式研究

网络信息环境下大数据的兴起为情报学领域带来新机遇和新挑战,该文简述了情报与情报分析的概念,指出情报分析员面临的现实挑战,对情报分析法的特点优势进行了概述,归纳了形式化情报分析法的5种应用模式,为弥补情报界在分析技术方面的不足提供了借鉴,帮助分析人员克服思维误区,为明智决策、任务成功提供更优化的情报支持。

BAN类逻辑的由来与发展

BAN(Burrows,Abadi and Needham)类逻辑可以辅助设计、分析和验证网络和分布式系统中的密码协议。该文介绍了 BAN逻辑的产生、成分和分析步骤 ,进而全面指出了 BAN逻辑的缺陷 ,由此而产生的改进的 BAN逻辑和现状 ,从而对 BAN类逻辑作了全面的回顾与展望 ,并得出结论 :BAN类逻辑仍然是密码协议分析和设计的主要工具 ,但理想化步骤是 BAN类逻辑的致命缺陷。指出了 BAN类逻辑研究工作的展望。