检索结果-南通市图书馆

在线全文

学校读者我要写书评

暂无评论

安全协议的设计与逻辑分析

软件学报 2003年第7期14卷 1300-1309页

作者：卿斯汉中国科学院信息安全技术工程研究中心

随着网络应用的迅速发展,网络安全的问题日益重要.研究下述课题:安全协议的设计原则;安全协议设计中形式化方法的应用;各种形式化分析方法,特别是逻辑分析方法的特点.另外,还探讨了串空间模型在逻辑分析中的应用以及串空间模型指导安全... 详细信息

随着网络应用的迅速发展,网络安全的问题日益重要.研究下述课题:安全协议的设计原则;安全协议设计中形式化方法的应用;各种形式化分析方法,特别是逻辑分析方法的特点.另外,还探讨了串空间模型在逻辑分析中的应用以及串空间模型指导安全协议形式化设计的可能性.

关键词：安全协议设计逻辑分析 BAN类逻辑串空间

在线全文

学校读者我要写书评

暂无评论

安全协议多目标语言代码自动化实现方案

通信学报 2012年第9期33卷 152-159页

作者：李兴华李帅团李登马建峰西安电子科技大学计算机学院陕西西安710071 南京大学计算机软件新技术国家重点实验室江苏南京210032

提出了安全协议多目标语言代码自动化实现方案。首先,基于XML语言,设计了安全协议描述方法;其次,开发了一个图形用户接口GUI,用户通过GUI配置安全协议,自动化生成协议的XML描述文档;最后,设计并实现了一个安全协议编译器,将先前得到的XM... 详细信息

提出了安全协议多目标语言代码自动化实现方案。首先,基于XML语言,设计了安全协议描述方法;其次,开发了一个图形用户接口GUI,用户通过GUI配置安全协议,自动化生成协议的XML描述文档;最后,设计并实现了一个安全协议编译器,将先前得到的XML描述文档作为输入,生成所需的目标语言代码。分析表明同已有方案相比,该方案具有明显的优势。

关键词：安全协议代码实现自动化 XML

安全协议的扩展Horn逻辑模型及其验证方法

在线全文

学校读者我要写书评

暂无评论

计算机学报 2006年第9期29卷 1666-1678页

作者：李梦君李舟军陈火旺国防科学技术大学计算机学院长沙410073 北京航空航天大学计算机科学与工程学院北京100083

分析了Bruno Blanchet和Martin Abadi提出的基于Horn逻辑的安全协议模型及其验证方法,针对它们构造不满足安全性质的安全协议反例的不足,提出了安全协议的扩展Horn逻辑模型和修改版本的安全协议验证方法,使得能够从安全协议的扩展Horn... 详细信息

分析了Bruno Blanchet和Martin Abadi提出的基于Horn逻辑的安全协议模型及其验证方法,针对它们构造不满足安全性质的安全协议反例的不足,提出了安全协议的扩展Horn逻辑模型和修改版本的安全协议验证方法,使得能够从安全协议的扩展Horn逻辑模型和修改版本的安全协议验证过程中自动构造不满足安全性质的安全协议反例.在基于函数式编程语言Objective Caml开发的安全协议验证工具SPVT中,实现了上述算法,验证了算法的正确性.

关键词：安全协议扩展Horn逻辑模型形式化验证

安全协议逻辑程序不停机性快速预测的动态方法

在线全文

学校读者我要写书评

暂无评论

计算机学报 2011年第7期34卷 1275-1283页

作者：周倜李梦君李舟军国防科学技术大学计算机学院长沙410073 北京航天飞行控制中心软件室北京100094 北京航空航天大学计算机学院北京100083

基于一般逻辑程序停机性刻画的动态方法,研究了解形式不动点不停机的一种动态刻画方法,给出了安全协议Horn逻辑扩展模型解形式不动点不停机性的一个充分条件.基于这个充分条件给出了一种不动点计算不终止的预测方法,该方法能够根据新产... 详细信息

基于一般逻辑程序停机性刻画的动态方法,研究了解形式不动点不停机的一种动态刻画方法,给出了安全协议Horn逻辑扩展模型解形式不动点不停机性的一个充分条件.基于这个充分条件给出了一种不动点计算不终止的预测方法,该方法能够根据新产生的解形式逻辑规则,预测不动点计算的不终止性,同时定位模型中导致解形式不动点无穷计算的解形式逻辑规则.解形式不动点不停机性的预测结果将作为选择精确验证方法或者抽象验证方法验证安全协议的基本依据.相关实验结果表明文中给出的预测算法是高效的.

关键词：安全协议验证不动点计算不停机性预测

在线全文

学校读者我要写书评

暂无评论

