检索结果-南通市图书馆

基于观察等价性的协议猜测攻击形式化检测方法

在线全文

学校读者我要写书评

暂无评论

密码学报 2023年第2期10卷 306-319页

作者：苗旭阳顾纯祥陆思奇数学工程与先进计算国家重点实验室郑州450001 网络密码技术河南省重点实验室郑州450001

由于口令的低熵性,针对基于口令的安全协议存在特有的口令猜测攻击,当前的形式化语义不能较好地刻画攻击者执行口令猜测攻击的条件,对于协议抗猜测攻击能力没有统一的形式化安全属性定义.本文提出了基于观察等价性的协议猜测攻击形式化... 详细信息

由于口令的低熵性,针对基于口令的安全协议存在特有的口令猜测攻击,当前的形式化语义不能较好地刻画攻击者执行口令猜测攻击的条件,对于协议抗猜测攻击能力没有统一的形式化安全属性定义.本文提出了基于观察等价性的协议猜测攻击形式化检测方法.使用多集重写规则对协议交互流程进行形式化建模,给出了口令初始化、口令猜测行为的标准化规则,修改完善基于口令的对称加密原语,以支持包含基于口令的对称加密的协议验证.理论上将协议口令猜测攻击的形式化分析检测转换为正确猜测和错误猜测下多集重写规则双系统的观察等价性是否成立的判断问题;实现上使用Tamarin形式化分析工具对协议是否存在口令猜测攻击进行自动化分析,首次实现了形式化分析工具对口令猜测攻击路径的自动化生成.使用该方法对EKE、SPAKE等传统口令认证协议和多因子认证协议进行形式化建模和分析,对其中存在口令猜测攻击的协议自动化生成可行的口令猜测攻击路径,验证了方法的正确性和有效性.

关键词：形式化分析观察等价性口令猜测攻击 Tamarin-Prover

基于标记配对相干态光源的实用化诱骗态量子随机数发生器

在线全文

学校读者我要写书评

暂无评论

密码学报 2023年第1期10卷 73-86页

作者：李元昊费洋扬王卫龙孟祥栋王洪段乾恒马智数学工程与先进计算国家重点实验室郑州450001 河南省网络密码技术重点实验室郑州450001

基于维度目击的量子随机数发生协议中需要使用完美的单光子源,现实中难以低成本、较方便地实现.本文给出了一种基于标记配对相干态光源的实用化诱骗态量子随机数生成协议,利用三强度诱骗态的方法可以准确估计出随机数生成协议的最小熵,... 详细信息

基于维度目击的量子随机数发生协议中需要使用完美的单光子源,现实中难以低成本、较方便地实现.本文给出了一种基于标记配对相干态光源的实用化诱骗态量子随机数生成协议,利用三强度诱骗态的方法可以准确估计出随机数生成协议的最小熵,随机数提取率比基于弱相干态光源的诱骗态量子随机数生成协议更高.分析探测器的探测效率、后脉冲和探测效率不匹配对该协议安全性造成的影响,探测器的探测效率与最小熵呈正相关;后脉冲增加会降低输出的最小熵,影响随机数的安全性;在非对称基矢探测器效率的情况下,若其中一个测量基的探测效率较高,则该协议可以在另一个测量基的探测效率任意接近于0的情况下输出量子随机数.

关键词：量子随机数发生器标记配对相干态光源诱骗态

在线全文

学校读者我要写书评

暂无评论

面向物联网的轻量级可验证群组认证方案

电子学报 2022年第4期50卷 990-1001页

作者：陈书仪刘亚丽林昌露李涛董永权江苏师范大学计算机科学与技术学院江苏徐州221116 福建师范大学福建省网络安全与密码技术重点实验室福建福州350007 河南省网络密码技术重点实验室河南郑州450001

随着物联网应用的广泛扩展,越来越多的物联网设备出现在人们的日常生活中,包括智能电表、智能家居、智能穿戴等.它们在带给人民生活便利的同时,由于物联网设备通过无线开放信道进行交互,造成诸多安全和隐私问题的出现.身份认证是解决物... 详细信息

随着物联网应用的广泛扩展,越来越多的物联网设备出现在人们的日常生活中,包括智能电表、智能家居、智能穿戴等.它们在带给人民生活便利的同时,由于物联网设备通过无线开放信道进行交互,造成诸多安全和隐私问题的出现.身份认证是解决物联网安全和隐私问题的关键技术之一.传统的点对点认证方案没有考虑到物联网海量节点和节点资源受限的情况,而群组认证是一种一次验证一组成员身份的认证技术,为物联网节点的身份认证提供了新的思路.然而,现有适用于物联网场景的群组认证方案存在安全隐患,无法抵抗伪造、重放等恶意攻击并且无法防止群组管理者对组成员的欺骗.本文利用可验证秘密共享技术设计了一种适用于物联网场景的轻量级可验证群组认证方案以抵抗群组管理者的欺骗行为.另外,在物联网场景下,节点可能会动态地加入和撤出网络,针对这种情况,本文在可验证群组认证方案的基础上设计密钥更新环节以更新组成员的权限.安全性分析表明,本文方案满足正确性、机密性,能够抵抗重放、伪造、冒充等恶意攻击.性能分析和实验仿真表明,与现有典型的物联网群组认证方案相比,本文方案在保证安全性的同时降低了组成员的计算代价.

