期刊文献+
共找到14篇文章
< 1 >
每页显示 20 50 100
Dolev-Yao攻击者模型的形式化描述 被引量:8
1
作者 唐郑熠 李祥 《计算机工程与科学》 CSCD 北大核心 2010年第8期36-38,45,共4页
模型检测技术能够实现安全协议的自动化分析,是一种高效的形式化分析方法。然而,对于攻击者的建模却一直缺乏通用的方法,这导致了模型检测方法的自动化程度降低。本文为安全协议分析中,应用最为广泛的Dolev-Yao攻击者模型建立了一套形... 模型检测技术能够实现安全协议的自动化分析,是一种高效的形式化分析方法。然而,对于攻击者的建模却一直缺乏通用的方法,这导致了模型检测方法的自动化程度降低。本文为安全协议分析中,应用最为广泛的Dolev-Yao攻击者模型建立了一套形式化描述方法。遵循这一方法,可以使用任何建模语言机械地建立Dolev-Yao攻击者模型,从而大大地减少了人工分析的成份。同时,本文还使用该方法验证了两个目的完全不同的协议,证明了它的通用性。 展开更多
关键词 dolev-yao攻击者模型 形式化描述 模型检测 SPIN NSPK A(0)
下载PDF
网络敌手模型研究 被引量:1
2
作者 蒋建春 文伟平 《信息网络安全》 2008年第9期15-18,共4页
本文首先分析网络攻击特性,给出其形式定义、研究分析了网络攻击特点及攻击模型发展状况,提出了一个网络敌手模型,该模型由三个子模型组成,即网络敌手心智子模型、网络敌手攻击决策子模型、网络敌手攻击行为变迁子模型。这三个子模型将... 本文首先分析网络攻击特性,给出其形式定义、研究分析了网络攻击特点及攻击模型发展状况,提出了一个网络敌手模型,该模型由三个子模型组成,即网络敌手心智子模型、网络敌手攻击决策子模型、网络敌手攻击行为变迁子模型。这三个子模型将刻画网络攻击敌手的特征,包括敌手内部心智及外在的行为。该模型克服已有模型的不足,模型的能力也更强,能够描述攻击者的意图、决策及行为。并进行形式化分析网络敌手的特征、决策规划、攻击行为过程等网络攻击环节。其目的在于知己知彼,为网络信息安全对抗技术及网络安全策略的研究提供理论基础和指导依据。 展开更多
关键词 网络敌手模型 计算机网络 网络安全 网络攻击模型
下载PDF
基于CK模型SNEP安全分析 被引量:3
3
作者 沈明玉 薛伟 《计算机工程与应用》 CSCD 2012年第25期118-121,202,共5页
无线传感器网络(WSN)由于受节点特点限制,不适合采用公钥体制进行数据加密以及身份认证等。SNEP协议是针对WSN特点提出的SPINS协议中的重要部分,主要负责基于可信基站的节点间会话密钥建立以及认证。采用可证明安全模型中的CK模型构建... 无线传感器网络(WSN)由于受节点特点限制,不适合采用公钥体制进行数据加密以及身份认证等。SNEP协议是针对WSN特点提出的SPINS协议中的重要部分,主要负责基于可信基站的节点间会话密钥建立以及认证。采用可证明安全模型中的CK模型构建了一个理想模型下与现实模型下SNEP协议相对应的新协议,通过两种模型下的敌手ADV与UDV对它们进行形式化分析,得出SNEP协议构成了现实环境中安全通道的结论。 展开更多
关键词 SNEP协议 CK模型 敌手 安全通道
下载PDF
基于LU分解的安全外包求解线性代数方程组方法
4
作者 冯达 周福才 +1 位作者 吴淇毓 李鲍 《东北大学学报(自然科学版)》 EI CAS CSCD 北大核心 2024年第4期457-463,506,共8页
由于现有协议的安全性为基于某种安全假设的计算安全,依赖于敌手的计算能力,因此,本文针对恶意敌手模型,使用矩阵伪装技术对方程的系数矩阵进行隐藏,结合矩阵的LU分解(lower-upper decomposition)算法,提出一种新的信息论安全外包求解... 由于现有协议的安全性为基于某种安全假设的计算安全,依赖于敌手的计算能力,因此,本文针对恶意敌手模型,使用矩阵伪装技术对方程的系数矩阵进行隐藏,结合矩阵的LU分解(lower-upper decomposition)算法,提出一种新的信息论安全外包求解线性代数方程组(information-theoretically secure outsourcing of linear algebraic equations,ITS-OutsLAE)方法 .与之前的研究相比,在保持计算和通信复杂度与现有最优方案保持一致的同时,首次将方程组唯一解的安全性提升至信息论安全(完美保密).给出了形式化的安全性证明,并通过理论分析和实验证明了所提方法的实用性. 展开更多
关键词 线性代数方程组 信息论安全 安全外包 LU分解 恶意敌手模型
下载PDF
基于多密钥全同态加密方案的无CRS模型安全多方计算 被引量:6
5
作者 唐春明 胡业周 李习习 《密码学报》 CSCD 2021年第2期273-281,共9页
利用多密钥全同态加密方案(multi-key fully homomorphic encryption scheme,MFHE)可以设计一个安全多方计算协议.在公共随机串(common random string,CRS)模型中构造的安全多方计算协议,每一个参与方在生成公钥阶段要用到一个公共随机... 利用多密钥全同态加密方案(multi-key fully homomorphic encryption scheme,MFHE)可以设计一个安全多方计算协议.在公共随机串(common random string,CRS)模型中构造的安全多方计算协议,每一个参与方在生成公钥阶段要用到一个公共随机矩阵,这削弱了每个人独立生成公钥的能力.本文首先设计一个无CRS的基于GSW的安全多方计算协议,与已有的同类协议相比,由于我们的方案利用了编码操作,从而把单密钥密文扩展成多密钥密文,提高了效率,并将解密噪音从2(m4+m)mNBχ降低到(2+m)mNBχ.我们也以LWE假设为依据构造了一个无CRS模型的3轮安全多方计算协议,并证明其在半恶意敌手的情形下是安全的. 展开更多
关键词 多密钥全同态加密 CRS模型 LWE 安全多方计算 半恶意敌手
下载PDF
受限环境下委托握手DTLS协议的形式化分析与改进
6
作者 蒲鹳雄 缪祥华 袁梅宇 《数据通信》 2024年第1期14-22,共9页
物联网设备有着资源受限的特性,往往处于受限的网络环境中,在这之上又面临着安全的挑战。目前常见的受限网络协议栈为CoAP-DTLS/UDP-6LoWPAN,传输层使用UDP,其安全性由DTLS协议维持。但DTLS协议作为TLS在UDP上的扩展,基于PKI连接建立的... 物联网设备有着资源受限的特性,往往处于受限的网络环境中,在这之上又面临着安全的挑战。目前常见的受限网络协议栈为CoAP-DTLS/UDP-6LoWPAN,传输层使用UDP,其安全性由DTLS协议维持。但DTLS协议作为TLS在UDP上的扩展,基于PKI连接建立的方式使其在直接应用到受限环境下会产生诸多性能上的问题。针对DTLS协议在受限环境下的性能问题,国内外的研究学者提出了诸多解决方式,包括但不限于改进加密算法、使用特定硬件、优化证书链、委托可信三方进行密钥协商(即将DTLS握手委托给第三方)。因此,对委托握手的DTLS协议使用Scyther进行形式化分析,得出其交付密钥材料时使用长期预共享密钥存在的安全问题,并提出重用TLS/DTLS协议中PRF函数的改进方式,对改进后的方法进行分析,证明了该方法能有效降低交付密钥材料时存在的风险。 展开更多
关键词 数据报传输层安全(DTLS) 受限应用协议(CoAP) dolev-yao攻击者模型 完美前向安全(PFS) 安全协议形式化分析
下载PDF
基于状态转移系统的安全协议形式模型 被引量:1
7
作者 毛中全 刘楠 +1 位作者 顾纯祥 祝跃飞 《计算机工程》 CAS CSCD 北大核心 2008年第13期149-151,共3页
提出一种基于状态转移系统的安全协议模型,以Dolev-Yao攻击者模型为前提假设,以状态转移系统为框架,用语义编码的方式定义消息和事件,用重写关系定义协议规则,用事件的集合来描述协议的安全属性,并给出安全属性的检验策略。该模型能够... 提出一种基于状态转移系统的安全协议模型,以Dolev-Yao攻击者模型为前提假设,以状态转移系统为框架,用语义编码的方式定义消息和事件,用重写关系定义协议规则,用事件的集合来描述协议的安全属性,并给出安全属性的检验策略。该模型能够对安全协议进行精确的形式化描述,且便于实现自动化分析。 展开更多
关键词 安全协议 形式模型 状态转移系统 重写关系 dolev-yao攻击者模型
下载PDF
基于Lowe分类法的5G网络EAP-AKA’协议安全性分析 被引量:15
8
作者 刘彩霞 胡鑫鑫 +2 位作者 刘树新 游伟 赵宇 《电子与信息学报》 EI CSCD 北大核心 2019年第8期1800-1807,共8页
移动网鉴权认证协议攻击不断涌现,针对5G网络新协议EAP-AKA’,该文提出一种基于Lowe分类法的EAP-AKA’安全性分析模型。首先对5G网络协议EAP-AKA’、信道及攻击者进行形式化建模。然后对Lowe鉴权性质进行形式化描述,利用TAMARIN证明器... 移动网鉴权认证协议攻击不断涌现,针对5G网络新协议EAP-AKA’,该文提出一种基于Lowe分类法的EAP-AKA’安全性分析模型。首先对5G网络协议EAP-AKA’、信道及攻击者进行形式化建模。然后对Lowe鉴权性质进行形式化描述,利用TAMARIN证明器分析协议中安全锚点密钥KSEAF的Lowe鉴权性质、完美前向保密性、机密性等安全目标,发现了3GPP隐式鉴权方式下的4条攻击路径。最后针对发现的安全问题提出2种改进方案并验证其有效性,并将5G网络两种鉴权协议EAP-AKA’和5G AKA的安全性进行了对比,发现前者在Lowe鉴权性质方面更安全。 展开更多
关键词 网络安全 安全锚点密钥 EAP-AKA’ Lowe分类法 dolev-yao敌手模型 TAMARIN
下载PDF
安全协议的形式化分析技术与方法 被引量:61
9
作者 薛锐 冯登国 《计算机学报》 EI CSCD 北大核心 2006年第1期1-20,共20页
对于安全协议的形式化分析方法从技术特点上做了分类和分析.对于安全协议分析技术的发展历史、目前的状况以及将来的趋势作了总体的介绍和总结.根据作者的体会,从纵向和横向两个角度进行了总结.纵向方面主要是从用于分析安全协议的形式... 对于安全协议的形式化分析方法从技术特点上做了分类和分析.对于安全协议分析技术的发展历史、目前的状况以及将来的趋势作了总体的介绍和总结.根据作者的体会,从纵向和横向两个角度进行了总结.纵向方面主要是从用于分析安全协议的形式化方法的出现和发展的历史角度加以总结.横向方面主要从所应用的技术手段、技术特点入手,进行总结分析.说明了目前协议形式化分析发展的主要方向.对于目前国际流行的方法和模型进行了例解. 展开更多
关键词 安全协议 形式化分析 安全目标 dolev-yao模型 密码学可靠性
下载PDF
基于刚性与相似性概念的密码协议分析方法 被引量:3
10
作者 田园 王颖 +1 位作者 金锋 金月 《计算机学报》 EI CSCD 北大核心 2009年第4期618-634,共17页
如何融合计算密码学与形式演算模型两条途径以有效分析和证明复杂密码协议,是信息安全领域富有挑战性的问题之一.文中提出Dolev-Yao刚性和Dolev-Yao相似性概念,运用密码协议的语法骨架提取与语义赋值技术,建立起一个能涵盖除具有适应性... 如何融合计算密码学与形式演算模型两条途径以有效分析和证明复杂密码协议,是信息安全领域富有挑战性的问题之一.文中提出Dolev-Yao刚性和Dolev-Yao相似性概念,运用密码协议的语法骨架提取与语义赋值技术,建立起一个能涵盖除具有适应性入侵能力之外的任何主动攻击者和大部分有实际意义的非自由消息代数的理论分析框架.该框架内所证明的协议安全性质具有复合-稳定性,即所证明的安全性质在协议与环境复合时仍然保持成立.文中针对strand-图模型这一具体情形证明了Canetti的UC-相似性概念与这里所建立的Dolev-Yao相似性概念之间接近充分必要程度的对偶关系,从而对融合UC-理论/strand-图模型这一情形具体证明了该分析框架具有相容性和完备性.最后,根据以上理论结果讨论了如何建立一种对应的新的协议分析方法. 展开更多
关键词 计算密码学 形式模型 UC-相似 dolev-yao刚性 dolev-yao相似性
下载PDF
关于安全协议的形式化分析方法的研究
11
作者 亓文华 张其善 刘建伟 《遥测遥控》 2007年第2期67-72,共6页
对安全协议的形式化分析方法从历史发展和思想体系上作出分类和分析。以历史发展为线索将安全协议形式化分析方法分为四个阶段,基于观察分析的早期阶段、以BAN(Burrows,Abadi,Needham)逻辑为代表的初期阶段、基于模型检测的转折阶段和... 对安全协议的形式化分析方法从历史发展和思想体系上作出分类和分析。以历史发展为线索将安全协议形式化分析方法分为四个阶段,基于观察分析的早期阶段、以BAN(Burrows,Abadi,Needham)逻辑为代表的初期阶段、基于模型检测的转折阶段和以串空间理论为代表的证明阶段。对安全协议四个阶段形式化分析方法的特点和优、缺点作了总结。分析结果为密码协议的研究人员提供一个借鉴。 展开更多
关键词 安全协议 形式化分析 dolev-yao模型
下载PDF
一种面向5G专网鉴权协议的形式化分析方案 被引量:3
12
作者 王跃东 熊焰 +1 位作者 黄文超 武建双 《信息网络安全》 CSCD 北大核心 2021年第9期1-7,共7页
文章提出一种面向5G专网鉴权协议EAP-TLS的细粒度形式化建模与验证方案。方案以TS 33.501文档为依据,首先构建基于Diffie-Hellman模式的协议交互模型;然后扩展Dolev-Yao攻击者模型,提出了两种参与方受控场景和混合信道模型;最后使用验... 文章提出一种面向5G专网鉴权协议EAP-TLS的细粒度形式化建模与验证方案。方案以TS 33.501文档为依据,首先构建基于Diffie-Hellman模式的协议交互模型;然后扩展Dolev-Yao攻击者模型,提出了两种参与方受控场景和混合信道模型;最后使用验证工具SmartVerif验证保密性、认证性、隐私性3类安全属性。实验结果表明,协议在保密性和认证性方面存在3类安全隐患。文章分析了出现安全隐患的根本原因并提出了修订方案,修订后的协议可以满足文章定义的全部安全属性。 展开更多
关键词 5G专网 EAP-TLS认证协议 dolev-yao攻击者模型 形式化方法
下载PDF
基于全同态加密的安全多方计算探讨 被引量:1
13
作者 李习习 胡业周 《电脑知识与技术》 2020年第21期19-22,共4页
随着云计算的发展与应用,数据的隐私保护越来越受到人们的关注。而全同态加密这一密码学原语的提出,为数据的隐私计算提供了一个强有力的工具。另一方面,安全多方计算允许人们共同计算一个函数得到想要的结果而不泄露自己的私有数据,在... 随着云计算的发展与应用,数据的隐私保护越来越受到人们的关注。而全同态加密这一密码学原语的提出,为数据的隐私计算提供了一个强有力的工具。另一方面,安全多方计算允许人们共同计算一个函数得到想要的结果而不泄露自己的私有数据,在现实生活中有着众多的应用。研究发现全同态加密可以作为安全多方计算协议的构建模块,且在LWE的假设下,协议在面对一个半恶意的敌手是安全的,进一步,在CRS模型下可由非交互的零知识证明将协议转换成面对恶意敌手也是安全的。 展开更多
关键词 全同态加密 安全多方计算 LWE (半)恶意敌手 CRS模型
下载PDF
常规隐信道下可证明安全隐写术的有效构造方法 被引量:1
14
作者 朱岩 余孟扬 +2 位作者 胡宏新 Ahn Gail-Joon 赵红佳 《中国科学:信息科学》 CSCD 2013年第5期657-669,共13页
隐写术是在看起来无害媒体中隐藏信息的科学.文中为了解决在常规隐信道下可证明安全隐写术的有效构造问题,在不依赖于任何采样假设的前提下,提供了一种基于计算不可区分的安全隐写术构造.文中结果表明,隐信道采样器中影射函数的不可区... 隐写术是在看起来无害媒体中隐藏信息的科学.文中为了解决在常规隐信道下可证明安全隐写术的有效构造问题,在不依赖于任何采样假设的前提下,提供了一种基于计算不可区分的安全隐写术构造.文中结果表明,隐信道采样器中影射函数的不可区分性是安全隐写系统抵抗自适应选择隐文攻击的必要条件.在此基础上,完整地证明了l(-1+5-2)—安全隐写系统能在-1伪随机函数和-2无偏采样函数下有效地被构造,其中,-1和-2是任意两个可忽略错误,l是多项式的隐文长度.更为重要的,文中的研究不依赖于密码系统的密文伪随机性假设和完美采样假设,因此,我们的结果对于安全隐写系统的构造和隐写分析都具有现实意义. 展开更多
关键词 密码学 隐写术 不可区分性 采样器 不可预测性 敌手模型
原文传递
上一页 1 下一页 到第
使用帮助 返回顶部