牛乐园，杨伊彤，王德军，孟 博

（中南民族大学计算机科学学院，武汉 430074）

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

牛乐园，杨伊彤，王德军，孟 博

（中南民族大学计算机科学学院，武汉 430074）

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

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

1 概述

远程登录所使用的安全内壳（Secure Shell，SSH）［1］协议可以保证在不可信网络中的安全远程登录，目前有很多网络服务都支持该协议。SSH协议中敏感数据都是经过加密来传输，可以预防中间人窃取信道中传输的私密信息。

Tatum Ylonen在1995年发布SSH协议作为第1个版本规范SSHV 1，2006年提出SSH的第2个版本规范SSHV2。SSHV1数据流程中的加密算法主要是数据加密标准（Data Encryption Standard，DES）、三重数据加密标准（Triple DES，3DES）等对称加密算法，非对称加密算法用来实现数据流程中加密算法的密钥交换。在后续使用中发现SSHV1

使用保证数据完整性的循环冗余校验码（Cyclic Redundancy Check，CRC）存在漏洞，因此发布第2版本SSHV2，它用数字签名算法（Digital Signature Algorithm，DSA）和Diffie-Hellman（DH）算法代替RSA算法完成传输协议中的密钥交换，用Hash消息验证码（Hash-based Message Authentication Code，HMAC）来保证数据完整。作为对SSHV 1的补充，SSHV2增加了高级加密标准（Advanced Encryption Standard，AES）和Twofish等对称加密算法。OpenSSH是最常见的SSH协议实现，它支持SSHV2和安全文件传输协议（Secure File Transfer Protocol，SFTP）。本文着重研究SSHV2协议的认证性。

2 SSHV2协议结构

SSHV2协议是保证数据在应用层和传输层上安全传输的安全协议，主要由以下3个部分构成：

（1）传输层协议［2］提供服务端认证的认证性，保证数据传输保密性和信息内容的完整传输等。

（2）用户认证协议［3］主要是保证客户端的身份认证。

（3）连接协议［4］提供交互式登录会话，远程执行命令，转发TCP/IP和X 11连接，在连接协议中将所有加密通道多路复用到一个加密通道。

3 SSHV2消息流程

在SSHV2数据流程中，为保证SSHV2的安全传输［5］，服务端与客户端的消息交互有如下4个阶段：

（1）协议版本信息协商。SSH目前包括SSHV1和SSHV2 2个版本，客户端和服务端发送消息商定版本，文章默认使用SSHV2版本。

（2）密钥和算法协商阶段。SSHV2支持多种加密算法，客户端和服务端根据自身所支持的算法信息协商出最终使用的算法。

（3）密钥交换阶段。客户端和服务端通过密钥交换信息来协商新密钥，密钥交换算法为Diffie-Hellman。

（4）认证阶段。客户端请求身份验证，服务端通过签名信息对客户端进行身份认证。

3.1 SSHV2的密钥协商和密钥交换

SSHV2在传输层协议的消息传输共有9条消息［6］，如图1所示，分别是CtoS版本协商、StoC版本协商、Client算法协商消息SSH-MSG-KEX INIT、Server算法协商消息SSH-MSG-KEXINIT、SSHMSG-KEXDH-GEX-REQUEST密钥交换请求、SSH-MSG-KEXDH-GEX-GROUP密钥交换参数回应、SSH-MSG-KEXDH-GEX-INIT密钥交换初始化、SSH-MSG-KEXDH-GEX-REPLY密钥交换回应、SSH-MSG-NEWKEYS确认新密钥。

图1 SSHV2的密钥协商和密钥交换

3.1.1 版本协商

首先服务端通过端口 22建立连接。客户端（Client，简称C）向服务端（Server，简称S）发起TCP初始连接请求，连接成功后，C向S发送C所支持的版本信息。

版本协商：Client-----＞Server

消息内容：client-version

S收到C的版本信息后和自身所支持的版本信息进行比较。如果版本一样则使用该版本。如果C支持的最高版本信息比 S所支持的最低版本低，同时S可以支持C的低协议版本，就商定使用低版本，否则版本协商失败。

版本协商：Server-----＞Client

消息内容：server-version

3.1.2 算法协商

