基于事件逻辑的WMN客户端与LTCA认证协议安全性分析

2019-06-26肖美华李娅楠宋佳雯王西忠钟小妹

计算机研究与发展 2019年6期

肖美华李娅楠,2 宋佳雯王西忠李伟钟小妹

1(华东交通大学软件学院南昌 330013)2(中国铁建重工集团有限公司长沙 410100)

网络发展给世界带来巨大变化，人们的日常生活离不开信息科技.信息在安全信道传输会遇到各种攻击，如消息窃听、消息拦截、消息篡改[1]等.网络安全问题是全球性问题，2017年3月，维基解密(WiKiLeaks)公布数千份资料，其中揭秘一些黑客入侵事件[2]，不法组织不仅入侵iPhone手机、Android手机、智能电视，还攻击操作系统获取机密文件,甚至控制智能汽车发起暗杀活动[3].同年5月，在全球范围内爆发“WannaCry”比特币勒索病毒，结合蠕虫方式[4]进行传播，利用MS17-010漏洞向用户的445端口发送数据包，远程执行代码后加密用户文件，并释放一个压缩包，压缩包中文件隐藏释放到本地目录，文件中毒后被加密锁死.对150多个国家和地区、10多万组织和机构以及30多万网民产生恶劣影响，损失高达500多亿人民币.

无线Mesh网(wireless mesh network，WMN)[5-6]拥有固定且电源充足的主干路由器，设计时不需要考虑太多能耗和移动性问题，适合投放于覆盖大面积开放区域.认证技术[7]在有线网络中比较成熟，但是在无线网络中由于存储设备、带宽等限制因素使其发展相对困难，无线网络面临比常规有线网络更严重复杂的威胁，如何构建合理的WMN认证体系很是关键.认证是安全通信的基础，通过机密消息对移动节点身份进行认定，只有经过认证的节点才能访问网络资源[8].

形式化方法通过严格数学概念和逻辑方法对协议进行描述，语义清晰、无歧义，可以发现其他方法不易被发现的网络安全协议漏洞[9].定理证明描述并发与分布式系统，是一种协议和算法的逻辑，侧重协议正确性，难以自动化[10].定理证明将协议描述为公理系统，协议安全目标表示需要证明的定理，协议是否满足安全目标对应于公理系统中目标定理是否成立，可用于无限状态空间协议正确性证明[11].事件逻辑(logic of events theory， LoET)[12]是定理证明的一种逻辑方法，用来刻画加密协议在交互过程中的消息动作.肖美华等人[13-15]合作运用事件逻辑理论对安全协议进行形式化分析工作，克服协议组合逻辑PCL在协议分析过程中存在的不足.

1 WMN客户端与LTCA认证协议

轻量级动态容侵证书授权中心(lite and tolerate certificate authority, LTCA)认证机制结合门限密码思想与轻量级公钥体制[8]，并支持WMN基础设施，相较于MANET及WSN的节点资源丰富[16].

本文在研究通信双方交互过程中进行5点假设：

1) 随机数是新鲜的，移动用户不生成相同随机数；

2) 以多跳形式经过中间转发的用户节点忽略不计；

3) 不存在任何值得注意的网络延迟现象；

4) 无线网络环境包括非法Mesh客户端在内所有用户均可窃取传输信息；

5) 本文所涉及的用户特指本地用户.

WMN客户端与LTCA间认证协议满足5点:

1) 用户或节点的私钥由自己生成，节点主要指负责认证的服务器[17].

3) LTCA.由1组Mesh网认证服务器组成(MASs是WMN中负责认证的Mesh路由器)，负责WMN中用户MU的初始化，将MU主公钥与身份IDMU由LTCA私钥SKLTCA绑定签名生成辅公钥，对WMN异地用户进行身份认证(此部分不做研究)[8].

结合协议假设和满足条件，当本地用户MU与其他用户通信时，WMN客户端与LTCA间双向认证协议详细过程如图1所示：

LTCA→MU:{RLTCA}

Fig. 1 Two-way authentication between user and LTCA
图1 用户与LTCA双向认证

1) LTCA→MU.LTCA在收到用户MU请求时，生成随机数

LTCA

，然后发送给用户MU.

WMN客户端MU与LTCA之间确定双向认证可信性，具体交互过程如图2所示：

Fig. 2 Two-way authentication description图2 双向认证描述

2 事件逻辑理论

2.1 事件逻辑

