计算模型下的SSHV2协议认证性自动化分析

作     者：牛乐园 杨伊彤 王德军 孟博 NIU Leyuan;YANG Yitong;WANG Dejun;MENG Bo

作者机构：中南民族大学计算机科学学院武汉430074 

出 版 物：《计算机工程》 (Computer Engineering)

年 卷 期：2015年第41卷第10期

页      面：148-154页

学科分类：12[管理学] 1201[管理学-管理科学与工程(可授管理学、工学学位)] 08[工学] 

基　　金：湖北省自然科学基金资助项目"安全协议代码的安全性自动化验证及软件工具开发"(2014CFB249) 湖北省自然科学基金资助项目"有限射影几何方法研究高纬线性码的汉明重量"(2014CFB440) 国家民族事务委员会自然科学基金资助项目"面向位置服务的隐私保护理论与方法研究"(12ZNZ009) 

主　　题：第二代安全内壳协议 安全协议 计算模型 认证性 CryptoVerif工具 自动化分析 

摘      要：安全内壳(SSH)协议可以实现本地主机与远程节点的网络文件传输、远程登录、远程命令执行及其他应用程序的安全执行,其在保障网络安全方面发挥着重要作用。针对第二代安全内壳(SSHV2)协议的安全性进行研究,介绍SSHV2协议体系结构,解析出认证消息的消息结构,基于计算模型应用概率多项式进程演算,即Blanchet演算,对SSHV2安全协议进行形式化建模,并应用安全协议自动化分析工具CryptoVerif分析其认证性,结果表明,在计算模型下SSHV2安全协议具有认证性。