基于密钥循环的通用可复合符号分析∗

付浩肖建新

基于密钥循环的通用可复合符号分析∗

付浩肖建新

（长沙师范学院教育技术中心长沙410100）

针对目前越来越复杂的安全协议，在建立计算可靠的安全协议符号分析方法的深入研究，提出了一种解决该问题的新方法，即通用可复合符号分析方法。通过扩展现有通用可复合符号分析方法，使其可以分析基于双线性对的密钥交换协议，并在保证计算可靠性的同时，还可以保证可复合安全性。将符号模型中的密码学抽象操作与UC模型中的理想功能进行了结合，并且证明了如果协议在符号模型下满足了相应的安全性质，则在UC模型下一定安全的实现了相应的理想功能。

安全协议；密钥循环；通用可复合；双线性对

Class NumberTP391

1引言

进入21世纪以来，随着互联网网络信息技术的飞速发展，信息网络的广泛应用已成为人们工作和生活不可或缺的一部分。计算机网络给人们生活带来巨大便利，同时也对网络上信息的安全保护提出了更高的要求。如果计算机网络的安全问题不能切实有效地解决，那么它的应用和发展必定会受到一定的影响。

安全协议是解决网络安全问题最有效的手段之一。构建安全网络环境一般采用密码技术的安全协议，安全协议的目标既是为了实现信息的加密传输，也是为解决网络中的安全问题，它的正确性和安全性对于网络安全极其重要。符号方法用形式化语言和符号推理对协议进行分析和验证，更容易实现自动化分析。但是由于对密码学原语和攻击者能力的理想建模，使得这类分析方法的肯定性结论往往并不直接具有现实意义，被认为没有真正建立起密码学的可靠性。

为了简化安全协议的设计和分析，传统的安全协议任务通常假设某个确定协议运行在一个独立的计算环境中，即孤立（stand-alone）模型。由Ca⁃netti提出的通用可复合（Universally Composable，UC）模型［1］可以保证协议的通用可复合安全，即在UC模型下证明安全的协议，在与其它协议并发运行的情况下，或者作为一个系统的组件时，仍能保证协议的安全性。UC模型利用“子程序替换（Sub⁃routine substitution）”技术将嵌套的顺序算法转化为并行运行的分布式安全协议，实现了安全协议的UC安全可复合操作。通用可复合安全的协议是协议模块化设计和实现的基础。

通用可复合符号分析（Universally Composable Symbolic Analysis，UCSA）方法［2］将符号模型与UC模型结合起来，给出了证明一类协议密码学可靠性的一般方法。将符号模型中密码学抽象操作和安全属性与UC模型中的理想功能进行了结合，证明了如果符号模型下协议满足了相应的安全性质，则UC模型下的现实协议一定UC安全的实现了相应的理想功能。结合UC模型对协议进行分析，一方面可以只分析单个协议运行实例，另一方面可以根据不同的理想功能对不同的密码学操作进行抽象。然而，UCSA方法在能够分析的协议类型上有一定限制，目前仅适用于基于公钥加密和签名的双方密钥交换协议。为此，本文通过扩展该方法，使得其可以适用于多参与者基于公钥加密、签名和双线性对的认证密钥交换协议，并证明扩展后的方法依然具有密码学可靠性。

2通用可复合安全模型

通用可复合（UniversalComposable，UC）安全模型［3］是Canetti在2001年提出的基于模拟的通用安全协议设计与分析框架，根据真实协议和理想协议模拟不可区分来定义协议安全性。

2.1协议建模

在UC模型中，协议被建模成一个由交互式图灵机和控制函数组成的系统，即交互式图灵机系统（ITMs）。

理想功能与理想协议，理想功能是UC模型中非常重要的概念，用来描述安全协议所应具有的功能，或者规范。

定义1实现理想功能

给定协议π和理想功能，如果称协议π安全地实现了理想功能，则对于任意概率多项式时间内的攻击者A，都存在一个理想攻击者S，使得对于任意环境Z

