检索结果-南通市图书馆

在线全文

学校读者我要写书评

暂无评论

针对猜测攻击的Athena方法的扩展

计算机科学 2007年第12期34卷 65-67,81页

作者：李超董荣胜桂林电子科技大学计算机系桂林541004

猜测攻击是安全协议中一类特殊问题,对其进行研究具有现实意义。本文针对猜测攻击,引入了基于串空间模型的Athena分析方法,并考虑了攻击者对弱口令的猜测能力。为此,在串空间模型的消息项中引入了可验证项的概念,以描述猜测攻击条件中... 详细信息

猜测攻击是安全协议中一类特殊问题,对其进行研究具有现实意义。本文针对猜测攻击,引入了基于串空间模型的Athena分析方法,并考虑了攻击者对弱口令的猜测能力。为此,在串空间模型的消息项中引入了可验证项的概念,以描述猜测攻击条件中的验证项,同时扩展了串空间中攻击者的能力,赋予了攻击者对弱口令的猜测能力;为在Athena后继函数搜索算法中实现对验证项的关联,以判断猜测攻击,在Athena方法的状态表示法中引入猜测验证目标及猜测验证目标绑定的概念,对状态、推理规则进行相应的修改,同时扩展后继状态函数,使扩展后的函数具备分析猜测攻击的能力;最后运用扩展后的Athena方法对会话密钥建立协议(key-establishment protocol)进行分析。分析发现,当pk为对称密钥时,协议存在猜测攻击,并给出了攻击路径。

关键词： Athena 猜测攻击串空间弱口令认证性

改进的OpenID Connect协议及其安全性分析

在线全文

学校读者我要写书评

暂无评论

计算机应用 2017年第5期37卷 1347-1352页

作者：鲁金钿尧利利何旭东孟博中南民族大学计算机科学学院武汉430074

Open ID Connect协议是最新的单点登录协议之一,已经广泛应用于用户身份认证领域,其安全性受到了人们的重点关注。为增强Open ID Connect协议的安全性,首先引入数字签名及非对称加密技术,对其进行改进,重点关注改进后协议的秘密性和认证... 详细信息

Open ID Connect协议是最新的单点登录协议之一,已经广泛应用于用户身份认证领域,其安全性受到了人们的重点关注。为增强Open ID Connect协议的安全性,首先引入数字签名及非对称加密技术,对其进行改进,重点关注改进后协议的秘密性和认证性;其次基于符号模型,应用应用PI演算对改进的Open ID Connect协议进行形式化建模;然后为验证改进后协议的认证性和秘密性,分别使用非单射性和query对认证性和秘密性进行建模;最后把改进的Open ID Connect协议的应用PI演算模型转换为安全协议分析工具ProVerif的输入,应用ProVerif对其进行形式化分析。实验结果表明,改进后的Open ID Connect协议具有认证性和秘密性。

关键词：非对称加密数字签名认证性符号模型形式化方法 Pro Verif

基于Spi演算的密码协议自动化分析技术研究

在线全文

学校读者我要写书评

暂无评论

基于Spi演算的密码协议自动化分析技术研究

作者：袁霖中国人民解放军信息工程大学

学位级别：硕士

密码协议是网络通信和许多分布式系统的安全基础,协议的正确性和安全性对于保证攻击者不能获得秘密信息或实施不公平认证起着至关重要的作用。由于在协议的设计过程中对协议运行环境的安全需求估计不足或采用技术不当,往往会导致密码协... 详细信息

密码协议是网络通信和许多分布式系统的安全基础,协议的正确性和安全性对于保证攻击者不能获得秘密信息或实施不公平认证起着至关重要的作用。由于在协议的设计过程中对协议运行环境的安全需求估计不足或采用技术不当,往往会导致密码协议存在安全漏洞或缺陷,且这些漏洞与缺陷往往只有在遭到恶意攻击时才会暴露出来,通过静态测试和手工验证方法,无法检测到协议的某些缺陷和对协议的潜在攻击,因此,密码协议自动化分析技术成为了研究热点。本文主要从分析和实现的角度对密码协议自动化分析技术进行了研究,所做的工作主要有以下几个方面: (1) 在对Spi演算研究的基础上,提出了一种扩展的Spi演算,并根据扩展Spi演算语法定义了密码协议的秘密性和认证性,给出了其便于自动化实现的分析方法。 (2)构建了一个基于扩展Spi演算的类型系统,给出了该类型系统的类型规则及相应的类型操作,并证明了如果一个进程在该类型系统被证明是类型完善的,则该进程不会泄漏秘密级别的数据。 (3)通过基于扩展Spi演算的类型系统证明了一个典型密码协议秘密性。 (4)利用逻辑程序方法,设计了一个以扩展Spi演算作为对密码协议形式化描述的自动化分析器,并介绍了其基本原理,证明了该分析器在密码协议秘密性的分析方法上与基于扩展Spi演算的类型系统是一致的。在秘密性分析的基础上给出了该分析器对密码协议认证性的分析原理。 (5)给出了扩展Spi演算对密码协议的描述到霍恩子句的转换规则,设计实现了协议分析器的自动翻译部分,完成了扩展Spi演算描述的协议到霍恩子句的自动转换。

