可信密码模块的模型检测分析

陈小峰; 冯登国

您当前的位置：

首页 >

文章列表页 >

可信密码模块的模型检测分析

学术论文 | 更新时间：2024-10-14

- 可信密码模块的模型检测分析
- Model checking of trusted cryptographic module
- 通信学报 2010年31卷第1期页码：59-64
- 作者机构：
  
  中国科学院软件研究所信息安全国家重点实验室
- 作者简介：
- 基金信息：
- DOI：
  中图分类号： TP393.08
- 纸质出版日期：2010
- 稿件说明：
移动端阅览
陈小峰, 冯登国. 可信密码模块的模型检测分析[J]. 通信学报, 2010,31(1):59-64.

CHEN Xiao-feng, FENG Deng-guo. Model checking of trusted cryptographic module[J]. 2010, 31(1): 59-64.
陈小峰, 冯登国. 可信密码模块的模型检测分析[J]. 通信学报, 2010,31(1):59-64. DOI：

CHEN Xiao-feng, FENG Deng-guo. Model checking of trusted cryptographic module[J]. 2010, 31(1): 59-64. DOI：

摘要

根据可信密码模块规范的非形式化描述

利用模型检测工具SPIN对可信密码模块安全性进行形式化分析

给出了可信密码模块形式化分析的基本框架

重点分析了AP授权协议和可信密码模块初始化子系统。指出了AP授权协议存在的缺陷

并给出了具体的改进措施;同时验证可信密码模块初始化子系统状态的一致性。

Abstract

The formal security analysis was given for the trusted cryptographic module according to the specification of the trusted cryptographic module using model checking tools. The flaws in the AP protocol were pointed and the solution was given. Meanwhile

the framework was proposed for analyzing the security property of the trusted cryptographic module using the model checking tools.

关键词

Keywords

references

浏览量

295

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

基于程序局部性引导的有界模型检测优化方法

基于时间自动机的物联网网关安全系统的建模及验证

基于模型检测的服务链信息流安全可组合验证方法