計算模型下的SSHV2協(xié)議認證性自動化分析

牛樂園，楊伊彤，王德軍，孟 博

（中南民族大學(xué)計算機科學(xué)學(xué)院，武漢 430074）

計算模型下的SSHV2協(xié)議認證性自動化分析

牛樂園，楊伊彤，王德軍，孟 博

（中南民族大學(xué)計算機科學(xué)學(xué)院，武漢 430074）

安全內(nèi)殼（SSH）協(xié)議可以實現(xiàn)本地主機與遠程節(jié)點的網(wǎng)絡(luò)文件傳輸、遠程登錄、遠程命令執(zhí)行及其他應(yīng)用程序的安全執(zhí)行，其在保障網(wǎng)絡(luò)安全方面發(fā)揮著重要作用。針對第二代安全內(nèi)殼（SSHV2）協(xié)議的安全性進行研究，介紹SSHV2協(xié)議體系結(jié)構(gòu)，解析出認證消息的消息結(jié)構(gòu)，基于計算模型應(yīng)用概率多項式進程演算，即Blanchet演算，對SSHV2安全協(xié)議進行形式化建模，并應(yīng)用安全協(xié)議自動化分析工具CryptoVerif分析其認證性，結(jié)果表明，在計算模型下SSHV2安全協(xié)議具有認證性。

第二代安全內(nèi)殼協(xié)議；安全協(xié)議；計算模型；認證性；CryptoVerif工具；自動化分析

1 概述

遠程登錄所使用的安全內(nèi)殼（Secure Shell，SSH）［1］協(xié)議可以保證在不可信網(wǎng)絡(luò)中的安全遠程登錄，目前有很多網(wǎng)絡(luò)服務(wù)都支持該協(xié)議。SSH協(xié)議中敏感數(shù)據(jù)都是經(jīng)過加密來傳輸，可以預(yù)防中間人竊取信道中傳輸?shù)乃矫苄畔ⅰ?/p>

Tatum Ylonen在1995年發(fā)布SSH協(xié)議作為第1個版本規(guī)范SSHV 1，2006年提出SSH的第2個版本規(guī)范SSHV2。SSHV1數(shù)據(jù)流程中的加密算法主要是數(shù)據(jù)加密標(biāo)準（Data Encryption Standard，DES）、三重數(shù)據(jù)加密標(biāo)準（Triple DES，3DES）等對稱加密算法，非對稱加密算法用來實現(xiàn)數(shù)據(jù)流程中加密算法的密鑰交換。在后續(xù)使用中發(fā)現(xiàn)SSHV1

使用保證數(shù)據(jù)完整性的循環(huán)冗余校驗碼（Cyclic Redundancy Check，CRC）存在漏洞，因此發(fā)布第2版本SSHV2，它用數(shù)字簽名算法（Digital Signature Algorithm，DSA）和Diffie-Hellman（DH）算法代替RSA算法完成傳輸協(xié)議中的密鑰交換，用Hash消息驗證碼（Hash-based Message Authentication Code，HMAC）來保證數(shù)據(jù)完整。作為對SSHV 1的補充，SSHV2增加了高級加密標(biāo)準（Advanced Encryption Standard，AES）和Twofish等對稱加密算法。OpenSSH是最常見的SSH協(xié)議實現(xiàn)，它支持SSHV2和安全文件傳輸協(xié)議（Secure File Transfer Protocol，SFTP）。本文著重研究SSHV2協(xié)議的認證性。

2 SSHV2協(xié)議結(jié)構(gòu)

SSHV2協(xié)議是保證數(shù)據(jù)在應(yīng)用層和傳輸層上安全傳輸?shù)陌踩珔f(xié)議，主要由以下3個部分構(gòu)成：

（1）傳輸層協(xié)議［2］提供服務(wù)端認證的認證性，保證數(shù)據(jù)傳輸保密性和信息內(nèi)容的完整傳輸?shù)取?/p>

（2）用戶認證協(xié)議［3］主要是保證客戶端的身份認證。

（3）連接協(xié)議［4］提供交互式登錄會話，遠程執(zhí)行命令，轉(zhuǎn)發(fā)TCP/IP和X 11連接，在連接協(xié)議中將所有加密通道多路復(fù)用到一個加密通道。

3 SSHV2消息流程

在SSHV2數(shù)據(jù)流程中，為保證SSHV2的安全傳輸［5］，服務(wù)端與客戶端的消息交互有如下4個階段：

