基本信息来源于合作网站,原文需代理用户跳转至来源网站获取       
摘要:
可信信道是一个与终端的系统平台状态信息安全绑定的安全信道.现有的关于可信信道的研究工作都没有从理论上对所设计的可信信道的安全属性进行分析.本文首先提出一个基于SSH安全信道协议的可信信道协议,然后利用形式化模型检测器NuSMV分析该协议的安全属性,最后基于检测器执行轨迹所构成的反例,提出了一个强壮的SSH可信信道协议.本文提出的建模和验证方法具有通用性,可用于分析其他基于安全信道协议的可信信道协议的安全属性.
推荐文章
基于Rebeca模型的硬件设计形式化验证
形式化验证
Rebeca模型
Modere
基于扩展Petri网的系统建模及形式化验证方法
形式化验证
建模
实时有色Petri网
嵌入式系统
基于TLA的事件图模型形式化验证方法
仿真模型
验证、确认和认定
模型检验
行为时态逻辑
事件图
嵌入式操作系统的形式化验证方法
操作系统
形式化验证
定理证明
模型检测
嵌入式软件
内容分析
关键词云
关键词热度
相关文献总数  
(/次)
(/年)
文献信息
篇名 SSH可信信道安全属性的形式化验证
来源期刊 北京交通大学学报 学科 工学
关键词 SSH TCG远程证明 可信信道 模型检测 NuSMV
年,卷(期) 2012,(2) 所属期刊栏目 计算机与信息技术
研究方向 页码范围 8-15
页数 分类号 TP393.08
字数 7993字 语种 中文
DOI 10.3969/j.issn.1673-0291.2012.02.002
五维指标
作者信息
序号 姓名 单位 发文数 被引次数 H指数 G指数
1 常晓林 北京交通大学计算机与信息技术学院 11 13 2.0 3.0
2 秦英 北京交通大学计算机与信息技术学院 1 4 1.0 1.0
3 邢彬 北京交通大学计算机与信息技术学院 4 20 3.0 4.0
4 左向晖 北京交通大学计算机与信息技术学院 1 4 1.0 1.0
传播情况
(/次)
(/年)
引文网络
引文网络
二级参考文献  (0)
共引文献  (0)
参考文献  (2)
节点文献
引证文献  (4)
同被引文献  (1)
二级引证文献  (4)
1983(1)
  • 参考文献(1)
  • 二级参考文献(0)
1997(1)
  • 参考文献(1)
  • 二级参考文献(0)
2012(1)
  • 参考文献(0)
  • 二级参考文献(0)
  • 引证文献(1)
  • 二级引证文献(0)
2012(1)
  • 引证文献(1)
  • 二级引证文献(0)
2015(1)
  • 引证文献(1)
  • 二级引证文献(0)
2016(1)
  • 引证文献(1)
  • 二级引证文献(0)
2017(2)
  • 引证文献(1)
  • 二级引证文献(1)
2018(2)
  • 引证文献(0)
  • 二级引证文献(2)
2019(1)
  • 引证文献(0)
  • 二级引证文献(1)
研究主题发展历程
节点文献
SSH
TCG远程证明
可信信道
模型检测
NuSMV
研究起点
研究来源
研究分支
研究去脉
引文网络交叉学科
相关学者/机构
期刊影响力
北京交通大学学报
双月刊
1673-0291
11-5258/U
大16开
北京西直门外上园村3号
1975
chi
出版文献量(篇)
3626
总下载数(次)
7
总被引数(次)
38401
论文1v1指导