形式化分析

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

检索结果分析

结果分析中...
选择条件：
  • 期刊=通信学报x
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于身份认证的BACnet/IP分析与改进
《通信学报》2024年第3期227-243,共17页谢鹏寿 朱家锋 康永平 冯涛 李威 冉玉翔 
国家自然科学基金资助项目(No.61862040,No.62162039)。
为了解决BACnet/IP身份认证存在多种可攻击漏洞和密钥泄露带来的安全问题,提出了一种安全增强的BACnet/IP-SA协议认证方案。研究协议身份认证消息流模型,基于着色Petri网理论和CPNTools对身份认证消息流建模,采用Dolev-Yao攻击者模型和...
关键词：BACNET/IP 形式化分析 着色PETRI网 BAN逻辑 协议改进 
基于CPN的安全协议形式化建模及安全分析方法被引量：6
《通信学报》2021年第9期240-253,共14页龚翔 冯涛 杜谨泽 
国家自然科学基金资助项目(No.62162039,No.61762060);甘肃省高等学校科研基金资助项目(No.2017C-05);甘肃省科技厅重点研发计划基金资助项目(No.20YF3GA016)。
为了解决有色Petri网(CPN)对安全协议进行形式化建模分析时,仅能判断协议是否存在漏洞而无法找出漏洞具体位置和攻击路径的问题,以及CPN建模时随着攻击者模型引入,安全协议的形式化模型可能的消息路径数量激增,状态空间容易发生爆炸导...
关键词：有色PETRI网 安全协议 形式化分析 状态空间 攻击路径 
基于计算模型的安全协议Swift语言实施安全性分析被引量：1
《通信学报》2018年第9期178-190,共13页孟博 何旭东 张金丽 尧利利 鲁金钿 
国家自然科学基金资助项目(No.61272497);湖北省自然科学基金资助项目(No.2014CFB249;No.2018ADC150);中南民族大学中央高校基本科研业务费专项资金资助项目(No.CZZ18003;No.QSZ17007)~~
分析IOS平台上的安全协议Swift语言实施安全性,对保障IOS应用安全具有重要意义。首先对已有安全协议Swift语言实施进行分析,确定Swift语言子集SubSwift,并给出其BNF;其次基于操作语义,建立SubSwift语言到Blanchet演算的映射模型,主要包...
关键词：安全协议 实施安全性 Swift语言 形式化分析 模型抽取 
基于SAT的安全协议惰性形式化分析方法被引量：2
《通信学报》2014年第11期117-125,共9页顾纯祥 王焕孝 郑永辉 辛丹 刘楠 
河南省科技创新杰出青年基金资助项目(134100510002);河南省基础与前沿技术研究基金资助项目(142300410002);数学工程与先进计算国家重点实验室开放基金资助项目~~
提出了一种基于布尔可满足性问题的安全协议形式化分析方法 SAT-LMC,通过引入惰性分析的思想优化初始状态与转换规则,提高了安全性的检测效率。另一方面,通过在消息类型上定义偏序关系,SAT-LMC能够检测出更丰富的类型缺陷攻击。基于此...
关键词：安全协议 形式化分析 布尔可满足性 惰性分析 类型缺陷攻击 
基于串空间的匿名形式化分析扩展被引量：2
《通信学报》2011年第6期124-131,共8页董学文 牛文生 马建峰 谢晖 毛立强 
国家科技部重大专项(2011zx03005-002);国家自然科学基金资助项目(61072066;60872041);中央高校基本科研业务费专项资金资助(JY10000903006;JY10000903012;JY10000903001;JY10000901034)~~
为了使串空间满足匿名性分析的特殊需求,利用串空间丛消息解析等价技术,结合观察视角,分别定义2种发送者匿名性、接收者匿名性;基于不同的侧重点,定义出不同的关系匿名性,在此基础上扩展并完善了基于串空间的匿名性形式化框架。同时,定...
关键词：串空间 匿名协议 等价丛 匿名程度 
传感器网络安全协议的分析和改进被引量：8
《通信学报》2011年第5期139-145,共7页闫丽丽 彭代渊 高悦翔 
四川省教育厅青年基金资助项目(08zb025)~~
分析A.Perrig提出的传感器网络安全协议套件的安全性,发现其中的节点密钥协商协议存在攻击,即攻击者可以冒充合法节点发送密钥协商请求。针对以上攻击,给出了一个改进协议。为了分析改进协议的安全性,对原始串空间理论进行了扩展,并使...
关键词：无线传感器网络 安全协议 形式化分析 串空间 
可证明安全的MANET按需源路由协议分析被引量：3
《通信学报》2009年第1期38-44,共7页毛立强 马建峰 李兴华 
国家高技术研究发展计划("863"计划)基金资助项目(2007AA01Z429;2007AA01Z405);国家自然科学基金重点资助项目(60633020);国家自然科学基金资助项目(60573036;60702059;60503012;60803150)~~
对MANET安全按需源路由协议的一种形式化分析模型进行了深入分析,指出其中存在的合并相邻敌手节点等不合理操作以及该模型下endairA协议安全性证明过程中的错误,并给出了一种针对endairA协议的隐蔽信道攻击,表明该协议即使在其安全分析...
关键词：路由协议 可证明安全 形式化分析 模拟 隐蔽信道攻击 
对Bellare-Rogaway 3PKD模型安全性定义的修正被引量：1
《通信学报》2007年第9期1-6,共6页刘军 廖建新 朱峰 王纯 
国家杰出青年科学基金资助项目(60525110);国家重点基础研究发展计划("973"计划)基金资助项目(2007CB307100;2007CB307103);新世纪优秀人才支持计划(NCET-04-0111)~~
指出Bellare和Rogaway在1995年提出的三方密钥分发模型——Bellare-Rogaway 3PKD模型的安全性定义存在缺陷。为此,设计了一个新的三方密钥分发协议P-Flaw。该协议在Bellare-Rogaway 3PKD模型下是可证明安全的。但是通过分析发现该协议...
关键词：安全模型 可证明安全性 密钥分发 形式化分析 
运行模式法分析密码协议实例研究
《通信学报》2005年第B01期129-132,共4页王春玲 唐志坚 张玉清 薛纪文 
在介绍两方密码协议运行模式分析法的基础上，运用运行模式分析法对自行设计的TW两方密码协议进行了分析，成功地发现了TW协议的攻击，并验证了此协议的安全性，说明了两方密码协议运行模式分析法的有效性。
关键词：密码协议 形式化分析 运行模式 
CC安全功能组件形式化分析
《通信学报》2003年第7期164-169,共6页黄元飞 何德全 陈明奇 
国家科技兴贸行动计划基金资助项目(2001-EE-66-0008)
先提出了一种CC(common criteria)安全功能组件的形式化分析方法,对CC中的135个组件分别作形式化分析,评估各组件规范安全功能要求的确定性,并在此基础上进一步分析安全功能类的标准化规范程度及其优缺点。
关键词：CC 安全功能组件 安全功能要求 信息安全 形式化分析 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部