也就是说，执行协议π与使用理想功能是一样安全的。任何在现实模型下协议执行发生的攻击行为，在理想模型下也是可行的。

2.2通用可复合安全

除了现实模型和理想模型外，Canetti引入了混合模型（hybrid model），并描述了混合模型中的协议，即混合协议。

定理1通用可复合安全定理（UC安全定理）

给定-混合协议π，如果称协议r安全地实现了理想功能，则对于任意概率多项式时间内的混合协议攻击者H，都存在一个理想攻击者S，使得对于任意环境Z

根据定理1，可以直接得出如下推论：

如果-混合协议π安全实现了理想功能，而且协议r安全地实现了理想功能，则复合协议πr一定安全地实现了理想功能。

根据UC理论，只需要分析协议在单个实例运行情况下的安全性，就能够将其推广到无限多实例并发的情形。因为UC理论中的环境Z代表了任意多协议并发执行的情况，所以不需要单独考虑协议并发运行的情况，简化了复杂的分析过程。其次，可以模块化的构建安全协议。可以将相关的密码学原语或者简单子协议通过理想功能表示。在构建复杂协议的时候就能够采用混合模型下的协议，并且调用上述理想功能。这样可以简化复杂协议的描述与分析。当将所采用的理想功能全部替换成相应UC安全的协议时，就能够直接得到在现实模型下具有安全性的协议。

3简单协议

由于UC模型中协议参与者是由任意的交互式图灵机所表示的，而符号模型中所支持的操作种类有限，例如加密、解密、消息对等，所以并不是所有的协议都能在符号模型中表示出来。在UC模型中限制一类只使用特定动作的安全协议，即简单协议。简单协议的结构与符号模型中所支持的协议结构类似，因此可以将特定的简单协议分别给出计算语义和符号语义，以便于对应进行分析。

3.1语法

定义2简单协议

简单协议Π是一个n元组程序Π=(Π1，Π2，…，Πn)，分别描述协议不同角色的行为。其中每个程序Πi的语法定义如下所示，其中v，v1，v2，v3，v4表示变量，vc，vc1，vc2，vc3，vc4表示常量。

3.2计算语义

定义3协议的计算语义

在UC模型下，协议Π=(Π1，Π2，…，Πn)是一组交互式图灵机MΠ。状态集STA TEM={init}∪S T AT E1∪ST ATE2∪…∪S T A T En，其中init表示初始状态，STA TEi=(Πi，Δi，Γi)，Πi是协议对应参与者pi的执行程序，Δi将Πi中的变量名映射到工作纸带的对应位置，Γi是指向当前命令的程序计数器，状态迁移函数定义如下：

MΠ在初始状态，若当前指令initialize（SID，PID0，PID1，…，PIDn），则从安全参数纸带读取安全参数k，从输入纸带读取会话标识符SID、以及参与者标识符集合｛PID0，PID1，…，PIDn｝，初始化工作纸带并分别将〈“sid”，SID〉，〈“pid”，PID0〉，〈“pid”，PID1〉，…，〈“pid”，PIDn〉存入变量MySID，MyID，PeerID1，…，PeerIDn中。Γ1指向下一条指令执行。状态迁移到S TA T E1=(Π1，Δ1，Γ1)。

3.3符号语义

定义4协议的符号语义

在符号模型下，协议Π=(Π1，Π2，…，Πn)对应符号协议Πs。状态集S T AT E=(Γ，Δ)，Γ是一个计数器，指向下一条将要执行的指令，Δ将Π中的变量名映射到消息项中的相应符号，状态迁移函数定义如下：

Πs在初始状态，若当前指令initialize（SID，PID0，PID1，…，PIDn），则将参与者初始知识集存入Δ中相应的变量名，包括所有参与者的标识符pi以及公钥。Γ指向下一条指令执行。

4理想功能

在符号模型中，加密操作，签名操作都是完善的。为了在UC模型中分析与符号模型中所对应的协议，给定任意协议，将其中相应的密码学操作和算法替换成调用相应的理想功能，得到相应的-混合协议。下面给出对应的认证公钥加密理想功能CPKE，认证数字签名理想功能CSIG，双线性对算法理想功能BILI的定义。