事件逻辑对安全协议基本原语进行形式化规约，在协议研究中建立包含地址和事件的模型来证明协议安全属性，信息以多种形态存储在地址中，以消息形式在不同地址间进行传递.通过事件逻辑理论验证加密协议安全性，定义事件逻辑方法的布尔值(B)、标示符(Id)、原子(Atom)，其中原子表示随机数、签名、密文以及加密密钥等不可预测数据[9].定义事件、事件类以及事件结构构建认证理论，对协议强认证性质进行证明.

2.1.1 基本定义

1)Atom类型

Atom类型表示保密信息，其成员用atoms表示，atoms是不可预测的.Atom类型成员是基本元素，没有结构且不能被生成.Atom类型用来评价规范形式tok(a),tok(b),…,记为tokens，其中a,b,…为其中参数.

置换规则.事件逻辑中对任意判断J(a,b,…),其中a,b,…为有限集，则J(a′,b′,…)的真值过程a|→a′,b|→b′,…是一个置换.

2) 独立性

事件逻辑理论中定义(state aftere)为事件e发生后主体出现的状态，事件e本质是一个空间或时间点.

(x:T‖a)表示T类型元素不包含原子a，当x属于T类型时，x‖a表示x和a独立，即T类型的x独立于a.

3) 事件结构

分布式计算的形式化模型可定义分布式系统的运算以及认证[9]，在运算中，e,events等消息是在迁移的，其中信息交互初始阶段为info(e).事件集是信息在一些存储位置(如主体在事件发生时进程、线程)中事件出现的空间时间点.事件在单个位置时间点没有重叠，是整体序.无论如何迁移(消息传递、消息共享)，事件各主体间均会产生因果序.

计算系统语义通过事件结构语言描述，事件语言是任何语言的扩展.E,loc,<,info即事件序(event-ordering)，其中loc是事件E上的函数，<是事件E的一个因果关系，是一个本地有限集.事件包含有限个前驱.e∈E,loc(e)是事件存储单元，info(e)表示事件发生时将消息交付给本地loc(e).e1

认证协议交互信息包括随机数、签名以及名字等元组信息，可以转化为

Data≡defTree(Id+Atom).

事件结构中事件语言建模时需满足：

① ≤表示局部有限偏序(每个事件e包含有限个前驱)[10]；

②e1

③ 认证理论中，loc(e)的位置是事件e发生的主体，对一些标示符X来说loc(e)=X；

④ 协议安全性证明中e′

事件逻辑为消息自动机提供健全语义，消息可靠发送包含named,fifo,link，每一条信息都有关联标签，是头信息.事件包含类型、价值，收到的信息在linkl包含tagtg，是类型为rcv(l,tg)的事件e.消息类型依靠(link,tag)来判断，例如sender(e)

事件e发送消息独立于原子a，sends(e)‖a即∀e′:E.(isrcv(e′)∧sender(e′)=e)⟹val(e′)‖a.

2.1.2 加密系统建模

1) 随机数n(nonce)

主体i通过虚服务si对主体生成随机数能力进行模型构建，该服务用来构建si到i的连接li以及i到si的连接li，记录在无重复包含指针的列表ats内.主体i需要随机数时在连接li发送一个包含随机数的请求消息，通过si收到的请求消息在E(Noncei)中生成事件n响应，即Noncei(n)，其中主体atoms在ats中是独立的.

域E(Noncei)中，若随机数n∈E(Noncei)和事件e满足n≤e⟹(val(e)‖Noncei(n))，则从events到atoms中偏序函数Noncei属于随机数交互，即除非事件在随机数生成后与之产生因果，否则其值不包含该随机数.

2) 事件类(event class)

事件逻辑理论中，通过事件对协议进行分类描述，使用事件序语言、事件类对协议进行构建.T类型事件类从事件到T类型值是简单的偏函数，如果X是一个事件类，则规定E(X)是X范围内的事件集，E(X)中事件属于类X.对于事件e∈E(X)，X(e)是类X分配给e的T类型值.

一个事件类可以是任何不同事件类中的成员，如果Y是类型T′的事件类，f是T→T′的函数，那么X(v)⟹Y(f(v))等价于∀e.e∈X(v)⟹e∈Y(f(v)).

若随机数n∈E(Noncei),事件e∈E(X)没有关联，则(loc(e)≠si⟹X(e))‖Noncei(n).

类中事件转换成原子X类中事件e信息包含原子a，则：

X(e) hasa≡def(e∈∃(X)∧(X(e):T‖a)).

