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

Automatic Analysis on Authentication of SSHV2 Protocol in Computational Model

作　　者：牛乐园[1] 杨伊彤 王德军[1] 孟博[1] 

机构地区：[1]中南民族大学计算机科学学院,武汉430074

出　　处：《计算机工程》2015年第10期148-154,共7页Computer Engineering

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

摘　　要：安全内壳(SSH)协议可以实现本地主机与远程节点的网络文件传输、远程登录、远程命令执行及其他应用程序的安全执行,其在保障网络安全方面发挥着重要作用。针对第二代安全内壳(SSHV2)协议的安全性进行研究,介绍SSHV2协议体系结构,解析出认证消息的消息结构,基于计算模型应用概率多项式进程演算,即Blanchet演算,对SSHV2安全协议进行形式化建模,并应用安全协议自动化分析工具CryptoVerif分析其认证性,结果表明,在计算模型下SSHV2安全协议具有认证性。Secure Shell（SSH）protocol can ensure the implementation of network file transfer between the local host and remote host,remote login,executing commands remotely and safe execution of other applications.It plays an important role in the protecting network security.This paper studies the security of the protocol.The main content of this article is the automated analysis of Secure Shell Version2（SSHV2）protocol.This paper introduces the architecture of SSH protocol and gets the message terms by analyzing the authentication message flow of SSHV2 protocol.Based on computational model and application Blanchet calculus to give the formal model of SSHV2 security protocol,and analyzes the protocol＇s certification by applying the security protocol automatic analysis tool CryptoVerif,shows that SSHV2 security protocol has authentication under the computational model.

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

分 类 号：TP915.04[自动化与计算机技术]