协议组合逻辑在实例化空间模型中的语义解释

肖茵茵，苏开乐

（1.广东技术师范学院计算机学院，广东 广州 510665；2.中山大学信息科学与技术学院广东省信息安全重点实验室，广东 广州 510275；3.浙江师范大学数理与信息工程学院，浙江 金华 321004）

协议组合逻辑在实例化空间模型中的语义解释

肖茵茵1，2，苏开乐2，3

（1.广东技术师范学院计算机学院，广东 广州 510665；2.中山大学信息科学与技术学院广东省信息安全重点实验室，广东 广州 510275；3.浙江师范大学数理与信息工程学院，浙江 金华 321004）

安全协议的验证是个不可判问题.为了对实例化空间逻辑ISL的语义表达能力给出理论上的衡量与评价，选择另一种实用的协议组合逻辑PCL，分析了ISL和PCL之间的关系.在此基础上，将PCL的索状空间语义模型转换为ISL的实例化空间语义模型，在实例化空间下对PCL的主要公式、定理、推导规则做了语义解释.研究表明，实例化空间能够完全表示PCL的语义，且ISL的语义表达能力强于PCL.新的模型解释使PCL更易于扩展，且使得用PCL理论验证的协议能够利用ISL的自动化验证工具SPV进行分析.

安全协议验证；实例化空间；协议组合逻辑；索状空间；语义解释

1 引言

安全协议形式化验证逻辑是检验安全协议正确性的一类重要方法.其中，实例化空间逻辑ISL（Instantiation Space Logic）［1-2］以实例化空间为语义模型，并拥有一组尽可能完备的纯命题逻辑的公理模式，可验证工业级复杂协议的认证性、秘密性等相关安全性质.因为协议的验证是个不可判问题［3］，所以无法直接对ISL进行严格的完备性证明.为了对ISL的语义表达能力给出理论上的衡量与评价，本文选取Dolev-Yao模型下的另一种实用的安全协议验证逻辑-协议组合逻辑PCL（Protocol Compositional Logic）［4-5］，利用PCL与ISL的相似性，用ISL的实例化空间语义模型解释PCL，转换的成功说明ISL的语义表达能力足以描述PCL.另一方面，我们还说明了现有的PCL不能够完全表示ISL的语义，这种单向的语义对应关系证明ISL的公理集比现有的一些验证逻辑刻画了更一般的情形，具有较强的语义表达能力.目前，国内外对安全协议形式化验证逻辑语义方面的研究较少，因此该工作在一定程度上填补了这方面研究的空白.

PCL主要用于验证公钥加密体制下协议的认证性和秘密性，是一种包含模态算子和描述协议动作的进程算子的逻辑，其推理过程是基于动作的：即把协议的执行过程看成是参与主体的动作集合，其公理和推导规则与每一步协议的执行动作相关，每个动作导致一个推理结果的产生，最后在协议动作执行完毕时检验相应的逻辑结果是否满足相关的安全性质.这种“模态动作逻辑”在验证过程中的系统状态会随着协议规模的增大而迅速增加，难以自动化.迄今为止，还未见到与PCL对应的自动化验证工具.而ISL的公理集在算法上可完全实现，其自动化验证工具SPV（Security Protocol Verifier）能高效验证大规模复杂协议的性质［1，6-7］.本文把PCL的语义转化到实例化空间下，将使得用PCL理论验证的协议能够利用SPV进行自动化验证.另外，因为实例化空间更具有一般性，因此该模型解释下的PCL具有更好的扩展性.

2 实例化空间逻辑ISL与协议组合逻辑PCL简介

为便于理解，本节将对实例化空间逻辑ISL与协议组合逻辑PCL作简单介绍，关于本节内容的详细论述可参见文献［1-2］和［4-5］，本文未特别说明的符号和术语均与文献一致.

2.1 实例化空间逻辑ISL