关键词：群组认证物联网轻量级可验证秘密共享动态群组

C2P:基于Pi演算的协议C代码形式化抽象方法和工具

在线全文

学校读者我要写书评

暂无评论

软件学报 2021年第6期32卷 1581-1596页

作者：张协力祝跃飞顾纯祥陈熹数学工程与先进计算国家重点实验室河南郑州450001 网络密码技术河南省重点实验室河南郑州450002

形式化方法为安全协议分析提供了理论工具,但经过形式化验证过的协议标准在转换为具体程序实现时,可能无法满足相应的安全属性.为此,提出了一种检测安全协议代码语义逻辑错误的形式化验证方法.通过将协议C源码自动化抽象为Pi演算模型,基... 详细信息

形式化方法为安全协议分析提供了理论工具,但经过形式化验证过的协议标准在转换为具体程序实现时,可能无法满足相应的安全属性.为此,提出了一种检测安全协议代码语义逻辑错误的形式化验证方法.通过将协议C源码自动化抽象为Pi演算模型,基于Pi演算模型对协议安全属性形式化验证.最后给出了方案转换的正确性证明,并通过对Kerberos协议实例代码验证表明方法的有效性.根据该方案实现了自动化模型抽象工具C2P与成熟的协议验证工具ProVerif结合,能够为协议开发者或测试人员检测代码中的语义逻辑错误提供帮助.

关键词：协议实现形式化验证 Pi演算模型抽取 ProVerif

在线全文

学校读者我要写书评

暂无评论

密码算法旁路立方攻击改进与应用

电子与信息学报 2020年第5期42卷 1087-1093页

作者：王永娟王涛袁庆军高杨王相宾战略支援部队信息工程大学郑州450001 河南省网络密码技术重点实验室郑州450001

立方攻击的预处理阶段复杂度随输出比特代数次数的增长呈指数级增长,寻找有效立方集合的难度也随之增加。该文对立方攻击中预处理阶段的算法做了改进,在立方集合搜索时,由随机搜索变为带目标的搜索,设计了一个新的目标搜索优化算法,优... 详细信息

立方攻击的预处理阶段复杂度随输出比特代数次数的增长呈指数级增长,寻找有效立方集合的难度也随之增加。该文对立方攻击中预处理阶段的算法做了改进,在立方集合搜索时,由随机搜索变为带目标的搜索,设计了一个新的目标搜索优化算法,优化了预处理阶段的计算复杂度,进而使离线阶段时间复杂度显著降低。将改进的立方攻击结合旁路方法应用在MIBS分组密码算法上,从旁路攻击的角度分析MIBS的算法特点,在第3轮选择了泄露位置,建立关于初始密钥和输出比特的超定的线性方程组,可以直接恢复33 bit密钥,利用二次检测恢复6 bit密钥。所需选择明文量221.64,时间复杂度225。该结果较现有结果有较大改进,恢复的密钥数增多,在线阶段的时间复杂度降低。

关键词：立方攻击旁路攻击预处理二次检测 MIBS算法

在线全文

学校读者我要写书评

暂无评论

Shor整数分解算法的线路优化

计算机科学 2022年第S1期49卷 649-653页

作者：刘建美王洪马智数学工程与先进计算国家重点实验室郑州450001 河南省网络密码技术重点实验室郑州450001

借助加窗技术和模整数的陪集表示技术,在加法的近似编码表示基础上给出Shor算法量子线路的整体优化和资源估计,并对设计的量子线路进行了仿真实验。借助加窗技术和模整数的陪集表示技术可以有效减少Toffoli门的数目以及降低整个量子线... 详细信息

借助加窗技术和模整数的陪集表示技术,在加法的近似编码表示基础上给出Shor算法量子线路的整体优化和资源估计,并对设计的量子线路进行了仿真实验。借助加窗技术和模整数的陪集表示技术可以有效减少Toffoli门的数目以及降低整个量子线路的深度,其中Toffoli门数目为0.18n^(3)+0.000465n^(3)log n,线路深度为0.3n^(3)+0.000465n^(3)log n。由于采用加窗的半经典傅里叶变换,使得空间资源代价为3n+O(log n)个量子比特。在增加少量近似误差(误差可以随着填充数目的增加呈指数减小)的前提下,实现了时间空间资源代价的折衷。

关键词：整数分解量子算法量子线路

在线全文

学校读者我要写书评

暂无评论