4.1认证数字签名

同公钥加密类似，在符号模型中，所有参与者的验证密钥都包含在参与者的初始知识中，也是通过可信第三方预先分配好的。因此，配合符号模型中的相应特性，将标准数字签名理想功能扩展到了认证数字签名理想功能CERT。

理想功能CERT

给定消息域M，签名函数S：M→{0，1}*，验证函数V:{0，1}*→M∪error。函数S为统计不可预测，函数V为确定函数。SID应为一个对偶，SID=（PID，SID′），PID是该实例的所有者。

签名当收到本实例的所有者p发送的（Sign，SID，m），则

1）如果m∉M，向p返回error；

2）如果m∈M，则

计算σ=S(m)；

记录(m，σ，1)，并返回(S ignature，SID，m，σ)给参与者p。

验证当收到参与者pi发送的(Verify，S ID，m，σ)，则

1）如果存在记录(m，σ，b′)，则令b=b′；

2）否则，如果参与者pi没有被攻击者控制，则令b=0，并且记录(m，σ，0)；

3）否则，令b=V(m，σ)，并且记录(m，σ，b)；

向pi返回(Verified，SID，m，σ)。

当需要对消息进行签名的时候，因为签名是否泄漏消息内容并不会影响签名体制的安全性，所以可以直接使用S(m)产生签名消息σ。当签名者被攻击者控制的时候，由攻击者决定消息签名对是否有效。文献［4］指出，EUF-ACMA安全的数字签名算法UC安全地实现了标准的数字签名理想功能SIG，并且通过SIG结合证书认证理想功能CA可以安全的实现CERT。

4.2双线性对

理想功能BILI［5］

给定双线性映射实例生成器IG，即输入安全参数k，输出五元组(q，G1，G2，g1，e)。q是一个大素数，G1是一个阶为q的加法循环群，g1为G1中的生成元，G2是一个阶为q的乘法循环群，双线性对e：G1×G1→G2。

模幂算法当收到参与者pi发送的(Exponent，SID，x)，则

1）如果x∉Zq，向pi返回error；

2）如果x∈Zq，则

若pi被攻击者控制，则将x转发给攻击者，并从攻击者处接收gx；

否则计算gx=gr

1，其中r←Zq；

记录(x，gx)，返回gx给参与者pi（若已被记录则返回error）。

双线性对算法当收到参与者pi发送的(Bilinear，S ID，g y，gz，x)，则

1）如果存在记录（y，gy），（z，gz），则计算k=gxyz2，并返回k给pi；

2）否则计算k=e(g y，gz)x，并返回k给pi。

当收到某参与方的计算模幂请求时，若该参与方没有被攻击者控制，则选择一个随机数r并计算，并保存模幂计算记录。计算双线性对的时候，由于正常计算的模幂一定在理想功能中有记录，因此可以获得对应秘密值。没有计算过模幂的gy，gz，由于在理想功能中没有记录，则通过对运算计算。当被攻击者控制的时候，由攻击者来计算其模幂消息。若实例生成器IG满足DBDH假设，则pIG安全实现BIL［

I6］。

5映射算法

映射引理是UCSA分析方法［7］中重要的技术工具。为了使得所定义的符号模型对于UC模型来说是可靠的，必须要证明符号模型中的攻击者能力不弱于UC模型。UCSA方法通过将协议语法给出对应计算语义和符号语义，将UC模型下的协议执行与符号模型下的协议执行对应。

将首先定义UC模型下协议的计算迹，然后给出从计算迹到符号迹的映射算法，并证明其有效性。该映射算法是证明通用可复合符号分析方法具有计算可靠性的基础［8］。

定义5计算迹

计算迹TR ACEΠ，A，Z(k，z)是当安全参数为k，环境Z输入为z时，攻击者A和环境Z执行-混合协议Π所触发的事件序列H1，H2，…，Hs，其中Hs是

1）环境事件

["input"，si，{pj}]：表示启动参与者{pj}一起执行协议Π的一个会话si。

