2026, Vol. 58
当今时代，互联网已经融入社会生活，采用安全协议是保障互联网安全性的重要手段之一。安全协议是基于密码学理论和算法的协议。公平交换协议是安全协议的一种，它可以保证协议中的其他主体不能获得比诚实主体更多的利益。电子合同签署协议、电子购物协议、电子邮件协议等都属于公平交换协议。形式化方法是用来研究安全协议的一种复杂的数学方法，包括定理证明和模型检测。定理证明方法不限制系统状态，同时具有严谨性和精确性，但需要足够的数学知识。模型检测方法的自动化程度较高，节省人力，但只能处理有限状态系统。事件逻辑[1]是定理证明方法的一种，由肖美华等于康奈尔大学提出，是一种强大的证明协议安全属性的方法，它包括事件系统公理、推论及其相关性质，还包括对协议的执行步骤进行模型化、对协议的执行过程和安全目标进行精确的形式化描述和定义。事件逻辑对协议的完整性和机密性进行了严谨的证明，协议分析过程中的复杂性也大大降低 [2-4]。
Huang等[5]提出了混淆乐观公平交换方案(ambiguous OFE, AOFE), 该方案对基于身份的密码加密进行深入的研究，同时定义了身份混淆属性，但该方案在密钥可信度上缺乏研究。Zhang等[6]提出时间相关密码协议逻辑(time-dependent cryptographic protocol logic，TCPL)来分析安全协议时间敏感性, 该方法对安全协议的安全属性随时间变化进行了有效定义，但缺乏对信道的完整认识。陈明等[7]提出一种全新的逻辑，引入了离散时间序列，但该逻辑缺乏对协议的整体性分析。牛翠翠等[8]利用博弈的方式分析了协议的公平性。Lohr等[9]从代价公平性角度对安全协议进行了形式化的分析，但缺乏对交换过程的公平性研究，因此目前研究存在着诸多亟待深入解决的问题[10]。
安全性证明中的时间因素至关重要，消息的发送与接收，以及消息的有效性等都需要时间来进行严格要求，因此，如果缺乏对时间的刻画就不能真正满足公平性。本文对基于身份的乐观公平交换协议(ID-AOFE)进行研究时加入了时间因素[11]，根据不同发起者的状态分析协议的公平性，基于时间的事件理论逻辑也可以用于类似协议的公平性分析，例如Micali协议[12]的形式化分析等。
1 时间-事件逻辑 1.1 语法及语义事件逻辑中原子类消息即为不可猜测的数据，它可以表示随机数、密钥、签名等，一般用小写字母a，b，…代表原子。
在事件逻辑中，X为参与协议的主体，m收到的是明文消息或者主体产生的新消息，Send(X, m, t)表示在t时刻主体X发送消息m, Receive(X, m, t)表示在t时刻主体X接收消息m，New(X, m, t)代表在t时刻主体X产生消息m，Encrypt(X, m, k, t)代表主体X在t时刻利用密钥k加密消息m, Decrypt(X, m, k, t)代表主体X在t时刻利用密钥k解密消息m，Sign(X, m, k, t)代表主体X在t时刻利用密钥k签名消息m，Verify(X, m, k, t)代表主体X在t时刻利用密钥k验签消息m，Has(X, m, t)代表主体X在t时刻拥有消息m。φ代表原子公式，
在事件逻辑中引入时间因素，此时的事件逻辑系统包括三种公理。
1) 知识集公理(axioms of knowledge set)。
| $ \begin{aligned} & \operatorname{ ORIG: } {New}(X, m, t) \supset {Has}(X, m, t) \wedge m \in \mathit{Γ}_X, \\ & \quad \operatorname{REC} 1: {Receive}(X, m, t) \supset {Has}(X, m, t) \wedge \\ & m \in \mathit{Γ}_X, \\ & \;\;\quad \operatorname{REC} 2: {Receive}\left(X, m_1\left\|m_2\right\| \cdots m_n, t\right) \supset(\forall i, i \in \\ & [1, n] \wedge i \in Z), \\ & \quad \operatorname{SEND}: {Send}(X, m, t) \supset {Has}(X, m, t) \wedge m \in \mathit{Γ}_X 。\end{aligned} $ |
公理ORIG(origin)表示如果一个主体X在时间t生成一个新消息m，那么该主体X在t时刻拥有消息m，且该消息m被纳入主体X的知识集Γ中。
公理REC(receive)意为接收，公理REC1表示如果一个主体X在t时刻接收到消息m，那么该主体在t时刻拥有消息m，且纳入知识集Γ中。
公理REC2表示如果主体X在t时刻收到多个消息组成的串联消息，那么X将拥有其中的任何一个消息，且纳入知识集Γ。
公理SEND代表发送，表示如果主体X在t时刻发送了消息m，那么m纳入X的知识集Γ中。
| $ \begin{aligned} & \;\;\;\;\;\;\;\text { ENC: } {Has}\left(X, m, t_1\right) \wedge {Has}\left(X, k, t_2\right) \supset\left(\exists t_3: T, t_3>\right. \\ & \max \left(t_1, t_2\right) \wedge {Has}\left(X, E N C_k\{|m|\}, t_3\right) \wedge E N C_K\{|m|\} \in \\ & \left.\mathit{Γ}_X\right), \end{aligned} $ |
| $ \begin{aligned} & \;\;\;\;\;\;\;\operatorname{DEC}: {Has}\left(X, E N C_k\{|m|\}, t_1\right) \wedge {Has}\left(X, k^{-1}, \right. \\ & \left.t_2\right) \supset\left(\exists t_3: T, t_3>\max \left(t_1, t_2\right) \wedge {Has}\left(X, m, t_3\right) \wedge\right. \\ & \left.m \in \mathit{Γ}_X\right) \text { 。} \end{aligned} $ |
公理ENC(encryption)意为加密，它表示主体X在t1时刻拥有消息m，且在t2时刻拥有密钥k，那么必然存在一个时间t3, 大于时间t1，t2，主体X利用加密密钥k和消息m生成加密消息ENCk{ |m| }。
公理DEC(decryption)意为解密，它表示主体X在时间t1拥有加密后消息，在t2时刻拥有加密密钥k-1，则必然存在一个t3, 大于时间t1，t2, 主体X利用密钥进行解密得到消息m，并将此消息m纳入知识集Γ中。
| $ \begin{aligned} & \quad \operatorname{TUP}: {Has}\left(X, m_1, t_1\right) \wedge {Has}\left(X, m_2, t_2\right) \supset\left(\exists t_3:\right. \\ & \left.T, t_3>\max \left(t_1, t_2\right)\right) \wedge {Has}\left(X, m_1 \| m_2, t_3\right) \wedge m_1 \| \\ & m_2 \in \mathit{Γ}_X, \end{aligned} $ |
| $ \begin{aligned} & \;\;\;\;\;\;\;\operatorname{PROJ}: {Has}\left(X, m_1 \| m_2, t\right) \supset {Has}\left(X, m_1, t\right) \wedge \\ & {Has}\left(X, m_2, t\right) \wedge m_1 \in \mathit{Γ}_X \wedge m_2 \in \mathit{Γ}_X 。\end{aligned} $ |
公理TUP(tuple)意为元组，它表示在t1时刻拥有消息m1，在t2时刻拥有消息m2, 那么在t3大于t1和t2时刻，主体X拥有m1，m2组成的级联消息，并将其纳入知识集Γ。
公理PROJ(project)表示如果主体X拥有两个消息组成的二元组，那么主体X将其子消息纳入知识集Γ中。
2) 因果公理(causal axioms)。
| $ \begin{aligned} & \;\;\;\;\;\;\;\text { CAU1: } \operatorname{Verify}\left(X, \operatorname{Sign}(m), k_{Y \text {. ver }}, t_1\right) \supset\left(\exists t_2:\right. \\ & \left.T, t_2 <t_1 ; \exists Y, Y \neq X\right) \wedge {Sign}\left(Y, m, k_{Y \text {. sig }}, t_2\right), \end{aligned} $ |
| $ \begin{aligned} & \;\;\;\;\;\;\;\text { CAU2:} {Receive }\left(X, m^{\prime}, t_1\right) \supset\left(\exists t_2: T, t_2 <t_1 ;\right. \\ & \left.\exists m: M, {Contain}\left(m, m^{\prime}\right) ; \exists Y, Y \neq X\right) {Send}(Y, m, \\ & \left.t_2\right) 。\end{aligned} $ |
公理CAU(causal)意为因果，公理CAU1表示如果主体X在t1时刻利用公钥验证了签名的有效性，则必然存在一个不等于X的主体Y，在t2时刻(t2小于t1)利用私钥对消息进行签名，公式中Sign意为标记，它代表Y利用私钥k对消息m进行签名，Verify意为验证，它表示X利用公钥验证了签名的有效性。
公理CAU2表示如果主体X在t1时刻收到消息m′，则必然存在一个不等于X的主体Y，在t2时刻(t2小于t1)发送了消息m，且m包含于m′，Contain为消息包含。
3) 时间单调公理(axioms of time monotonicity)。
| $\begin{aligned} & \;\;\;\;\;\;\;\text { TM1: } {Has}\left(X, m, t_1\right) \supset\left(\forall t_3: T, t_2>t_1\right) {Has}(X, \\ & \left.m, t_2\right) \wedge m \in \mathit{Γ}_X, \end{aligned} $ |
| $\begin{aligned} & \;\;\;\;\;\;\;\text { TM2: }\left(\forall t^{\prime}: T, t_1<t^{\prime}<t_2\right) {Has}\left(X, m, t^{\prime}\right) \wedge \\ & \left(\forall t^{\prime \prime}: T, t_2<t^{\prime \prime}<t_3\right) {Has}\left(X, m, t^{\prime \prime}\right) \supset\left(\forall t: T, t_1 <\right. \\ & \left.t^{\prime}<t_2\right) {Has}(X, m, t) \wedge m \in \mathit{Γ}_X 。\end{aligned} $ |
公理TM(time)为时间之意，公理TM1表示如果主体X在t1时刻拥有知识m, 则在此后的时刻，主体X将一直拥有m。
公理TM2表示主体的知识一旦拥有就不会再消失。
本文采用的推理规则为
定义1 消息组件：一个消息M的组件，如果知道一组消息组件{c1, c2, …, ci}, 就等同于知道消息M本身, 那么我们说这些组件构成了M。
| $ M_{\cap}^{\cup}\left\{c_1, \cdots c_i\right\} 。$ |
定义2 非否认协议基本符号正式定义一个不涉及可信第三方的非否认协议的表示方式。一个这样的协议包括两个参与者(发起者A和接收者B), 协议由n个通信步骤组成, 每个步骤是A发送消息给B，或B发送消息给A。
| $ \left(i . A \rightarrow B: m_i\right) \text { or }\left(i . B \rightarrow A: m_i\right) \text {, } $ |
一个不可否认协议PA, Bn(M)必须向参与者提供两项主要服务：发起方不可否认和接收方不可否认。该协议通过生成和交换发起方和接收方的证据来实现这一点，证据指的是可以被仲裁者用来判断一个事实是否为真的信息。在不可否认协议中涉及两种类型的证据：发送方非否认证据(NRO)和接收方非否认证据(NRR)。NRO证明A确实发送了消息M给B，NRR证明B确实接收到了M。
定义3 作弊在不可否认协议PA, Bn(M)运行T结束时，发起方A可以成功作弊，如果它正式定义了在一个协议运行中发起者A或接收者B作弊成功的条件。那么
| $ N R R \in \kappa_A(T) \text { and } \begin{cases}N R O \notin \kappa_B(T) & \text { or } \\ M \notin \kappa_B(T) & \text {, }\end{cases} $ |
| $ N R R \notin \kappa_A(T) \text { and } \begin{cases}N R O \notin \kappa_B(T) & \text { or } \\ M \notin \kappa_B(T) & \text {, }\end{cases} $ |
其中：κA表示发起者A的知识集。
定义4 策略协议主体发送消息的不同执行路径选择。诚实主体遵循诚信原则发送和接收消息，不诚实主体即恶意主体可能存在发送虚假消息以及发送空消息的情况。
定义5 协议执行路径根据不同的主体策略选择不同的协议执行过程。
定义6 公平性定义 公平性包括发起者公平性和响应者公平性。
P为协议发起者，Q为协议响应者，发起者公平性是指发起者在协议运行过程中遵循诚实原则，而响应者为恶意主体，此时协议满足发起者公平性。响应者公平性是指响应者在协议运行过程中遵循诚实原则而发起者为恶意主体，此时协议满足响应者公平性。当协议既满足发起者公平性又满足响应者公平性，则称协议满足公平性，即
| $ { Fairness }(F E P) \triangleq { Fairness }(P) \cap { Fairness }(Q) { 。} $ |
形式化描述即通过事件逻辑对安全协议自身以及要满足的安全目标进行建模。形式化规约是使用事件逻辑证明系统中的公理、引理对安全协议的规则性质规约为逻辑公式，再形式化验证安全协议是否满足安全属性，如果满足即证明该协议是安全的，如果不满足则针对该协议可能存在的漏洞以及攻击提出相应的改进方案，进一步完善协议。形式化方法分析协议是建立在数学基础上的一种分析方法，具有严谨、细致以及准确的特点，是信息安全领域不可或缺的一种工具，它不仅能做到漏洞检测与修复，而且还可以进行安全协议设计指导，更好地保护信息时代网络安全。
2 协议形式化分析及验证我们选择研究基于身份属性的混淆乐观公平交换协议，其相较于传统的交换方案，乐观公平交换方案允许两方或者多方存在信息交换过程中，可信第三方(trusted thirty party，TTP)不必参与每次交换，只有在出现争端时才需要TTP进行解决，这样的方案使TTP工作量大幅降低。为了满足社交网络中密钥管理需要进行简化的要求，基于身份认证的混淆乐观公平方案(identity based-ambiguous optimistic fair exchange，ID-AOFE)被提出。
2.1 形式化描述协议戚珉等[13]提出了基于身份的混淆乐观公平交换协议, 该协议以文献[6]没有基于真实用户环境这一缺陷提出。本文基于真实的用户环境，防止签名验证者利用部分签名取得不公平的优势，协议描述如图 1所示。
|
图 1 ID-AOFE协议方案的信息交互模型 Fig. 1 Information interaction model of ID-AOFE protocol scheme |
图 1为正常的信息交换过程。交换开始，Alice拥有全部签名σA, F和部分签名σA，P，Alice将部分签名发送给Bob，Bob利用Pver算法(接收者接收部分签名验证算法)验证该签名的正确性，如果正确，则将自己的完整签名σB, F发送给Alice，Alice收到后将自己的完整签名σA, F发送Bob。其中，交换子协议结束时，Alice得到Bob的全部消息，Bob收到Alice的全部消息，如果主体Alice或者Bob没有正确接收，则启动争端解决子协议。
图 2中，当Bob收到核验正确的Alice部分签名后，向Alice发送了自己的全部签名σB, F，Alice未按协议要求继续发送自己的全部签名，此时进入响应者争端解决过程，Bob向TTP发送A, B, σA.P, σB.F，TTP在限制的时间T之前收到该消息，验证正确后，向Bob发送Alice的完整签名σA, F，若超时无论TTP验证消息是否正确均返回错误。
|
图 2 响应者发起争端请求 Fig. 2 The responder initiates a dispute request |
图 3中，当Alice已经发送自己的部分签名σA.P给Bob，但未收到Bob的完整签名σB.F，则进入争端解决，在大于时间T后，TTP检查自己的数据库是否存在Bob曾经的争端解决记录，若存在则发送σB.F给Alice，若不存在则返回错误。
|
图 3 发起者发起争端请求 Fig. 3 The initiator initiates a dispute request |
公平性是公平交换协议的核心属性，同时也是本文的主要研究内容。协议的强公平性是指在整个协议中，参与的协议主体均得到了想要得到的信息，或者均一无所获，这种公平性称为强公平性。如果参与协议的双方有诚实主体没有得到期望的消息，但通过可信第三方的协调在争端处理之后获得了所期望的信息，称为弱公平性。本文所称的公平性为弱公平性，在现实生活中，强公平性过于理想化而难以实现。
在公平交换协议中，恶意主体通常会通过延迟消息的发送、篡改伪造消息以及故意延迟消息发送并退出协议等方式造成主体被迫终止协议运行。
本文分析协议公平性的过程如下：首先，对协议进行形式化，主要是对协议中涉及的实体、消息以及动作进行逻辑抽象；其次，分别列出协议需要满足的发起者公平性和响应者公平性，用事件逻辑公式表达；最后，再列出所有恶意主体的可选择策略构成的路径，筛选出其中可能造成公平性缺失的路径，并利用加入了时间的时间逻辑公式分析诚实主体是否满足公平性。
ID-AOFE协议的初始状态定义为〈X, Θ0, Γ0, t0〉，X为协议参考主体，A，B，I分别为发起者Alice，接收者Bob，入侵者Intruder的缩写，ΘXt0为主体X在t时刻的状态，那么
| $ \begin{gathered} X \in\{A, B, T T P, I\} ; \mathit{Θ}_X^{t_0}= { Init } ; t_0=0, \\ \mathit{Γ}_A^{t_0}=\left\{\sum\limits_A^{t_0}=\{A, B, T T P\} ; M_A^{t_0}\right\}, \\ \mathit{Γ}_B^{t_0}=\left\{\sum\limits_B^{t_0}=\{B\} ; M_B^{t_0}\right\}, \\ \mathit{Γ}_{T T P}^{t_0}=\left\{\sum\limits_{T T P}^{t_0}=\{T T P\} ; M_{T T P}^{t_0}\right\}, \\ \mathit{Γ}_I^{t_0}=\left\{\sum\limits_I^{t_0}=\{I\} ; M_I^{t_0}\right\} 。\end{gathered} $ |
协议开始执行后，诚实主体按照规定行为序列进行信息交换，而恶意主体则有按照协议规定发送消息、发送虚假消息、不发送消息三种不同的选择。下面分别从发起者是恶意主体以及响应者为恶意主体两方面对协议公平性进行分析。
1) 发起者为恶意主体的形式化分析。
发起者Alice为恶意主体时，当其第一次发送消息时，有三种可执行策略，分别为按照协议规定正确发送消息σA，P、不发送消息和发送错误消息σA，P*给响应者Bob。当她正确发送消息σA，F时，Bob由于是诚实主体，在接收到Alice发来的消息后，按照协议规定将自己的消息σB，F发送给Alice，Alice在接收到Bob的消息后，此时仍有三种可以选择的策略。第一种策略是Alice选择诚信的发送自己的消息σA，F时，协议双方均得到了想要的消息，此时协议满足公平性；第二种策略是Alice选择发送空消息给Bob，Bob未接收到Alice的完整签名，此时向TTP请求帮助，TTP调用相应的验证算法进行争端处理，当Bob在小于时间参数T内完成请求，TTP验证其满足时间要求后，验证Alice的部分签名和Bob的完整签名，若验证有效，则从σA，P中恢复Alice的完整签名σA, F=(σA, σA, P)返回给Bob，并存储相应的争端解决记录，协议双方均得到了想要的消息，此时协议满足公平性。但需要注意的是，当恶意的Alice在Bob请求TTP解决纠纷过程中，完全阻隔Bob与TTP之间的通信，使得Bob不能成功完成请求，此时响应者Bob处于不公平状态，协议在此时不满足公平性；第三种策略是Alice选择发送虚假消息σA, F*给Bob，Bob由于缺乏相应的完整签名验证算法而无法识别此时消息的真伪，但Alice得到了其想要的签名消息，此时协议处于一种不公平状态。
当发起者Alice选择不发送消息给Bob时，Bob没有得到任何消息，同时根据协议要求，他没有发送任何消息，此时协议满足公平性。
当Alice在第一次发送消息时，选择发送虚假消息σA, P*给响应者Bob，Bob此时调用Pver(接收者接收部分签名验证算法)算法对此签名进行验证，验证没有通过，协议终止，此时协议满足公平性。
在发起者是恶意的情况下，协议不满足发起者公平性, 这种攻击主要是利用B向TTP请求时出现超时行为。TTP无法有效解决此时的纠纷，弥补方式是在真实的网络环境下，将Bob与TTP之间的通信时间参数设置为一个合理的时间值。图 4展示了发起者为恶意主体时的时限性缺陷。
|
图 4 发起者为恶意主体时的时限性缺陷 Fig. 4 Time-limited defect diagram when the initiator is a malicious subject |
Wai、Verify分别为协议主体等待或变化的状态，Receive、Send表示发送或接收消息的动作，Timer、tra、com分别表示协议主体所用的时间、消息传输的时间、处理消息的时间，Act表示协议主体在收到消息后处于活跃的状态，发起者为恶意主体时各个主体状态的详细分析过程如下。
| $ \begin{aligned} & \mathrm{A} \rightarrow \mathrm{~B}: \\ & \begin{gathered} t=t_1: e_1^{t_1}=\operatorname{Send}\left(A, \sigma_{A, P}, t_1\right) \Rightarrow \\ \mathit{Γ}_A^{t_1}=\delta\left(\mathit{Γ}_A^{t_0}, e_1^{t_1}\right), \mathit{Θ}_A^{t_1}=\delta\left(H_A^{\prime 0}, e_1^{t_1}\right)={ Wai } \wedge \oplus {Timer}_A 。\end{gathered} \end{aligned} $ |
| $ \begin{aligned} & \text { B : } \\ & \;\;\;\;\;t=t_2\left(t_2\right. \left.=t_1+t_{\mathrm{tra}}^u\right): \alpha_B^{t_2}=\left(e_1^{t_1}, e_2^{t_2}\right), \\ & \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;e_1^{t_2} ={Receive}\left(B, t_2, \sigma_{A, P}\right), \\ & e_2^{t_2}={Verify}\left(B, \sigma_{A, P}, t_2\right) \Rightarrow \mathit{Γ}_B^{t_2}=\delta\left(\mathit{Γ}_B^{t_0}, \alpha_B^{t_2}\right), \\ & \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\mathit{Θ}_B^{t_2}=\delta\left(\mathit{Θ}_B^{t_0}, \alpha_B^{t_2}\right)=A c t 。\end{aligned} $ |
| $ \begin{aligned} &\mathrm{B} \rightarrow \mathrm{~A}:\\ &\begin{gathered} t=t_3\left(t_3=t_2+t_{\mathrm{com}}^B\right), \\ e_1^{t_3}={Send}\left(B, t_3, \sigma_{B, F}\right) \Rightarrow \mathit{Γ}_B^{t_2}=\delta\left(\mathit{Γ}_B^{t_2}, e_B^{t_3}\right), \\ \mathit{Θ}_B^{t_2}=\delta\left(\mathit{Θ}_B^{t_2}, \alpha_B^{t_3}\right)={ Wai } \wedge \oplus { Timer }_{\circ} \end{gathered} \end{aligned} $ |
| $ \begin{aligned} &\text { A : }\\ &\begin{gathered} t=t_4\left(t_4=t_3+t_{\mathrm{tra}}^u\right), \alpha_A^{t_4}=e_1^{t_4}, \\ e_1^{t_4}={Receive}\left(A, t_4, \sigma_{B, F}\right) \Rightarrow \mathit{Γ}_A^{t_4}=\delta\left(\mathit{Γ}_A^{t_1}, e_A^{t_4}\right), \\ \mathit{Θ}_B^{t_2}=\delta\left(\mathit{Θ}_A^{t_3}, \alpha_A^{t_4}\right)= { Act } \wedge \oplus { Timer }_{\circ} \end{gathered} \end{aligned} $ |
2) 响应者为恶意主体的形式化分析。
如果响应者为恶意主体而发起者为诚实主体，响应者的目的在于骗取发起者对合同的承诺。此时响应者发送消息时同样有三种可选择策略。
第一种策略是响应者正确地发送消息。此时发起者Alice因为是诚实主体，双方均诚实地遵守约定，协议此时满足公平性。
第二种策略是响应者在接收到发送者的消息后，发送自己的虚假消息σB，F*骗取诚实主体的完整签名σA，F。此时发起者缺乏相应的完整签名检测验证算法而导致协议不满足公平性。
第三种策略是响应者在接收到发送者的消息后选择不发送任何消息。此时Alice去找TTP进行协议争端解决，在大于时间参数T时，TTP检查自己的数据库。若存在记录(Alice，Bob，σA, F, σB, F)，则返回σB, F给Alice，此时由于双方均得到了对方的完整签名，满足协议的公平性，否则返回错误，仍满足协议的公平性。
交换子协议中当响应者为恶意主体时各主体的状态如下所示。
| $ \begin{aligned} \mathrm{A} \rightarrow \mathrm{~B}: & \\ t=t_1: e_1^{t_1} & ={Send}\left(A, \sigma_{A, P}, t_1\right) \Rightarrow \mathit{Γ}_A^{t_1}=\delta\left(\mathit{Γ}_A^{t_0}, e_1^{t_1}\right), \\ \mathit{Θ}_A^{t_1} & =\delta\left(\mathit{Θ}_A^{t_0}, e_1^{t_1}\right)={ Wai } \wedge \oplus {Timer}_A \circ \end{aligned} $ |
| $ \begin{aligned} &\text { B: }\\ &\begin{gathered} t=t_2\left(t_2=t_1+t_{\mathrm{tra}}^u\right), \alpha_B^{t_2}=\left(e_1^{t_1}, e_2^{t_2}\right), \\ e_1^{t_2}={Receive}\left(B, t_2, \sigma_{A, P}\right), \\ e_2^{t_2}={Verify}\left(B, \sigma_{A, P}, t_2\right) \Rightarrow \mathit{Γ}_B^{t_2}=\delta\left(\mathit{Γ}_B^{t_0}, \alpha_B^{t_2}\right), \\ \mathit{Θ}_B^{t_2}=\delta\left(\mathit{Θ}_B^{t_0}, \alpha_B^{t_2}\right)=A c t。\end{gathered} \end{aligned} $ |
| $ \begin{aligned} & \mathrm{B} \rightarrow \mathrm{A} : \\ &\begin{gathered} t_3\left(t_3=t_2+t_{\mathrm{com}}^A\right), \\ \alpha_B^{t_3}=e_1^{t_3}=\sigma \vee \sigma^{\prime} \vee \sigma^*, \\ \sigma={Send}\left(B, \sigma_{B, F}, t_5, \right), \sigma^{\prime}={Send}\left(A, \varepsilon, t_5, \right), \\ \;\;\;\;\sigma^*={Send}\left(A, \sigma_{B, F}^*, t_5, \right) \Rightarrow \mathit{Γ}_B^{t_3}=\delta\left(\mathit{Γ}_B^{t_2}, e_B^{t_3}\right), \end{gathered} \\ & \;\;\;\;\;\;\mathit{Θ}_B^{t_3}=\delta\left(\mathit{Θ}_B^{t_3}, \sigma \vee \sigma^*\right)= \\ & \;\;\;\;\;\;\;Suc \vee \mathit{Θ}_B^{t_3}=\delta\left(\mathit{Θ}_B^{t_2}, \sigma^{\prime}\right)=A b o \wedge \otimes {Timer}_A 。\end{aligned} $ |
| $ \begin{aligned} &\text { A : }\\ &\begin{gathered} l t=t_4\left(t_4=t_3+t_{\mathrm{tra}}^u\right), \\ e_1^{t_4}={Receive}\left(B, \sigma \vee \sigma^{\prime} \vee \sigma^*, t_4\right), \Rightarrow \mathit{Γ}_A^{t_4}=\delta\left(\mathit{Γ}_A^{t_3}, e_1^{t_4}\right), \\ \mathit{Θ}_A^{t_4}=\delta\left(\mathit{Θ}_A^{t_4}, e_1^{t_4}\right)={Suc} \vee \mathit{Γ}_A^{t_4}=\delta\left(\mathit{Γ}_A^{t_3}, e_1^{t_4}\right), \\ \end{gathered} \\ & \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\mathit{Θ}_A^{t_4}=\delta\left(\mathit{Θ}_A^{t_4}, e_1^{t_4}\right)= \\ &\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;{ Act } \wedge \oplus { Timer }_B \vee \mathit{Γ}_A^{* t_4}=\delta\left(\mathit{Γ}_A^{t_3}, e_1^{t_4}\right), \\ &\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\mathit{Θ}_B^{t_4}=\delta\left(\mathit{Θ}_A^{t_4}, e_1^{t_4}\right)=\text { Abo } \wedge \otimes { Timer }_{\circ} \end{aligned} $ |
| $ \begin{aligned} &\text { A → TTP : }\\ &\begin{gathered} t=t_5\left(t_5=t_4+t_{\mathrm{com}}^A\right) ; \alpha_A^{t_5}=e_1^{t_5} ; \\ {Send}\left(A, B, \sigma_{A, F}, t_5\right) \Rightarrow \mathit{Γ}_A^{t_5}=\delta\left(\mathit{Γ}_A^{t_4}, e_A^{t_5}\right), \\ \mathit{Θ}_A^{t_5}=\delta\left(\mathit{Θ}_A^{t_4}\right) 。\end{gathered} \end{aligned} $ |
| $ \begin{aligned} &\text { TTP : }\\ &\begin{gathered} t=t_6\left(t_6=t_5+t_{\mathrm{com}}^A\right), \alpha_{\mathrm{TTP}}^{t_6}=e_1^{t_6}, \\ {Receive}\left(A, B, \sigma_{A, F}, t_6\right) \Rightarrow \mathit{Γ}_A^{t_6}=\delta\left(\mathit{Γ}_A^{t_5}, e_A^{t_6}\right), \\ \mathit{Θ}_A^{t_6}=\delta\left(\mathit{Θ}_A^{t_5}\right) \text { 。} \end{gathered} \end{aligned} $ |
| $ \begin{aligned} & \mathrm{TTP} \rightarrow \mathrm{~A}: \\ &\begin{gathered} t=t_7\left(t_7=t_6+t_{\mathrm{com}}^{T T P}\right) ; \alpha_{\mathrm{TTP}}^{t_7}=e_1^{t_7} ; \\ {Send}\left(\sigma_{B, F}, t_7\right) \Rightarrow \mathit{Γ}_A^{t_7}=\delta\left(\mathit{Γ}_A^{t_6}, e_A^{t_7}\right), \\ \mathit{Θ}_A^{t_7}=\delta\left(\mathit{Θ}_A^{t_6}\right) \text { 。} \end{gathered} \end{aligned} $ |
| $ \begin{aligned} &\text { A : }\\ &\begin{gathered} t=t_8\left(t_8\right. \left.=t_7+t_{\mathrm{tra}}^u\right): \alpha_{\mathrm{TTP}}^{t_8}=\left(e_1^{t_7}, e_2^{t_7}\right), \\ e_1^{t_2} ={Receive}\left(A, t_7, \sigma_{B, F}\right), \\ e_2^{t_7}={Verify}\left(B, \sigma_{B, F}, t_7\right) \Rightarrow \mathit{Γ}_A^{t_7}=\delta\left(\mathit{Γ}_A^{t_6}, \alpha_A^{t_6}\right), \\ \mathit{Θ}_A^{t_7}=\delta\left(\mathit{Θ}_A^{t_6}, \alpha_A^{t_7}\right)=\otimes { Timer }_{\circ} \end{gathered} \end{aligned} $ |
当响应者为恶意主体时, 不公平性主要是缺少对完整签名的验证算法。显然，在响应者作为恶意主体时，响应者得到了期望的消息，而发起者却没有收获，此时的ID-AOFE协议是不满足公平性的。
3 结语本文利用加入了时间因素的事件逻辑理论分析基于身份的混淆乐观公平协议(ID-AOFE)，并形式化建模需要满足的安全属性，形式化模型准确、完整地刻画了ID-AOFE协议的流程，并检验出该协议存在两个攻击漏洞以及不公平性，说明了加入时间因素的事件逻辑方法在分析协议公平性上是通用且可行的。本模型具有很好的扩展性, 这种时间细粒度建模方法同样也适用于类似的公平性交换协议，有助于发现协议交互过程中隐藏的时限性攻击。在以后的工作中将继续添加其他定理证明因素，使构建的验证平台能够更加快捷高效地证明网络协议的安全性。
| [1] |
XIAO M H, BICKFORD M. Logic of events for proving security properties of protocols[C]//2009 International Conference on Web Information Systems and Mining. Piscataway: IEEE Press, 2009: 519-523.
(  0) |
| [2] |
KULIK T, DONGOL B, LARSEN P G, et al. A survey of practical formal methods for security[J]. Formal aspects of computing, 2022, 34(1): 1-39. ( 0) |
| [3] |
韩志耕, 石青山, 杨鹏, 等. 不可否认协议分析的扩展ZQZ逻辑方法[J]. 密码学报, 2022, 9(1): 60-75. HAN Z G, SHI Q S, YANG P, et al. Extended ZQZ logic method for analysis of non-repudiation protocols[J]. Journal of cryptologic research, 2022, 9(1): 60-75. ( 0) |
| [4] |
钟同圣, 卫丰, 王鸷, 等. Python语言和ABAQUS前处理二次开发[J]. 郑州大学学报(理学版), 2006, 38(1): 60-64. ZHONG T S, WEI F, WANG Z, et al. Second development for fore treatment of ABAQUS using Python language[J]. Journal of Zhengzhou university (natural science edition), 2006, 38(1): 60-64. ( 0) |
| [5] |
HUANG Q, WONG D S, SUSILO W. A new construction of designated confirmer signature[J]. IEEE Transactions on information forensics and security, 2010, 5(1): 158-168. ( 0) |
| [6] |
ZHANG L, WU Q H, QIN B. Identity-based optimistic fair exchange in the standard model[J]. Security and communication networks, 2013, 6(8): 1010-1020. ( 0) |
| [7] |
陈明, 吴开贵, 吴长泽, 等. 公平交换协议形式逻辑[J]. 软件学报, 2011, 22(3): 509-521. CHEN M, WU K G, WU C Z, et al. Formal logic for fair exchange protocols[J]. Journal of software, 2011, 22(3): 509-521. ( 0) |
| [8] |
牛翠翠, 彭长根, 李新. 一种交换协议的理性模型及其公平机制设计[J]. 计算机应用研究, 2017, 34(5): 1504-1508. NIU C C, PENG C G, LI X. Rational model of exchange protocol and its mechanism design on fairness[J]. Application research of computers, 2017, 34(5): 1504-1508. ( 0) |
| [9] |
LOHR M, SCHLOSSER B, JVRJENS J, et al. Cost fairness for blockchain-based two-party exchange protocols[C]//2020 IEEE International Conference on Blockchain. Piscataway: IEEE Press, 2020: 428-435.
( 0) |
| [10] |
丁洪, 彭长根, 邝青青. 混合策略下的理性交换协议模型[J]. 网络与信息安全学报, 2016, 2(3): 68-75. DING H, PENG C G, KUANG Q Q. Rational exchange protocol model based on mixed strategy[J]. Chinese journal of network and information security, 2016, 2(3): 68-75. ( 0) |
| [11] |
杨科. 公平交换协议形式化分析关键技术研究[D]. 南昌: 华东交通大学, 2023. YANG K. Research on Key Techniques of Formal Analysis of Fair Exchange Protocol[D]. Nanchang: East China Jiaotong of University, 2023. ( 0) |
| [12] |
MICALI S. Simple and fast optimistic protocols for fair electronic exchange[C]//Proceedings of the Twenty-second Annual Symposium on Principles of Distributed Computing. New York: ACM Press, 2003: 12-19.
( 0) |
| [13] |
戚珉, 陈明. 标准模型下基于身份的混淆乐观公平交换方案[J]. 电子学报, 2020, 48(8): 1516-1527. QI M, CHEN M. ID-based ambiguous optimistic fair exchange in the standard model[J]. Acta electronica sinica, 2020, 48(8): 1516-1527. ( 0) |