认证协议包含发送、接收、随机数、签名、认证、加密、解密7类事件[10]，事件类对应相关信息，信息类型取决于事件类，事件类中相关信息包含原子，基于7类事件类的形式化身份认证理论的类型列表具体定义如图3所示：

Fig. 3 Event classes of the authentication theory
图3 认证理论的事件类

在图3中，类Sign,Verify中事件类型相同，均为三元组Data×Id×Atom，其中类Sign,Verify为signed(e),signer(e),signature(e).事件类型在类Encrypt,Decrypt中为三元组Data×Key×Atom，即encrypted(e),key(e),ciphertext(e).

对于e∈E(Sign)，事件信息Sign(e)=x,A,s表示事件e是主体A对密文x进行签名生成s.如果A是诚实主体，则loc(e)=A，诚实主体不会释放私钥.对于事件e′∈E(Verify)，该事件信息与签名信息相对应即Verify(e′)=x,A,s表示事件e′是主体B=loc(e′)成功验证主体A签名生成的密文x.

事件e∈E(Encrypt),Encrypt(e)=x,k,c表示事件e是主体A通过密钥k对明文x加密生成密文c，主体A拥有密钥k和消息x.事件e′∈E(Decrypt)中,Decrypt(e′)=x,k′,c表示事件e′是主体B通过密钥k′解密密文c生成明文x的过程.密文c生成时，对应解密公理AxiomD中存在一个匹配密钥.

2.2 事件逻辑公理、推论及性质

2.2.1 事件逻辑公理

对称密钥和私钥作为标示符是不可测的，两者并不相同，Key类型为Key≡defId+Atom+Atom.

事件逻辑中PrivKey函数的主体包含原子，MatchingKeys函数构建密钥间的关系，如图4所示：

事件逻辑公理[9]包含密钥公理、诚实公理、因果公理、不相交公理、流关系，具体为

1) 密钥公理(key axiom,AxiomK)

密钥公理(AxiomK)的匹配密钥间是对称的，密钥信息是主体特有，不同主体不会拥有相同私钥.主体A私钥仅能够与自身公钥匹配，具体表示为

∀A,B:Id.∀k,k′；Key.∀a:Atom
MatchingKeys(k;k′)⟺MatchingKeys(k′,k)∧
MatchingKeys(Symm(a);k)⟺k=Symm(a)∧
MatchingKeys(PrivKey(A);k)⟺k=A∧
MatchingKeys(A;k)⟺k=PrivKey(A)∧
PrivKey(A)=PrivKey(B)⟺A=B.

2) 诚实公理(honest axiom,AxiomS)

事件逻辑理论包含函数Honest：Id→B对诚实主体进行断言，诚实主体私钥不会释放，主体签名、加密以及解密事件均发生在诚实主体上，通过AxiomS对诚实主体性质刻化为

3) 因果公理(causal axioms)

因果公理是对事件类中接收事件Rcv、验证事件Verify、解密事件Decrypt所对应事件公理(接收公理AxiomR、验证公理AxiomV、解密公理AxiomD)关系的整合.AxiomR,AxiomV相似，任何接收或验证事件发生前存在一个与之相应且信息内容相同的发送或签名事件[10]，具体为

AxiomR:∀e:E(Rcv).∃e′:E(Send).(e′Rcv(e)=Send(e′).
AxiomV:∀e:E(Verify).∃e′:E(Sign).(e′Verify(e)=Sign(e′).

AxiomD与AxiomR和AxiomV相似，解密事件主体在事件发生前收到一个与之密钥匹配、其他信息相同的加密事件,具体表示为

∀e:E(Decrypt).∃e′:E(Encrypt).
e′plaintext(e)=plaintext(e′)∧
ciphertext(e)=ciphertext(e′)∧
MatchingKeys(key(e);key(e′)).

4) 不相交公理(disjointness axioms)

2个原子间不相交假设主要考虑2方面.一方面任意这7个事件类不在其他类中，即：

ActionDisjoint:∃f:E→Z.∀e:E.
(e∈E(New)⟹f(e)=1)∧
(e∈E(Send)⟹f(e)=2)∧…∧
(e∈E(Decrypt)⟹f(e)=7).

另一方面主体生成的随机数n与主体所持有的私钥、签名或密文不相同，且三者间不相交[18].签名可以是明文通过散列加密生成，而密文是明文加密生成，Data类型成员在散列加密后不等同于Data类型成员，那么签名不等价于密文，具体表示为

∀n:E(New).∀s:E(Sign).∀e:E(Encrypt).∀A:
Id.New(n)≠signature(e)∧New(n)≠
ciphertext(e)∧New(n)≠Private(A)∧
ciphertext(e)≠Private(A)∧
signature(s)≠Private(A)∧
signature(s)≠ciphertext(e).

5) 流关系(flow relation)

