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

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

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

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

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

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

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

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

1 概述

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

Tatum Ylonen在1995年發(fā)布SSH協(xié)議作為第1個版本規(guī)范SSHV 1，2006年提出SSH的第2個版本規(guī)范SSHV2。SSHV1數(shù)據(jù)流程中的加密算法主要是數(shù)據(jù)加密標準（Data Encryption Standard，DES）、三重數(shù)據(jù)加密標準（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增加了高級加密標準（Advanced Encryption Standard，AES）和Twofish等對稱加密算法。OpenSSH是最常見的SSH協(xié)議實現(xiàn)，它支持SSHV2和安全文件傳輸協(xié)議（Secure File Transfer Protocol，SFTP）。本文著重研究SSHV2協(xié)議的認證性。

2 SSHV2協(xié)議結構

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

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

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

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

3 SSHV2消息流程

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

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

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

（3）密鑰交換階段?？蛻舳撕头斩送ㄟ^密鑰交換信息來協(xié)商新密鑰，密鑰交換算法為Diffie-Hellman。

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

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ù)回應、SSH-MSG-KEXDH-GEX-INIT密鑰交換初始化、SSH-MSG-KEXDH-GEX-REPLY密鑰交換回應、SSH-MSG-NEWKEYS確認新密鑰。

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

3.1.1 版本協(xié)商

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

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

消息內容：client-version

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

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

消息內容：server-version

3.1.2 算法協(xié)商

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

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

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

消息結構：

消息結構：

3.1.3 密鑰交換參數(shù)

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

消息結構：

消息結構：P‖g

3.1.4 密鑰交換

密鑰交換參數(shù)信息結束后就是密鑰交換，具體過程如下：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是生成元。

消息結構：e

S發(fā)送給C的SSH-MSG-KEXDH-GEX-REPLY消息是S對C提供的密鑰交換信息的回復。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的服務端私鑰Sprivatekey）來對H進行簽名生成hash簽名serνer-sigture=sign（H，sks），其中，Ks是服務端公鑰Spublickey。

消息結構：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為會話標識。文章中選取sessionkey=h（K‖H‖″C″‖sessionid）來計算會話密鑰。

表2 sessionkey生成算法

在版本號協(xié)商完成后生成新的會話密鑰，服務端生成服務端公鑰S-P、sessionid發(fā)送給客戶端。客戶端生成會話密鑰sessionkey并計算res=sessionid⊕sessionkey，然后用服務端公鑰S-P加密res發(fā)送給服務端。

消息結構：res

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

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

3.2 SSHV2的用戶認證

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

SSHV 2協(xié)議支持3種用戶認證方法：公開密鑰認證方法（public key認證），基于口令的認證和基于主機的認證。本文采用的是 public key認證方式。在public認證方式中Client首先發(fā)起認證請求，Client向Server發(fā)送消息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進行驗證，如果驗證成功發(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é)議安全性。這種演算具有概率學語義，所有進程的運行都是多項式時間，協(xié)議所發(fā)送的消息以位串來表示，演算模型中的密碼原語以位串函數(shù)序列構成。

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

4.2 Blanchet演算模型建立流程

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

4.2.1 協(xié)議事件聲明

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

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）用來驗證服務端認證性，模型代碼如下：

4.2.2 初始化進程

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

4.2.3 客戶端進程

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

4.2.4 服務端進程

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

端所支持的算法信息，并與服務端自身所支持的算法信息比較來選出兩邊都支持的算法信息發(fā)送回客戶端，至此算法協(xié)商完成。進入密鑰協(xié)商階段，首先Server由通道c10接收Client發(fā)送的密鑰參數(shù)信息dhmindhP，dhmaχ，用來計算大質數(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是否存在于服務端，若存在則繼續(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）來驗證客戶端。服務端模型核心代碼如下：

4.3 Blanchet模型驗證結果

首先介紹SSHV2協(xié)議并對其數(shù)據(jù)流程進行分析，使用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協(xié)議的會話密鑰具有安全性［12］。以上結果表明，SSHV2協(xié)議具有認證性和安全性。

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

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

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

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

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

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

5 結束語

為了研究SSHV2協(xié)議在應用中的安全性，本文對SSHV2協(xié)議的消息流程進行分析。通過對每一步消息流中消息項的研究分析得出SSHV2協(xié)議整體的消息結構，最終實現(xiàn)服務端對客戶端的驗證以及服務端對客戶的認證流程分析?；贐lanchet演算將分析的消息流程應用一致性，對服務端認證客戶端和客戶端認證服務端流程建立模型。協(xié)議模型通過協(xié)議轉換工具轉換為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)的設計與實現(xiàn)［D］.北京：北京交通大學，2012.

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

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

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

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

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

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

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

2014-10-19

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