版本信息协商成功后进入算法协商阶段。客户端和服务端需要协商的算法包括密钥交换算法、签名算法、加密算法、消息验证码（Message Authentication Code，MAC）算法、压缩算法等。SSHV2密钥协商消息包含的字段如表1所示。

表1 密钥协商消息字段

S和C分别发送算法协商消息给对方，消息中包含自己支持的公钥算法、加密算法列表、MAC算法、压缩算法和cookie信息等。

消息结构：

消息结构：

3.1.3 密钥交换参数

版本协商和算法协商是SSHV 2协议消息传递的基本参数信息，接下来就是密钥交换的信息协商。密钥交换的第一条消息是SSH-MSG-KEXDHGEX-REQUEST，Server向Client发送密钥交换回应消息，这条消息包含2个高精度整数，即大质数P和生成元g。

消息结构：

消息结构：P‖g

3.1.4 密钥交换

密钥交换参数信息结束后就是密钥交换，具体过程如下：C是Client，S是Server，P是一个安全的大素数，g是生成元。Vs是S的识别字符串，Vc是C的识别字符串，Ks是S的public host key，Ic是C的SSH-MSG-KEXINIT消息的payload字符串，Is是S的SSH-MSG-KEXINIT消息的payload字符串。Client生成一个随机数rc（1＜rc＜（P-1）/2），计算e=grcmod P，并发送给Server，P是一个大素数，g是生成元。

消息结构：e

S发送给C的SSH-MSG-KEXDH-GEX-REPLY消息是S对C提供的密钥交换信息的回复。S生成一个随机数rs（1＜rs＜（P-1）/2），并计算f=grsmod P发送给C。S收到e后计算功效密钥shareK=ers，H=hash（VC‖VS‖IC‖IS‖KS‖e‖f‖shareK）（这些消息会依据他们的格式被加密），然后用S的sks（S的服务端私钥Sprivatekey）来对H进行签名生成hash签名serνer-sigture=sign（H，sks），其中，Ks是服务端公钥Spublickey。

消息结构：f‖Ks‖serνer-sigture

C收到消息后首先验证Ks是否是S的密钥（用证书信息或者本地数据库来判断），C也被允许可接收没有被验证的密钥，但是这样做会使协议遭受不安全的主动攻击。然后C通过密钥交换算法计算共享密钥shareK=frc，再计算hash签名H=hash（VC‖VS‖IC‖IS‖KS‖e‖f‖shareK）。在SSH-MSGKEXDH-GEX-REPLY消息中S发送Ks给C，C收到消息后可以用收到的f来计算分享的密钥，同时可以用相同的方式计算签名，并与收到的签名进行对比来验证签名信息。

3.1.5 新密钥的协商

协商新密钥，用于以后消息的加密。该密钥为会话密钥sessionkey，然后用Server的公钥加密，发给Server端。生成会话密钥所包含字段如表2所示，其中，K为共享密钥；H为密钥交换 hash算法；SID为会话标识。文章中选取sessionkey=h（K‖H‖″C″‖sessionid）来计算会话密钥。

表2 sessionkey生成算法

在版本号协商完成后生成新的会话密钥，服务端生成服务端公钥S-P、sessionid发送给客户端。客户端生成会话密钥sessionkey并计算res=sessionid⊕sessionkey，然后用服务端公钥S-P加密res发送给服务端。

消息结构：res

服务端用服务端私钥S-S对加密消息解密得到res。服务端计算res异或sessionid，得到sessionkey。Server用自己的私钥解密得到sessionkey，此时服务端和客户端都得到了会话密钥sessionkey和会话标

识sessionid，此后SSHV2的数据传输都使用会话密钥进行加密和解密。

3.2 SSHV2的用户认证

在SSHV 2中，服务端对用户的认证是由服务端决定的。首先，服务端向客户端发送自己所支持的认证方法，根据自身情况客户端选择一种或者多种方式进行认证。服务端支持多种认证方式可以使客户端认证操作比较灵活，这样增强了协议的实用性，也为客户端认证增加便利。

SSHV 2协议支持3种用户认证方法：公开密钥认证方法（public key认证），基于口令的认证和基于主机的认证。本文采用的是 public key认证方式。在public认证方式中Client首先发起认证请求，Client向Server发送消息SSH-MSG-USERAUTHREQUEST来请求认证。因为请求的验证方法是public key验证，那么methodname的内容为“public key”，method-sPecific的内容为signature-algorithm，Public key，signature。signature字段内容包括session ID，SSH-MSG-USERAUTH-REQUEST，user name，serνice，“publickey”，TRUE，algorithm name，Public key。