流关系是随机数因果序事件间的关联.Act类型包含7个事件类，记作actions.(ehasa)为真当且仅当action类型的e中包含a，具体表示为

ehasa≡def(e∈E(New)∧New(e) hasa)∨
(e∈E(Send)∧Send(e) hasa)∨
(e∈E(Rcv)∧Rcv(e) hasa)∨…

1)a从动作e1到动作e2发生在同一主体上；

2) 介于发送事件和接收事件间以明文发送a；

3)a在加密事件明文中，密文流向一个与之匹配的解密事件[18]，具体流关系递归为

6) 随机数公理(nonce axiom,AxiomF)

随机数公理记为AxiomF，包含3部分AxiomF1,AxiomF2,AxiomF3，其中AxiomF1关于流性质，应用在事件关联的随机数中，具体为

AxiomF2,AxiomF3介绍签名、密文以及包含2类事件的相关关系，没有规定签名或密文与特殊事件有关.如果一个动作包含签名或密文，则可以推断出具有相同信息的签名或加密动作[10]，具体为

2.2.2 事件逻辑引理及性质

基本序列是协议动作的参数列表，参数是主体标识符，由2个及以上组成[9].遵守协议的主体参与到多个线程，线程是协议基本序列实例且遵守协议[10].

引理 3.随机数引理.

协议Protocol(bss)是合法的，主体A是诚实主体且遵守Pr，线程thr是基本序列bss的一个实例，n=thr[j],n∈E(New),e=thr[i]和j

在协议强认证证明过程中，规定被证明协议合法，线程thr1相邻事件e0,e1不存在发送动作(或任何的动作发生)，由随机数引理可得，事件e1发生前随机数不会被释放.

安全协议形式化分析过程中，诚实主体在执行相关动作时需要满足5个性质[19]：

性质1.多组合信息交互.

诚实主体A本身持有可信第三方(trusted third party,TTP)授权且遵守协议Protocol(bss)，在认证过程中需要通过TTP授权进行验证，这属于诚实主体自身行为,即:

∀A:Id.∀e,e′:E(e)∈TTP∧(e∀e′:A|≡E[e].

在验证协议交互过程安全性问题中可以省略该证明，从而降低证明过程中的复杂度.

性质2.不叠加.

协议分析过程中，对于在匹配会话中已经验证过的动作，在新一轮的验证过程中可以直接引用验证结果来减少冗余.

∀A:Id.∀e1,e2:e1

性质3.事件匹配.

在7种事件类中，在遵守协议Protocol(bss)的前提下发起者主体A、响应者主体B(事件响应者可以不是相同的主体)必须参与的事件类是双方的或者多方的，从而保障事件发生的有效性.

∀A,B:(A≠B).∀e1,e2:((e1∈A,e2∈B)∧
(e1Verify(e2)∨Decrypt(e1)=Encrypt(e2).

性质4.去重复性.

在验证事件匹配的过程中，如果出现多个事件需要同时进行验证，则依据从上到下的原则进行验证来减少验证过程中的重复操作.

性质5.去未来性.

在考虑匹配动作的过程中，以当前已发生事件为基准，对于之后没有发生的动作不予考虑来减少验证过程中的不必要进程.

2.3 形式化方法描述协议

1) 线程

线程是动作在单个位置的有序列表，满足：

Thread≡def{thr:ActList|∀i:thr[i]

thr1≼thr2表示线程thr1是线程thr2前面发生的一个相邻线程，定义thr1≃thr2为

thr1≼thr2∨thr2≼thr1.

线程消息是线程中发送和接收动作的集合，即：

isMsg(e)≡defe∈E(Send)∨e∈E(Rcv)，
messages(thr)≡deffilter(isMsg,thr).

对于消息s和r，s是发送消息，r是接收消息，s和r间传递消息相同，则2条信息间是一个弱匹配关系，即s～r；如果s与r之间有直接因果关系，s发生在r之前，则s和r之间是一个强匹配关系，即为s|→r，具体为

s～r≡defs∈E(Send)∧r∈E(Rcv)∧
Send(s)=Rcv(r)，
s|→r≡defs～r∧s

2) 基本序列(basic sequence)

基本序列是协议动作的基本参数列表,在协议主体A,B参数是标示符，主体A遵守协议，参与协议多个线程，线程是协议中的实例，与主体B在不同位置进行交互[19].事件逻辑中所研究的协议允许多个主体参与.

基本序列是2个位置与一个线程的联系，当线程是基本序列给定的位置参数，则这个关系为真，基本序列类型成员为

Basic≡defId→Id→Thread→P.

注：其中P代表命题(proposition),在命题逻辑结构中跟布尔运算是不同的.

基本序列实例可以生成随机数、签名等，参数原子是在序列在关系中量化存在.线程thr是主体A中已知基本序列关系bss，记作thr=oneof(bss,A).关系inoneof(e,thr,bss,A)作为协议形式化定义，记作：e∈thr∧thr=oneof(bss,A).

3) 匹配会话及协议动作

① 匹配会话

线程thr1和thr2构成长度为n的匹配会话，如果它们至少包含n个消息，当每个线程中前n个消息成对，每对m1,m2满足m1|→m2∨m2|→m1，则构成强匹配会话，即为如果每对m1,m2只满足m1～m2∨m2～m1，得到一个弱匹配会话，记作

② 协议动作

使用基本协议动作描述协议ProtocolAction类来定义协议动作.所有成员类包含标签tag和值value，ProtocolAction类成员包含7种动作，定义如下：

{New(a)|a∈Atom}；
{Send(x)|x∈Data}；
{Rcv(x)|x∈Data}；
{Sign(t)|t∈Data×Id×Atom}；
{Verify(t)|t∈Data×Id×Atom}；
{Encrypt(t)|t∈Data×Key×Atom}；
{Decrypt(t)|t∈Data×Key×Atom}.

协议动作pa(protocol action)对应事件e，则：

e∈E(New)∧pa=new(New(e))∨
e∈E(Send)∧pa=send(Send(e))∨…

4) 事件逻辑方法描述协议

