SIP協(xié)議的SPIN模型檢測

尤啟房，楊晉吉

華南師范大學(xué)計算機學(xué)院，廣州510631

1 引言

SIP（Session Initiation Protocol）[1]會話初始協(xié)議是1999年IETF提出的在基于IP網(wǎng)絡(luò)中實現(xiàn)實時通信應(yīng)用的一種信令協(xié)議標準，用來創(chuàng)建、修改、終結(jié)多個參與者參加的多媒體會話進程。SIP協(xié)議的提出和發(fā)展適應(yīng)了Internet的發(fā)展，現(xiàn)已廣泛應(yīng)用于IP電話、網(wǎng)絡(luò)代理服務(wù)器、Vo IP網(wǎng)關(guān)、媒體服務(wù)器等，且已經(jīng)成為下一代網(wǎng)絡(luò)中軟交換和3G多媒體子系統(tǒng)的重要協(xié)議。不少學(xué)者對SIP協(xié)議的研究提出一些SIP認證方案[2-4]，但這些方案存在安全性或效率問題。2010年Yoon等人提出一種基于橢圓曲線的三要素SIP認證密鑰協(xié)商協(xié)議文獻[6]對其分析發(fā)現(xiàn)存在一些安全缺陷，并據(jù)此提出改進方案。

本文使用SPIN模型檢測工具對TAKASIP協(xié)議的改進分析，發(fā)現(xiàn)存在攻擊。最后，針對這些缺陷，提出一種有效的改進意見。

2 協(xié)議介紹

2.1 TAKASIP協(xié)議

TAKASIP協(xié)議包含三個階段，本文只對其認證與密鑰協(xié)商階段進行分析，協(xié)議結(jié)構(gòu)如圖1所示。

圖1 認證與密鑰協(xié)商階段的結(jié)構(gòu)

認證與密鑰協(xié)商的功能主要是為用戶和服務(wù)器進行身份認證和協(xié)商一次性會話密鑰。

協(xié)議符號說明：U表示用戶；S表示SIP服務(wù)器；ID表示用戶身份標識；PW表示用戶選擇的口令；B表示生物特征模版值；k表示S選擇的強密鑰；G1表示素數(shù)階q的加法交換群；P表示G1的生成元；Qx表示橢圓曲線上Q點的x坐標；xQ表示橢圓曲線的標量乘法運算；h(·)表示安全的單向哈希函數(shù)；d(·)表示校驗生物特征值的對稱參數(shù)函數(shù)；τ表示事先確定的生物特征校驗閥值；⊕表示對每個比特進行異或運算；||表示連接操作。

協(xié)議簡單描述如下：

（1）U首先輸入ID和PW，在傳感器上輸入自己的生物特征值B′，然后驗證生物特征值有效性，若d(B，B′)＜τ不成立，則終止這個階段；否則繼續(xù)執(zhí)行協(xié)議，計算s=v⊕h(ID||PW||B)，其中v=h(ID||k)⊕(ID||PW||B)，選擇隨機數(shù)a∈Z*q，并計算A=aP，Mac=h(s||A)，然后把＜ID，A，Mac＞發(fā)給S作為協(xié)議的第一條消息。

（2）S收到U發(fā)來的第一條消息后，首先驗證ID格式是否有效，若無效則拒絕請求；否則檢查是否U發(fā)來的Mac，若不是則終止協(xié)議；否則選擇隨機數(shù)b∈，計算B=bP，SKs=bA=abP；AuthS=h(nonce||realm||ID||Ax||Bx||S)，把＜nonce，realm，B，AuthS＞發(fā)給U作為協(xié)議的第二條消息。

（3）U接到S發(fā)來的第二條消息后，檢查是否S發(fā)來的AuthS，若不是則終止協(xié)議；否則計算SKu=aB=abP，AuthU=h(nonce+1||realm||ID||Ax||Bx||S)，把消息＜nonce，realm，AuthU＞發(fā)送給S作為協(xié)議的第三條消息。