消息结构：username‖servicename‖methodname‖method-specific

Server收到请求验证信息后对Client进行验证，如果验证成功发送消息SSH-MSG-USERAUTH-SUCCESS（不包含参数）消息给客户端，表示对Client的验证成功；如果公钥不合法或者Client提供的签名不合法，那么验证不成功，发回SSH-MSGUSERAUTH-FAILURE消息给Client，表示验证失败。

4 SSHV2协议形式化建模

4.1 Blanchet演算和CryptoVerif建模工具

Blanchet基于PI演算和其他多种演算的思想，提出的概率多项式演算Blanchet演算［7］，主要用来形式化证明安全协议。Blanchet团队开发了基于概率计算模型的自动化证明工具CryptoVerif。该工具用来对安全协议建立模拟化的安全模型，在协议并发运行的情况下可以证明存在主动攻击时协议安全性。这种演算具有概率学语义，所有进程的运行都是多项式时间，协议所发送的消息以位串来表示，演算模型中的密码原语以位串函数序列构成。

在CryptoVerif工具中，形式化方法的证明过程是通过Game序列的多次转换来模拟的［8］，以Blanchet演算的形式给出，证明的最终结果是特定安全属性被攻击成功的概率。协议模型在最初被转换为一个Game原型，初始Game将要进行分析和证明的协议，通过一系列Game转换，把初始Game经过若干次转换而变成一个满足安全属性的最终Game，其中重要的一类转换需要应用密码原语安全性定义。

4.2 Blanchet演算模型建立流程

Blanchet演算模型［9］主要包括类型定义、事件定义、方法定义、通道定义、事件声明、初始化进程描述、客户端进程描述与服务端进程描述。SSHV 2最主要的功能体现在客户端与服务端的消息传递。

4.2.1 协议事件声明

在Blanchet演算［10］中首先声明需要证明的事件。SSHV 2协议的消息流程中最重要的就是认证性和密钥的安全性。认证性包括客户端对服务端的认证和服务端对客户端的认证，安全性是对会话密钥的安全进行认证。

eνent client（χ，y，kχ，Pχ，gχ，gy，krsa）==＞serνer（χ，y，kχ，Pχ，gχ，gy，krsa）表示事件client发生之前事件server一定发生，用来验证客户端认证性［11］。eνent serνerA（ya）==＞clientA（y a）用来验证服务端认证性，模型代码如下：

4.2.2 初始化进程

ClientProcess表示客户端进程，ServerProcess表示服务端进程，！N ClientProcess表示多个ClientProcess进程并发执行，以此来模拟现实协议执行。协议模型初始化进程如下：

4.2.3 客户端进程

客户端的消息流程包括版本协商、算法协商、密钥协商、密钥交换和请求验证。版本协商是协商客户端服务端可以通用的版本，一般是客户端和服务端都支持的较高版本，在CV中选择Agreementνersion为协商版本，然后对比服务端与客户端的版本信息。算法协商阶段，服务端和客户端都向对方发送自己所支持的算法信息cookie，keχ-algorithms，encalgorithms，mac-algorithms，comPerssion-algorithms，然后以自己所支持的算法来协商共用的加密算法、压缩算法以及m ac算法。密钥协商阶段，客户端生成密钥交换参数minc，dP，maχc通过通道c9发送给服务端。密钥交换阶段，客户端自己生成客户端随机数r-c，用exp函数计算出dh-e，然后通过通道c13发给服务端。同时服务端收到客户端的消息，也会回发一个消息 dh-f-s给客户端，客户端通过通道c16接收到dh-f-s和r-c用以计算客户端的共享密钥clientshareK。客户端通过接收服务端发送的签名消息dh-signature-s和之前收到的信息用check方法进行验证，若验证为真则客户端对服务端验证成功。在此插入事件eνent client（clientνersion，Agreementνersion，clientshareK，P，dh-e，dh-f-s，Pkeyrsa-s）表明验证事件与server事件相对应。客户端对服务端的验证成功后客户端和服务端互发消息商量新密钥sessionkey，并规定此密钥为后续传递消息的加密密钥。clientshareK是在密钥交换阶段客户端计算的共享密钥，clienthash是客户端的消息摘要，sessionid是客户端的会话标识，然后使用方法 hashtokey（keyhash，sessionkeymes）计算这3个参数的hash值为sessionkey，并通过通道c17发送给服务端新密钥信息。密钥协商完成之后Client通过通道c19向Server发送SSH-MSG-USERAUTH-REQUEST认证请求消息，内容包括username，serνicename，methodname，method-sPecific，请求Server验证身份，并在此定义对客户端的验证事件clientA（request-signature）。客户端模型核心代码如下：