（1）協(xié)議版本信息協(xié)商。SSH目前包括SSHV1和SSHV2 2個版本，客戶端和服務(wù)端發(fā)送消息商定版本，文章默認使用SSHV2版本。

（2）密鑰和算法協(xié)商階段。SSHV2支持多種加密算法，客戶端和服務(wù)端根據(jù)自身所支持的算法信息協(xié)商出最終使用的算法。

（3）密鑰交換階段。客戶端和服務(wù)端通過密鑰交換信息來協(xié)商新密鑰，密鑰交換算法為Diffie-Hellman。

（4）認證階段?？蛻舳苏埱笊矸蒡炞C，服務(wù)端通過簽名信息對客戶端進行身份認證。

3.1 SSHV2的密鑰協(xié)商和密鑰交換

SSHV2在傳輸層協(xié)議的消息傳輸共有9條消息［6］，如圖1所示，分別是CtoS版本協(xié)商、StoC版本協(xié)商、Client算法協(xié)商消息SSH-MSG-KEX INIT、Server算法協(xié)商消息SSH-MSG-KEXINIT、SSHMSG-KEXDH-GEX-REQUEST密鑰交換請求、SSH-MSG-KEXDH-GEX-GROUP密鑰交換參數(shù)回應(yīng)、SSH-MSG-KEXDH-GEX-INIT密鑰交換初始化、SSH-MSG-KEXDH-GEX-REPLY密鑰交換回應(yīng)、SSH-MSG-NEWKEYS確認新密鑰。

圖1 SSHV2的密鑰協(xié)商和密鑰交換

3.1.1 版本協(xié)商

首先服務(wù)端通過端口 22建立連接。客戶端（Client，簡稱C）向服務(wù)端（Server，簡稱S）發(fā)起TCP初始連接請求，連接成功后，C向S發(fā)送C所支持的版本信息。

版本協(xié)商：Client-----＞Server

消息內(nèi)容：client-version

S收到C的版本信息后和自身所支持的版本信息進行比較。如果版本一樣則使用該版本。如果C支持的最高版本信息比 S所支持的最低版本低，同時S可以支持C的低協(xié)議版本，就商定使用低版本，否則版本協(xié)商失敗。

版本協(xié)商：Server-----＞Client

消息內(nèi)容：server-version

3.1.2 算法協(xié)商

版本信息協(xié)商成功后進入算法協(xié)商階段?？蛻舳撕头?wù)端需要協(xié)商的算法包括密鑰交換算法、簽名算法、加密算法、消息驗證碼（Message Authentication Code，MAC）算法、壓縮算法等。SSHV2密鑰協(xié)商消息包含的字段如表1所示。

表1 密鑰協(xié)商消息字段

S和C分別發(fā)送算法協(xié)商消息給對方，消息中包含自己支持的公鑰算法、加密算法列表、MAC算法、壓縮算法和cookie信息等。

消息結(jié)構(gòu)：

消息結(jié)構(gòu)：

3.1.3 密鑰交換參數(shù)

版本協(xié)商和算法協(xié)商是SSHV 2協(xié)議消息傳遞的基本參數(shù)信息，接下來就是密鑰交換的信息協(xié)商。密鑰交換的第一條消息是SSH-MSG-KEXDHGEX-REQUEST，Server向Client發(fā)送密鑰交換回應(yīng)消息，這條消息包含2個高精度整數(shù)，即大質(zhì)數(shù)P和生成元g。

消息結(jié)構(gòu)：

消息結(jié)構(gòu)：P‖g

3.1.4 密鑰交換

密鑰交換參數(shù)信息結(jié)束后就是密鑰交換，具體過程如下：C是Client，S是Server，P是一個安全的大素數(shù)，g是生成元。Vs是S的識別字符串，Vc是C的識別字符串，Ks是S的public host key，Ic是C的SSH-MSG-KEXINIT消息的payload字符串，Is是S的SSH-MSG-KEXINIT消息的payload字符串。Client生成一個隨機數(shù)rc（1＜rc＜（P-1）/2），計算e=grcmod P，并發(fā)送給Server，P是一個大素數(shù)，g是生成元。

消息結(jié)構(gòu)：e

