形式化分析

作品数：446被引量：1033H指数：13
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：王亚弟文静华韩继红冯登国张玉清更多>>
相关机构：解放军信息工程大学西安电子科技大学贵州大学中国科学院研究生院更多>>
相关期刊：更多>>
相关基金：国家自然科学基金国家高技术研究发展计划国家重点基础研究发展计划国家科技重大专项更多>>
-
在结果中检索

检索结果分析

结果分析中...
选择条件：
  • 期刊=信息网络安全x
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于递归认证测试的SIP协议形式化分析
《信息网络安全》2024年第10期1586-1594,共9页姚萌萌 王宇 洪瑜平 
国家重点研发计划[2022YFB4502000]。
文章以形式化分析方法证明协议安全为研究目的,以具有灵活性、开放性、可伸缩性等特性的SIP协议为研究对象,运用基于串空间理论改进的递归认证测试形式化分析方法,分析了一种BAN逻辑证明安全的SIP身份认证协商协议,发现了该协议执行过...
关键词：SIP协议 递归认证测试 串空间 形式化分析方法 
基于事件的群组密钥协商协议形式化分析研究被引量：3
《信息网络安全》2022年第5期30-36,共7页沈延 姚萌萌 
国家自然科学基金[91430214,6732018];核高基重大专项[2017ZX01028101]。
群组密钥协商协议应用于物联网、无线通信、区块链、视频会议等领域,是当前的一个研究热点。该协议的交互消息较多,且消息认证、加密所使用的密码算法也复杂,这就给密码协议的形式化描述与安全性分析带来一定的困难。文章基于串空间理论...
关键词：群组密钥协商协议 串空间 形式化分析 
一种基于拜占庭容错的PoS共识协议形式化分析方法被引量：1
《信息网络安全》2021年第8期35-42,共8页陈凯杰 熊焰 黄文超 武建双 
国家自然科学基金[61972369];国家重点研发计划[2018YFB2100301]。
区块链共识协议是一种确保区块链网络中不同节点的数据达成一致的重要机制,随着区块链应用的爆发性增长,针对区块链共识协议的攻击不断出现。文章提出一种基于拜占庭容错的PoS共识协议形式化分析方法,通过归纳建模共识节点整体状态迁移...
关键词：区块链共识协议 拜占庭容错 归纳建模 形式化分析 
基于物理不可克隆函数的Kerberos扩展协议及其形式化分析被引量：4
《信息网络安全》2020年第12期91-97,共7页张正 查达仁 柳亚男 方旭明 
国家重点研发计划[2017YFB0802802];国家自然科学基金[61902163]。
文章提出一种基于物理不可克隆函数(PUF)的Kerberos扩展协议。基于PUF的激励响应认证机制,利用PUF激励响应对代替Kerberos标准协议中的口令或数字证书,可以抵抗口令猜测攻击和假冒攻击。该协议优势在于实现认证服务器与设备的双向认证...
关键词：物理不可克隆函数 KERBEROS 认证 密钥分配 BAN逻辑 
基于串空间的安全协议形式化分析研究被引量：5
《信息网络安全》2020年第2期30-36,共7页姚萌萌 唐黎 凌永兴 肖卫东 
国家自然科学基金[91430214];核高基重大专项[2017ZX01028101]。
安全协议是信息安全领域的重要组成部分,随着新兴技术的快速发展,安全协议变得越来越复杂,给安全协议的形式化分析带来了挑战。近年来,基于串空间理论的形式化分析方法是一个研究热点,在安全协议分析领域得到了广泛的关注和研究,并取得...
关键词：串空间 形式化分析 安全协议 区块链 
基于时间自动机的工业控制系统网络安全风险分析被引量：2
《信息网络安全》2019年第11期71-81,共11页吕宗平 丁磊 隋翯 顾兆军 
国家自然科学基金[61601467,U1533104];民航科技基金[MHRD20140205,MHRD20150233];民航安全能力建设基金[PES A170003,PESA2018079,PESA2018082,PESA2019073,PESA2019074]
随着工业控制系统开放性增强,大量工业控制协议漏洞暴露在互联网上,造成了工业控制系统安全风险急剧上升。文章针对工业控制系统中最常用的Modbus协议,以典型灌装环节为例,提出了一种基于时间自动机的工业控制系统网络安全分析方法,并...
关键词：工业控制系统 形式化分析 时间自动机 MODBUS协议 UPPAAL 
一种基于一次性口令的增强Kerberos协议方法及其形式化分析被引量：3
《信息网络安全》2019年第10期57-64,共8页马利民 张伟 宋莹 
国家自然科学基金[61872043];中央引导地方科技发展专项：量子通信技术创新与行业应用[Z171100004717002];北京市教育委员会科技计划项目[KM201811232017]
Kerberos协议是分布式网络中一种重要的基于可信第三方认证协议,广泛应用于各主流操作系统以及云计算、无线网络等场景,但容易受到口令猜测攻击、重放攻击等。虽然基于公钥密码学的PKINIT协议可以增强Kerberos协议对这些攻击的抵抗能力...
关键词：KERBEROS PKINIT 一次性口令 口令猜测攻击 BAN逻辑 
一种改进的基于认证测试的形式化分析方法被引量：1
《信息网络安全》2019年第1期27-33,共7页姚萌萌 朱正超 刘明达 
国家自然科学基金[91430214;6732018];核高基重大专项[2017ZX01028101]
近年来,认证测试定理得到了改进,并应用于各种安全协议的分析。但是这些改进定理在应用范围和准确性方面存在一定的缺陷。针对这些缺陷,文章提出了一种改进的输入测试定理及加密测试定理,并给出了改进定理的证明。通过分析认证测试中常...
关键词：串空间 认证测试 形式化分析方法 安全协议 
基于主体关联度的安全协议形式化分析方法被引量：3
《信息网络安全》2018年第6期45-51,共7页余磊 魏仕民 江明明 
国家自然科学基金[61300048;61572224];安徽省自然科学基金[1608085MF143;1708085QF154];安徽省高校优秀青年人才计划项目[gxyq2017154];安徽省教育厅自然科学项目[KJ2014A231;KJ2016A627]
建立在协议主体参数新近一致性上的主体关联度由于能够正确反映协议安全属性与协议结构、消息组件和消息参数的逻辑关系,因此不仅能够为安全协议的正确性分析提供准确严谨的形式化判断依据,还能进一步降低协议分析的复杂度。为此,文章...
关键词：安全协议 认证测试 关联度 形式化分析 
交互型电子签名的形式化分析被引量：3
《信息网络安全》2016年第9期31-34,共4页朱鹏飞 张利琴 李伟 于华章 
交互型电子签名是一种与特定类型的密钥载体紧密结合的电子签名应用。在攻击者通过劫持主机等方式远程控制密钥载体的情况下,交互型电子签名能够有效阻止其冒用合法用户身份进行交易或篡改交易信息。文章利用形式化方法对交互型电子签...
关键词：交互型电子签名 形式化分析 行业标准 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部