4.2.4 服务端进程

服务端进程首先接收客户端进程发送的版本信息，并与自己的版本信息匹配协商得到协商版本Agreementνersion。版本信息协商完成之后接收客户

端所支持的算法信息，并与服务端自身所支持的算法信息比较来选出两边都支持的算法信息发送回客户端，至此算法协商完成。进入密钥协商阶段，首先Server由通道c10接收Client发送的密钥参数信息dhmindhP，dhmaχ，用来计算大质数P和生成元g组合为消息message-DhgrouP发给Client。Server在通道c14中接收到信息message-e并计算共享密钥K=eχP（mesage-e，r-s），hash（keyhash，messagedhhash）生成消息hash摘要hashserνer，最后生成用以进行Server验证的签名信息dh-signature发送给Client来对Server进行验证，并建立验证事件eνent serνer（serνerνersion，messageνersion-c，shareK，dhP，mesagee，dh-f，Pkeyrsa）。Server收到Client的验证请求后对Client进行验证，由通道c20接收Client发来的验证消息。首先匹配收到的session-id是否存在于服务端，若存在则继续下一步验证。用check方法检查concatauthserνer（sessionids，SSH-MSG-USERAUTHREQUEST，user-namec，serνice-client，methodnamec，flagt，signalgornamec，cPkey-c）消息段是否是Client发送的数字签名的消息段request-signaturec，若是则验证成功发回SSH-MSG-USERAUTH-SUCCESS消息给Client，否则发回SSH-MSG-USERAUTH-FAILURE消息。在此插入事件eνent serνerA（request-signaturec）来验证客户端。服务端模型核心代码如下：

4.3 Blanchet模型验证结果

首先介绍SSHV2协议并对其数据流程进行分析，使用Blanchet建立模型并自动化分析其安全性和认证性。经过流程跟进并使用自动化证明工具CryptoVerif对SSH模型进行模型建立，经过一系列的Game转换得出分析结果，如图2所示。A ll queries proved表示事件eνent client（χ，y，kχ，Pχ，gχ，gy，krsa）==＞serνer（χ，y，kχ，Pχ，gχ，gy，krsa）结果为proved，推出客户端对服务端认证成功；证明eνent serνerA（ya）==＞clientA（y a）结果为proved，推出服务端对客户端认证成功；query secret sessionkey的证明结果为proved，推出SSHV2协议的会话密钥具有安全性［12］。以上结果表明，SSHV2协议具有认证性和安全性。

图2 协议模型分析结果

4.4 SSHV2协议的抗攻击性

SSHV2协议的主要目的是保证数据消息完整地、安全地进行传输，在客户端与服务端传输数据时所遭受的主动攻击也是不可忽视的内容。攻击者可

以通过查找协议的漏洞，利用篡改密钥、冒充发送端等方式实现中间人攻击。最常见的攻击方式是不可信密钥攻击和SSH伪服务端欺骗。

在SSHV2协议密钥交换阶段中，客户端生成sessionkey，通过异或操作后用服务端的公钥加密，然后发给服务端，服务端用自己的私钥对密文解密得到sessionkey，在和客户端通信中会利用收到的hash摘要对收到的消息进行验证。如果客户端接收未验证的密钥，则可能造成信息泄露。未验证的密钥可能由第三方发出，因为服务端公钥在公用信道中都可获得，第三方会伪造一个假sessionkey并用服务端公钥加密然后发给服务端，该密钥被服务端接收后会用来加密传输数据，该数据则会被第三方攻击者截取并解密，得到传输数据，这样就会造成数据泄露。