S發(fā)送給C的SSH-MSG-KEXDH-GEX-REPLY消息是S對C提供的密鑰交換信息的回復(fù)。S生成一個隨機數(shù)rs（1＜rs＜（P-1）/2），并計算f=grsmod P發(fā)送給C。S收到e后計算功效密鑰shareK=ers，H=hash（VC‖VS‖IC‖IS‖KS‖e‖f‖shareK）（這些消息會依據(jù)他們的格式被加密），然后用S的sks（S的服務(wù)端私鑰Sprivatekey）來對H進行簽名生成hash簽名serνer-sigture=sign（H，sks），其中，Ks是服務(wù)端公鑰Spublickey。

消息結(jié)構(gòu)：f‖Ks‖serνer-sigture

C收到消息后首先驗證Ks是否是S的密鑰（用證書信息或者本地數(shù)據(jù)庫來判斷），C也被允許可接收沒有被驗證的密鑰，但是這樣做會使協(xié)議遭受不安全的主動攻擊。然后C通過密鑰交換算法計算共享密鑰shareK=frc，再計算hash簽名H=hash（VC‖VS‖IC‖IS‖KS‖e‖f‖shareK）。在SSH-MSGKEXDH-GEX-REPLY消息中S發(fā)送Ks給C，C收到消息后可以用收到的f來計算分享的密鑰，同時可以用相同的方式計算簽名，并與收到的簽名進行對比來驗證簽名信息。

3.1.5 新密鑰的協(xié)商

協(xié)商新密鑰，用于以后消息的加密。該密鑰為會話密鑰sessionkey，然后用Server的公鑰加密，發(fā)給Server端。生成會話密鑰所包含字段如表2所示，其中，K為共享密鑰；H為密鑰交換 hash算法；SID為會話標(biāo)識。文章中選取sessionkey=h（K‖H‖″C″‖sessionid）來計算會話密鑰。

表2 sessionkey生成算法

在版本號協(xié)商完成后生成新的會話密鑰，服務(wù)端生成服務(wù)端公鑰S-P、sessionid發(fā)送給客戶端?？蛻舳松蓵捗荑€sessionkey并計算res=sessionid⊕sessionkey，然后用服務(wù)端公鑰S-P加密res發(fā)送給服務(wù)端。

消息結(jié)構(gòu)：res

服務(wù)端用服務(wù)端私鑰S-S對加密消息解密得到res。服務(wù)端計算res異或sessionid，得到sessionkey。Server用自己的私鑰解密得到sessionkey，此時服務(wù)端和客戶端都得到了會話密鑰sessionkey和會話標(biāo)

識sessionid，此后SSHV2的數(shù)據(jù)傳輸都使用會話密鑰進行加密和解密。

3.2 SSHV2的用戶認證

在SSHV 2中，服務(wù)端對用戶的認證是由服務(wù)端決定的。首先，服務(wù)端向客戶端發(fā)送自己所支持的認證方法，根據(jù)自身情況客戶端選擇一種或者多種方式進行認證。服務(wù)端支持多種認證方式可以使客戶端認證操作比較靈活，這樣增強了協(xié)議的實用性，也為客戶端認證增加便利。

SSHV 2協(xié)議支持3種用戶認證方法：公開密鑰認證方法（public key認證），基于口令的認證和基于主機的認證。本文采用的是 public key認證方式。在public認證方式中Client首先發(fā)起認證請求，Client向Server發(fā)送消息SSH-MSG-USERAUTHREQUEST來請求認證。因為請求的驗證方法是public key驗證，那么methodname的內(nèi)容為“public key”，method-sPecific的內(nèi)容為signature-algorithm，Public key，signature。signature字段內(nèi)容包括session ID，SSH-MSG-USERAUTH-REQUEST，user name，serνice，“publickey”，TRUE，algorithm name，Public key。

消息結(jié)構(gòu)：username‖servicename‖methodname‖method-specific

Server收到請求驗證信息后對Client進行驗證，如果驗證成功發(fā)送消息SSH-MSG-USERAUTH-SUCCESS（不包含參數(shù)）消息給客戶端，表示對Client的驗證成功；如果公鑰不合法或者Client提供的簽名不合法，那么驗證不成功，發(fā)回SSH-MSGUSERAUTH-FAILURE消息給Client，表示驗證失敗。

4 SSHV2協(xié)議形式化建模

4.1 Blanchet演算和CryptoVerif建模工具