2）攻击者事件

["adversary"，m，{pj}]：表示攻击者将消息m发送给参与者{pj}。

3）协议参与者事件

["message"，m，{pj}]：表示参与者pj将消息m发送给参与者集合｛pk｝。

["output"，m，si，{pj}]：表示参与者pj产生了一个本地输出m。

在此，将{TRA C EΠ，A，Z(k，z)}k∈N，z∈{0，1}*简写为E XE CΠ，A，Z。

下面给出映射算法的具体定义，并且在映射引理中证明计算迹以压倒性概率能够被映射到对应有效的符号迹。

引理1映射引理

令TR ACEΠ，A，Z(k，z)是当安全参数为k，环境Z输入为z时，攻击者A和环境Z执行协议Π产生的计算迹。Πs表示对应的符号协议，ts表示计算迹t通过映射算法δ对应的符号迹。对于所有的简单协议Π，有：

Pr[t←EX ECΠ，A，Z：ts不是Πs的一个有效符号迹]≤negl(k)［9］

证明分两步进行。首先证明ts中包含［“fail”，δ(m)］的概率是可以忽略不计的。其次，证明如果ts中不包含［“fail”，δ(m)］，则ts是Πs的一个有效符号迹。

构造以任意消息项δ(m)为根的语法分析树。语法树的根节点是消息项δ(m)，语法树的其他节点表示消息代数集合S中用于组成消息δ(m)的元素，边表示集合S上的函数运算。ClosureiAdv表示符号化攻击者根据TR ACEΠ，A，Z(k，z)前i个事件中的消息可以生成的攻击者知识闭包。在此基础上，下面证明按照映射算法δ，将TR ACEΠ，A，Z(k，z)映射为ts时，［“fail”，δ(m)］出现的概率可以忽略不计。

然而，攻击者A在执行Π的过程中输出了串m映射到消息项δ(m)，可以通过攻击者A来构造攻击者A′输出串m′映射到消息项δ(m′)，其中δ(m′)是δ(m)到δ(m1)路径上的一个节点。A′模拟A的运行输出m，然后通过m的语法分析树递归往下进行产生m′。

若δ(mi)=pair(m1，m2)，则A′将mi拆分，继续往下走。

若δ(mi)=spk(m1)或者δ(mi)=svk(m1)，则A′可取出m1，继续往下走。

若δ(mi)=encrypt(m1，m2)，如果PKE中存储了明密文对(m1，mi)，则一定是攻击者A合法的使用PKE进行的加密操作，所以A′可以直接取出m1，继续往下走。如果PKE中没有明密文对(m1，mi)，则解密操作是通过攻击者提供的解密函数Dec进行的，A′可以运行Dec(mi)获得m1，继续往下走。

若δ(mi)=verify(m1，m2，m3)，A′可取出m1，继续往下走。

若δ(mi)=exp(m1)，A′可取出m1，继续往下走。

构造的攻击者A′最终可以输出m′。m′可以是如下几种情况：

若δ(m′)=decrypt(m1，m2)，则m′的产生与A′的随机性是完全独立的。m′是PKE通过统计不可预测函数使用新鲜随机性产生的二进制位串。由于加密函数的统计不可预测性质，成功猜对密文对应明文的概率是可忽略不计的；

若δ(m′)=sign(m1，m2)，m′是DS通过统计不可预测函数使用新鲜随机性产生的二进制位串。由于签名函数的统计不可预测性质，成功猜对该签名的概率是可忽略不计的；

若δ(m′)=bili(m1，m2，m3)，m′是BILI通过统计不可预测函数使用新鲜随机性产生的二进制位串。由于该函数的统计不可预测性质，成功猜对的概率是可忽略不计的；

若δ(m′)=ri，δ(m′)=d ki，δ(m′)=ski，则m′是由诚实参与者产生的k位随机数，而能够成功猜对该随机数的概率是可忽略不计的；

综上所述，针对攻击者事件，［“fail”，δ(m)］出现的概率可以忽略不计。