① 定义协议

事件逻辑理论使用Basic类型的基本序列关系表bss定义一个协议[10].协议是在存储位置的断言，类型为Id→P.

协议Protocol(bss)定义为

λA.∀e:Act.loc(e)=A⟹
(∃thr.inOneof(e,thr,bss,A))∧
∀thr1,thr2.(inOneof(e,thr1,bss,A)∧
inOneof(e,thr1,bss,A))⟹thr1≃thr2.

主体A动作是基本序列的实例成员，如果动作是一个或多个实例成员，则实例是兼容的.

② 认证

主体A,B为诚实主体且遵守协议，主体A发起一个会话序列，主体B的一个应答序列与之构成合法匹配会话.类似地，如果主体B执行全应答序列的一个实例，那么有一个和主体A的匹配会话，即接收消息和相匹配的发送消息内容一致[10].消息双方完成身份认证保证不会有攻击者借助之前拦截消息进行伪装会话攻击，匹配会话过程满足强匹配，协议Pr中基本序列bs认证n个消息，认证过程满足：

prauth(bs,n)≡def∀A,B.∀thr1.
(Honest(A)∧Honest(B)∧Pr(A)∧Pr(B)∧
A≠B∧loc(thr1)=A∧bs(A,B,thr1))⟹
∃

2.4 安全协议证明过程

事件逻辑理论描述协议强认证性质，具体如图5所示：

Fig. 5 The flowchart of event logic method which proves the protocol authentication 图5 事件逻辑方法证明协议认证性流程图

1) 定义基本序列

利用事件逻辑理论方法对安全协议进行形式化描述，定义发起者、响应者序列的具体动作[9]，规范协议基本序列，确认满足协议安全性需要证明的强认证性质.

2) 对强认证性质的单向进行证明

规定主体不同是诚实的且遵守协议，假设某一线程为协议基本序列的实例，定义线程上的动作，确定协议匹配事件.分析匹配事件，确认是否存在匹配会话以及匹配会话内部是否含有需要进一步证明的匹配事件.

3) 确定匹配事件，进行排除分析

查询相关匹配事件是否符合匹配会话，如果符合则进行由内而外对相关匹配会话的证明；如果不符合则进行下一轮匹配事件的筛选证明，确认整个匹配事件是否满足弱匹配.

4) 确认强认证性质

确认匹配会话属于弱匹配，分析协议交互过程的匹配会话长度，根据相关公理确认强匹配会话.

5) 单向证明成立后，进行双向强认证性质证明