轻量级分组密码PUFFIN的差分故障攻击

电子与信息学报 2020年第6期42卷 1519-1525页

作者：袁庆军张勋成高杨王永娟战略支援部队信息工程大学郑州450001 河南省网络密码技术重点实验室郑州450001

基于代换–置换网络结构的轻量级分组密码算法PUFFIN在资源受限的硬件环境中使用较广泛,差分故障攻击是针对硬件密码算法较为有效的攻击手段。该文针对PUFFIN算法,改进多比特故障模型,通过构建输出差分和可能输入值之间的关系,注入5次... 详细信息

基于代换–置换网络结构的轻量级分组密码算法PUFFIN在资源受限的硬件环境中使用较广泛,差分故障攻击是针对硬件密码算法较为有效的攻击手段。该文针对PUFFIN算法,改进多比特故障模型,通过构建输出差分和可能输入值之间的关系,注入5次故障即可确定单个S盒唯一输入值;在最后一轮加密过程中注入10次故障,成功恢复轮密钥的概率为78.64%,进而可恢复初始密钥。

关键词：差分故障攻击代换–置换网络结构 PUFFIN算法

在线全文

学校读者我要写书评

暂无评论

轻量级分组密码SLIM的差分故障攻击

密码学报 2022年第2期9卷 223-236页

作者：高杨王永娟高光普袁庆军王灿战略支援部队信息工程大学郑州450001 河南省网络密码技术重点实验室郑州450001

SLIM是2020年提出的新型轻量级分组密码算法,因其极低的门电路功耗和良好的硬件实现性能,在受限的小规模加密场合具有一定应用前景.差分故障攻击是研究轻量级密码算法的有效手段,本文采用半字节故障攻击模型对SLIM算法进行研究,分析算... 详细信息

SLIM是2020年提出的新型轻量级分组密码算法,因其极低的门电路功耗和良好的硬件实现性能,在受限的小规模加密场合具有一定应用前景.差分故障攻击是研究轻量级密码算法的有效手段,本文采用半字节故障攻击模型对SLIM算法进行研究,分析算法差分扩散规律,结合密钥扩展方案,提出一种故障注入策略.分别在第2至32轮注入宽度为1至4个半字节的故障,最少共注入62组故障可将恢复主密钥的计算复杂度降低至2^(3).本文研究SLIM算法S盒的差分不均匀性,通过分析输入差分、输出差分和可能输入值之间的对应关系建立S盒差分分布表,将差分方程的求解直接转化为查表操作,快速缩小方程解空间.进一步利用S盒差分分布统计规律系统分析了方程是否存在唯一解的情形,基于概率学知识计算出不同故障注入组数下各轮密钥恢复成功率,得到恢复主密钥所需故障注入组数期望值68.15组.经仿真模拟实验,1000次攻击恢复主密钥所需故障注入组数均值为69.07组,与理论结果较为接近.

关键词：差分故障攻击轻量级分组密码 SLIM算法概率分析

在线全文

学校读者我要写书评

暂无评论

基于证书的抗连续泄露签名机制

计算机学报 2022年第11期45卷 2363-2376页

作者：周彦伟马岿乔子芮杨波顾纯祥陕西师范大学计算机科学学院西安710062 河南省网络密码技术重点实验室郑州450052 广西密码学与信息安全重点实验室广西桂林541004

为进一步提升密码原语的安全性,近年来抵抗泄露攻击的密码机制相继被研究者提出.基于证书的密码体制在解决传统公钥基础设施中证书复杂管理问题的同时,也避免了身份基密码机制的密钥托管不足,上述优势使得该体制在实际环境中具有广泛的... 详细信息

为进一步提升密码原语的安全性,近年来抵抗泄露攻击的密码机制相继被研究者提出.基于证书的密码体制在解决传统公钥基础设施中证书复杂管理问题的同时,也避免了身份基密码机制的密钥托管不足,上述优势使得该体制在实际环境中具有广泛的应用前景,然而由于缺乏对该体制泄露容忍性的研究,制约了该机制在安全协议设计方面的应用推广.针对上述不足,为满足基于证书签名机制的抗泄露性需求,本文提出了基于证书的抗泄露签名机制的具体构造,并基于离散对数的困难性,在随机谕言机模型下使用分叉引理对本文方案的不可伪造性进行了形式化证明;由于未使用双线性映射运算,确保本文构造具有较高的计算效率.与现有相关机制的比较可知,在保持安全性可证明的基础上,本文构造为签名机制提供抵抗泄露攻击能力的同时,提升了相应的计算效率.此外,在上述基础方案之上,本文设计了基于证书的抗泄露聚合签名机制的具体构造,实现了同时完成多个签名的合法性验证目标,进一步提升了签名的合法性验证效率,上述优势确保本文构造能在实际应用中广泛使用,例如无线传感器网络等.

关键词：泄露容忍性基于证书的密码学基于证书的签名分叉引理