检索结果-南通市图书馆

在线全文

学校读者我要写书评

暂无评论

基于ATL的电子商务协议建模与形式化分析

微电子学与计算机 2009年第8期26卷 193-195,200页

作者：张梅文静华张焕国贵州财经学院信息学院贵州贵阳550004 武汉大学计算机学院湖北武汉430072

LTL和CTL等由于把协议看成封闭式并发系统进行研究,不能有效描述协议与外部环境的联系.引入一种新的基于博弈逻辑的ATL分析方法,能够对日益复杂的多方电子商务协议进行建模与分析.利用新方法对Markowitch和Kremer提出的多方非否认协议... 详细信息

LTL和CTL等由于把协议看成封闭式并发系统进行研究,不能有效描述协议与外部环境的联系.引入一种新的基于博弈逻辑的ATL分析方法,能够对日益复杂的多方电子商务协议进行建模与分析.利用新方法对Markowitch和Kremer提出的多方非否认协议进行建模与严格的形式化分析,发现该协议存在的不公平性问题并提出改进方法.

关键词： ATL逻辑形式化分析公平性多方电子商务协议

在线全文

学校读者我要写书评

暂无评论

OAuth2.0协议的安全性形式化分析

计算机工程与设计 2016年第7期37卷 1746-1751页

作者：魏成坤刘向东石兆军中国航天科工集团第二研究院706所北京100854

为使用户信任安全系统,保证OAuth2.0协议的有效实施,提出对OAuth2.0协议进行详细的安全性分析。通过对Scyther的研究和OAuth2.0协议的分析,形式化验证OAuth2.0协议的安全性。将OAuth2.0协议标准转化为Scyther的形式化语义,分析协议的安... 详细信息

为使用户信任安全系统,保证OAuth2.0协议的有效实施,提出对OAuth2.0协议进行详细的安全性分析。通过对Scyther的研究和OAuth2.0协议的分析,形式化验证OAuth2.0协议的安全性。将OAuth2.0协议标准转化为Scyther的形式化语义,分析协议的安全目标,将安全目标转化为安全属性,与形式化语义相结合,利用Scyther的对手模型和基于模型的改进算法进行安全性形式化分析。结合实例分析协议角色执行轨迹,得到协议的攻击路径。

关键词： OAuth2.0 Scyther 形式化分析云计算安全性

基于SPIN的远程证明协议的形式化分析及改进

在线全文

学校读者我要写书评

暂无评论

计算机工程与应用 2017年第1期53卷 34-38,72页

作者：秦嫚蔓王峥王莉太原理工大学计算机科学与技术学院太原030024

远程证明是解决移动支付安全问题的有效手段之一。通过对可信计算远程证明协议进行分析,发现用户平台配置信息的隐私性、用户的认证性和远程验证者的认证性存在脆弱点,使用SPIN模型检测工具,应用模型检测方法对协议进行了形式化分析,检... 详细信息

远程证明是解决移动支付安全问题的有效手段之一。通过对可信计算远程证明协议进行分析,发现用户平台配置信息的隐私性、用户的认证性和远程验证者的认证性存在脆弱点,使用SPIN模型检测工具,应用模型检测方法对协议进行了形式化分析,检测出破坏性攻击漏洞。针对协议中的漏洞对协议进行改进,提出了一种基于用户属性加盐哈希的方法,通过用户属性保证协议的安全传输。最后使用SPIN检测改进后的协议,证明了改进方案的有效性、安全性,阻断了发现的攻击。

关键词：移动支付远程证明协议用户属性形式化分析 SPIN模型检测

在线全文

学校读者我要写书评

暂无评论

物联网中安全通信协议的形式化分析

桂林理工大学学报 2013年第2期33卷 333-338页

作者：吴名欢程小辉桂林理工大学广西矿冶与环境科学实验中心广西桂林541004 桂林理工大学信息科学与工程学院广西桂林541004

针对物联网通信协议安全性不足和使用非形式化方法进行分析时容易出现错误的问题,提出了一种物联网安全通信协议,建立了协议主体模型和攻击者模型,采用通信顺序进程CSP的形式化方法对协议模型进行了分析。该通信协议对传送的信息进行加... 详细信息

针对物联网通信协议安全性不足和使用非形式化方法进行分析时容易出现错误的问题,提出了一种物联网安全通信协议,建立了协议主体模型和攻击者模型,采用通信顺序进程CSP的形式化方法对协议模型进行了分析。该通信协议对传送的信息进行加密,采用的加密方式是散列函数结合异或运算。协议主体进行了相互认证,认证服务器为协议主体通信分配了会话密钥,解决了读写器非法扫描和信息安全传送的问题。利用故障发散改进检测器(FDR)对该协议模型CSP进程进行了检测,结果表明:该协议主体进行了相互认证,会话密钥是安全的,所提出的物联网通信协议是安全可靠的,CSP方法用于分析协议的安全性是可行的。

关键词：物联网形式化分析安全协议通信顺序进程

在线全文