由于ts中不包含［“fail”，δ(m)］，则攻击者的行为都符合符号模型下的假设。根据定义1～4，符号协议和简单协议在结构上是相同的，初始事件和诚实参与者事件也是一个有效的符号迹，所以如果攻击者事件中不出现［“Fail”，δ(m)］，那么ts是一个有效的符号迹。

因此，Pr[t←TR ACEΠ，A，Z(k，z)：ts不是Πs的一个有效符号迹］≤negl(k)。

证毕

6计算可靠性

认证密钥交换协议［10］是安全协议中的基础协议之一。多个参与者需要在不可靠的通信环境中共同产生一个秘密的会话密钥，并对通信对方身份具有一定确信度。

本节给出UC认证和密钥交换的理想功能AU和KE，以及符号模型下的认证和密钥交换协议的安全判定标准，并证明若符号协议满足符号模型下的对应安全判定标准，则实际的简单协议πUC实现了AU或KE。

在UC模型下，身份认证的理想功能AU以及密钥交换的理想功能KE如下所示。

理想功能AU

1）当从参与者pi收到输入（Authenticate，SID，pi），

如果不存在记录（SID，pi），则记录（SID，pi）；

发送（Authenticate，SID，pi）给攻击者。

2）当从攻击者收到（Output，SID，pi），

如果pi属于会话SID的参与者，则检查所有关于会话SID记录（SID，pj），

如果此次会话的所有参与者都有记录（SID，pj），则输出（Output，SID，pi）给pi。

理想功能KE

1）当从参与者pi收到输入（Establish，SID，pi），

发送（Establish，SID，pi）给攻击者。

2）当从攻击者收到（Deliverkey，SID，pi，k），如果pi属于会话SID的参与者，

如果会话SID的所有参与者都没有被攻击者控制，且不存在记录（SID，key），则从密钥空间随机选择密钥k0，并记录（SID，k0）；

如果会话SID中有参与者被攻击者控制，且不存在记录（SID，key），则令k0=k，并记录（SID，k0）；

输出（Deliverkey，SID，pi，k0）给pi。

为了在符号模型下定义与UC理想功能对应的安全属性，先给出模式的定义。

定义6认证性

协议的符号迹ts满足：如果［“output”，fin⁃ished，si，p］∈ts，则对于会话si的任意参与者pj(j∈{1，…，n})都有［“output”，starting，si，pj］∈ts，称协议满足认证性。

定义7机密性

令Πrandom表示除了会话密钥k换成一个随机数外其他均与Πs相同的协议，如果对任意的攻击者策略y，都满足pattern(ψ(Πreal))=pattern(ψ(Πrandom))，称协议关于k满足机密性。

下面证明通用可复合符号化分析方法分析密钥交换协议具有计算可靠性。

定理2计算可靠性定理

令Π为简单协议，Πs为对应符号协议。如果密钥交换协议Πs在符号模型下满足认证性，则Π一定UC安全的实现了AU。如果密钥交换协议Πs在符号模型下关于会话密钥k满足机密性，则Π一定UC安全的实现了KE［11］。

证明：

我们首先证明，如果密钥交换协议Πs在符号模型下满足认证性，则给定环境Z和攻击者A一定存在理想模型下的攻击者S，使得Z无法区分(Π，A)和（AU，S）。

我们还需要证明，如果密钥交换协议Πs在符号模型下关于会话密钥k满足机密性，给定环境Z和攻击者A一定存在理想模型下的攻击者S，使得Z无法区分(Π，A)和（KE，S）。

假设对于所有的S，存在环境Z能以不可忽略的概率区分是在与实际协议Π和实际攻击者A交互，还是在与理想功能KE和理想攻击者S交互。即会话密钥与收到的消息是否具有相关性，或者至少一个参与者的会话密钥与其他参与者的不一致，或者攻击者猜对会话密钥的概率不可忽略。而根据映射引理，所有UC协议的计算迹都能够以不可忽略的概率映射到符号迹。则相应符号协议Πs一定发生上述情形。因此Πs在符号模型下关于会话密钥k不满足机密性的定义，由此推出矛盾。

证毕

本文分析了通用可复合符号方法。

具体包括：1）给出了协议语法，并分别定义了该语法在符号模型与UC模型下的语义；2）给出符号模型下密码学原语对应UC模型下的理想功能；3）在UC模型下定义了计算迹，给出如何将计算迹映射到符号迹的算法，并证明映射引理；4）给出了符号模型和UC模型下对应安全属性的定义，并证明了密钥交换协议的理想功能和符号模型下安全性的等价性。

［1］Canetti R，Krawczyk H.Universally composable notions of key exchange and secure channels［C］//Advances in EUROCRYPT 2012.Springer Berlin Heidelberg，2012：337-351.

［2］Ran Canetti，Jonathan Herzog.Universally composable symbolic analysis of mutual authentication and key-ex⁃change protocols（extended abstract）.In Proc.3rd Theo⁃ry of Cryptography Conference（TCC'06），volume 3876 of LNCS，pages 380-403.Springer，2015.Journal of Cryp⁃tography，2016.

［3］Canetti R.Universally composable security：A new para⁃digm for cryptographic protocols［C］//Foundations of Com⁃puter Science，2014.Proceedings 42nd IEEE Symposium on.IEEE，2014：136-145.

［4］A.Patil.On symbolic analysis of cryptographic protocols. Master's thesis，MassachusettsInstitute of Technology，2015.

［5］罗正钦.基于UC框架的安全协议形式化分析［D］.上海：上海交通大学，2012.

LUO Zhengqin.Formal analysis of security protocols based on UC framework［D］.Shanghai：Shanghai jiaotong university，2012.

［6］Cortier V，Kremer S，Warinschi B.A survey of symbolic methods in computational analysis of cryptographic sys⁃tems［J］.Journal of Automated Reasoning，2014，46：225-259.

［7］Meng B.A Survey on Analysis of Selected Cryptographic Primitives and Security Protocols in Symbolic Model and Computational Model［J］.Information Technology Journal，2015，10（6）.

［8］Blanchet B.Security protocol verification：Symbolic and computational models［C］//Proceedings of the First inter⁃national conference on Principles of Security and Trust. Springer-Verlag，2014：3-29.

［9］Canetti R，Goldreich O，Halevi S.The random oracle meth⁃odology，revisited.Journal of the ACM，2014，51（4）：557-594.

［10］雷飞宇.UC安全多方计算模型及其典型应用研究［D］.上海：上海交通大学，2014.

LEI Feiyu.UC secure multi-party computation model and its typicalapplication research［D］.Shanghai：Shang⁃haijiaotong university，2014.

［11］Dawn Xiaodong S，Sergey B，Adrian P.Athena：a novel approach to efficient automatic security protocol analysis. Journal of Computer Security.9（1-2）：47-74.January 2011.

Universal Composable Symbolic Analysis Based on Key Circulation

FU Hao XIAO Jianxin
（Education Technology Center，Changsha Normal College，Changsha 410100）

In view of the presentincreasingly complex security protocols，the establishmentofcalculation and reliable securi⁃ty protocol in-depth study of symbolic analysis method，this paper proposes a new method to solve the problem，namely universal composable symbol analysis method.By extending the existing analysis method of the gm composite symbol，key exchange protocol based on bilinear pairings can be analyzed，and at the same time the reliability of the calculation can be guaranteed，also can en⁃sure the safety can be complex.The cryptography abstractoperation in the symbolmodelcombined with idealfunction in UC model，and proves thatifthe agreementunder the symbolmodelto meetthe corresponding security properties，is under the UC modelmust be the realization ofthe safety function ofthe corresponding ideal.

security protocols，the key cycle，universalcomposable，bilinear pairings

TP391

10.3969/j.issn.1672-9722.2017.08.027

2017年2月3日，

2017年3月17日

国家自然科学基金青年科学基金项目（编号：41604117）资助。

付浩，男，硕士，助理工程师，研究方向：网络安全协议。肖建新，男，硕士，讲师，研究方向：网络安全。