SSH可信信道安全属性的形式化验证

• 作者: 左向晖 常晓林 秦英 邢彬
• 来源期刊: 北京交通大学学报
• 学科: 工学
• 关键词: SSH TCG远程证明 可信信道 模型检测 NuSMV
• 年，卷（期）: 2012,（2）
• 所属期刊栏目: 计算机与信息技术
• 页码范围: 8-15
• 分类号: TP393.08
• 字数: 7993字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-0291.2012.02.002

摘要

可信信道是一个与终端的系统平台状态信息安全绑定的安全信道.现有的关于可信信道的研究工作都没有从理论上对所设计的可信信道的安全属性进行分析.本文首先提出一个基于SSH安全信道协议的可信信道协议,然后利用形式化模型检测器NuSMV分析该协议的安全属性,最后基于检测器执行轨迹所构成的反例,提出了一个强壮的SSH可信信道协议.本文提出的建模和验证方法具有通用性,可用于分析其他基于安全信道协议的可信信道协议的安全属性.

作者信息

序号	姓名	单位	发文数	被引次数	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