如果证明成立，则说明协议是安全的；在整个证明过程中，如果一边的匹配事件不能满足弱匹配，说明协议同样不满足强认证性质，在认证阶段不能达成双向身份认证，协议易被攻击者伪装身份进行攻击，存在消息重放的可能，协议主体不安全[10].

以流程图的方法简化事件逻辑理论证明协议安全性.

3 事件逻辑理论证明WMN客户端与LTCA认证协议

通过事件逻辑理论对WMN客户端与LTCA双向认证协议进行基本序列排序，定义I1,I2,I3为发起方在协议交互过程中产生的基本序，R1，R2，R3为协议响应者在协议交互过程中产生的基本序.LTCA作为协议交互过程中动作发起方(initiator)，用户MU作为协议交互过程中动作响应方(res-ponder),协议具体描述如图6所示.

Fig. 6 Basic sequence description of two-way authentication图6 双向认证基本序列描述

基于事件逻辑理论定义协议满足安全性需要满足的身份认证性质，验证WMN客户端与LTCA协议认证性[18]，协议基本序列如图7所示.

根据协议中定义的基本序列，定义WMN客户端与LTCA间双向认证协议Protocol([I1,I2,I3,R1,R2,R3]).

协议需要验证的强认证性质为

Nseauth(I3,2)∧Nseauth(R3,3).

1) 对Nseauth(I3,2)进行证明

证明. 假设诚实主体MU≠LTCA且遵守WMN客户端与LTCA双向认证协议，线程thr1是

Fig. 7 Basic sequence of two-way authentication protocol
图7 双向认证协议的基本序列

基本序

的实例，

loc

…<

loc

为线程

thr

上的动作，那么事件

,…,

发生的主体为LTCA.对原子

则有：

(1)

由AxiomD以及AxiomS可知，存在事件e′,e″,e′″,e″″使得主体MU同时满足4个条件：

① 事件e′中e′

② 事件e″中e″

③ 事件e′″中e′″

④ 事件e″″中e″″

对于事件发生的主体满足：

Encrypt(e′)=RMU,PKLTCA,S3.
Encrypt(e″)=h1,PKLTCA,S2.
Encrypt(e′″)=,
.
Encrypt(e″″)=RLTCA,SKMU,S1.

根据性质4，以事件e′为研究对象，因为主体MU遵守WMN客户端和LTCA双向认证协议，事件e′必然为WMN客户端与LTCA双向认证协议的基本序列之中的一个实例成员[10].在协议交互过程中包含加密Encrypt( )动作的是I3,R1,R2,R3，根据性质5以及图6可知，MU基本序R2,R3发生在基本序I3后，故基本序R2,R3可以排除.

(2)

在主体中，SKLTCA和PKLTCA分别为LTCA的私钥和主公钥，符合AxiomD定义构成匹配，则主体满足：

1RMU=RMU,PKA=PKLTCA,1S3=S3,A=L,
1h1=h1,1S2=S2,1S1=S1,RA=RLTCA.

可得到：

(3)

可得到：

(4)

由线程thr1的初始式(1)可知，基本序I3内可以构成完整(Send,Rcv)的是事件e1和e2.根据事件逻辑的认证规则，结合式(1)以及式(4)可得，Send(e1)=L,RLTCA和Rcv(e2)=得到一个长度为2的(弱)匹配.

Nseauth(I3,2).

证毕.

2) 对Nseauth(R3,3)进行证明

(5)

由AxiomD以及AxiomS可知，主体LTCA满足存在事件e″‴,e″‴′,e″‴″使得加密解密事件匹配成立，即：

则事件发生主体满足：

根据性质4，以事件e″‴为研究对象，因为主体LTCA遵守WMN客户端和LTCA双向认证协议，事件e″‴必然为认证协议的基本序列的实例成员.在协议交互过程中包含加密Encrypt( )动作的是I3,R1,R2,R3，根据性质3以及图6可知，对于基本序R1,R2可以进行排除.

(6)

可得到：

(7)

可以得到：

(8)

线程thr2所涉及式(5)可知，在基本序R3中可以构成完整的(Send,Rcv)是事件e0,e5,e6.根据协议形式化认证规则，结合式(1)(4)(5)(8)可得，Rcv(e0)=L,RLTCACertLTCA,S6,S4,T2此时就可以得到一个长度为3的(弱)匹配.

Nseauth(R3,3).

证毕.