学校读者我要写书评

暂无评论

基于串空间的安全协议形式化分析研究

信息网络安全 2020年第2期 30-36页

作者：姚萌萌唐黎凌永兴肖卫东江南计算技术研究所无锡214063 国防大学联合勤务学院北京100858

安全协议是信息安全领域的重要组成部分,随着新兴技术的快速发展,安全协议变得越来越复杂,给安全协议的形式化分析带来了挑战。近年来,基于串空间理论的形式化分析方法是一个研究热点,在安全协议分析领域得到了广泛的关注和研究,并取得... 详细信息

安全协议是信息安全领域的重要组成部分,随着新兴技术的快速发展,安全协议变得越来越复杂,给安全协议的形式化分析带来了挑战。近年来,基于串空间理论的形式化分析方法是一个研究热点,在安全协议分析领域得到了广泛的关注和研究,并取得了一定的成果。文章扩展了串空间理论,提出了匹配串、匹配结点、同一执行丛等概念,并基于扩展的串空间理论形式化分析了基于区块链的公平多方不可否认协议,发现了该协议的不能满足公平性的缺陷。

关键词：串空间形式化分析安全协议区块链

在线全文

学校读者我要写书评

暂无评论

调和两种观点的安全协议形式化分析方法研究

调和两种观点的安全协议形式化分析方法研究

作者：尹学永山东大学

学位级别：硕士

随着计算机网络的发展和电子商务的兴起与广泛应用,人们对网络安全的要求越来越迫切。在网络安全中,各种安全服务由安全协议来保证,因此,安全协议的安全性就显得尤为重要。在过去二十多年中,人们提出了很多安全协议,但后来的事实证明,... 详细信息

随着计算机网络的发展和电子商务的兴起与广泛应用,人们对网络安全的要求越来越迫切。在网络安全中,各种安全服务由安全协议来保证,因此,安全协议的安全性就显得尤为重要。在过去二十多年中,人们提出了很多安全协议,但后来的事实证明,这些安全协议都存在着各种安全隐患,因此,如何设计一个安全的安全协议,如何对一个已经存在的安全协议进行形式化分析,成为安全协议研究领域中两个最重要的方面。安全协议,就是两个或两个以上的参与者采取一系列步骤来完成某项特定的安全任务。目前,在安全协议的形式化分析方面存在两种截然不同的观点:符号观点和计算观点。符号观点一般不考虑安全协议使用的具体密码算法,而是把安全协议的安全特性抽象成一组可操作的符号,然后用形式逻辑或定理证明的方法来分析协议是否能达到预期的安全目标。计算观点下,安全协议的安全特性以概率和时间复杂度的形式进行定义,协议形式化证明是数学证明某个定理成立,这通常涉及到一个归约变换,把协议的安全性归约到计算复杂性理论中一个公认的不可能的突破。本文的主要工作有: 1)系统介绍安全协议的相关知识,包括安全协议的概念,性质和分类。分析安全协议的常见攻击方法,并在此基础上,总结归纳设计安全协议需要尊循的一些原则。 2)以BAN逻辑为例介绍符号观点下基于推理的结构性方法.对Yahalom协议进行改进,并用BAN逻辑对其进行分析。以Bellare和Rogaway所做的工作为例介绍计算观点下“归约为矛盾”的安全协议分析方法。 3)介绍赵华伟和李大兴提出的一种调和两种观点的安全协议分析方法,讨论时间戳在安全协议中的使用情况,对上面的方法进行改进,加入时间戳语义,使其可用于分析具有时间戳的安全协议。 4)简单介绍Kerberos认证协议,对Kerberos协议流程进行细化,对流程中含密码操作的消息进行具体描述.用改进的调和分析法,从完全性和正确性两方面对Kerberos协议的安全性进行形式化分析. 最后,总结本文主要工作,分析指出该领域进一步的研究问题和方向。

关键词：安全协议符号观点计算观点形式化分析 Kerberos协议

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

安全协议形式化分析技术的应用与研究

安全协议形式化分析技术的应用与研究

作者：冯皓楠北京邮电大学

学位级别：硕士

安全协议运用密码算法,实现认证和密钥分配等目标。但是安全协议本身仍然存在安全隐患,对安全协议的各类攻击,导致个人、企业或国家机密信息泄露,造成财产损失。借助计算机和数学手段,形式化分析技术可以自动、快速和全面地对安全协议... 详细信息

