形式化

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

检索结果分析

结果分析中...
选择条件：
  • 期刊=计算机科学x
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于信任链技术的SSH传输层协议改进
《计算机科学》2025年第2期353-361,共9页王兴国 孙云霄 王佰玲 
主机密钥是SSH(安全外壳,Secure Shell)服务器的身份标识,用户通过检查主机密钥指纹实现对SSH服务器的身份认证。但在实际应用中,用户往往并不重视指纹检查过程,使得基于主机密钥替换的中间人攻击成为可能。为此,基于信任链思想提出一种...
关键词：SSH协议 信任链 中间人攻击 安全协议 形式化分析 
面向龙芯处理器的一种CompCert可信编译器重定向实现
《计算机科学》2024年第S02期747-755,共9页胡少儒 王隽伟 王生原 
国家重点研发计划(2022YFB3305204)。
CompCert是著名的C语言可信编译器,它借助于交互式定理证明工具Coq实现,能够确保生成的目标汇编代码保持源代码的语义,具有极高的可信度,近年来被广泛应用于学术界和工业界的许多安全攸关任务的研发工作中。CompCert编译器的当前版本支...
关键词：CompCert 编译器 编译器重定向 龙芯架构 形式化验证的编译器 COQ 
一种基于变量隐藏抽象的IC3硬件验证算法
《计算机科学》2023年第S02期783-788,共6页杨柳 范洪宇 李东方 贺飞 
国家重点研发计划课题(2018YFB1308601);国家自然科学基金(62072267,62021002);国防基础科学科研计划(XX2020204B028)。
随着硬件设计复杂性和规模的大幅度提升,硬件验证工作更加具有挑战性。模型检验技术作为一种自动化验证技术,可以自动构建反例路径,也因此成为硬件验证领域内最重要的研究方向之一。IC3算法是近些年来最成功的比特级别的硬件验证算法。...
关键词：硬件验证 IC3算法 形式化方法 模型检验 变量隐藏抽象 
基于CPN的供应链合约的形式化验证被引量：1
《计算机科学》2023年第S01期707-713,共7页郑红 钱诗慧 刘泽润 杜渂 
2019年度上海市信息化发展(大数据发展)专项资金项目(201901043)。
智能合约的安全性对于区块链在供应链领域的应用尤为重要。目前,大多数对智能合约的形式化验证工作集中于漏洞检测,对于如何在部署上链前生成安全的智能合约的关注仍然比较少,如何有效规范地将特定领域的属性安全地映射为智能合约代码...
关键词：智能合约 形式化方法 模型检查 CPN 供应链 
基于Coq的逆矩阵运算的形式化被引量：1
《计算机科学》2023年第S01期848-854,共7页沈楠 陈钢 
矩阵是一种在计算机科学中应用广泛的数据结构,其运算正确性具有重要意义。矩阵求逆在矩阵形式化工作当中缺乏合理且实用的形式化工作。其原因在于,工程中现有的两种常见求逆方法的形式化均存在难点。第一种是基于伴随矩阵求解方法,难...
关键词：形式化验证 形式化工程数学 逆矩阵形式化 COQ 软件安全 
SDN网络边缘交换机异常检测方法被引量：1
《计算机科学》2023年第1期362-372,共11页赵扬 伊鹏 张震 胡涛 刘少勋 
河南省重大科技专项(智能网联汽车内生安全关键技术研究及示范应用2022012);国家自然科学基金(61872382,62101598,61521003)。
软件定义网络(SDN)为网络赋予了可编程性,降低了网络管理的复杂性,促进了新型网络技术的发展。SDN交换机作为数据转发与策略执行的设备,其权限不应被未经授权的实体窃取。然而,SDN交换机并不总是执行控制器下发的命令,恶意攻击者通过侵...
关键词：软件定义网络 数据平面安全 形式化认证与分析 通信顺序进程 受损交换机检测 
EAP-TLS协议的形式化验证研究被引量：1
《计算机科学》2022年第S02期685-689,共5页陈丽萍 徐鹏 王丹琛 徐扬 
国家自然科学基金(61976130);四川省科技计划项目(2020YJ0270);中央高校基本科研业务费专项资金(2682021GF012);四川省无线电监测站科研计划([2019]4)
EAP-TLS是5G标准定义的在特定物联网环境中提供密钥服务的安全协议,然而EAP-TLS协议无法提供用户设备与网络之间的双向认证,存在设计缺陷的协议在运行时将危害系统安全,因此在协议实施之前分析其安全性,尽可能找到潜在缺陷并将其改进是...
关键词：认证协议 EAP-TLS 形式化验证 Proverif 非安全信道 
面向无人机通信的认证和密钥协商协议被引量：5
《计算机科学》2022年第8期306-313,共8页蹇奇芮 陈泽茂 武晓康 
国家自然科学基金面上项目(61872430);国家优秀青年科学基金(42122025);湖北省杰出青年科学基金(2019CFA086)。
针对无人机通信中密钥配置的安全性和轻量化需求,面向不同计算性能的无人机系统分别提出了基于椭圆曲线密码算法的认证和密钥协商协议DroneSec,以及基于对称密码算法的认证和密钥协商协议DroneSec-lite。所提协议实现了无人机和地面站...
关键词：无人机 双向认证 密钥协商 通信安全 安全协议 形式化验证 
基于进程代数的Otway-Rees协议的形式化验证
《计算机科学》2021年第S01期477-480,共4页蔡雨桐 王勇 王然然 姜正涛 代桂平 
广西密码学与信息安全重点实验室研究课题(GCIS201808)。
Otway-Rees协议的目的是完成发起者和响应者之间的双向认证,并且分发服务器产生的会话密钥。该协议的特点是简单实用,没有使用复杂的同步时钟机制或双重加密,仅用少量的信息提供了良好的时效性。此协议允许通过一个网络的个别通信认证...
关键词：Otway-Rees 安全协议 协议验证 形式化 进程代数 
基于进程代数的Yahalom协议正确性的形式化验证
《计算机科学》2021年第S01期481-484,共4页王然然 王勇 蔡雨桐 姜正涛 代桂平 
广西密码学与信息安全重点实验室研究课题(GCIS201808)。
通信过程中为了使得通信双方之间的对话过程是安全传输的,在引入可信第三方的基础上,Yahalom协议借助于可信第三方为通信双方分配"好"的会话密钥,利用该共享密钥加密对话内容保证双方对话的安全。Yahalom协议的形式化验证具有很重要的...
关键词：Yahalom协议 进程代数 形式化的验证 可信第三方 ACP公理系统 
全选清除导出
共21页<12345678910>
检索报告 对象比较 聚类工具 使用帮助 返回顶部