综合证明1)和2)可知，强认证性质Nseauth(I3,2)∧Nseauth(R3,3)得到完整证明，即WMN客户端和LTCA间双向认证协议同时满足2个强认证性质，此过程不存在消息重放的可能性，协议安全性得证，即WMN客户端和LTCA间双向认证协议是安全的且攻击者无法通过伪装合法用户进行重放攻击.此时客户端获得LTCA的认证证书，可以与其他的客户端用户进行有效通信.

4 形式化方法对比分析

形式化方法用数学模型描述推理基于计算机的系统概念或方法，即规范语言+形式推理.规范语言包括：抽象模型规范法、代数规范法、状态迁移规范法和公理规范法.形式化方法有形式化描述、形式化设计和形式化验证，几十年来国内外专家学者在这3方面研究工作做出巨大贡献.事件逻辑理论是定理证明方法的一种，定理证明优于其他形式化方法的地方在事件逻辑理论中均有体现，但事件逻辑理论相较于其他形式化方法也存在不足.本节综合其他形式化方法对事件逻辑理论进行概述.

4.1 事件逻辑与模态逻辑比较

模态逻辑是目前应用最广泛的形式化方法，包括BAN逻辑、类BAN逻辑，其中类BAN逻辑包含十多种逻辑方法.各类逻辑方法的语法定义各具特色，协议安全属性验证过程采用逻辑推理方式进行证明，这与基于事件逻辑理论的定理证明方法一致.

以BAN逻辑为例，相较事件逻辑理论方法，BAN逻辑要进行大量理想化处理，这其中包含协议前提、协议本身、协议目标等，这些动作通过形式化描述实现.

1) BAN逻辑形式化描述协议初始化假设、安全协议预期目标，这些步骤与事件逻辑理论方法类似，但BAN逻辑对所处执行环境、参与协议执行主体和协议使用密钥等作出的初始假设过分依赖.事件逻辑理论对协议初始化方面没有过分处理，但对协议客观环境进行假设要求，在协议交互过程进行合理抽象化处理.

2) BAN逻辑对协议理想化处理过分依赖分析者直觉，理想化过程会产生问题，使得理想化后协议与原来协议有一定差距.例如忽略或增加协议前提或内容，对协议目标描述不够准确，易造成分析结果与原协议设计有一定出入[20].事件逻辑理论定义严谨的数学规则，规范一系列公理推论规则约束，从而保证强认证性质证明过程的严谨性.

3) BAN逻辑利用规则进行按步推理，运用严谨推理逻辑证明协议.但是BAN逻辑语义刻画不够清晰，证明协议安全性并不能让人很好信服，同样BAN逻辑不能很好保证协议证明的实用性.事件逻辑理论定义的定理规则，结构清晰、无歧义，保证协议在证明过程中的真实可靠性，使得协议安全属性更具有可信性.

4) BAN逻辑规则定义相较事件逻辑理论更加成熟，研究方面更广泛.在定义规则上，BAN逻辑规则可读性更强，使用者不需要过高的数学基础以及逻辑推理能力.在使用BAN逻辑证明过程中，使用者可以通过调用定义规则对目标进行证明.

5) 模态逻辑与事件逻辑理论一样，需要大量的手工作业，在形式化自动化验证方面有待提高.

4.2 事件逻辑理论与PCL比较

协议组合逻辑(protocol composition logic, PCL)是一种证明加密协议安全系统的逻辑方法.PCL与事件逻辑理论方法一样，协议形式化建模生成随机数、接收发送消息、对消息执行加密操作以及签名验证.

1) 协议安全属性验证中，PCL方法只能对部分协议性质进行刻画，对数据签名协议的认证性质不能进行刻画，而基于事件逻辑理论的定理证明方法可以对其他安全属性进行刻画认证.

2) PCL方法在协议交互动作建模中不够严谨，对描述线程的前序动作序列机制缺乏定义.事件逻辑理论方法对协议形式化建模线程机制进行明确定义，通过原子独立性规范事件发生先后线程状态.

3) PCL方法对协议信息数据类型缺乏必要约束、限制，事件逻辑理论定义特有Atom类型对没有结构且不能被生成的基本元素进行规范化定义，保证协议信息数据类型的规范充分.

4) PCL方法描述Diffie-Hellman代数行为及散列函数的能力不足，以散列函数加密为例，事件逻辑理论在处理加密动作时选择对其进行刻画.以散列函数加密为例，在消息解密验证过程中，事件逻辑理论方法通过有效信息生成新的散列加密，然后与刻画的加密动作进行比较证明.

5) PCL在应用中经历时间长久，特别是在协议动作分布自动化方面做了大量工作，此方面是事件逻辑理论方法亟待改进的.

