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

作     者：常晓林 秦英 邢彬 左向晖 CHANG Xiaolin;QIN Ying;XING Bin;ZUO Xianghui

作者机构：北京交通大学计算机与信息技术学院北京100044 

基　　金：中央高校基本科研业务费专项基金资助(2009JBM017 2010YJS024) 

出 版 物：《北京交通大学学报》 (JOURNAL OF BEIJING JIAOTONG UNIVERSITY)

年 卷 期：2012年第36卷第2期

页      码：8-15页

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

主 题 词：SSH TCG远程证明 可信信道 模型检测 NuSMV 

学科分类：0810[工学-土木类] 0839[0839] 08[工学] 0805[工学-能源动力学] 0812[工学-测绘类] 

D　O　I：10.3969/j.issn.1673-0291.2012.02.002

馆 藏 号：203663352...