公开(公告)号：CN115169269A

公开(公告)日：2022-10-11

申请号：CN202210599036.0

申请日：2022-05-30

Applicant: 西南交通大学 ,  成都纺织高等专科学校 ,  成都电迅达科技有限公司

Inventor： 徐鹏 ,  马方立 ,  陈美荣 ,  何永东 ,  王丹琛 ,  王秀珍

IPC: G06F30/33

Abstract: 本发明公开了一种基于FPGA设计的集成电路可信性验证工具与方法，涉及集成电路芯片设计安全领域，包括FPGA模型、形式化模型、形式化验证和结果输出；所述FPGA模型包括高级程序语言实现模型和硬件语言实现模型；形式化模型实施高级程序语言实现模型与硬件语言实现模型的一致性检验，并形成逻辑公式，直接构建硬件语言实现的形式化模型，并转换为逻辑公式；进行可信性验证，接入逻辑公式推理求解系统，通过对逻辑公式求解得到是否可满足结论，进一步反映模型是否存在缺陷；然后输出可信性验证结果，既保障模型高级语言与硬件语言实现的一致性，又提高硬件语言代码的安全性。

公开(公告)号：CN115174143A

公开(公告)日：2022-10-11

申请号：CN202210598491.9

申请日：2022-05-30

Applicant: 西南交通大学 ,  成都纺织高等专科学校

Inventor： 徐鹏 ,  贾昊洲 ,  王秀珍 ,  王丹琛 ,  陈美荣

IPC: H04L9/40 ,  H04L67/01

Abstract: 本发明公开了一种基于安全协议的网络空间安全可信性验证方法，涉及网络安全协议技术领域，包括以下步骤：S1、将安全协议划分为协议规范和协议实施代码两个部分；S2、协议规范的形式化验证，对协议规范构建形式化模型，将其转换为逻辑求解公式，通过逻辑求解系统进行求解验证；S3、协议实施代码的形式化验证，先实施协议安全性质的程序代码描述，再构建协议实施代码的形式化模型，进行验证；S4、实施协议安全性质的一致性检验；本发明结合协议模型和实施代码共同对协议形式化建模和验证，减少安全协议本身的缺陷和可能存在的攻击方式，解决安全协议抽象规范和代码之间存在的语义断层问题,协议规范与实施代码的可信性验证均满足协议安全性质。

公开(公告)号：CN115174143B

公开(公告)日：2024-01-26

申请号：CN202210598491.9

申请日：2022-05-30

Applicant: 西南交通大学 ,  成都纺织高等专科学校

Inventor： 徐鹏 ,  贾昊洲 ,  王秀珍 ,  王丹琛 ,  陈美荣

IPC: H04L9/40 ,  H04L67/01

Abstract: 本发明公开了一种基于安全协议的网络空间安全可信性验证方法，涉及网络安全协议技术领域，包括以下步骤：S1、将安全协议划分为协议规范和协议实施代码两个部分；S2、协议规范的形式化验证，对协议规范构建形式化模型，将其转换为逻辑求解公式，通过逻辑求解系统进行求解验证；S3、协议实施代码的形式化验证，先实施协议安全性质的程序代码描述，再构建协议实施代码的形式化模型，进行验证；S4、实施协议安全性质的一致性检验；本发明结合协议模型和实施代码共同对协议形式化建模和验证，减少安全协议本身的缺陷和可能存在的攻击方式，解决安全(56)对比文件Yuan Liang;K E Guo;Jianping Li.Theremote attestation design based on theidentity and attribute certificates《.2014 11th International ComputerConference on Wavelet Actiev MediaTechnology and Information Processing》.2717-2722.