4.3 事件逻辑通用性

事件逻辑理论对分布式系统协议和算法进行描述，通过捕捉分布式系统模型实现.在事件逻辑理论基本定义中，对原子类型、独立性、事件结构进行初步建模，保证加密系统建模过程中随机数、事件类建模的完备性.事件逻辑理论通用性具体表现在3个方面：

1) 复杂协议对象简化处理

协议对象的简化处理要求对协议抽象过程、协议通用属性进行标识，保证协议对象的平凡性；对特有属性进行特别标识，保证协议对象独特性.例如，在WMN客户端与LTCA交互认证协议中，客户端与LTCA具有共有属性公私钥(PK,SK),但2个主体有各自独特性，客户端拥有特有辅公钥LTCA通过合法程序生成客户端用户辅公钥的权限，在认证过程中生成唯一的证书CertL，需要在协议形式化描述中对这些性质进行特别刻画.

2) 协议交互环境合理化假设

有线网络与无线网络环境对于协议应用要求有很大不同，相较而言，无线网络环境下安全协议设计有挑战性.安全协议不仅要保证用户能够承受有线网络信息传递过程遇到的风险，还要面临无线网络环境独有的危险，对协议安全性认证也是挑战.

① 不同协议适用条件有所不同，协议形式化描述前要对协议执行条件进行了解，对协议交互条件进行合理化分析.

例如WMN客户端协议对比有线网络安全协议没有可靠的认证中心，对LTCALCA形式化描述要求具体化，轻量级CA与客户端认证中加入辅公钥以及证书机制，加入门限机制容侵的轻量级CA则在LTCA基础上加入时间戳T保证LTCA在加密解密信息迭代的时间有效性.

② 对不同协议提出合理化假设条件，在合理假设条件中要求研究者了解协议运行的基本环境和独特环境.在提出假设的过程中，假设条件不宜过多，反之体现协议运行条件的苛刻，对协议独特的运行环境进行合理化提取.

例如WMN客户端间认证协议要求移动主体A与移动主体B在有安全保障条件下进行通信，在A,B节点间进行双向认证并产生安全的会话密钥.安全保障不是说协议交互环境绝对安全，协议交互过程有受到攻击者攻击的可能，安全保障是指在协议交互过程中不会受到恶劣自然环境或大型设备故障等非人为蓄意情况的影响.客户端间交互时，双方都收到认证中心的认证，拥有认证中心颁发的证书.

3) 协议交互过程删繁就简

协议信息在无线网络通道传递的过程中包含各种基本信息，例如数据在物理层、网络层等的传输交互，这些信息在事件逻辑理论形式化描述过程中均不做具象处理，以信息Msg来定义.但是协议动作对消息处理要进行明确标注，保证事件逻辑理论方法在协议建模时信息传递过程的有效性.

例如Needham-Schroeder协议交互双方在进行信息传递过程中，主体A通过主体B的公钥PKB对自己产生的随机数Na以及时间戳T1进行加密，将消息传递给用户主体B.在形式化描述过程中，对信息的各层封装交互并不做研究描述，直接总括这一过程，即A→B:SignPKB{A,Na,T1}.

5 结论

5.1 总结

信息安全涉及信息资源交互中的机密性、完整性以及可用性，安全协议形式化方法在长期积累中形成比较完善的理论体系以及模型，定理证明是形式化方法的一种，基于严格数学理论知识和逻辑推导，从而确定协议在合理假设条件下是否满足要验证的安全属性[21].本文基于事件逻辑理论，使用定理证明的方法对WMN客户端协议认证性进行分析，所取得的成果具体有4个方面：

1) 对事件逻辑理论进行扩展，提出置换规则保证协议交互用户在置换中性质的等价转换.将基于事件逻辑理论证明协议安全性的过程通过流程图表述，详细介绍事件逻辑理论证明过程.

2) 通过事件逻辑描述客户端与LTCA间交互协议的基本序列，对协议交互动作形式化描述.证明协议强认证性质，得出WMN客户端与LTCA间认证协议在合理假设下是安全的.表明事件逻辑理论可以对安全协议不同身份主体间的认证性进行证明.

3) 结合文献[10,19]可知，事件逻辑不仅可以对有线网络安全协议的安全属性进行证明，对无线网络安全协议的安全属性也可以给予合理论证，进而保证安全协议在用户交互过程中的可靠性.

4) 分析事件逻辑理论方法与其他逻辑证明方法的优缺点，说明事件逻辑理论具有通用性.