ISL的加密消息交换CME(Cryptographical Message Exchange)模型Σ=（M，K，e，Ag，Pk，Sk，Label，Nonce，Gn，Dh，Init，Recv，Sent）定义在消息代数（M，K）基础上，用于说明主体之间如何进行加密消息的交换.为方便起见，CME模型中定义了一些有用的函数，如Sub、Recvs、Poss、Encr、Computes、Fresh等等.另一方面，安全协议P是由原子消息符号集和协议体构成的多元组（AG，PK，SK，INIT，BODY），P中所有消息符号用MSGP来表示.协议中的各个角色都有自己的局部协议，用于刻画与自身有关的行为.对于一个协议P和CME模型Σ，二元组（ρ，c）表示以随机数或时戳c为标识消息的主体ρ的局部运行.对于每个局部运行（ρ，c），可定义一个消息赋值函数：f:MSGP→M，对于每个MP∈MSGP，f（MP）是在P中的局部运行（ρ，c）中扮演协议所定义的MP的具体消息.若f描述了局部运行（ρ，c）中主体ρ的动作与角色A的行为间的对应关系，则称f为一个（ρ，c，A，l）-函数（l是协议执行的某一步，必须小于A的局部协议的长度），又称为A的实例化函数，记为

实例化空间Ω=（Σ，L，F，譓）是一个基于实例化函数和CME模型的安全协议验证逻辑语义模型.其中，Σ是CME模型，L是协议P相关联的标识消息集，F是实例化函数集，譓是关于主体Ag行为的假设集.

实例化空间逻辑是以实例化空间为语义模型的逻辑理论ΘP.ΘP中的role、norm、poss、sees、said、fresh和secr等原子公式描述了主体在局部运行中如何扮演协议角色.ΘP的公理模式基于纯命题逻辑，其中最重要的公理为角色假设定理和（n，1）-Secrecy定理.这些公理比现有的一些验证逻辑刻画了更一般的情形，可有效地验证协议的安全性质.

2.2 协议组合逻辑PCL

PCL的基本概念有项、动作、索带和索状空间.

串S为动作序列：S：=aS|a，a∈action.～为作用于串上的关系：ST～TS当且仅当S、T之间没有值的相互依赖（S、T为串）.设≈为包含～的自反传递闭包的最小等价关系，则索带C为串集合在≈划分下的等价类.直观上看，索带就是不存在值传递的串拼接的集合.每个索带都用中括号［］括起来，［］表示空索带.

协议角色与具体主体的对应通过为索带提供静态接口实现.设协议P的角色集合为A主体集合为定义Asi为增加静态接口操作：，其中为角色A中需要实例化的角色名，（A，B，…）称为A的静态接口.定义Sb为静态绑定操作：Sb（A，ρ，μ，…）=（）［］<ρ，μ，…>；Asi（A），其中ρ，μ，…∈<ρ，μ，…>；Asi（A）表示将Asi（A）中的角色名依次替换成<ρ，μ，…>中的具体主体名.静态绑定操作将静态接口中的抽象变量替换成具体值，使协议角色对应于具体主体.

协议P的一个运行R是P中角色发生消息交互的状态序列.一个初始状态可能产生不同的状态序列，因此可能产生不同的运行.索状空间包含了协议P所有角色之间消息交互的所有可能状态，从而包含了P的所有可能运行.状态的每次转换使得索带中的某个变量x被某个确定的项m替代，事件则为动作a中所有变量都被确定的项替代的结果.设A为协议P的角色，称为A在R中的轨迹，其中为作用在ai上且在R中发生的事件.直观理解，R|A表示了角色A在R中的局部运行.

PCL基于一阶逻辑与模态逻辑，以协议P的一次运行R为语义模型.该逻辑除了通常的一阶谓词公式外，还有一个描述主体行为的原子公式集以及模态算子.在此基础上，PCL提出了一系列依赖于主体动作的定理和推导规则，用于验证协议相关的安全性质.

2.3 PCL与ISL的相似性

PCL理论与ISL理论具有一定的相似性：

1.两个理论都属于安全协议逻辑证真法，基于Dolev-Yao攻击者模型对协议所有可能的运行进行推理，证明协议在无穷会话中的正确性，并且在推理过程中允许存在未完成的会话；