Blanchet基于PI演算和其他多種演算的思想，提出的概率多項式演算Blanchet演算［7］，主要用來形式化證明安全協(xié)議。Blanchet團隊開發(fā)了基于概率計算模型的自動化證明工具CryptoVerif。該工具用來對安全協(xié)議建立模擬化的安全模型，在協(xié)議并發(fā)運行的情況下可以證明存在主動攻擊時協(xié)議安全性。這種演算具有概率學(xué)語義，所有進程的運行都是多項式時間，協(xié)議所發(fā)送的消息以位串來表示，演算模型中的密碼原語以位串函數(shù)序列構(gòu)成。

在CryptoVerif工具中，形式化方法的證明過程是通過Game序列的多次轉(zhuǎn)換來模擬的［8］，以Blanchet演算的形式給出，證明的最終結(jié)果是特定安全屬性被攻擊成功的概率。協(xié)議模型在最初被轉(zhuǎn)換為一個Game原型，初始Game將要進行分析和證明的協(xié)議，通過一系列Game轉(zhuǎn)換，把初始Game經(jīng)過若干次轉(zhuǎn)換而變成一個滿足安全屬性的最終Game，其中重要的一類轉(zhuǎn)換需要應(yīng)用密碼原語安全性定義。

4.2 Blanchet演算模型建立流程

Blanchet演算模型［9］主要包括類型定義、事件定義、方法定義、通道定義、事件聲明、初始化進程描述、客戶端進程描述與服務(wù)端進程描述。SSHV 2最主要的功能體現(xiàn)在客戶端與服務(wù)端的消息傳遞。

4.2.1 協(xié)議事件聲明

在Blanchet演算［10］中首先聲明需要證明的事件。SSHV 2協(xié)議的消息流程中最重要的就是認證性和密鑰的安全性。認證性包括客戶端對服務(wù)端的認證和服務(wù)端對客戶端的認證，安全性是對會話密鑰的安全進行認證。

eνent client（χ，y，kχ，Pχ，gχ，gy，krsa）==＞serνer（χ，y，kχ，Pχ，gχ，gy，krsa）表示事件client發(fā)生之前事件server一定發(fā)生，用來驗證客戶端認證性［11］。eνent serνerA（ya）==＞clientA（y a）用來驗證服務(wù)端認證性，模型代碼如下：

4.2.2 初始化進程

ClientProcess表示客戶端進程，ServerProcess表示服務(wù)端進程，！N ClientProcess表示多個ClientProcess進程并發(fā)執(zhí)行，以此來模擬現(xiàn)實協(xié)議執(zhí)行。協(xié)議模型初始化進程如下：

4.2.3 客戶端進程

客戶端的消息流程包括版本協(xié)商、算法協(xié)商、密鑰協(xié)商、密鑰交換和請求驗證。版本協(xié)商是協(xié)商客戶端服務(wù)端可以通用的版本，一般是客戶端和服務(wù)端都支持的較高版本，在CV中選擇Agreementνersion為協(xié)商版本，然后對比服務(wù)端與客戶端的版本信息。算法協(xié)商階段，服務(wù)端和客戶端都向?qū)Ψ桨l(fā)送自己所支持的算法信息cookie，keχ-algorithms，encalgorithms，mac-algorithms，comPerssion-algorithms，然后以自己所支持的算法來協(xié)商共用的加密算法、壓縮算法以及m ac算法。密鑰協(xié)商階段，客戶端生成密鑰交換參數(shù)minc，dP，maχc通過通道c9發(fā)送給服務(wù)端。密鑰交換階段，客戶端自己生成客戶端隨機數(shù)r-c，用exp函數(shù)計算出dh-e，然后通過通道c13發(fā)給服務(wù)端。同時服務(wù)端收到客戶端的消息，也會回發(fā)一個消息 dh-f-s給客戶端，客戶端通過通道c16接收到dh-f-s和r-c用以計算客戶端的共享密鑰clientshareK。客戶端通過接收服務(wù)端發(fā)送的簽名消息dh-signature-s和之前收到的信息用check方法進行驗證，若驗證為真則客戶端對服務(wù)端驗證成功。在此插入事件eνent client（clientνersion，Agreementνersion，clientshareK，P，dh-e，dh-f-s，Pkeyrsa-s）表明驗證事件與server事件相對應(yīng)?？蛻舳藢Ψ?wù)端的驗證成功后客戶端和服務(wù)端互發(fā)消息商量新密鑰sessionkey，并規(guī)定此密鑰為后續(xù)傳遞消息的加密密鑰。clientshareK是在密鑰交換階段客戶端計算的共享密鑰，clienthash是客戶端的消息摘要，sessionid是客戶端的會話標(biāo)識，然后使用方法 hashtokey（keyhash，sessionkeymes）計算這3個參數(shù)的hash值為sessionkey，并通過通道c17發(fā)送給服務(wù)端新密鑰信息。密鑰協(xié)商完成之后Client通過通道c19向Server發(fā)送SSH-MSG-USERAUTH-REQUEST認證請求消息，內(nèi)容包括username，serνicename，methodname，method-sPecific，請求Server驗證身份，并在此定義對客戶端的驗證事件clientA（request-signature）。客戶端模型核心代碼如下：

