SIP協議的SPIN模型檢測

尤啟房，楊晉吉

華南師范大學計算機學院，廣州510631

1 引言

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

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

2 協議介紹

2.1 TAKASIP協議

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

圖1 認證與密鑰協商階段的結構

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

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

協議簡單描述如下：

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

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

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

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

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

2.2 對協議的改進

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

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

首先校驗0＜Ts-Tu＜ΔT是否成立，其中Ts為S當前時鐘值；然后計算R1'=R1－(Tu×h(ID||k))P，檢查R2是否和kR1'相等，不等則停止執行協議；計算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發來的消息后，計算SKu=r1R3=r1r3P，檢查是否U發來的h1，若不是則終止協議；否則U認證了服務器的身份，計算會話密鑰SK=h(ID||S||R1||R2||R3||SKu)。

3 對改進協議的Prom ela建模及分析

3.1 攻擊者模型

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

（1）可以在主體間通信過程中截獲或轉發任何消息；

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

（3）可以對任何消息進行重構，試圖欺騙用戶或服務器；

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

3.2 協議的系統屬性

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

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

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

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

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

3.3 驗證結果的分析

運用基于Promela語言的SPIN工具分別對協議的改進分析，發現存在攻擊，攻擊軌跡如圖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 協議的改進受攻擊的軌跡圖

（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）的消息后轉發給S，S驗證消息（1）后回復消息（3）給I；I隨后對消息（1）進行修改：選一個數r∈，并計算R1'=R1+rP=(r1+r+Tu×s)P，R2'=R2'+rQ=(r1+r)kP，其中Q為系統公開參數，把消息（4）發送到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發響應消息（5）給I，并計算新的會話密鑰SK′=h(ID||S||R1'||R2'||R3'||SKs′)；最后I發送消息（6）給U，U驗證消息（6）后計算會話密鑰SK。

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

3.4 對TAKASIP協議的改進意見

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

（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 改進方案能抵抗重放攻擊。

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

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

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

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

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

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

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

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

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

4.2 性能分析

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

5 結論

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

[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協議的分析和改進[J].計算機應用，2012，32（2）：468-471.

[7]吳昌，肖美華.基于SPIN的IKEv2協議高效模型檢測[J].計算機工程與應用，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.