2.两个理论都无需对攻击者的行为进行显式的模型化和推理，而是将攻击者模型视为协议运行环境的一个因素；

3.两个逻辑的语义都很自然，不像BAN类逻辑［8-9］一样需要对协议进行非标准的理想化.

这些相似性使PCL和ISL存在着某些对应关系.在下一节中，我们将证明ISL的实例化空间语义模型可以完全解释PCL；但是，PCL具有一定的局限性，因此不能够完全解释ISL的语义，这将在第4节中进一步说明.

3 用实例化空间解释PCL

PCL以索状空间作为语义模型，ISL以实例化空间作为语义模型.因此，实现从PCL到ISL语义转换的前提是索状空间能够转换成对应的实例化空间.本节首先将索状空间中有关消息的概念对应到实例化空间的CME模型集合中，并将协议形式做相应转换，再为索状空间生成对应的实例化空间集合，最后实现两种逻辑语义模型的转换，证明由索状空间语义模型解释的PCL能够被实例化空间语义模型解释，将PCL的主要公式、定理、推导规则对应到ISL中.

3.1 由索状空间构建CME模型

3.1.1 从消息项到消息代数

直观上看，索状空间的项集包括协议所需的全体消息集，索状空间的密钥项集则对应消息代数中的密钥消息集，因此PCL的项集可以对应CME模型的消息代数.

3.1.2 构建CME模型

索状空间只描述主体动作之间的顺序关系，不考虑动作执行的具体时间，是一个相对抽象的模型；而实例化空间更为具体，需要描述主体行为的具体执行时间.因此，一个索状空间对应了无穷多个具体的CME模型.

证明：首先，每个Σ都是一个描述C中消息交换的CME模型：由定理1可知与构成了消息代数；黑客控制下的通信环境e由C的非诚实主体集构成；Ag对应的诚实通信主体集；Pk元组集合描述了中每个主体的公钥和对应的私钥；索状空间主要描述了公钥体制下的协议，在对称密钥体制下只对DH密钥进行了描述，因此主体间的共享密钥集Sk只包含DH密钥；索状空间未引入时戳的概念，因此标识信息集Label只包含随机数集Nonce；Nonce函数将每个主体映射到该主体通过新建动作产生的消息集，由于在索状空间中新建动作产生的项具有随机数的作用，因此Nonce函数可以看作是从每个主体到其产生的随机数集的映射，而且索状空间假定新建动作在主体执行协议前一次性完成，与CME模型中随机数在初始化过程中产生是一致的；Init将主体映射到其初始拥有的明文消息；Recv和Sent函数分别将主体映射到该主体通过接收动作和发送动作收到和发出的消息集.

其次，因为索状空间不描述主体行为的具体时间，所以CME模型中的t是任意的，所有满足定理2中条件的CME模型都描述了.因此一个索状空间C的消息交换对应了一个CME模型的集合.

备注1在索状空间对应的CME模型中，Sk和Label包含的内容都比原有的定义有所缩减，这证明CME模型比索状空间下的消息定义、交换等概念更具一般性.

3.2 协议形式的转换

索状空间与实例化空间对协议有着不同的形式化描述，索状空间下的协议形式能够转换到实例化空间下.设索状空间?描述了协议P，则有如下定理：

定理3的证明与定理2类似，在此不再详述.可以看到，转换后角色的共享密钥集只包含DH密钥.

3.3 从索状空间到实例化空间

1.R中存在静态绑定操作：Sb（A，ρ，…）=（）［］<ρ，…>；Asi（A）=（）［］<ρ，…>；（A，…）Create（A）；

3.设［a1…ai…an］A中发送动作和接收动作的个数为lA，则l

以上条件说明在R中ρ为扮演角色A的主体，c为ρ产生的随机数.可证明，P在实例化空间下的运行完全等价于在索状空间下的运行，并且（ρ，c）标识的局部运行等价于索状空间的R|A，lA为（ρ，c）标识的局部运行会话的长度.该证明方法与文献［10］中从串空间模型到智能体系统的转换类似，这里不再详述.

1.Σ属于索状空间C的消息交换对应的CME模型集合；