4.2.4 服務(wù)端進程

服務(wù)端進程首先接收客戶端進程發(fā)送的版本信息，并與自己的版本信息匹配協(xié)商得到協(xié)商版本Agreementνersion。版本信息協(xié)商完成之后接收客戶

端所支持的算法信息，并與服務(wù)端自身所支持的算法信息比較來選出兩邊都支持的算法信息發(fā)送回客戶端，至此算法協(xié)商完成。進入密鑰協(xié)商階段，首先Server由通道c10接收Client發(fā)送的密鑰參數(shù)信息dhmindhP，dhmaχ，用來計算大質(zhì)數(shù)P和生成元g組合為消息message-DhgrouP發(fā)給Client。Server在通道c14中接收到信息message-e并計算共享密鑰K=eχP（mesage-e，r-s），hash（keyhash，messagedhhash）生成消息hash摘要hashserνer，最后生成用以進行Server驗證的簽名信息dh-signature發(fā)送給Client來對Server進行驗證，并建立驗證事件eνent serνer（serνerνersion，messageνersion-c，shareK，dhP，mesagee，dh-f，Pkeyrsa）。Server收到Client的驗證請求后對Client進行驗證，由通道c20接收Client發(fā)來的驗證消息。首先匹配收到的session-id是否存在于服務(wù)端，若存在則繼續(xù)下一步驗證。用check方法檢查concatauthserνer（sessionids，SSH-MSG-USERAUTHREQUEST，user-namec，serνice-client，methodnamec，flagt，signalgornamec，cPkey-c）消息段是否是Client發(fā)送的數(shù)字簽名的消息段request-signaturec，若是則驗證成功發(fā)回SSH-MSG-USERAUTH-SUCCESS消息給Client，否則發(fā)回SSH-MSG-USERAUTH-FAILURE消息。在此插入事件eνent serνerA（request-signaturec）來驗證客戶端。服務(wù)端模型核心代碼如下：

4.3 Blanchet模型驗證結(jié)果

首先介紹SSHV2協(xié)議并對其數(shù)據(jù)流程進行分析，使用Blanchet建立模型并自動化分析其安全性和認證性。經(jīng)過流程跟進并使用自動化證明工具CryptoVerif對SSH模型進行模型建立，經(jīng)過一系列的Game轉(zhuǎn)換得出分析結(jié)果，如圖2所示。A ll queries proved表示事件eνent client（χ，y，kχ，Pχ，gχ，gy，krsa）==＞serνer（χ，y，kχ，Pχ，gχ，gy，krsa）結(jié)果為proved，推出客戶端對服務(wù)端認證成功；證明eνent serνerA（ya）==＞clientA（y a）結(jié)果為proved，推出服務(wù)端對客戶端認證成功；query secret sessionkey的證明結(jié)果為proved，推出SSHV2協(xié)議的會話密鑰具有安全性［12］。以上結(jié)果表明，SSHV2協(xié)議具有認證性和安全性。

圖2 協(xié)議模型分析結(jié)果

4.4 SSHV2協(xié)議的抗攻擊性

SSHV2協(xié)議的主要目的是保證數(shù)據(jù)消息完整地、安全地進行傳輸，在客戶端與服務(wù)端傳輸數(shù)據(jù)時所遭受的主動攻擊也是不可忽視的內(nèi)容。攻擊者可

以通過查找協(xié)議的漏洞，利用篡改密鑰、冒充發(fā)送端等方式實現(xiàn)中間人攻擊。最常見的攻擊方式是不可信密鑰攻擊和SSH偽服務(wù)端欺騙。

