期刊文献+
共找到67篇文章
< 1 2 4 >
每页显示 20 50 100
A Novel Formal Theory for Security Protocol Analysis of Denial of Service Based on Extended Strand Space Model
1
作者 JIANG Rui 《China Communications》 SCIE CSCD 2010年第4期23-28,共6页
Denial of Service Distributed Denial of Service (DOS) attack, especially (DDoS) attack, is one of the greatest threats to Internet. Much research has been done for it by now, however, it is always concentrated in ... Denial of Service Distributed Denial of Service (DOS) attack, especially (DDoS) attack, is one of the greatest threats to Internet. Much research has been done for it by now, however, it is always concentrated in the behaviors of the network and can not deal with the problem exactly. In this paper, we start from the security of the protocol, then we propose a novel theory for security protocol analysis of Denial of Service in order to deal with the DoS attack. We first introduce the conception of weighted graph to extend the strand space model, then we extend the penetrator model and define the goal of anti-DoS attack through the conception of the DoS-stop protocol, finally we propose two kinds of DoS test model and erect the novel formal theory for security protocol analysis of Denial of Service. Our new formal theory is applied in two example protocols. It is proved that the Internet key exchange (IKE) easily suffers from the DoS attacks, and the efficient DoS- resistant secure key exchange protocol (JFK) is resistant against DoS attack for the server, respectively. 展开更多
关键词 Denial of Service Security Protocol Analysis Formal Theory strand space model Internet Key Exchange
在线阅读 下载PDF
安全协议分析的界——综合模型检查与Strand Spaces(英文)
2
作者 刘怡文 李伟琴 《中国科学院研究生院学报》 CAS CSCD 2002年第3期288-294,共7页
Strand Spaces是一种用于分析安全协议的机器证明方法.简要介绍了 Strand Spaces的基本特点,分析了其优劣,提出了构造协议的理想子环的算法,并以此来约束协议入侵者的能力和协议并行运行的次数.将模型检查与 Strand Spaces结合在一起,... Strand Spaces是一种用于分析安全协议的机器证明方法.简要介绍了 Strand Spaces的基本特点,分析了其优劣,提出了构造协议的理想子环的算法,并以此来约束协议入侵者的能力和协议并行运行的次数.将模型检查与 Strand Spaces结合在一起,提出了一种综合分析方法来验证协议的安全特性,该方法可充分发挥模型检查与 Strand Spaces二者的优势. 展开更多
关键词 安全协议分析 模型检查 strand spaceS 定理证明 机器证明 安全特性 网络安全
在线阅读 下载PDF
基于Strand Space模型的CCITT X.509协议分析 被引量:4
3
作者 蒋睿 李建华 潘理 《上海交通大学学报》 EI CAS CSCD 北大核心 2004年第z1期169-173,共5页
运用前沿的安全协议形式化分析方法——StrandSpace模型理论,对CCITTX.509协议进行了分析,指出了该协议在保密性和认证正确性方面的缺陷,得到了BAN逻辑分析没有得到的保密性缺陷和相同的认证正确性缺陷.同时提出了改进的X.509协议,并用S... 运用前沿的安全协议形式化分析方法——StrandSpace模型理论,对CCITTX.509协议进行了分析,指出了该协议在保密性和认证正确性方面的缺陷,得到了BAN逻辑分析没有得到的保密性缺陷和相同的认证正确性缺陷.同时提出了改进的X.509协议,并用StrandSpace模型论证了改进协议的保密性和认证正确性. 展开更多
关键词 strand space模型 安全协议 形式化方法 CCITT X.509
在线阅读 下载PDF
基于Strand模型的Needham-Schroeder协议分析
4
作者 贾立伟 周清雷 赵东明 《微计算机信息》 北大核心 2008年第27期37-39,共3页
Strand空间模型是一种安全协议分析模型,使用图的形式来描述协议,证明协议的正确性。通过分析研究,本文建立了攻击者模型,并在此基础上运用安全协议的形式化分析方法—Strand空间模型,对公开密钥协议NSPK进行了分析,说明了该方法进行协... Strand空间模型是一种安全协议分析模型,使用图的形式来描述协议,证明协议的正确性。通过分析研究,本文建立了攻击者模型,并在此基础上运用安全协议的形式化分析方法—Strand空间模型,对公开密钥协议NSPK进行了分析,说明了该方法进行协议分析的过程,证明了该协议在保密性和认证性方面的正确性,并分析了该协议存在的安全缺陷。 展开更多
关键词 串空间 攻击者模型 形式化分析 安全协议
在线阅读 下载PDF
Strand空间中基于安全密钥概念的证明思路 被引量:1
5
作者 任侠 吕述望 《通信学报》 EI CSCD 北大核心 2005年第2期29-34,共6页
提出了Strand空间模型中证明安全协议的一个新思路,它从安全密钥的概念出发,参照基于理想概念的证明方法,得出证明所需的预备结论,从而对协议的秘密属性与认证属性进行证明。此外,还给出了一个针对Yahalom-BAN协议安全性的证明实例,从... 提出了Strand空间模型中证明安全协议的一个新思路,它从安全密钥的概念出发,参照基于理想概念的证明方法,得出证明所需的预备结论,从而对协议的秘密属性与认证属性进行证明。此外,还给出了一个针对Yahalom-BAN协议安全性的证明实例,从中可以看到该思路非常适于采用对称加密体制且具有密钥分发功能的三方认证协议的证明,并且它还使得证明过程简洁而直观。 展开更多
关键词 计算机科学技术基础学科 安全协议证明 strand空间模型 安全密钥 理想概念
在线阅读 下载PDF
一种基于Strand空间的认证协议检测方法
6
作者 姜志坚 韩芳溪 《计算机应用》 CSCD 北大核心 2004年第1期76-79,共4页
Strand空间是一种安全协议分析模型 ,使用图的形式来描述协议 ,证明协议的正确性。通过分析研究 ,本文建立了攻击者知识模型 ,在此基础上提出了一种基于Strand空间的认证协议检测方法 ,该方法产生状态少 ,避免了状态空间的爆炸。并以Nee... Strand空间是一种安全协议分析模型 ,使用图的形式来描述协议 ,证明协议的正确性。通过分析研究 ,本文建立了攻击者知识模型 ,在此基础上提出了一种基于Strand空间的认证协议检测方法 ,该方法产生状态少 ,避免了状态空间的爆炸。并以Needham Schroeder公钥协议为例 ,说明了该方法进行协议分析的过程。 展开更多
关键词 strand空间 BUNDLE 攻击者知识模型 状态搜索
在线阅读 下载PDF
基于第三方的安全移动支付方案 被引量:21
7
作者 黄晓芳 周亚建 +1 位作者 赖欣 杨义先 《计算机工程》 CAS CSCD 北大核心 2010年第18期158-159,162,共3页
在现有移动支付方案研究的基础上,提出一种新的基于第三方的安全移动支付方案。该方案以第三方支付平台为基础,在交易过程中采用"一次一密"的密钥分配机制,改善了现有移动支付方案的缺陷,在安全性上实现交易信息的保密性、不... 在现有移动支付方案研究的基础上,提出一种新的基于第三方的安全移动支付方案。该方案以第三方支付平台为基础,在交易过程中采用"一次一密"的密钥分配机制,改善了现有移动支付方案的缺陷,在安全性上实现交易信息的保密性、不可伪造性及不可否认性等特性,并利用串空间模型的形式化分析方法对相关协议进行安全性证明。 展开更多
关键词 移动支付 一次一密 协议形式化分析 串空间模型
在线阅读 下载PDF
Formal analysis of robust email protocol based on authentication tests 被引量:1
8
作者 蒋睿 胡爱群 《Journal of Southeast University(English Edition)》 EI CAS 2009年第2期147-151,共5页
Based on the authentication tests and the strand space model, the robust email protocol with perfect forward secrecy is formally analyzed, and the security shortcomings of the protocol is pointed out. Meanwhile, the m... Based on the authentication tests and the strand space model, the robust email protocol with perfect forward secrecy is formally analyzed, and the security shortcomings of the protocol is pointed out. Meanwhile, the man-in-the-middle attack to the protocol is given, where the attacker forges the messages in the receiving phase to cheat the two communication parties and makes them share the wrong session keys with him. Therefore, the protocol is not ensured to provide perfect forward secrecy. In order to overcome the above security shortcomings, an advanced email protocol is proposed, where the corresponding signatures in the receiving phase of the protocol are added to overcome the man-in-the-middle attack and ensure to provide perfect forward secrecy. Finally, the proposed advanced email protocol is formally analyzed with the authentication tests and the strand space model, and it is proved to be secure in authentication of the email sender, the recipient and the server. Therefore, the proposed advanced email protocol can really provide perfect forward secrecy. 展开更多
关键词 email protocol authentication tests formal method perfect forward secrecy strand space model
在线阅读 下载PDF
基于认证测试方法的EAP-AKA协议分析 被引量:9
9
作者 王鹏 李谢华 陆松年 《计算机工程与应用》 CSCD 北大核心 2007年第15期157-159,共3页
EAP-AKA(Extensible Authentication Protocol-Authentication and Key Agreement)是WLAN的认证和密钥分配协议;认证测试是一种以串空间理论为基础的安全协议分析验证方法。运用认证测试方法对EAP-AKA协议的双向身份认证过程进行了分析... EAP-AKA(Extensible Authentication Protocol-Authentication and Key Agreement)是WLAN的认证和密钥分配协议;认证测试是一种以串空间理论为基础的安全协议分析验证方法。运用认证测试方法对EAP-AKA协议的双向身份认证过程进行了分析证明,结果说明EAP-AKA能够保证移动终端和认证服务器之间的双向认证。 展开更多
关键词 EAP-AKA协议 认证测试方法 串空间模型 3G WLAN 形式化方法
在线阅读 下载PDF
基于CPK的可信平台用户登录认证方案 被引量:6
10
作者 马宇驰 赵远 +1 位作者 邓依群 李益发 《计算机工程与应用》 CSCD 北大核心 2010年第1期90-94,共5页
用户登录身份认证是建立操作系统可信性的一个非常重要的环节,是建立可信计算环境的基础。首先讨论了认证的相关技术,介绍了CPK(组合公钥)原理,然后根据可信计算组织的规范,利用CPK算法和动态验证码的技术,提出了一种基于CPK的可信平台... 用户登录身份认证是建立操作系统可信性的一个非常重要的环节,是建立可信计算环境的基础。首先讨论了认证的相关技术,介绍了CPK(组合公钥)原理,然后根据可信计算组织的规范,利用CPK算法和动态验证码的技术,提出了一种基于CPK的可信平台用户登录认证方案,该方案属于双因素认证方案,将认证和授权严格分开,并启发式分析了方案的特色和安全,最后在串空间模型下证明了方案的安全性,取得了比TCG标准中引用的方案更好的性能。 展开更多
关键词 可信计算 组合公钥(CPK) 身份认证 可信登录 串空间模型
在线阅读 下载PDF
基于认证测试的安全协议分析 被引量:16
11
作者 杨明 罗军舟 《软件学报》 EI CSCD 北大核心 2006年第1期148-156,共9页
认证测试是一种新型的在Strand空间模型基础上发展而来的安全协议分析与辅助设计技术,可用于大部分协议的关联属性的分析;但是与Strand空间模型一样,它主要用于协议正确性证明,在协议为何不正确以及如何进行改进这个问题上处理分析能力... 认证测试是一种新型的在Strand空间模型基础上发展而来的安全协议分析与辅助设计技术,可用于大部分协议的关联属性的分析;但是与Strand空间模型一样,它主要用于协议正确性证明,在协议为何不正确以及如何进行改进这个问题上处理分析能力较弱.在认证测试概念的基础上,结合逻辑分析的优点,提出了增强型认证测试EAT(enhanced authentication test)和Correspondence函数等概念来对安全协议进行关联属性的分析,很好地解决了这一问题.与原有技术相比,该方法更为形式化,协议分析人员可以很方便地进行手动分析,并且更有利于协议分析自动化工具的实现. 展开更多
关键词 网络安全 协议分析 strand空间模型 认证测试 认证逻辑
在线阅读 下载PDF
基于公钥的EAP-AKA协议改进及安全性分析 被引量:3
12
作者 董春冻 王聪 +2 位作者 刘军 周星 张玉静 《计算机工程与设计》 CSCD 北大核心 2014年第1期32-36,157,共6页
为了提高3G网络和WLAN之间认证的安全性和可靠性,实现两者之间的安全连接与通信,针对扩展认证密钥协商(EAP-AKA)协议存在的安全缺陷及现有一些改进方法的不足,提出了一种基于公钥密码体制的改进方案。在WLAN接入网和3G网络服务器之间增... 为了提高3G网络和WLAN之间认证的安全性和可靠性,实现两者之间的安全连接与通信,针对扩展认证密钥协商(EAP-AKA)协议存在的安全缺陷及现有一些改进方法的不足,提出了一种基于公钥密码体制的改进方案。在WLAN接入网和3G网络服务器之间增设公钥来实现两者的相互认证以及对用户身份等信息的加密传输,建立了共享密钥K的更新机制,运用串空间模型和认证测试方法对改进方案进行了相应的安全性分析和证明。分析结果表明,该方案具有良好的性能和安全性,可以实现3G网络和WLAN之间的安全认证与互联。 展开更多
关键词 第三代移动通信 无线局域网 扩展认证密钥协商协议 公钥 串空间模型 认证测试
在线阅读 下载PDF
基于串空间的Ad Hoc安全路由协议攻击分析模型 被引量:8
13
作者 董学文 马建峰 +2 位作者 牛文生 毛立强 谢辉 《软件学报》 EI CSCD 北大核心 2011年第7期1641-1651,共11页
根据ad hoc安全路由协议的特点,分析串空间理论的优势和不足,并在串空间分析协议的基础上,设计出一种返回不存在路由的协议攻击分析模型.以扩展SRP协议为例,验证了模型的正确性.
关键词 串空间 攻击分析模型 不存在路由 SRP(security ROUTING protocol)协议
在线阅读 下载PDF
基于串空间的匿名形式化分析扩展 被引量:2
14
作者 董学文 牛文生 +2 位作者 马建峰 谢晖 毛立强 《通信学报》 EI CSCD 北大核心 2011年第6期124-131,共8页
为了使串空间满足匿名性分析的特殊需求,利用串空间丛消息解析等价技术,结合观察视角,分别定义2种发送者匿名性、接收者匿名性;基于不同的侧重点,定义出不同的关系匿名性,在此基础上扩展并完善了基于串空间的匿名性形式化框架。同时,定... 为了使串空间满足匿名性分析的特殊需求,利用串空间丛消息解析等价技术,结合观察视角,分别定义2种发送者匿名性、接收者匿名性;基于不同的侧重点,定义出不同的关系匿名性,在此基础上扩展并完善了基于串空间的匿名性形式化框架。同时,定性分析多种匿名性之间的匿名程度差异,并以一个ad hoc网络下的基于区域的k匿名路由协议为例,验证形式化框架的正确性和高效性。 展开更多
关键词 串空间 匿名协议 等价丛 匿名程度
在线阅读 下载PDF
安全协议关联性分析 被引量:5
15
作者 杨明 罗军舟 《通信学报》 EI CSCD 北大核心 2006年第7期39-45,52,共8页
提出安全协议本质上是协议主体利用密码学手段通过挑战-响应来对协议另一方的存在做出判断,并同时完成对一些数据例如会话密钥等的协商。依据这种思想,结合认证逻辑中的一些成果,提出了一种新的安全协议关联性的分析方法,该方法对协议... 提出安全协议本质上是协议主体利用密码学手段通过挑战-响应来对协议另一方的存在做出判断,并同时完成对一些数据例如会话密钥等的协商。依据这种思想,结合认证逻辑中的一些成果,提出了一种新的安全协议关联性的分析方法,该方法对协议认证目标进行了基于线空间模型语义的定义,并将关联性分析归结为Strand的存在关系和Strand参数一致性的分析问题。 展开更多
关键词 网络安全 协议分析 挑战-响应 线空间模型
在线阅读 下载PDF
协议主体密钥在测试组件构造上的性质分析 被引量:6
16
作者 余磊 魏仕民 《计算机工程与应用》 CSCD 2013年第6期114-117,共4页
针对认证测试理论在测试组件构造方面缺少具体形式化构造规则的不足,根据协议主体在认证测试中的角色特点,以及包含惟一源发消息的消息组件在认证测试中的作用和性质,对消息组件进行分类和定义并提出认证测试模型的概念,基于认证测试模... 针对认证测试理论在测试组件构造方面缺少具体形式化构造规则的不足,根据协议主体在认证测试中的角色特点,以及包含惟一源发消息的消息组件在认证测试中的作用和性质,对消息组件进行分类和定义并提出认证测试模型的概念,基于认证测试模型给出协议主体密钥在测试组件构造上的性质命题,同时运用认证测试基础理论对命题进行正确性证明,从而确定测试组件构造的形式化规则。 展开更多
关键词 安全协议 形式化分析方法 串空间模型 认证测试 消息组件 测试组件
在线阅读 下载PDF
基于CPK的TLS握手协议的设计与研究 被引量:3
17
作者 程克非 贾廷强 《电子科技大学学报》 EI CAS CSCD 北大核心 2013年第3期420-424,共5页
TLS协议作为当今应用最广泛的传输层安全协议,受到了人们的极大关注,但是其自身存在证书管理复杂、握手交互过多和安全缺陷等诸多问题。对TLS握手协议分析和研究,并结合基于身份的组合公钥密码体制(CPK)的特点,提出了基于CPK的握手协议... TLS协议作为当今应用最广泛的传输层安全协议,受到了人们的极大关注,但是其自身存在证书管理复杂、握手交互过多和安全缺陷等诸多问题。对TLS握手协议分析和研究,并结合基于身份的组合公钥密码体制(CPK)的特点,提出了基于CPK的握手协议方案。通过对其安全性分析和基于串空间模型理论的形式化证明,证明了该方案的安全可靠性高。在相同安全条件下进行仿真,实验结果显示与原方案对比该方案具有握手交互次数少、鉴别简捷、建立可信连接过程简单、高效等明显优点。 展开更多
关键词 组合公钥 握手协议 安全分析 串空间模型 TLS
在线阅读 下载PDF
基于Diff-Hellman的改进Yang-Shieh智能卡认证协议 被引量:3
18
作者 杨照芳 程小平 《西南师范大学学报(自然科学版)》 CAS CSCD 北大核心 2006年第6期110-113,共4页
提出了基于Diff-Hellman的改进Yang-Shieh智能卡认证协议(DHYS),并采用串空间理论形式化证明了DHYS的安全性.DHYS在增强Yang-Shieh认证协议安全性的同时,无任何附加限制,保留了原Yang-Shieh协议的全部优点.
关键词 认证协议 认证测试 串空间模型 智能卡
在线阅读 下载PDF
Needham-Schroeder协议的认证测试方法形式化分析 被引量:1
19
作者 李廷元 秦志光 +1 位作者 刘晓东 张选芳 《计算机工程与应用》 CSCD 北大核心 2010年第19期100-102,共3页
在安全协议的形式化分析方法中,串空间模型和基于串空间模型的认证测试方法是比较常用的验证方法。针对Need-ham-Schroeder协议存在中间人攻击的缺陷,提出对协议的改进并采用认证测试方法,验证了改进的协议可以满足协议的安全目标。
关键词 安全协议 形式化分析 串空间模型 认证测试方法 Needham-Schroeder协议
在线阅读 下载PDF
认证协议两种形式化分析方法的比较 被引量:11
20
作者 卿斯汉 《软件学报》 EI CSCD 北大核心 2003年第12期2028-2036,共9页
串空间模型和CSP方法是当前最著名的分析认证协议的形式化方法.通过一个具体的认证协议例子,比较两种方法的不同特点.
关键词 认证协议 形式化分析 串空间模 CSP方法
在线阅读 下载PDF
上一页 1 2 4 下一页 到第
使用帮助 返回顶部