2.L是与协议P相关联的标识消息集（随机数集）；

3.F为协议P的所有角色在Σ下的实例化函数集合；

定理4是在之前几部分的理论基础上提出的.该定理说明，索状空间能够完全转换成实例化空间的集合.

3.4 语义模型的转换

协议组合逻辑PCL以P的某次运行R为语义模型：设尴为PCL中的公式，P，R|=尴表示尴在P的运行R中成立；实例化空间逻辑ISL以实例化空间Ω为语义模型：设φ为实例化空间逻辑中的公式，Ω|=φ表示φ在Ω模型中成立.

ISL公式的语义涉及到具体时间，我们用Ω，t|=φ表示在t时刻，φ在Ω模型中成立，其中t∈时间集合.

证明：Ω是实例化空间.根据实例化函数的假设，ρ∈Ag产生的随机数c最多只在协议的一次运行中使用.给定P的运行R，c是否在R中使用是可判的，所以F的子集必定是关于运行R的实例化函数集，因此每个都是与（P，R）对应的实例化空间.为解释PCL中的公式，需要指明实例化空间中对应公式的成立时间，所以引入时间点t.因此，{（，t）}是与（P，R）对应的实例化空间语义模型集合.

3.5 PCL公理系统在实例化空间中的语义解释

3.5.1 主要公式的语义解释

为描述公式的语义，PCL定义了两个谓词：EVENT（R，ρ，action）表示动作action在运行R中发生，由ρ执行；LAST（R，ρ，action）表示在运行R的最后阶段，有EVENT（R，ρ，action）成立.PCL的主要公式分为三类：

1.动作公式：New（ρ，m）、Send（ρ，m）、Receive（ρ，m）、Encrypt（ρ，m）、Sign（ρ，m）、Decrypt（ρ，m）和Verify（ρ，m）分别表示在协议运行的最后阶段，主体ρ进行了新建、发送、接收、加密、签名、解密、验证动作，相关项为m.

2.普通公式：Has（ρ，m）表示主体ρ在运行中拥有项m；Fresh（ρ，m）表达了新鲜性；Honest（ρ）表示在协议运行中ρ是诚实的；Contains（m，）表示为m的子项；Start（ρ）表示ρ还未执行任何动作；Source（m，ρ，，k）表示ρ之外的主体只能从中直接或间接地获得m，即ρ是项m的“源”；ψ∧尴、┐尴和埚x.尴与普通一阶逻辑中的对应公式含义相同；时态算子（◇尴和扌尴与线性时态逻辑LTL（Linear Temporal Logic）［11］中的时态算子含义相同，在运行的一系列状态中，前者表示尴在过去的某个状态下成立，后者表示尴在过去的所有状态下都成立.

3.模态公式：模态公式ψ［action］ρ尴表示在公式ψ成立且主体ρ执行了动作action的情况下，有尴成立.

这些公式在（P，R）模型下的形式化语义详见文献［4-5］，这里给出这些形式化语义在，t）模型中的语义对应关系（由于项实质上就是消息，在下文的描述中不再专门区分“项”和“消息”这两个概念）：

如果LAST（R，ρ，（vm））成立，则有P，R|= New（ρ，m），即主体ρ在R中新建了消息m，这与nonce（ρ，m）语义一致.根据实例化空间的假设，随机数在0时刻即生成，因此这里有t≥0.

如果LAST（R，ρ，）成立，则有P，R|= Send（ρ，m），即主体ρ在R中发送了消息m，这与sent（ρ，m）语义一致.

如果LAST（R，ρ，（m））成立，则有P，R|= Receive（ρ，m），即主体ρ在R中接收了消息m，这与recv（ρ，m）语义一致.

Encrypt（ρ，{m}k）和encr（ρ，{m}k）都表示主体ρ构造了加密消息.具体分析，若LAST（R，ρ，{m}k）成立，则ρ构造了加密消息，因此P，R|=Encrypt（ρ，{m}k）.在Ω'模型下，若ρ构造了加密消息{m}k表示{m}k∈Encr（ρ，t），因此有{Ω'，t}|=encr（ρ，{m}k）成立.反之亦然.