S接收U發(fā)來的第三條消息后，檢查是否U發(fā)來的AuthU，若不是則終止協(xié)議；否則S認證了U的身份并接受U的認證請求。

協(xié)議成功執(zhí)行后，U和S共同協(xié)商一次性會話密鑰SK=abP。

2.2 對協(xié)議的改進

文獻[6]對TAKASIP協(xié)議分析后，給出了一種改進，它也是基于橢圓曲線離散對數(shù)問題的，其所采用的符號與原協(xié)議相同，且消息形式與原協(xié)議類似。改進方案有三消息形式和二消息形式兩種，本文只對其二消息形式的認證與密鑰協(xié)商階段進行分析，簡單描述如下：

計算s=v⊕h(PW||N||B)，其中v=h(ID||k)⊕(PW||N||B)，N是隨機數(shù)；R1=(r1+Tu×s)P，R2=r1kP，其中r1∈，Tu為token當(dāng)前時鐘值。

首先校驗0＜Ts-Tu＜ΔT是否成立，其中Ts為S當(dāng)前時鐘值；然后計算R1'=R1－(Tu×h(ID||k))P，檢查R2是否和kR1'相等，不等則停止執(zhí)行協(xié)議；計算R3=r3P，SKs=r3R1'=r1r3P，h1=h(ID||S||R1||R2||R3||SKs||h(ID||k))，其中r3∈；計算會話密鑰SK=h(ID||S||||R1||R2||R3||SKs)。

（3）U接收S發(fā)來的消息后，計算SKu=r1R3=r1r3P，檢查是否U發(fā)來的h1，若不是則終止協(xié)議；否則U認證了服務(wù)器的身份，計算會話密鑰SK=h(ID||S||R1||R2||R3||SKu)。

3 對改進協(xié)議的Prom ela建模及分析

3.1 攻擊者模型

攻擊者能對網(wǎng)路和通信進行不良行為，其具備以下知識能力：

（1）可以在主體間通信過程中截獲或轉(zhuǎn)發(fā)任何消息；

（2）可以以自己的身份冒充用戶或服務(wù)器參與協(xié)議的運行；

（3）可以對任何消息進行重構(gòu)，試圖欺騙用戶或服務(wù)器；

（4）對消息進行解密（必須具備相應(yīng)的知識能力）。

3.2 協(xié)議的系統(tǒng)屬性

TAKASIP協(xié)議及其改進方案在秘密狀態(tài)下用戶和服務(wù)器的身份相互鑒別，并協(xié)商一次性會話密鑰，因此協(xié)議必須滿足認證性和秘密性，同時需要保證會話密鑰一致性。

認證性：U與S成功運行了一次協(xié)議，那么U相信其通信對方就是S且S相信其通信對方就是U，即通信雙方的真實身份相互鑒別。用LTL公式表示如下：

其中&&表示邏輯與，?表示邏輯等價，[]表示always。

秘密性：保證需要保密的協(xié)議消息內(nèi)容，在傳送過程中不被非法竊取。根據(jù)橢圓曲線中的Diffie-Hellman算法計算特點，通信雙方都有一個不在網(wǎng)絡(luò)上傳輸?shù)碾S機數(shù)，攻擊者無法獲得其隨機數(shù)，從而無法計算一次性會話密鑰；同時協(xié)議采用單向的哈希函數(shù)，攻擊者無法通過逆運算獲得秘密參數(shù)。因此，只要協(xié)議成功一次運行，LTL公式就能保證秘密性。

U與S成功運行了一次協(xié)議后，通過斷言來驗證會話密鑰一致性，其斷言公式：assert(SKu==SKs)，其中SKu、SKs分為U和S的會話密鑰。

3.3 驗證結(jié)果的分析

運用基于Promela語言的SPIN工具分別對協(xié)議的改進分析，發(fā)現(xiàn)存在攻擊，攻擊軌跡如圖2所示。

攻擊過程如下：

（1）U→I(S)：REQUEST(ID，R1，R2，Tu)