安全协议运用密码算法,实现认证和密钥分配等目标。但是安全协议本身仍然存在安全隐患,对安全协议的各类攻击,导致个人、企业或国家机密信息泄露,造成财产损失。借助计算机和数学手段,形式化分析技术可以自动、快速和全面地对安全协议进行分析,不但能寻找安全协议的漏洞,还可以证明协议的安全性。该技术自提出以来,已经被应用到大量协议的分析中,促进了安全协议的研究与发展。但是,形式化分析技术目前仍旧不够成熟。本文对安全协议的形式化分析技术进行应用与研究,深入探讨了ProVerif形式化分析工具的原理,提出了利用ProVerif工具对安全协议进行形式化分析的方法,并以FIDO UAF为例进行了验证分析,最后对ProVerif和形式化分析方法进行了评估,找到了 ProVerif工具以及形式化分析方法的相关缺陷,并提出了改进方案。本文的主要工作和创新点包括:(1)提出了一种基于ProVerif的安全协议形式化分析方法,该方法提出了进程通信模型下恶意实体的建模方法、不可链接性的验证方法以及最小化假设的验证方法。(2)使用本文提出的方法对UAF协议进行形式化分析。首先对UAF协议的文档进行梳理,并对协议流程、安全假设、安全目标进行形式化翻译。其次提出UAF协议的ProVerif模型,开发UAFVerif工具,对UAF协议的所有可能场景进行分析,并自动寻找协议的最小化安全假设。在此基础上,论文提出针对UAF协议的攻击方式,成功将认证器重绑定攻击实施在两类应用中,获得CNNVD漏洞。最后提出了对UAF协议的改进建议。(3)总结ProVerif工具以及形式化分析过程的缺陷并提出了改进方案,其中包括ProVerif难以支持非Dolev-Yao模型下的协议分析、难以支持复杂的数学操作和计数器模型、不支持实体操作可变下认证性的分析以及难以支持实体遭到破坏的场景下不可链接性的分析等。

关键词：安全协议形式化分析 ProVerif FIDO UAF

WAPI认证与密钥协商协议形式化分析与研究

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

WAPI认证与密钥协商协议形式化分析与研究

作者：叶海松北京邮电大学

学位级别：硕士

无线局域网中终端设备和本地网络接入点之间通过空口通信,容易遭受攻击,因此无线局域网安全一直是研究的热点问题。为了保障无线局域网安全,我国独立提出了无线局域网鉴别与保密基础架构协议,该协议广泛应用于工业互联网控制、公安系统... 详细信息

无线局域网中终端设备和本地网络接入点之间通过空口通信,容易遭受攻击,因此无线局域网安全一直是研究的热点问题。为了保障无线局域网安全,我国独立提出了无线局域网鉴别与保密基础架构协议,该协议广泛应用于工业互联网控制、公安系统、国家电网等关键领域。WAPI用于提供终端设备与本地网络接入点之间的身份验证、密钥协商和MAC层数据加密等安全功能,但WAPI协议的安全性尚未得到充分的讨论与研究。本文采用了形式化的分析方法,使用形式化分析工具ProVerif对WAPI认证与密钥协议建模并对其安全性做系统全面的分析。本文的主要工作如下:1.对WAPI认证与密钥协商协议的中基于证书的身份鉴别过程、单播密钥协商和组播密钥协商过程进行形式化描述,并梳理协议交互流程图,这是后续对协议进行形式化建模的基础;2.提出了 WAPI认证与密钥协商协议的安全目标与威胁模型。在WAPI协议的标准文档中并没有提及WAPI认证与密钥协商协议需要满足的安全目标,本文通过参考WPA2等无线局域网安全协议的形式化分析工作,并结合WAPI协议的使用场景,总结了 WAPI协议的威胁模型与其需要满足的安全目标,这是对WAPI协议进行形式化分析的关键;3.对WAPI认证与密钥协商协议进行形式化建模与分析,发现了 WAPI认证与密钥协商协议存在多种漏洞。本文使用ProVerif对WAPI认证与密钥协商协议进行分析,发现协议并不能完全满足认证性和机密性目标,在协议运行过程中存在DoS攻击、MitM攻击、单播密钥无法更新攻击和组播密钥重用攻击等,并给出了详细攻击流程;4.为WAPI认证与密钥协商协议给出了改进建议。根据上述分析结果本文总结了 WAPI认证与密钥协商协议中出现攻击的根本原因,并给出了改进建议,相应的建议可以指导WAPI后续的更新与迭代。

关键词：无线局域网 WAPI 形式化分析拒绝服务攻击中间人攻击

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

电子支付协议的博弈逻辑模型与形式化分析

微电子学与计算机 2007年第9期24卷 113-115页

作者：文静华张梅张焕国贵州财经学院信息学院贵州贵阳550004 武汉大学计算机学院湖北武汉4300724

提出用一种新的基于博弈逻辑ATL(Alternating-time Temporal Logic)的电子支付协议建模与分析方法。新方法克服了传统时序逻辑把协议看成封闭系统进行分析的缺点,可以成功地对电子商务中的对抗与合作行为进行描述。利用新方法对Bolignan... 详细信息

提出用一种新的基于博弈逻辑ATL(Alternating-time Temporal Logic)的电子支付协议建模与分析方法。新方法克服了传统时序逻辑把协议看成封闭系统进行分析的缺点,可以成功地对电子商务中的对抗与合作行为进行描述。利用新方法对Bolignano协议进行了严格的形式化分析,发现该协议不能满足公平性要求。

关键词：电子支付协议公平性形式化分析 ATL