Sign（ρ，{m}k）和sign（ρ，{m}k）都表示主体ρ构造了签名消息{m}k.两者的语义关系与公式Encrypt和encr的关系类似.

Decrypt（ρ，{m}k）和decr（ρ，{m}k）都表示主体ρ能够对{m}k消息用k进行解密.具体分析，若LAST（R，ρ，（{m}k/{m}k））成立，则ρ能对{m}k进行解密匹配，因此P，R|=Decrypt（ρ，{m}k）.在模型下，若ρ拥有逆钥k，才可对{m}k解密，即若{m}k∈Poss（ρ，t）∧k∈Poss（ρ，t）成立，才有{，t}|=decr（ρ，{m}k）成立.两者语义相同.要注意的是，当Decrypt和decr公式中的消息不为{m}k形式时，两个公式都为假.

Verify（ρ，{m}k）和veri（ρ，{m}k）都表示主体ρ能够用密钥k验证签名{m}k.两者的语义关系与公式Decrypt和decr的关系类似.当Verify和veri公式中的消息不为{m}k形式时，两个公式都为假.

Has（ρ，m）和poss（ρ，m）都表示主体ρ拥有消息m.具体分析，Has成立的几种情况都可对应于poss成立的情况：

（3）若P，R|=Has（ρ，m1）∧…∧Has（ρ，mn）∧（m=［m1，…，mn］），或有P，R|=Has（ρ，∧Has（ρ，k）∧（m={}k），则P，R|=Has（ρ，m）.即m可由主体ρ对已知的消息进行加密或联合得到，并且该嵌套过程从情况（1）开始.对应到模型下，与情况（2）类似，有m∈cl（Init（ρ）∪Recvs（ρ，t）），即{，t}|=poss（ρ，m）成立.反之亦然.

Fresh（ρ，m）表示若ρ曾新建消息m，或曾新建且m=g（），且ρ未发送包含m的消息，则m为新鲜的.因此在Ω'模型下有以上对应.我们没有使用ISL的新鲜性公式fresh直接对应PCL下的新鲜性，是由于CME模型的Fresh函数包含了更多的情况（如当消息m是新鲜的，则包含m的加密消息也是新鲜的），因此fresh（ρ，c，m）比Fresh（ρ，m）描述了更一般的情况.

10.对于Honest（ρ），如果主体ρ是诚实主体，则有P，R|=Honest（ρ）.在模型中，没有将该谓词对应成公式，而是作为假设，假定Ag集合中都为诚实主体.

δ尴表示通过置换δ替换公式尴中的所有自由变量得到的新公式.由于实例化空间逻辑中的公式不考虑自由变量，也没有置换的概念，因此δ尴在P，R中为真相当于尴在模型中为真.

18.由于实例化空间逻辑ISL的公理系统基于一阶逻辑，因此PCL的合取公式、非公式和存在公式语义与ISL中相同.

3.5.2 主要定理的语义证明

下面证明PCL的定理在实例化空间解释下也是成立的.定义：

首先给出PCL中与主体动作相关的定理（表1）的语义证明：

表2 PCL主要基本定理

定理ORIG表示当ρ产生随机数m时，ρ也拥有消息m.

定理REC表示当ρ收到消息m时，ρ即拥有m.

定理ENC表示当ρ拥有消息m和密钥k时，ρ也拥有加密消息{m}k.

定理PROJ表示当ρ拥有组合消息时，ρ也拥有其中的子消息.

定理DEC1表示当ρ拥有加密消息{m}k和密钥k时，ρ也拥有原来的消息m.因为前提条件说明ρ有能力构造{m}k，所以ρ自然也知道未加密之前的消息.

定理DEC2表示若ρ能够对{m}k解密，则必定知道m，因为m是对{m}k解密的结果.

定理SEC说明诚实主体不会窃取其它主体的私钥，因此只能对用自身公钥加密的消息解密.

10.定理VER在实例化空间中成立.因为t

定理N1表示每个随机数只能由一个主体产生.在实例化空间中，这个定理的成立由CME模型的假设保证.

