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.