（2）I(U)→S：REQUEST(ID，R1，R2，Tu)

（3）S→I(U)：RESPONSE(ID，realm，R3，h1)

圖2 協(xié)議的改進受攻擊的軌跡圖

（4）I(U)→S：REQUEST(ID，R1'，R2'，Tu)

（5）S→I(U)：RESPONSE(ID，realm，R3'，h1')

（6）I(S)→U：RESPONSE(ID，realm，R3，h1)

攻擊過程描述：

I截獲了（1）的消息后轉(zhuǎn)發(fā)給S，S驗證消息（1）后回復(fù)消息（3）給I；I隨后對消息（1）進行修改：選一個數(shù)r∈，并計算R1'=R1+rP=(r1+r+Tu×s)P，R2'=R2'+rQ=(r1+r)kP，其中Q為系統(tǒng)公開參數(shù)，把消息（4）發(fā)送到S；S接收到消息（4）后，若在時間間隔比較短時，0＜Ts-Tu＜ΔT依然成立，接著計算R1''=R1'-(Tu×h(ID||k))P=(r1+r)P，剛好R2'=(r1+r)kP與kR1''=k(r1+r)P相等，這樣S又重新認證了U的請求，S發(fā)響應(yīng)消息（5）給I，并計算新的會話密鑰SK′=h(ID||S||R1'||R2'||R3'||SKs′)；最后I發(fā)送消息（6）給U，U驗證消息（6）后計算會話密鑰SK。

通過上述分析，U和S雖然實現(xiàn)相互認證，但U的會話密鑰SK和S的會話密鑰SK′不一致；但由于無法獲知會話密鑰，I無法從中獲益。

3.4 對TAKASIP協(xié)議的改進意見

TAKASIP協(xié)議受攻擊的原因是U無法辨認S的真實身份，而其改進受攻擊的原因是S無法辨認U的真實身份；在TAKASIP協(xié)議設(shè)計中，U和S共享了一個秘密值s=h(ID||k)，第三方無法獲得，這樣分別在消息的參數(shù)中加入s，將有效保證消息的身份認證，從而無法對協(xié)議進行攻擊。改進后的TAKASIP協(xié)議的認證與密鑰協(xié)商階段如下：

（1）U→S：REQUEST(ID，A，Mac)

（2）S→U：CHALLENGE(nonce，realm，B，AuthS)

（3）U→S：RESPONSE(nonce，realm，AuthU)其中，AuthS=h(nonce||realm||ID||Ax||Bx||S||s)，AuthU=h(nonce+1||realm||ID||Ax||Bx||S||s)。

4 改進方案的安全性和性能分析

4.1 安全性分析

定理1 改進方案能抵抗重放攻擊。

證明假設(shè)攻擊者截斷第一條消息后冒充合法用戶U，攻擊者無法計算出SK=abP，因為要從B=bP中獲取b會面臨ECDLP難題，或用A=aP和B=bP來計算SK=abP會面臨ECDHP難題，攻擊者也沒有s=h(ID||k)，因此攻擊者無法構(gòu)造第一條消息中的Mac=h(s||A)和第三條消息中的AuthU=h(no-nce+1||realm||ID||Ax||Bx||S||s)，同理攻擊者無法冒充服務(wù)器S，因為無法構(gòu)造第二條消息中的AuthS=h(nonce||realm||ID||Ax||Bx||S||s)。

定理2 改進方案能抵抗猜測攻擊。

證明攻擊者截獲通信中的REQUEST、CHALLENGE和RESPONSE三條消息來計算s=h(ID||k)或k，由于哈希函數(shù)的單向性，攻擊者無法猜測出正確的s=h(ID||k)或k。

定理3 改進方案能抵抗中間人攻擊。