定理CON表示组合消息包含了其中的每个子消息.

PCL中还有一系列与DH密钥假设相关的定理（表3），对于其中描述的性质，实例化空间中也有对应的解释：

1.定理DH 1在实例化空间中成立.因为若Compute（ρ，）成立，根据该公式的语义，可得在实例化空间中有∈Computes（ρ，t）.又根据Poss函数的定义，可得∈Poss（ρ，t），即|=poss（ρ，）.

表3 PCL中DH假设相关定理

PCL中存在时态算子，因此还提出了一系列与时序相关的定理来描述主体动作间的顺序关系.而实例化空间模型描述了主体行为的具体执行时间，因此，我们可以利用语义模型集合{（，t）}中时间t的大小关系给出与这些定理相应的描述.这部分定理与普通线性时序逻辑中的定理类似，这里不再详述.

3.5.3 推导规则的对应

PCL的推导规则分为三种：

1.通用规则

与∧，圯等一阶逻辑连接符相关的推导规则.如：

等.实例化空间逻辑ISL基于一阶逻辑，因此也有对应的通用规则.

2.顺序规则

提供了顺序合并动作的规则：

在ISL中，此规则等价于（┐ψ∨覫）∧（┐ψ∨φ）圯（┐ψ∨φ），这可由一阶逻辑的性质推出.

3.保持规则

描述了主体执行某些动作后，谓词的真值是否能保持的规则.具体分析，New（ρ，m）、Send（ρ，m）、Receive（ρ，m）、Decrypt（ρ，m）、Verify（ρ，m）、Has（ρ，m）等公式一旦为真，则无论主体再执行什么动作，这些谓词仍然为真；而对于Source（m，ρ，k）和Fresh（ρ，m），接收、新建、匹配动作能够保持其真值，但对发送动作有限制.以Source（m，ρ，，k）为例，若ρ执行<>，则要求m芫，Source才能保持真值.因为若m哿，ρ执行<>后将泄漏m，m不再唯一由{}k解密得到，Source（m，ρ，，k）的值将为假.而对于Fresh（ρ，m），只要主体ρ发送了包含m的消息，则Fresh（ρ，m）的值就变为假.由前面定理的语义转换，不难推出ISL也有类似的保持规则.

4 PCL与ISL关系的进一步讨论

我们已经证明，PCL的语义能够完全被实例化空间模型解释.但是，ISL的描述能力强于PCL，因此现有的PCL不能完全表示ISL.具体体现在以下几个方面：

首先，PCL主要用来验证公钥加密体制下协议的认证性和秘密性，也成功地验证了许多应用协议.例如，在文献［4］中，该逻辑被用于模块化地验证一组密钥交换协议集合；在文献［12］中，Kerberos V5协议通过PCL得到了验证；在文献［13-15］中，PCL被用于验证无线网络与移动网络中的安全协议；文献［16］着重分析了PCL的组合证明方法.但是，PCL在对称密钥体制下只对DH密钥进行了描述，只有对PCL作适当扩充，该逻辑才能够完整地验证共享密钥加密体制下的协议.而ISL可以灵活地在公钥、私钥、共享密钥（包括动态生成的会话密钥，如DH密钥等）和hash密钥等加密系统中推导协议性质，其自动化工具SPV已经被成功地应用到Kerberos协议、SET协议等工业级协议的验证上［1，6-7］.

其次，ISL的定理比PCL中的定理更具有一般性.例如，根据PCL中Source谓词的定义，如果一个加密随机数的产生者发送了两个以上的包含该随机数的消息，PCL将不能推导出该随机数的来源.而实例化空间逻辑的（1，0）-Secrecy定理则没有这种限制：假设主体ρ产生了一个随机数c，并分别用主体ρ1和ρ2的公钥k1和k2进行加密，发送{c}k1和{c}k2，那么当ρ收到随机数c时，由（1，0）-Secrecy定理可以推出said（ρ1，c）∨said（ρ2，c）（ρ1对{c}k1解了密，或ρ1对{c}k2解了密）.另外，PCL只支持一对一的消息交换，而ISL的（n，1）-Secrecy定理能够描述多个主体对一个主体的消息交换.

