SSH可信信道安全属性的形式化验证
常晓林
秦英
邢彬
左向晖
1.北京交通大学计算机与信息技术学院,北京,1000442.北京交通大学计算机与信息技术学院,北京,1000443.北京交通大学计算机与信息技术学院,北京,1000444.北京交通大学计算机与信息技术学院,北京,100044
摘要：可信信道是一个与终端的系统平台状态信息安全绑定的安全信道.现有的关于可信信道的研究工作都没有从理论上对所设计的可信信道的安全属性进行分析.本文首先提出一个基于SSH安全信道协议的可信信道协议,然后利用形式化模型检测器NuSMV分析该协议的安全属性,最后基于检测器执行轨迹所构成的反例,提出了一个强壮的SSH可信信道协议.本文提出的建模和验证方法具有通用性,可用于分析其他基于安全信道协议的可信信道协议的安全属性.
关键词：SSHTCG远程证明可信信道模型检测NuSMV
分类号：TP393.08(计算技术、计算机技术)
资助基金：中央高校基本科研业务费专项基金资助(2009JBM017)中央高校基本科研业务费专项基金资助(2010YJS024)
论文发表日期：2012-01-01
在线出版日期：2025-08-15（本平台首次上网日期，不代表文献的发表时间）
页数：8( 8-15 )
英文信息