證明攻擊者截獲REQUEST消息，于是選擇隨機數(shù)e∈，并計算E=eP，但是由于沒有s=h(ID||k)，無法正確計算出Mac′=h(s||E)，服務(wù)器S驗證REQUEST時會拒絕此請求；同樣由于攻擊者要從A=aP和B=bP來計算SK=abP會面臨ECDHP難題，攻擊者也沒有s=h(ID||k)，所以攻擊者無法偽造CHALLENGE(nonce，B，AuthS)消息欺騙用戶U。

定理4 改進方案能提供雙向認證。

證明協(xié)議是基于橢圓曲線離散對數(shù)問題的，協(xié)議中的三條消息的來源正確性都得到對方的安全驗證，因此協(xié)議能提供雙向認證。

定理5 改進方案能提供完美前向安全性。

證明即使攻擊者獲取了舊會話中的會話密鑰SK=abP，口令PW，生物特征值B和當(dāng)前的A=a′P和B=b′P，但是最新的一次性會話密鑰SK′=a′b′P，攻擊者由于ECDHP問題無法計算出正確的SK′，因此改進方案提供了完美前向性。

4.2 性能分析

改進方案在原協(xié)議的基礎(chǔ)上增加了鏈接秘密值操作，增加的運算代價可以忽略，因此性能上與原協(xié)議一樣。文獻[6]對原協(xié)議及其改進的計算代價和通信代價已經(jīng)做了詳細的比較，這里不再介紹。但是文獻[6]提出的改進協(xié)議ETAKASIP的用戶U還需要計算h(PW||N||B)，服務(wù)器S還需要計算h(ID||k)，因為這兩個值都是臨時計算的，這樣三消息形式的ETAKASIP協(xié)議需要8次哈希運算，7次橢圓曲線點乘運算和1次橢圓曲線加法運算；而本方案與原協(xié)議一樣只需8次哈希運算，4次橢圓曲線點乘運算，在計算效率上保持高效性。

5 結(jié)論

本文使用Promela語言對TAKASIP協(xié)議的改進方案進行建模，通過驗證協(xié)議必須滿足的安全性質(zhì)描述（LTL公式、斷言），成功找到反例。最后，分析這些缺陷產(chǎn)生的原因，并給出一種改進意見，改進后的協(xié)議能夠滿足安全協(xié)議的要求。SPIN模型檢測技術(shù)是分析安全協(xié)議的有力工具，下一步工作是設(shè)計更復(fù)雜的模型分析其他的安全協(xié)議。

[1]Rosenberg J，Schulzrinne H.SIP：Session initiation protocol[S].2002.

[2]Ring J，Choo K K R.A new authentication mechanism and key agreement protocol for SIP using identity-based cryptography[C]//Proc of Aus CERT Asia Pacific Information Technology Security Conference.Brisbane：University of Queensland Publication，2006：57-72.

[3]Wu L F，Zhang Y Q，Wang F J.A new provably secure authentication and key agreement protocol for SIP using ECC[J].Computer Standards and Interface，2009，31（2）：286-291.

[4]Hankerson D，Menezes A，Vanstone S.Guide to elliptic curve cryptography[M].New York，USA：Springer-Verlag，2004.

[5]Yoon E J，Yoo K Y.A three-factor authenticated key agreement scheme for SIP on elliptic curves[C]//Proceedings of the 4th International Conference on Network and System Security（NSS’10）.Piscataway：IEEE，2010：334-339.

[6]唐宏斌，劉心松.對TAKASIP協(xié)議的分析和改進[J].計算機應(yīng)用，2012，32（2）：468-471.

[7]吳昌，肖美華.基于SPIN的IKEv2協(xié)議高效模型檢測[J].計算機工程與應(yīng)用，2008，44（5）：158-161.

[8]Clarke E M，Grumberg O，Peled D A.Model checking[M].London：M IT Press，1999.

[9]Holzmann G J.The spin model checker primer and reference manual[M].Boston：Addison-Wesley，2003.

[10]M arrero W，Clarke E M，Jha S.A model checker for authentication protocols[C]//Proceedings of the DIMACS Workshop on Design and Formal Verification of Security Protocols，1997.