第三，PCL只描述了主体的诚实性，不能表达实例化空间中的主体行为假设集譓.

5 相关研究工作

索状空间模型是在串空间模型［17］的基础上发展改进而来的，因此PCL验证法在分析安全协议时与串空间模型验证法比较相似［18］，只是前者还加入了逻辑推理的内容，其公理和推导规则又与协议的每一步执行动作相关；而ISL验证法是一个知识推理的多智能体系统.Halpern和Pucella比较完整地对串空间模型与多智能体系统进行了比较［10］，并尝试将两者互相转换，但文中讨论的情况比较简单和抽象，对于具体、复杂的安全协议验证逻辑之间关系的研究工作，目前还比较缺乏.本文将这两个复杂的具体逻辑进行具体比较和语义转换，得出的结果具有一定的实用性.

Cremers等给出了普通安全协议的一个通用的形式化的操作语义［19］.在该操作语义下，能使用模型检测工具检验安全协议的秘密性，却不能检验安全协议的认证性［20］.如果找出实例化空间语义模型与安全协议通用操作语义的对应关系，并实现安全协议的操作语义在实例化空间下的完全表示，将从理论上更进一步说明实例化空间语义模型具有足够强的表示能力描述安全协议.另一方面，通过语义模型的转换，将使原形式下的安全协议能够直接利用SPV进行认证性等重要安全性质的自动验证.

结束语实例化空间逻辑ISL与协议组合逻辑PCL是两种有效的安全协议形式化验证方法.为了在理论上衡量与评价ISL的语义表达能力，给出了PCL在ISL语义模型下的语义解释，并且说明现有的PCL不能够完全表示ISL的语义，这种单向的语义对应关系证明ISL的公理集比现有的一些安全协议验证逻辑刻画了更一般的情形，具有较强的语义表达能力.把PCL的语义转化到ISL语义模型下，还使得用PCL理论验证的协议能够利用ISL的自动化验证工具SPV进行自动验证.另外，新语义模型下的PCL也将更容易扩展.

下一步的工作将着眼于以下几个方面：首先，经过语义转换后，PCL下的协议可以使用SPV进行自动验证，但是语义转换的过程目前只能用手工实现，为提高分析效率，可尝试开发相应的自动化语义转换工具.其次，将对ISL与其它相关工作进行比较，剖析它们之间的联系和优缺点，从而进一步扩充ISL，使其具有更强的语义表达能力.另外，改进PCL，如消除PCL中公式对主体动作的依赖等，使其能够完全表示ISL的语义，达到两种逻辑的一一对应，也是未来的工作方向.

［1］苏开乐，岳伟亚，陈清亮，等.实例化空间:一种新的安全协议验证逻辑的语义模型［J］.计算机学报，2006，29（9）:1657-1665.

［2］Xiao Yinyin,Su Kaile.The DH exponentiation extension in a verification logic of local sessions［C］//CSAE 2012,Zhangjiajie:IEEE CPS,2012:499-503.

［3］薛锐,冯登国.安全协议的形式化分析技术与方法［J］.计算机学报,2006,29（1）:1-20.

［4］A.Datta,A.Derek,J.C.Mitchell,el al.A derivation system and compositional logic for security protocols［J］. Journal of Computer Security,2005,13:423-482.

［5］A.Datta,A.Derek,J.C.Mitchell,el al.Protocol composition logic（PCL）［J］.Electronic Notes in Theoretical Computer Science,2007,172:311-358.

［6］肖茵茵,苏开乐,马震远,等.实例化空间逻辑下的SET支付协议验证及改进［J］.华中科技大学学报, 2013,41（7）:97-102.

［7］肖茵茵,苏开乐,岳伟亚,等.SET证书申请协议在SPV下的自动化验证及改进［J］.计算机学报, 2008,31（6）:1035-1045.

［8］Burrows M,Abadi M,Needham R.A logic of authentication［J］.ACM Transactions on Computer Systems, 1990,8（1）:18-36.

