形式化

作品数：5172被引量：11555H指数：35
导出分析报告
相关领域：自动化与计算机技术文化科学更多>>
相关作者：关永施智平薛锦云张广泉段振华更多>>
相关机构：华东师范大学国防科学技术大学西安电子科技大学清华大学更多>>
相关期刊：更多>>
相关基金：国家自然科学基金国家高技术研究发展计划国家重点基础研究发展计划国家社会科学基金更多>>
-
在结果中检索

检索结果分析

结果分析中...
选择条件：
  • 期刊=计算机应用研究x
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于Tamarin的MQTT协议安全性分析方法被引量：4
《计算机应用研究》2023年第10期3132-3137,3143,共7页郑红兵 王焕伟 赵琪 董姝岐 井靖 
国家重点研发项目(2019QY502)。
MQTT是物联网中被广泛应用的消息传输协议,其安全性问题备受关注。当前MQTT协议安全性分析主要面向协议实现平台,缺少面向协议标准的安全性测试,导致协议标准本身存在的安全缺陷难以发现。针对该问题,采用协议形式化分析技术,提出了一...
关键词：MQTT协议 保密属性 认证属性 形式化分析 TAMARIN 
一种针对安全可达动态系统的形式化学习方法
《计算机应用研究》2023年第8期2411-2416,共6页鲁腾飞 娄攀登 王胜朴 丁觅 林望 
国家自然科学基金资助项目(62272416)。
在动态系统建模问题中,深度学习为建模提供了更便捷和灵活的方法,但其难以解释的特点降低了模型的可靠性。针对具有安全性和可达性的动态系统,提出了一种形式化模型学习方法,将安全性和可达性引入到对目标系统的学习过程中,使模型满足...
关键词：形式化方法 动态系统学习 安全性 可达性 
基于安全协议代码的形式化辅助建模研究被引量：2
《计算机应用研究》2023年第4期1189-1193,1202,共6页葛艺 黄文超 熊焰 
国家自然科学基金面上项目(61972369);国家自然科学基金青年项目(62102385);安徽省自然科学基金资助项目(2108085QF262)。
随着安全协议形式化分析技术的不断发展,利用工具自动验证虽已得到实现,但建模环节仍需依赖专业人员手工建模,难度大且成本高,限制了此技术的进一步推广。为了提高建模的自动化程度,提出了依据安全协议代码进行形式化模型辅助生成的方...
关键词：形式化验证 形式化建模 协议代码 污点分析 TAMARIN 
区块链拍卖退款交易智能合约DoS漏洞优化研究被引量：2
《计算机应用研究》2023年第2期343-348,共6页陈虹 王颖辉 金海波 曹玥 
国家自然科学基金资助项目(62173171)。
针对智能合约的DoS漏洞可能在拍卖退款交易中造成资源耗尽问题进行了研究,设计了拍卖退款交易中智能合约DoS漏洞优化方案。首先构造可能存在DoS漏洞的智能合约,然后采用增加映射以及压栈出栈方法完成漏洞优化,最后通过形式化验证运行优...
关键词：智能合约 形式化验证 拍卖退款 DoS漏洞 
基于CRT的gNB间切换认证方法与密钥协商协议
《计算机应用研究》2022年第11期3450-3454,3460,共6页谢桢 季新生 游伟 
国家重点研发计划资助项目;国家自然科学基金资助项目。
针对当前UE在gNB间的切换认证与密钥协商过程存在的仅有两跳前向安全性和易受拒绝服务攻击等问题,提出了一种基于中国剩余定理(CRT)的切换认证与密钥协商协议。该协议利用秘密共享原理,令源gNB和所有可能的目标gNB构成一个群体,把真实...
关键词：5G gNB 切换认证 形式化分析 
基于双线性映射的三因子远程身份认证协议研究被引量：3
《计算机应用研究》2020年第1期221-224,共4页魏春英 郭中华 
国家自然科学基金资助项目(61565014).
为了提高多服务器环境身份认证的安全性,降低计算复杂度,提出一种基于双线性映射的三因子认证协议,这些因子包括生物信息、智能卡和双线性映射密码。该协议包括系统设置、服务器注册、用户注册、登录、认证和密钥协商,以及密码更新六个...
关键词：多服务器 身份认证 双线性映射 生物信息 智能卡 形式化证明 
单向网络安全设备的分析与证明被引量：3
《计算机应用研究》2019年第4期1120-1124,共5页王雪健 赵国磊 常朝稳 王瑞云 
国家自然科学基金资助项目(61572517)
单向网络安全设备是不同密级间网络信息传输的主要安全设备。为了保证单向网络安全设备内部的安全性和通信系统的安全性,分析了单向网络安全设备的安全需求,提出无干扰模型形式化建模,用数学归纳法证明单向网络安全设备安全需求与形式...
关键词：单向网络安全设备 形式化 无干扰模型 安全策略 数学归纳法 
一种水下群机器人路径规划算法的形式化研究被引量：3
《计算机应用研究》2019年第2期490-494,共5页张杰 刘耕阳 关永 
国家自然科学基金资助项目(61572331)
为了增强基于遗传算法的水下群机器人路径规划算法正确性的说服力,使用定理证明对其进行形式化研究,给出算法在定理证明器HOL4中的形式化模型。基于算法形式化的一般步骤,对算法的设计进行了详细的分析,指出算法设计的核心步骤和建模难...
关键词：遗传算法 群机器人 路径规划 定理证明 形式化建模 HOL4 
基于信息流控制的HDFS敏感数据安全增强被引量：2
《计算机应用研究》2018年第11期3432-3435,共4页吴泽智 陈性元 杜学绘 杨智 
国家"863"计划资助项目(2015AA016006;2012AA012704);国家重点研发计划资助项目(2016YFB0501900)
针对HDFS已有保护方法如认证授权、数据加密、访问控制和审计方法都不能保证敏感数据端到端的安全性,提出了一个用于HDFS的安全代数语言SALH(security algebra language for HDFS),给出了SALH的语义和语法;采用SALH形式化描述了HDFS信...
关键词：分布式文件系统 信息流跟踪 安全代数 无干扰 形式化分析 
基于形式化的测试框架及实例分析被引量：1
《计算机应用研究》2018年第6期1778-1782,共5页李元平 李华 阮宏玮 赵俊岚 王彪 
国家自然科学基金资助项目(61163011);赛尔网络下一代互联网技术创新项目(NGII20150112)
测试工作细致繁杂,如何保证测试工作的全面性、完整性并建立统一的测试理论,指导测试工作自动、高效地展开,继而提高测试的复用性,是人们长久以来追求的目标。设计了通用的测试框架,依托基于模型的测试理论,支持通用的测试序列产生方法...
关键词：测试框架 IPV6 OpenFlow 测试引擎 
全选清除导出
共9页<123456789>
检索报告 对象比较 聚类工具 使用帮助 返回顶部