PUFs是一种可将其视为硬件形式的单向函数[1]，硅芯片制造的物理系统即使基于相同的制造工艺，在物理特性上也很难克隆、复制或预测[2]，其电路实现可以被认为是一种特殊的、轻量级的硬件安全原语，广泛应用于集成电路防伪、无密钥安全通信、智能设备识别和认证等[3]．Suh和Devadas认证了利用PUFs进行低成本身份验证和密钥生成的可行性，并首次提出了基于PUFs的认证方法[4]．基于该方法学者们设计了大量PUFs认证协议，然而在实际应用中很多PUFs认证协议被证明存在多种攻击[5]．面对这些安全问题，学者们展开了PUFs认证协议安全性分析．Armknecht等[6]针对不同类型PUFs安全原语构建了形式模型，为基于PUFs的安全协议安全性分析提供形式基础．张正等[7]用BAN逻辑形式化分析了一种基于PUFs的Kerberos扩展协议的安全性．李涛和刘亚丽[8]对Liang[9]等提出的基于双PUFs的RFID认证协议进行了安全性分析，指出其存在多种攻击．李晖等[10]分析了基于PUFs和超轻量级认证的PUMAP协议不能防止位置跟踪攻击．Mukhopadhyay[11]使用机器学习训练出激励响应对(challenge-response pair，CRP)的线性模型成功地攻击了物联网中基于PUFs的两个安全协议，证明了其不能抵抗机器学习的模型训练攻击．目前基于PUFs的认证协议安全分析研究中，主要采用直接密码分析法分析协议密码机制的安全性，然而协议本身的认证逻辑正确性直接决定协议是否能达到其安全目标，在有限分析协议认证逻辑正确性的研究中，学者们主要采用类BAN模态逻辑进行分析，由于模态逻辑理想化过程的非形式化、逻辑语义不完整及过度依赖初始假设等局限性，很难用于规约PUFs安全协议和刻画须要满足的安全属性，因此即使采用模态逻辑证明了协议是安全的，实际协议中仍然存在安全问题[12]．事件逻辑理论(logic of events theory，LoET)是一种用于分析分布式系统安全性的定理证明形式逻辑[13]，文献[14]将LoET扩展用于对协议安全性进行分析，引入协议组合逻辑(protocol composition logic，PCL)思想[15]，通过对LoET扩展分析证明了多个不同应用领域的安全协议的安全性[16-18]．本研究通过引入随机数关联事件时序概念与相关规则，形式化抽象PUFs随机会话秘钥生成功能，规约基于PUFs认证协议的相互认证过程，刻画协议须要满足的安全属性．以文献[19]协议为例，基于扩展的LoET推理证明了该协议满足强认证性．1 LoET理论LoET基于类型理论，以消息自动机为模型，通过发送和接收消息动作执行内部状态迁移．分析过程中将诚实主体交互动作抽象为不同类型的事件，采用事件语言将协议的交互过程形式化定义为基本事件序列，基于LoET公理系统推理证明协议是否满足其安全属性．事件逻辑理论及相关规则参考文献[13-18，20]．1.1　基本概念Atom用于抽象协议中无固定结构和不可猜测的协议基本原语，如挑战数、密钥、签名和密文等，协议形式模型中，将协议交互过程中的发送和接收、签名和认证、加密和解密及随机数生成等处理消息的动作定义为事件[13]，利用事件对协议行为进行形式化构建[20]，不同主体之间的交互用匹配会话描述．1.1.1　匹配会话将协议实体某次运行的全序动作集定义为线程，Thread≡def{t:ActList|∀i:t[i]loct[i+1]}，同一运行实例中符合全序关系的动作列表ActList中的第i个动作表示为t[i]．如在ISO/IEC 9798—2协议中主体A和B通过两条消息进行交互，消息1：A-B{Ta，B}Kab，消息2：B-A{Tb，A}Kab，对于实体A与B的某一次参与协议运行中的线程t1可表示为包含加密、发送、接收和解密事件序列{encrypt(〈Ta，B〉，Kab，sm)，send(sm，B)，rcv(x，B)，decrypt(〈Tb，A〉，Kab，x)}，即主体A首先通过加密事件encrypt采用公共秘钥Kab对消息〈Ta，B〉加密后得到密文sm，通过发送事件send(将其发送给B，然后主体B通过接收事件rcv(接收消息x并对其进行解decrypt，验证其是否符合接收信息消息〈Tb，A〉的要求．协议认证过程中若不同线程的发送事件s和接收事件r的消息一致，则满足弱匹配，定义为s∼r≡defs∈E(Send)∧r∈E(Rcv)∧Send(s)=Rcv(r)，其中：E(Send)函数获取发送类事件集；E(Rcv)函数获取接收类事件集；Send(s)和Rcv(r)函数分别为s和r的事件消息．若s满足s∼r的同时s为r的前序事件，则s和r满足强匹配，定义为s↦r≡defs∼r∧sr．存在n个消息事件对的两个线程t1和t2，若它们对应的消息事件对〈Send(s)，Rcv(r)〉都满足强匹配，则t1，t2满足强匹配会话，记为t1≈nt2；若消息事件对仅满足弱匹配，则满足弱匹配会话，记为t1∼nt2．1.1.2　认证性将协议形式化定义为各参与诚实主体的线程集合，分析协议中不同线程是否满足匹配会话来证明协议的认证性．诚实主体指按照协议规范参与协议运行的主体，用函数Honest表示，基本序列定义为线程中动作事件的集合，如果一个协议满足诚实主体双方的认证线程间的强匹配会话，那么该协议满足强认证属性，如在认证协议Pr认证过程中，诚实主体A对B认证满足一个n条认证消息的认证属性可形式化定义为Pr⊨auth(bs,n)≡def∀A,B.∀t1.(Honest(A)∧Honest(B)∧Pr(A)∧Pr(B)∧A≠B∧loc(t1)=A∧bs(A,B,t1))⇒∃t2.loc(t2)=B∧t1≈nt2.如果协议Pr满足不同诚实主体A对B的强认证属性，那么主体A对B的任意一个认证线程t1与基本序列bs，协议主体B存在一个线程t2与t1形成一个认证消息长度为n的匹配会话．1.2　证明系统LoET通过公理和相关推理规则对协议安全属性进行证明[20]．本研究只对协议分析中使用到的相关公理和规则进行描述．1.2.1　秘钥公理协议中密钥Key≡defId+Atom+Atom，其中公钥定义为协议主体身份标识Id，对称密钥或私钥定义为函数MatchingKeys:Key→Key→𝔹，描述密钥之间的匹配关系，函数PrivKey:Id→Atom为主体Id指定一个Atom类私钥，秘钥公理定义为AxiomK:∀A,B:Id.∀k,k':Key.∀a:AtomMatchingKeys(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.AxiomK假设秘钥匹配是对称关系，诚实主体的私钥只匹配对应的公钥，对称密钥只匹配自身，不存在两个不同诚实主体具有相同的私钥．1.2.2　因果序公理因果序公理假设事件的因果关系，AxiomR公理假设某个接收事件发生前必须有相应的发送事件，并且事件消息一致，那么这对消息事件符合因果序性质，同样AxiomV和AxiomD分别假设签名与验证、加密与解密事件间的因果关系，分别定义为AxiomR:∀e:E(Rcv).∃e':E(Send).(e'e)∧Rcv(e)=Send(e')AxiomV:∀e:E(Verify).∃e':E(Sign).(e'e)∧Verify(e)=Sign(e')AxiomD:∀e:E(Decrypt).∃e':E(Encrypt).(e'e)∧DEMatch(e,e').解密公理AxiomD中引入了匹配函数DEMatch，∀e:E(Decrypt).∃e':E(Encrypt).DEMatch(e,e')≡defplaintext(e)=plaintext(e')∧ciphertext(e)=ciphertext(e')∧MatchingKeys(key(e),key(e')).匹配的加密和解密事件具有相同的明文plaintext和密文ciphertext，并且e和e'事件对应的秘钥key(e)和key(e')相匹配．1.2.3　诚实公理诚实公理假设诚实主体不会主动泄露自己的私钥，因此只有诚实主体本身能够用自己的私钥完成签名、加密及解密事件．诚实公理AxiomS定义为AxiomS:∀A:Id.Honest(A).∀s:E(Sign).∀e:E(Encrypt).∀d:E(Decrypt).signer(s)=A⇒(loc(s)=A)∧key(e)=PrivateKey(A)⇒(loc(e)=A)∧key(d)=PrivateKey(A)⇒(loc(d)=A)，式中：signer(s)和loc(s)分别为事件s的签名实体和发生主体；PrivateKey(A)为主体A的私钥．引理1 若e1,e2∈E(New)且New(e2)=New(e1)，则e1=e2．New为随机数生成事件类，如果e1生成的随机数New(e1)与e2生成的随机数New(e2)相等，那么根据安全协议随机数语义，e1和e2为同一个事件．1.3　扩展概念和规则本研究基于事件逻辑理论提出相关时序概念描述协议中不同主体线程间的事件时态顺序，用于分析协议的强认证性质．1.3.1　FirstSendNonce函数在协议交互过程中为了分析与随机数相关事件在不同主体线程中的时态顺序，引入首次发送随机数函数FirstSendNonce:Send→Atom→𝔹，该函数判断发送事件是否首次发送随机数，定义为∀n:E(New).∀s:E(Send).∀e:EFirstSendNonce(s,a)≡defloc(n)=loc(s)∧New(n)=Send(s)=a∧¬(loc(e)≠loc(n)∧e has a∧es).谓词has表示逻辑包含，根据以上定义，如果随机数a在s事件中满足首次发送，那么很容易推理出其他线程中拥有该随机数的事件一定发生在其后，FNRule1规则定义为FNRule1:∀n:E(New).∀s:E(Send).∀e:ENew(n)=a∧FirstSendNonce(s,a)∧e has a∧loc(n)≠loc(e)⇒se.1.3.2　NonceOrigin函数引入NonceOrigin:Thread→Atom→𝔹函数判断随机数与线程之间的关系，用于分析事件关联消息为随机数的时态性质，形式定义为∀t:Thread.∀e:E(New).NonceOrigin(t,a)≡defe∈t∧New(e)=a.在该布尔函数中，若Atom类的某个随机数a由线程t中某个随机数生成事件e产生，则NonceOrigin(t，a)为真．如果不同主体的两个线程拥有相同的随机数，那么在其中一个满足NonceOrigin的线程中一定存在一个事件满足FirstSendNonce，FNRule2规则定义为FNRule2:∀t1,t2:Thread.∀n:E(New).∀e:ENew(n)=a∧NonceOrigin(t1,a)∧loc(t1)≠loc(t2)∧e∈t2∧e has a⇒∃s:E(Send).s∈t1∧FirstSendNonce(s,a).2 协议介绍PUFs认证协议使用不可克隆技术产生的响应值建立协议认证主体间的临时共享密钥，大部分PUFs的认证协议都是基于Suh和Devadas提出的身份认证框架[4]，本研究对一种基于该框架的SRAM PUFs安全双向认证协议[19]进行分析．协议中服务器为认证方，内嵌PUFs电路的客户端为被认证方，双方使用挑战应答模式进行认证．认证服务器与客户端须预先拥有一个共享长期密钥，在注册阶段认证服务器预先在安全的环境下从客户端PUFs读取一批激励响应对CRP保存，在认证阶段认证服务器选择一组CRP，依据挑战查找匹配响应用于建立认证信息随机会话密钥．PUFs协议认证流程如下，流程图见图1．10.13245/j.hust.240209.F001图1基于SRAM PUFs双向认证流程a．认证服务器与PUFs客户端共享长期秘钥K，服务器首先向客户端发送认证请求．b．客户端生成随机数New(r1)，秘钥K作为激励产生PUFs响应R'，对其进行纠错编码后加密得到密文t1，连同客户端ID、随机数r1一起发送给服务器端．c．服务器收到客户端发送的消息后解密，在已存储的CRP中找到激励K对应的响应R并用相应的纠错码解码算法恢复响应R'生成会话随机密钥Kg，随后服务器生成随机数r2，使用Kg对〈r1，r2〉加密后生成密文t2并发送给客户端．d．客户端对响应R'计算Kg，解码恢复t1得到明文消息〈r1',r2'〉，若r1=r1'，则客户端对服务器端认证成功．e．客户端生成随机数r3，使用Kg将信息〈r2',r3〉加密后生成密文t3发送给认证方．f．认证服务器解密获得〈r2'',r3'〉后，若r2=r2''，则服务器认证客户端成功，最终完成相互认证．3 协议形式化分析LoET是基于进程演算形式化分析协议的理论，因此首先通过定义协议不同角色进程，分析基本序列中匹配会话的消息，通过分析主体之间发送和接收动作的消息是否相同及动作的时序关系，用定理刻画协议要满足的强认证属性．3.1　PUFs功能形式化抽象协议中首先须在认证服务器和客户端之间基于PUFs建立会话随机秘钥，LoET形式化如下所示．a．含有PUF的被认证方生成HD (helper data)：R'=PUF(K)new(r1)h=encode(r1)⊕R'P=ENCK(h)send(〈ID，r1，P〉)b．认证方生成随机秘钥：Receive(〈ID，r1，P〉)HD=DECK(P)r1=decoding(h⊕R)R'=Rep(R，HD)Kg=hash(R')认证双方在协议安全注册阶段共享固定密钥K和被认证方身份ID，认证服务器存储了客户端PUFs设备的CRP，客户端收到服务器的认证请求后，产生当前响应R'=PUF(K)，同生成的随机数r1编码值进行异或运算后，得到纠错编码辅助值HD用于对响应纠错，抽象表示为h=Gen(R'，r1)，将其用K加密后得到密文P=ENCK(h)，然后将ID，r1和P发送给认证方．认证服务器收到ID后，读取数据库中相应的CRP〈K，R〉，用K解密P，得到h=DECK(P)并恢复响应，抽象表示为R'=Rep(R，h)，最后对R'进行Hash运算后生成当前会话密钥Kg．由于本研究分析的是协议认证性，而协议第一阶段是利用PUFs物理随机数特性构建会话随机密钥，因此可以使用LoET中相同特性的随机数生成事件将秘钥建立进行形式化抽象为Kg=New(e)．3.2　协议基本序列定义进程Initiator和Responder分别描述认证服务器和客户端主体协议交互．将LoET中接收、验证和解密事件的前序动作定义为一个基本序列，定义I1~I4和R1~R3分别为Initiator和Responder基本序列．其中Initiator基本系列为：I1：{rcv(〈ID，r1，t1〉)}；I2：{I1，decrypt(〈〈Kg〉，K，t1〉)，new(r2)，encrypt(〈〈r2，r1〉，Kg，t2〉)}；I3：{I1，I2，send(t2)}；I4：{I1，I2，I3，rcv(〈t3〉)，decrypt(〈〈r3，r2〉，Kg，t3〉)}．Responder基本系列为：R1：{new(r1)，new(Kg)，encrypt(〈〈Kg〉，K，t1〉)，send(〈ID，r1，t1〉)}；R2：{R1，rcv(t2)}；R3：{R1，R2，decrypt(〈〈r2，r1〉，Kg，t2〉)，new(r3)，encrypt(〈〈r3，r2〉，Kg，t3〉)，send(t3)}．3.3　协议强认证性分析以上协议基本序列可知Initiator要满足在协议中的强认证性，须与Responder端有3次消息发送与接收动作的交互，即存在长度为3的匹配会话，该性质刻画为SP⊨auth(I4，3)，SP|=auth(I4,3)≡def ∀ Initiator,Responder.∀t1.Honest(Initiator)∧Honest(Responder)∧SP(Initiator)∧SP(Responder)∧Initiator≠Responder∧loc(t1)=Initiator∧bs(Initiator,Responder,t1)⇒∃t2.loc(t2)=Responder∧t1≈3t2.相应地，Responder要满足强认证性须与Initiator端进行长度为2的匹配会话，该性质刻画为SP|=auth(R3,2)，SP|=auth(R3,2)≡def ∀ Initiator,Responder.∀t1.(Honest(Initiator)∧Honest(Responder)∧SP(Initiator)∧SP(Responder)∧Initiator≠Responder∧loc(t1)=Responder∧bs(Initiator,Responder,t1)⇒∃t2.loc(t2)=Initiator∧t1≈2t2.3.4　SP|=auth(I4,3)证明假设诚实主体A为认证服务器Initiator，B为客户端Responder，且A≠B，A和B共享永久密钥K、PUF的响应R和B的秘密身份ID，由于诚实主体遵循协议规则，因此A，B的参与协议运行的任意线程都是SP的基本序列实例．令t1为认证主体A基本序列I4的一个实例，则存在e0loce1…loce6事件序，对于Atom类型参数t1~t3，Kg，K，r1~r3，t1事件序列实例为rcv(e0)=〈ID,r1,t1〉∧decrypt(e1)=〈〈Kg〉,K,t1〉∧new(e2)=〈r2〉∧encrypt(e3)=〈〈r2,r1〉,Kg,t2〉∧send(e4)=〈t2〉∧rcv(e5)=〈t3〉∧decrypt(e6)=〈〈r3,r2〉,Kg,t3〉.由AxiomD和AxiomS公理可知，对于解密事件e6，协议的某个线程中必定存在加密事件e'，且e'e6∧DEMatch(e6,e')∧loc(e')=B∨loc(e')=A，在协议所有基本序列中包含Encrypt( )加密动作的有I1~I4和R1~R3，而e'为响应者主体B发生的事件，意味着响应者基本序列R1~R3中存在着一个与I4匹配的会话事件序列．假设e'为R1中的事件，那么对于Atom类型的r1',Kg',K',t1'，在主体B上存在事件e0',e1',e3'为e0'loce1'loce'loce3'∧new(e0')=〈r1'〉∧new(e1')=〈Kg'〉encrypt(e')=〈〈Kg'〉,K',t1'〉∧send(e2')=〈ID,r1',t1'〉. (1)根据AxiomD公理可知，若满足DEMatch(e，e')，则plaintext(e')=plaintext(e6)，而通过式(1)分析出plaintext(e')=Kg'与plaintext(e6)=〈r2，r1〉不匹配，因此排除e'是R1中的事件，同理也可证明e'不属于R2序列中的事件．最后分析如果e'属于R3序列实例线程t2中的事件，并假设各事件消息用Atom类型的常量表示为t2',t3',r1',r2',r3',Kg'，主体B的标识为ID'，则t2线程中存在e0',e1',e2',e3',e4',e5',e6',e8'事件与e'组成的事件序列为e0'loce1'loce2'loce3'loce4'loce5'loce6'loce'loce8'∧new(e0')=〈r1'〉∧new(e1')=〈Kg'〉encrypt(e2')=〈〈Kg'〉,K',t1'〉∧send(e3')=〈ID',r1',t1'〉∧rcv(e4')=〈t2'〉∧decrypt(e5')=〈〈r2',r1'〉,Kg',t2'〉∧new(e6')=〈r3'〉∧encrypt(e')=〈〈r3',r2'〉,Kg',t3'〉∧send(e8')=〈t3'〉. (2)由于DEMatch(e6，e')，根据AxiomKey公理，plaintext(e')=plaintext(e6)∧ciphertext(e')=ciphertext(e6)∧MatchingKeys(Kg,Kg')⇒r2'=r2∧r3'=r3∧t3'=t3∧Kg'=Kg.可得出t3=t3'⇒send(e8')=rcv(e5)，由于t2线程中存在解密事件e5'，根据AxiomD和AxiomS公理，存在e''满足e''e5'∧DEMatch(e5',e'')∧ loc(e'')=A∨loc(e'')=B，因此须要进行新一轮协议交互分析．假设e''为协议实例t3的加密事件，包含encrypt( )动作的有I2~I4和R1~R3．同上一轮分析类似，可以将R1~R3排除，得出I2~I4中存在一个基本序列包含e''．假设e''是t3线程在I2上的实例加密事件，对于K2'',K'',r1''r2'',t1'',t2''主体A发生事件e0'',e1'',e2'',e4''，则e0''loce1''loce2''loce''loce4''∧rcv(e0'')=〈ID'',r1'',t1''〉∧dec(e1'')=〈〈K2''〉,K'',t1''〉∧new(e2'')=〈r2''〉∧encrypt(e'')=〈〈r2'',r1''〉,K2'',t2''〉∧send(e4'')=〈t2''〉. (3)由式(2)和(3)可得出，线程thr3中I2系列实例中的加密事件e''与thr2线程解密事件e5'匹配(DEMatch(e'',e5'))，则plaintext(e'')=plaintext(e5')∧ciphertext(e'')=ciphertext(e5')∧MatchingKeys(Kg'',Kg')⇒r1''=r1'=r1∧r2''=r2'=r2. (4)线程t3和线程t1中new(e2)=new(e2'')，由引理1可知e2=e2''，根据事件逻辑中协议定义，若协议中两个线程拥有同一事件，则这两个线程是一致的，也就是t1与t3中事件实例相同，那么e''=e3⇒t2''=t2，可得出：t2=t2'⇒send(e4)=rcv(e4')，t3事件系列改写为e0''loce1''loce2''loce''loce4''∧rcv(e0'')=〈ID,r1,t1〉∧dec(e1'')=〈〈Kg〉,K,t1〉∧new(e2'')=〈r2〉∧encrypt(e'')=〈〈r2,r1〉,Kg,t2〉∧send(e4'')=〈t2〉.同样，若以上事件系列中存在解密事件e1''，则协议某个系列中必须存在事件e'''，且e'''e1''∧ DEMatch(e1'',e''')∧loc(e''')=A∨loce'''=B成立，即encrypt(e''')=〈〈Kg〉,K,t1〉成立．包含encrypt( )动作的有I2~I4和R1~R3．同样地，可以排除系列I1~I4，得出R1~R3中存在一个基本序列包含序列e'''．假设e'''是R1上的一个实例，那么对于Atom类型的r1''',Kg''',K''',t1'''及主体ID'''，在主体B上存在线程t4，其中事件e0''',e1''',e3'''关系为e0'''loce1'''loce'''loce3'''∧new(e0''')=〈r1'''〉∧ new(e1''')=〈Kg'''〉encrypt(e''')=〈〈Kg'''〉,K''',t1'''〉∧send(e3''')=〈ID''',r1''',t1'''〉.根据DEMatch(e1'',e''')，从上述对于事件系列的描述中可以推出encrypt(e''')=〈〈Kg'''〉,K''',t1'''〉∧dec(e1'')=〈〈Kg〉,K,t1〉⇒Kg'''=Kg. (5)由式(5)可知，new(e1''')=new(e1')⇒e1'''=e1'，因此线程t4与t2相一致，两个线程事件相同，t4事件系列可改写为e0'''loce1'''loce'''loce3'''∧new(e0''')=〈r1'〉∧new(e1''')=〈Kg'〉encrypt(e''')=〈〈Kg'〉,K',t1'〉∧send(e3''')=〈ID',r1',t1'〉. (6)根据式(4)和(6)，由DEMatch(e1'',e''')可得出t1=t1'∧r1=r1'⇒send(e3')=rcv(e0)，得证rcv(e0)=send(e3')=〈ID,r1,t1〉∧send(e4)=rcv(e4')=〈t2〉∧rcv(e5)=send(e8')=〈t3〉.以上结果表明对于诚实主体A任何一个线程，诚实主体B存在一个消息数为3的线程与之形成弱匹配会话．接着分析它们是否为强匹配会话，即分析会话事件是否满足e3'e0,e4e4',e8'e5事件时间序．若线程t2中有随机数生成事件new(e0')=r1，则该线程满足NonceOrigin(t2，r1)，且t2基本序列e0'e1'e'e3'中只有e3'为Send事件且发送的消息为随机数r1，根据FNRule2，得出First-SendNonce(e3',r1)，根据FNRule1，所有拥有原子消息r1的其他线程中的事件一定发生在e3'之后，包括t1中的rcv(e0)=〈ID,r1,t1〉，因此e3'e0．同理，可分析出e4e4',e8'e5．通过以上分析可知，主体A中认证线程在主体B中存在与之强匹配会话，即SP|=auth(I4,3)得证．3.5　SP|=auth(R3,2)证明令t1为实体B中基本序列R3的一个实例，定义e0loce1…loce8为线程t1上的事件，则对于一些Atom类型参数t1~t3，K，Kg，r1~r3有new(e0)=〈r1〉∧new(e1)=〈Kg〉∧encrypt(e2)=〈〈Kg〉,K,t1〉∧send(e3)=〈ID,r1,t1〉∧rcv(e4)=〈t2〉∧decrypt(e5)=〈〈r2,r1〉,Kg,t2〉∧new(e6)=〈r3〉∧encrypt(e7)=〈〈r3,r2〉,Kg,t3〉∧send(e8)=〈t3〉.由AxiomD和AxiomS公理可知，存在与解密事件e5匹配的加密事件e'，且e'   e5∧DEMatch(e5,e')∧loc(e')=B∨loc(e')=A，由于A和B为诚实主体，因此e'为I2~I4和R1~R3中某个基本系列中的事件，与3.4节类似，可以排除R1~R3．假设e'为线程t2的事件序列I2中的成员，则对于K',Kg',r1',r2',t1',t2'和ID'，在主体A上存在事件e0',e1',e2',e',e4'有e0'loce1'loce2'loce'loce4'∧rcv(e0')=〈ID',r1',t1'〉∧decrypt(e1')=〈〈Kg'〉,K',t1'〉∧new(e2')=〈r2'〉∧encrypt(e')=〈〈r2',r1'〉,Kg',t2'〉∧send(e4')=〈t2'〉.由于DEMatch(e5,e')，根据AxiomK可知plaintext(e')=plaintext(e5)∧ciphertext(e')=ciphertext(e5)∧MatchingKeys(Kg,Kg')⇒r2'=r2∧r1'=r1∧t2'=t2∧Kg'=Kg.进而得出t2=t2'⇒send(e4')=rcv(e4)；同时，thr2线程中存在解密事件e1'，同样根据解密公理AxiomD和诚实公理AxiomS，存在e''，使得e''e1'∧DEMatch(e1',e'')∧loc(e'')=A∨loc(e'')=B成立，因此须要新一轮协议交互分析．假设e''为协议实例t3的加密事件，包含encrypt( )动作的有I2~I4和R1~R3．同样地，可以将I2~I4排除，得出R1~R3中存在一个基本序列包含e''．若e''是R1上的实例加密事件，则主体B存在事件e0'',e1'',e'', e3''，对于Atom类型参数r1'',Kg'',K'',t1''和主体ID''，有e0''loce1''loce''loce3''∧new(e0'')=〈r1''〉∧new(e1'')=〈Kg''〉encrypt(e'')=〈〈Kg''〉,K'',t1''〉∧send(e3'')=〈ID'',r1'',t1''〉.根据公理AxiomD可知，若要满足DEMatch(e1'，e'')，则plaintext(e'')=plaintext(e1')∧ciphertext(e'')=ciphertext(e1')⇒r1''=r1'=r1∧t1''=t1', (7)因此t3和t1中的new(e0)=new(e0'')，根据引理1可知e0=e0''，那么e''=e2⇒t1''=t1，由式(7)得出t1=t1'∧r1=r1'⇒send(e3)=rcv(e0')．根据以上证明可得send(e3)=rcv(e0')=〈ID,r1,t1〉∧rcv(e4)=send(e4')=〈t2〉.以上结果表明，对于诚实主体B的任意线程，诚实主体A存在一个消息数为2的线程与之形成弱匹配会话．接下来分析它们是否为强匹配会话，即证明e3e0'和e4'e4．若线程t1中new(e0)=r1，则该线程满足NonceOrigin(t1，r1)，且t1基本序列e0e1e2e3中只有e3为发送事件且发送的消息为随机数r1，依据FNRule2规则，在线程t1中满足FirstSendNonce(e3，r1)．根据FNRule1规则，所有拥有原子消息r1的其他线程中的事件一定发生在e3之后，包括thr2中的事件rcv(e0')=〈ID',r1,t1〉接收的消息中包含r1，因此e3e0'．同理，可分析出e4'e4．以上分析推导出主体B中的任意线程，在主体A中存在强匹配会话线程，即SP|=auth(R3,2)得证．最终协议满足双向强认证性，表示为SP|=auth(I4,3)∧SP|=auth(R3,2)．4 结语本研究通过引入FirstSendNonce和NonceOrigin随机数关联事件时序概念及相关重要规则对事件逻辑理论进行了扩展，用于分析事件与消息之间的匹配关系和消息匹配事件间的时态顺序，形式化抽象PUFs随机密钥建立功能，定义PUFs协议进程和基本序列用于描述协议，形式化规约协议双方须满足的强认证属性，采用定理证明方法推理证明协议双方认证基本序列满足强认证性．将事件逻辑扩展用于分析基于PUFs硬件认证协议的安全性，从理论上证明了协议满足强认证性，然而并未考虑到协议在实际运行环境下的安全性，如环境扰动带来的PUFs干预环境下的安全性分析，因此未来将进一步对协议代码实现级进行安全性验证．认证性和秘密性是安全协议非常重要的两个安全属性，目前LoET只支持协议认证性的分析，未来工作将扩展事件逻辑理论以支持分析安全协议的秘密性．