［9］M.Abadi,M.R.Tuttle.A semantics for a logic of authentication［C］//Proceedings of the Tenth Annual ACM Symposium on Principles of Distributed Computing,1991:201-216.

［10］Joseph Y.Halpern,Riccardo Pucella.On the relationship between strand spaces and multi-agent systems［J］.ACM Transactions on Information and System Security（TISSEC）,2003,6（1）:43-70.

［11］Zohar Manna,Amir Pnueli.The Temporal Logic of Reactive and Concurrent Systems:Specification［M］. Springer-Verlag,1992.

［12］A.Roy,A.Datta,A.Derek,et al.Secrecy analysis in protocol composition logic［C］//Proceedings of 11th Asian Computing Science Conference,Tokyo,Japan: Springer,2006,4435:197-213.

［13］郭显,冯涛,袁占亭.协议组合逻辑安全的Ad Hoc网络路由协议安全验证方法［J］.小型微型计算机系统,2013,34（12）:2794-2799.

［14］王丽丽,冯涛,马建峰.协议组合逻辑安全的4G无线网络接入认证方案［J］.通信学报,2012,33（4）: 77-84.

［15］C.He,M.Sundararajan,A.Datta,et al.A modularcorrectness proof of IEEE 802.11i and TLS［C］//ACM CCS 2005:2-15.

［16］鲁来凤.安全协议形式化分析理论与应用研究［D］.西安:西安电子科技大学,2012.

［17］F.J.Thayer Fabrega,J.C.Herzog,and J.D.Guttman. Strand spaces［R］.The MITRE Corporation,November, 1997.

［18］皮建勇,杨雷,刘心松,等.一种新的安全协议及其串空间模型分析［J］.计算机科学,2010,37（1）:118-121.

［19］C.J.F.Cremers and S.Mauw.Operational semantics of security protocols［M］.Springer-Verlag,2011.

［20］Cremers C,Mauw S.Checking secrecy by means of partial order reduction［C］//The 4th System Analysis and Modeling Workshop.Berlin:Springer,2004:177-194.

［责任编辑：刘向红］

Semantic Interpretation of Protocol Com positional Logic in Instantiation Space M odel

XIAO Yin-yin1，2，SU Kai-le2，3
（1.Department of Computer Science,Guangdong Polytechnic Normal University,Guangzhou 510665,China；2.Guangdong Province Key Lab for Information Security,College of Information Science&Technology, Sun Yat-Sen University,Guangzhou 510275,China；3.College of Mathematics,Physics and Information Engineering,Zhejiang Normal University,Jinhua 321004,China）

The verification of protocols is an undecidable problem.In order to evaluate the semantics expressive ability of Instantiation Space Logic（ISL）theoretically,another practical protocol logic called Protocol Compositional Logic（PCL）was chosen,and the relationship between ISL and PCL was analyzed.Based on the relationship,the PCL semantic model called Cord Space was changed into the ISL semantic model,and themain formulas,axioms and inference rules of PCL were interpreted in Instantiation Space.The research shown that the Instantiation Space could express the semantics of PCL completely,and the expressive ability of ISL was stronger than that of PCL.The new interpreted PCL could be extended more easily,and those security protocols described in PCL could be verified by Security Protocol Verifier（SPV)of ISL automatically.

Security protocols analyzing；Instantiation space；Protocol compositional logic；Cord space；Semantic interpretation

TP 301.2

B

1672-402X（2016）02-0008-12

10.13408/j.cnki.gjsxb.2016.02.003

2015-11-11

国家自然科学基金（60903054，61379019），国家“973”重点基础研究发展计划资助项目(2010CB328103)，中国博士后科学基金面上项目（2013M540704），广东高校优秀青年创新人才培育项目(LYM11085，LYM11084)资助.

肖茵茵（1983－），女，广东梅州人，博士，广东技术师范学院讲师，研究方向：电子商务、网络安全、安全协议验证、形式化方法.

苏开乐（1964－），男，湖南长沙人，博导，暨南大学教授，研究方向：数理逻辑、形式化方法.