关键词：密码协议 Spi演算类型系统霍恩子句秘密性认证性

安全协议的进程代数规约到逻辑程序的自动转换

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

计算机工程与科学 2006年第1期28卷 22-24,27页

作者：周倜李梦君刘万伟李舟军国防科技大学计算机学院湖南长沙410073

安全协议用于实现开放互连网络的安全通讯,它本质上是分布式并发程序,使用进程代数可以将其描述为角色进程的并发合成系统。使用抽象方法,安全协议角色进程并发合成模型可以转化为逻辑程序;通过计算逻辑程序的不动点,能够对安全协议无... 详细信息

安全协议用于实现开放互连网络的安全通讯,它本质上是分布式并发程序,使用进程代数可以将其描述为角色进程的并发合成系统。使用抽象方法,安全协议角色进程并发合成模型可以转化为逻辑程序;通过计算逻辑程序的不动点,能够对安全协议无穷会话的并发交叠运行进行验证。本文基于Objective Caml语言,实现了安全协议进程代数描述到安全协议逻辑程序的自动转化。

关键词：安全协议进程代数形式化验证认证性 Objective Canal

在线全文

学校读者我要写书评

暂无评论

适用于智能电网的组合密码体制研究

适用于智能电网的组合密码体制研究

作者：韩亚楠电子科技大学

学位级别：硕士

智能电网作为新一代的电力系统,它不再是一个单一的网络结构,而是利用先进的设备技术、传感和测量技术以及现代信息通讯技术等来实现可靠、高效、安全、环境友好等目标的智能电力系统。相对于传统的电网,智能电网的一个显著特色是实现... 详细信息

智能电网作为新一代的电力系统,它不再是一个单一的网络结构,而是利用先进的设备技术、传感和测量技术以及现代信息通讯技术等来实现可靠、高效、安全、环境友好等目标的智能电力系统。相对于传统的电网,智能电网的一个显著特色是实现了智能电表和电表数据管理系统之间的双向通信。这一特色使得智能电网能够实时地监控用户的用电信息,从而更好地维护电力系统的稳定。同时信息的频繁交互使智能电网更容易遭受监测、篡改、伪造等攻击。为了保护智能电网的稳定,智能电网通信消息的机密性和认证性成为近几年研究的热点。因此,如何解决智能电网中的安全问题是本文的主要工作。为了解决上述问题,在本篇论文中,我们首次将组合密码应用到智能电网中,从而设计出了一个高效的的密码通信协议来解决这些安全问题。本文的主要工作包括:(1)本文以双线性对为工具,首先提出了一个基于身份的在线/离线加密方案。在随机预言模型下,该方案能够在适应性选择密文攻击下满足密文不可区分性。同时该方案采用在线/离线的方式可以将消息在加密过程中大部分耗时的复杂运算提前在可信任的服务器上完成,而智能电网只需要完成少量简单的操作即可。此外,我们将该方案和现有的其他五个加密方案做对比,从计算成本和通信成本两方面进行了性能分析。最后我们利用MIRACL库对该方案进行了实现。(2)利用上述基于身份的在线/离线加密方案和一个高效的基于身份的在线/离线签名方案,我们构造了一个组合公钥密码方案。同时我们还给出了此组合公钥密码方案在随机预言模型下的安全性证明。此外,我们将组合密码方案的签名部分和现有的其他四个签名方案做对比,从计算成本和通信成本两方面进行了性能分析。最后,我们使用MIRACL库对组合密码方案的签名部分进行了实现。(3)我们设计了一个保障智能电网安全通信的密码协议,并利用逐跳路由传输方式减少了智能电表和电表数据管理系统之间的通信延时。因此该协议能更好地保障智能电网的实时特性。此外我们具体的展示了整个协议的通信过程,并给出了该协议的安全和性能分析。

关键词：智能电网认证性机密性组合公钥密码体制

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

分层哈希链表及其在数据查询认证中的应用

分层哈希链表及其在数据查询认证中的应用

作者：杨牧洲东北大学

学位级别：硕士