安全协议的SPIN建模与分析

南京航空航天大学学报 2009年第5期41卷 672-676页

作者：陈春玲田国良南京邮电大学软件学院南京210003

总结了利用模型检测工具SPIN对安全协议进行建模的方法。以Helsinki协议和Helsinki改进协议作为分析实例,用Promela语言建模并使用SPIN对模型进行行为模拟和属性校验,发现了Helsinki存在的Horng-Hsu攻击漏洞以及Helsinki改进协议存在的... 详细信息

总结了利用模型检测工具SPIN对安全协议进行建模的方法。以Helsinki协议和Helsinki改进协议作为分析实例,用Promela语言建模并使用SPIN对模型进行行为模拟和属性校验,发现了Helsinki存在的Horng-Hsu攻击漏洞以及Helsinki改进协议存在的DoS攻击隐患。该方法具有较好的通用性,容易推广到有多个主体参与的安全协议的分析。

关键词：安全协议 Helsinki协议 Promela语言建模

在线全文

学校读者我要写书评

暂无评论

安全协议20年研究进展

软件学报 2003年第10期14卷 1740-1752页

作者：卿斯汉中国科学院信息安全技术工程研究中心中国科学院软件研究所信息安全国家重点实验室北京100080

总结了安全协议的20年研究进展情况,指出形式化方法在安全协议的设计与分析中的重要应用.对安全协议的若干热点研究方向进行了归纳和展望.

关键词：安全协议设计分析形式化方法

在线全文

学校读者我要写书评

暂无评论

安全协议的形式化规范

电子与信息学报 2004年第4期26卷 556-561页

作者：胡成军郑援吕述望沈昌祥海军潜艇学院信息研究所青岛266071 中国科学院研究生院信息安全国家重点实验室北京100039 海军计算技术研究所北京100841

该文给出用PVS(Prototype Verification System)对安全协议进行形式化规范的一种方法。该方法以高阶逻辑为规范语言,利用trace模型来描述协议的行为,并假设系统中存在强攻击者和理想加密系统。重要的结构如消息、事件、协议规则等都... 详细信息

该文给出用PVS(Prototype Verification System)对安全协议进行形式化规范的一种方法。该方法以高阶逻辑为规范语言,利用trace模型来描述协议的行为,并假设系统中存在强攻击者和理想加密系统。重要的结构如消息、事件、协议规则等都通过语义编码方式定义.

关键词：安全协议形式化规范 PVS 高阶逻辑 trace模型语义编码

在线全文

学校读者我要写书评

暂无评论

安全协议的时限责任分析

电子学报 2002年第10期30卷 1450-1454页

作者：梁坚敖青云尤晋元上海交通大学计算机科学与工程系上海200030

本文针对安全协议中的时限责任问题 ,提出结合责任性与新鲜性来分析时间标记 .这种思路体现在我们新的时限逻辑框架中 ,比较Kudo[8] 的方法 ,新的逻辑体系因为有对消息完整性的判断 ,能更有效地防止消息的篡改与重发攻击 ,且更加简洁和... 详细信息

本文针对安全协议中的时限责任问题 ,提出结合责任性与新鲜性来分析时间标记 .这种思路体现在我们新的时限逻辑框架中 ,比较Kudo[8] 的方法 ,新的逻辑体系因为有对消息完整性的判断 ,能更有效地防止消息的篡改与重发攻击 ,且更加简洁和实用 .

关键词：安全协议时限责任形式化分析 Kudo逻辑

在线全文

学校读者我要写书评

暂无评论

分析安全协议猜测攻击的模态逻辑方法

计算机学报 2007年第6期30卷 924-933页

作者：毛晨晓罗文坚王煦法中国科学技术大学计算机科学与技术系合肥230027

以CKT5逻辑为基础,对其进行了多方面重要的扩展;在原有对称密钥机制的基础上,增加了公开密钥机制和Vernam加密机制以增强其描述协议的能力;打破完善加密假设,给出了一组定义和规则使主体具备猜测和验证口令的能力;给出了与在线猜测攻击... 详细信息

以CKT5逻辑为基础,对其进行了多方面重要的扩展;在原有对称密钥机制的基础上,增加了公开密钥机制和Vernam加密机制以增强其描述协议的能力;打破完善加密假设,给出了一组定义和规则使主体具备猜测和验证口令的能力;给出了与在线猜测攻击相关的定理以反映在线猜测攻击的特点;通过相关引理和定理的证明,简化了猜测攻击的分析过程,使该文方法比现有方法更加简洁高效.扩展后的逻辑能够用于分析安全协议的猜测攻击,包括在线猜测攻击.

关键词：安全协议猜测攻击 CKT5逻辑模态逻辑形式化分析