SSHV 2的用户认证方式为“public key”认证，实现了服务端对客户端的认证。单方面的用户认证机制只保证了对客户端的认证，但是不能保证服务端的可信性，此时就存在SSH伪服务端欺骗攻击。第三方攻击者冒充可信服务端与客户端进行信息交互以达到消息窃取的目的。为了防止类似的伪服务端欺骗攻击，SSHV2协议不仅实现了对客户端的认证，同时也在密钥交换阶段通过使用自己的私钥对共享密钥和其他消息进行数字签名发送回客户端，客户端通过鉴别数字签名对服务端进行认证，以达到认证服务端，保证数据传输安全性。

5 结束语

为了研究SSHV2协议在应用中的安全性，本文对SSHV2协议的消息流程进行分析。通过对每一步消息流中消息项的研究分析得出SSHV2协议整体的消息结构，最终实现服务端对客户端的验证以及服务端对客户的认证流程分析。基于Blanchet演算将分析的消息流程应用一致性，对服务端认证客户端和客户端认证服务端流程建立模型。协议模型通过协议转换工具转换为CryptoVerif的输入代码sshofcv.cv，使用CryptoVerif对模型进行自动化分析，并证明了SSHV2协议具有认证性。下一步工作将给出SSHV2协议的Java安全代码，并分析其认证性。

［1］ Ylonen T，Lonvick C.The Secure Shell（SSH）Protocol Architecture［S］.RFC 4251，2006.

［2］ Ylonen T，Lonvick C.The Secure Shell（SSH）Transport Layer Protocol［S］.RFC 4253，2006.

［3］ Ylonen T，Lonvick C.The Secure Shell（SSH）Authentication Protocol［S］.RFC 4252，2006.

［4］ Ylonen T，Lonvick C.The Secure Shell（SSH）Connection Protocol［S］.RFC 4254，2006.

［5］ 李延松，江国华.一种改进 SSH协议主机认证方法［J］.电子科技，2013，26（2）：133-136.

［6］ 曹 玮.基于SSH协议的WebShell系统的设计与实现［D］.北京：北京交通大学，2012.

［7］ 唐郑熠，李 祥.Dolev-Yao攻击者模型的形式化描述［J］.计算机工程与科学，2010，32（8）：36-38，45.

［8］ 邵 飞.基于概率进程演算的安全协议自动化分析技术研究［D］.武汉：中南民族大学，2011.

［9］ 朱玉娜.密码协议符号分析方法的计算可靠性研究［D］.郑州：解放军信息工程大学，2008.

［10］ 郑清雄.基于Spi演算的安全协议验证［J］.计算机应用与软件，2011，28（3）：262-264，292.

［11］ 陈 伟，杨伊彤，牛乐园.改进的OAuth2.0协议及其安全性分析［J］.计算机系统应用，2014，23（3）：25-30.

［12］ Xu Xingdong，Niu Leyuan，Meng Bo.Automatic Verification of Security Properties of OAuth 2.0 Protocol with CryptoVerif in Computational Model［J］.Information Technology Journal，2013，12（12）：2273-2285.

编辑顾逸斐

Automatic Analysis on Authentication of SSHV2 Protocol in Computational Model

NIU Leyuan，YANG Yitong，WANG Dejun，MENG Bo

（College of Computer Science，South-Central University for Nationalities，Wuhan 430074，China）

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 Version 2（SSHV2）protocol.This paper introduces the architecture of SSH protocol and gets the message term s 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，show s that SSHV2 security protocol has authentication under the computational model.

Secure Shell Version 2（SSHV2）protocol；security protocol；computational model；authentication；CryptoVerif tool；automatic analysis

牛乐园，杨伊彤，王德军，等.计算模型下的 SSHV2协议认证性自动化分析［J］.计算机工程，2015，41（10）：148-154.

英文引用格式：Niu Leyuan，Yang Yitong，Wang Dejun，et al.Automatic Analysis on Authentication of SSHV2 Protocol in Computational Model［J］.Computer Engineering，2015，41（10）：148-154.

1000-3428（2015）10-0148-07

A

TP915.04

10.3969/j.issn.1000-3428.2015.10.028

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

牛乐园（1990-），女，硕士研究生，主研方向：信息安全；杨伊彤，硕士研究生；王德军，讲师、博士；孟 博（通讯作者），教授、博士后。

2014-10-19

2014-11-22E-mail：mengscuec@gmail.com