分布式环境下的数据发布模式与传统的,数据拥有者承担用户查询处理的集中式模式相比具有网络等待时间短,服务器维护便宜,抗DDoS攻击等一系列的优势,具有广阔的应用前景。然而在分布式网络环境中,发布服务器的可信性很低,因而保证查询结... 详细信息

分布式环境下的数据发布模式与传统的,数据拥有者承担用户查询处理的集中式模式相比具有网络等待时间短,服务器维护便宜,抗DDoS攻击等一系列的优势,具有广阔的应用前景。然而在分布式网络环境中,发布服务器的可信性很低,因而保证查询结果的正确性,正成为这一领域中研究的热点。认证跳表等方案在处理简单的查询认证问题方面性能优秀,但无法正确认证诸如关系查询等复杂查询的结果。近年来一些学者提出的签名链方案弥补了该缺点,但对每个数据项都签名的实现手段却使其效率过低。本文在分析了现有数据认证方案不足的基础上,提出了分层哈希链表(Hierarchical Hash Linklist, HHL),给出了HHL的构建、更新、查询和认证算法。通过对HHL中冗余哈希节点的分析,提出了效率更优秀的分层哈希链表改进方案,将其应用于分布式环境下的三方认证模型中。通过利用统计学的方法对HHL的代价进行理论分析,指出其拥有O(logn)的代价。并列举多种破坏数据认证性的手段对应用HHL的认证模型进行安全性分析,表明该模型能够检测出任何一种对查询结果认证性的破坏行为。将HHL与签名链方案进行了仿真比较,实验数据表明HHL在通信及计算等认证代价方面要优于签名链方案。本文将HHL应用于关系查询结果的认证中,解决了不同种类关系查询的结果认证问题。设计并实现了一个数据查询认证原型系统,保证了在分布式数据发布中,发布服务器只返回用户想要的结果,但却能提供足够的证据证明所有的返回结果都具有认证性和来源可靠性。研究结果表明基于HHL的数据认证在空间和时间方面是高效的。

关键词：数据认证分布式数据发布 HHL 认证性关系查询

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

基于计算模型生成密码学安全的安全协议代码

基于计算模型生成密码学安全的安全协议代码

作者：牛乐园中南民族大学

学位级别：硕士

目前安全协议的安全性仍是学术界关注的重点,但是安全协议的安全性分析仅仅停留在对安全协议抽象分析和验证方面,很难应用于日常研究中,而且在安全协议的代码实现中难免会出现一些人为漏洞,这可能会给安全协议引入更大的漏洞。安全协议... 详细信息

目前安全协议的安全性仍是学术界关注的重点,但是安全协议的安全性分析仅仅停留在对安全协议抽象分析和验证方面,很难应用于日常研究中,而且在安全协议的代码实现中难免会出现一些人为漏洞,这可能会给安全协议引入更大的漏洞。安全协议代码的一般安全性(如数组下标越界、内存泄露、类型安全等),国内外学者已经做了很多有效的工作,但是关于安全协议实现代码的研究人们做的工作很少,故本文重点关注安全协议代码的密码学安全性。安全协议的最主要的安全性分析方法有两种,一种是构造攻击下的安全性分析,另外一种是模型形式化分析。本文基于安全协议的模型形式化分析方法,由代码级出发,进而研究安全协议的安全性,也就是对安全协议代码的安全性进行研究,以得到具有更强实用性的安全协议代码。针对这些问题,本文首先对概率标号迁移系统进行研究,探索提出安全协议代码的密码学安全性模型;其次探索应用概率进程演算:Blanchet演算建模安全协议抽象规范的方法,给出安全协议抽象规范建模的模版;以Blanchet演算建立的安全协议抽象规范模型为基础,研究代码转换的可行性,并建立与Java代码之间的映射关系。本文探索从安全协议抽象规范模型生成安全协议Java代码SP[Java]的方法。从进程、角色、目标多方面来建立Blanchet演算语言的映射模型,介绍转换软件的词法分析器、语法分析器、简化器、模板器的工作原理来阐述软件的开发过程。最后开发生成安全协议Java代码的自动化转换软件工具CV2JAVA。本文最后基于计算方法的自动化证明工具Crypto Verif证明SSHV2协议的抽象模型具有认证性,同时使用自动转换软件CV2JAVA对SSHV2建立的Blanchet演算模型语言进行转换,生成SSHV2的规范流程Java核心代码。SSHV2协议生成的核心代码嵌入Java环境进行验证分析,结果表明生成的安全协议代码具有SSHV2协议定义的身份认证性。

关键词：安全性协议实现代码形式化分析抽象模型认证性

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