在SSHV2協(xié)議密鑰交換階段中，客戶端生成sessionkey，通過異或操作后用服務(wù)端的公鑰加密，然后發(fā)給服務(wù)端，服務(wù)端用自己的私鑰對密文解密得到sessionkey，在和客戶端通信中會利用收到的hash摘要對收到的消息進行驗證。如果客戶端接收未驗證的密鑰，則可能造成信息泄露。未驗證的密鑰可能由第三方發(fā)出，因為服務(wù)端公鑰在公用信道中都可獲得，第三方會偽造一個假sessionkey并用服務(wù)端公鑰加密然后發(fā)給服務(wù)端，該密鑰被服務(wù)端接收后會用來加密傳輸數(shù)據(jù)，該數(shù)據(jù)則會被第三方攻擊者截取并解密，得到傳輸數(shù)據(jù)，這樣就會造成數(shù)據(jù)泄露。

SSHV 2的用戶認證方式為“public key”認證，實現(xiàn)了服務(wù)端對客戶端的認證。單方面的用戶認證機制只保證了對客戶端的認證，但是不能保證服務(wù)端的可信性，此時就存在SSH偽服務(wù)端欺騙攻擊。第三方攻擊者冒充可信服務(wù)端與客戶端進行信息交互以達到消息竊取的目的。為了防止類似的偽服務(wù)端欺騙攻擊，SSHV2協(xié)議不僅實現(xiàn)了對客戶端的認證，同時也在密鑰交換階段通過使用自己的私鑰對共享密鑰和其他消息進行數(shù)字簽名發(fā)送回客戶端，客戶端通過鑒別數(shù)字簽名對服務(wù)端進行認證，以達到認證服務(wù)端，保證數(shù)據(jù)傳輸安全性。

5 結(jié)束語

為了研究SSHV2協(xié)議在應(yīng)用中的安全性，本文對SSHV2協(xié)議的消息流程進行分析。通過對每一步消息流中消息項的研究分析得出SSHV2協(xié)議整體的消息結(jié)構(gòu)，最終實現(xiàn)服務(wù)端對客戶端的驗證以及服務(wù)端對客戶的認證流程分析?；贐lanchet演算將分析的消息流程應(yīng)用一致性，對服務(wù)端認證客戶端和客戶端認證服務(wù)端流程建立模型。協(xié)議模型通過協(xié)議轉(zhuǎn)換工具轉(zhuǎn)換為CryptoVerif的輸入代碼sshofcv.cv，使用CryptoVerif對模型進行自動化分析，并證明了SSHV2協(xié)議具有認證性。下一步工作將給出SSHV2協(xié)議的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協(xié)議主機認證方法［J］.電子科技，2013，26（2）：133-136.

［6］ 曹 瑋.基于SSH協(xié)議的WebShell系統(tǒng)的設(shè)計與實現(xiàn)［D］.北京：北京交通大學(xué)，2012.

［7］ 唐鄭熠，李 祥.Dolev-Yao攻擊者模型的形式化描述［J］.計算機工程與科學(xué)，2010，32（8）：36-38，45.

［8］ 邵 飛.基于概率進程演算的安全協(xié)議自動化分析技術(shù)研究［D］.武漢：中南民族大學(xué)，2011.

［9］ 朱玉娜.密碼協(xié)議符號分析方法的計算可靠性研究［D］.鄭州：解放軍信息工程大學(xué)，2008.

［10］ 鄭清雄.基于Spi演算的安全協(xié)議驗證［J］.計算機應(yīng)用與軟件，2011，28（3）：262-264，292.

［11］ 陳 偉，楊伊彤，牛樂園.改進的OAuth2.0協(xié)議及其安全性分析［J］.計算機系統(tǒng)應(yīng)用，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協(xié)議認證性自動化分析［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

湖北省自然科學(xué)基金資助項目“安全協(xié)議代碼的安全性自動化驗證及軟件工具開發(fā)”（2014CFB249）；湖北省自然科學(xué)基金資助項目“有限射影幾何方法研究高緯線性碼的漢明重量”（2014CFB440）；國家民族事務(wù)委員會自然科學(xué)基金資助項目“面向位置服務(wù)的隱私保護理論與方法研究”（12ZNZ009）。

牛樂園（1990-），女，碩士研究生，主研方向：信息安全；楊伊彤，碩士研究生；王德軍，講師、博士；孟 博（通訊作者），教授、博士后。

2014-10-19

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