基于事件逻辑的移动支付协议形式化分析

基于事件逻辑的移动支付协议形式化分析

作者：杨科华东交通大学

学位级别：硕士

随着移动设备的迅速普及以及移动互联网的飞速发展,移动支付给人们的生活带来很大的便利。移动支付是实现移动电子商务交易成功的关键环节,安全的移动支付协议是保障移动支付顺利进行的基石。由于安全协议往往运行在复杂的、不安全的网... 详细信息

随着移动设备的迅速普及以及移动互联网的飞速发展,移动支付给人们的生活带来很大的便利。移动支付是实现移动电子商务交易成功的关键环节,安全的移动支付协议是保障移动支付顺利进行的基石。由于安全协议往往运行在复杂的、不安全的网络环境中,产生的错误很难发现,难以保证协议安全性分析的准确性,必须采用形式化方法和工具来分析。针对移动支付中存在的安全问题,对移动支付协议进行形式化分析,旨在发现移动支付协议中潜在的安全漏洞具有重要意义。事件逻辑是一种描述分布式系统中状态迁移的形式化方法,可用于证明网络安全协议的安全性。本文基于事件逻辑理论并对其进行扩充,对移动支付协议进行形式化分析。本文主要研究内容如下:1.详细介绍事件逻辑理论的产生背景、发展现状、基本思想;对事件系统中的消息自动机和事件系统结构做了阐述,说明事件逻辑是如何去捕捉并描述一个分布式系统;给出事件逻辑理论中的基本定义,包括Atom原子、事件序、事件类,给出了事件逻辑证明系统中的六条公理以及相关引理及性质,其中着重对协议形式化建模中基于事件逻辑的协议建模逻辑与普通的消息-箭头描述方法进行了对比,突出了事件逻辑在协议建模方面的优势;总结归纳了基于事件逻辑的安全协议形式化证明流程图。2.针对移动支付协议中主体数目、协议交互步骤数目较多的情况下,提出迁移规则和可继承性,协议线程中的动作可以迁移到下一个序列中,对于多个协议主体数目、协议交互步骤数目多的协议,能够简化协议证明流程,有效减少协议证明的复杂性。通过事件逻辑理论分析移动支付协议KerNeeS协议安全性,对POS、NFC Phone和Authentication Server间交互进行分析。形式化描述协议双向认证过程、分析协议交互双方的基本序列,基于事件逻辑证明系统对强认证性质进行证明,得出POS和NFC Phone之间能够实现双向认证。3.针对事件逻辑只能分析安全协议认证性而不能分析不可否认性的缺陷,对事件逻辑理论进行扩展。增添了Has、CanProve、Claims、Controls等谓词,扩展协议证明系统,加入拥有公理、管辖公理、签名公理,让扩展的新方法能够对包含不可否认性的协议进行描述与分析。4.对不可否认性进行了定义与分析,使用事件逻辑对其进行形式化刻画说明,阐述了形式化分析不可否认性的具体步骤。首先列举协议的初始状态,包括协议的初始消息拥有集合和初始信念集合,对协议主体的初始状态集合进行了说明,并给出消息、信念的生成规则;接着列举发送方非否认证据EOO和接收方非否认证据EOR,分析EOO和EOR是否符合不可否认性要求;最后分析协议是否达到不可否认性目标,当协议运行在任何阶段时,是否有EOO∈和EOR∈同时成立,从而来分析协议的不可否认性是否满足。根据上述证明流程,以移动支付协议FMPP协议为例进行了形式化分析,说明了结果扩展的事件逻辑能够分析移动支付协议的不可否认性。

关键词：形式化方法事件逻辑理论移动支付协议认证性不可否认性

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

一种基于进程代数的安全协议验证消解算法

计算机工程与科学 2006年第7期28卷 14-16,27页

作者：刘万伟周倜李梦君李舟军国防科技大学计算机学院湖南长沙410073

安全协议本质上是分布式并发程序,可以描述为多个子进程的并发合成系统。将安全协议对应的并发合成系统抽象为一组逻辑规则,能够对安全协议无穷会话的交叠运行进行验证。本文首先给出了将安全协议基于进程代数的形式描述转化成为一组逻... 详细信息

安全协议本质上是分布式并发程序,可以描述为多个子进程的并发合成系统。将安全协议对应的并发合成系统抽象为一组逻辑规则,能够对安全协议无穷会话的交叠运行进行验证。本文首先给出了将安全协议基于进程代数的形式描述转化成为一组逻辑规则的方法,并提出了基于逻辑规则分类的高效逻辑程序消解算法,对安全协议认证性和保密性进行验证。

关键词：安全协议进程代数消解保密性认证性