# Formal Analysis of Fairness for Optimistic Multiparty Contract Signing Protocol

Authors: Xiaoru Li; Xiaohong Li; Guangquan Xu; Jing Hu; Zhiyong Feng
Journal: Journal of Applied Mathematics
 (2014)

---

## Abstract

Optimistic multiparty contract signing (OMPCS) protocols are proposed for exchanging multiparty digital signatures in a contract. Compared with general two-party exchanging protocols, such protocols are more complicated, because the number of protocol messages and states increases considerably when signatories increase. Moreover, fairness property in such protocols requires protection from each signatory rather than from an external hostile agent. It thus presents a challenge for formal verification. In our analysis, we employ and combine the strength of extended modeling language CSP# and linear temporal logic (LTL) to verify the fairness of OMPCS protocols. Furthermore, for solving or mitigating the state space explosion problem, we set a state reduction algorithm which can decrease the redundant states properly and reduce the time and space complexity greatly. Finally, this paper illustrates the feasibility of our approach by analyzing the GM and CKS protocols, and several fairness flaws have been found in certain computation times.


---

## Body

## 1. Introduction

The first optimistic multiparty contract signing protocol (OMPCS) was designed by Asokan et al. in 1997 [1]. The goal of this protocol is for all signatories to send signatures on a preagreed-upon contract text to all others and for every signatory to obtain all other signatories’ signatures on this contract. With the asymmetric structure, one partner must first send out his signature to the others; thus the fairness of such protocols is hard to guarantee. One method to solve the problem is to use a Trust Third Party (TTP) as an intermediary [2], but this method is not efficient and the TTP becomes a bottleneck as all signatories have to communicate with it. The other method is to design the so-called optimistic multiparty contract signing protocol which has the idea that only when an unfairness problem arises the TTP intervenes [1]. In 2009, Mauw et al. proposed the notion abort-chaining attacks and analyzed the message complexity of OMPCS protocols [3]. Resolve-impossibility which means that it is impossible to define a trusted party protocol for a special OMPCS protocol was presented [4].Some specific properties such as fairness, timeliness, and abuse-freeness should be satisfied in OMPCS protocols. Asokan defines a fairness system as that if a player behaves correctly, the other players will not gain any advantage over the correctly behaving player, and he divides fairness into strong fairness and weak fairness. Strong fairness means that, when the protocol has completed,A has B’s item, or B has gained no additional information about A’s item, and vice versa. Here, the assumed “item” means the signed contract, and “additional information” means information which can be obtained from the signed contract. However, weak fairness means that either strong fairness is achieved or a correctly behaving node can prove to an arbiter that an unfair situation has occurred [5].Although not so much attention has been paid to optimistic multiparty contract signing protocols, there have been several researchers who did certain remarkable work in the weak fairness verification field and got some achievements. The pioneer work can be traced to Chadha et al. [6]. Based on the alternation transition system (ATS) and symbolic tool Mocha, GM protocol was verified to be unfair when the number of signatories is four. Those authors also presented a CKS protocol and verified that the fairness can be guaranteed in the case of four. Then such method was used in [7] to analyze the fairness of MRT [8] and MR [9] protocols. The MRT protocol failed to satisfy fairness when the number of participators is three, and no flaw has been revealed in the MR protocol.As an analyzing method, the strand space model has lots of magnificent qualities such as intuitiveness and strictness. In [10], Mukhamedov et al. used a strand space model to describe the GM protocol and found a flaw. Theorem proving method uses formulae to verify the correctness of protocols. The CKS protocol was shown to have flaws in [11] by using the Isabelle/HOL theorem proving machine.This paper describes a precise and nature formulation of the desired weak fairness and universal OMPCS protocol models that includes multisignatories and contract texts promises simultaneously, formalizes protocol arithmetic, and considers composite attackers of the dishonest signatory. Besides, to mitigate the state explosion problem, a state reduction algorithm is proposed, and conversions between processes are supported, all of such actions can help our analysis to reach cases of more signatories. Furthermore, a visual attacking trace will be given when there exist error traces.The paper is structured as follows. Section2 defines the notion of OMPCS protocols and weak fairness. The CSP# language and the LTL logic are briefly introduced in Section 3. This section also explains how to build models for OMPCS protocols and how to express the weak fairness property. In the next section, we apply our novel method to the analysis of two typical OMPCS protocols GM and CKS. Finally, conclusions and future work are summarized.


## 2. Definitions

Definition 1 (optimistic multiparty contract signing).
A protocol for at leastn
(
n
≥
2
) signatories P
1
,
…
,
P
i
,
…
P
j
,
…
P
n to sign a contract m over a Trust Third Party is called a multiparty contract signing (MPCS) protocol. If all signatories are honest, the protocol terminates without T ever sending or receiving any messages; it is called an optimistic multiparty contract signing (OMPCS) protocol. An OMPCS protocol consists of three subprotocols: main subprotocol, recovery subprotocol, and abort subprotocol. The main subprotocol for n signers is divided into n-levels, which can be described recursively. The recovery and abort subprotocols are used to contact T when something goes wrong.
In an OMPCS protocol, every signer has a public and private key pair and can make a digital signature with the private key.PC
S
P
1
(
m
,
P
2
,
T
) (T is short for TTP) denotes the promise signed by P
1 and sent to P
2, and [10](a)
PC
S
P
1
(
m
,
P
2
,
T
) is generated by P
1;
(b)
P
2 can forge PC
S
P
1
(
m
,
P
2
,
T
) but can be distinguished by P
1, P
2, and T;
(c)
onlyP
1 and T can transfer PC
S
P
1
(
m
,
P
2
,
T
) into a digital signature S
P
1
(
m
) which can be universally verified.Definition 2 (weak fairness).
For a protocolΓ, a contract m, and signers P
i and P
j with each one’s signed contract S
P
i
(
m
) and S
P
j
(
m
), we call the protocol Γ  which satisfies weak fairness if and only if we get one of the following conditions:(a)
when the protocol is terminated, bothP
i and P
j have not received S
P
j
(
m
) and S
P
i
(
m
) from each other
(b)
or when the protocol is terminated, bothP
i and P
j have received S
P
j
(
m
) and S
P
i
(
m
) from each other.


## 3. Formal Method

Unlike classical security protocols, besides the security property, the OMPCS protocols also need to guarantee fairness between participants. For verifying such property, this paper described an innovative method and Figure1 shows the structure of it.Figure 1
Structure of the method.


### 3.1. Assumption

Considering the general conditions of OMPCS protocol, assumptions for our fairness analyzing method are as follows.(a)
Channel assumption (lower-case): channels between participants are not trusty; that is to say, the transmitting messages may be delayed and lost. However, channels between participants and the TTP are really reliable; that is, although the transmitting messages may be delayed, they will reach the destination in the limited time.
(b)
Participants of protocols: participants may not be honest, but there is at least one honest among a number of participants. The TTP is always honest, and the honest one will follow protocols. A dishonest one can be legal user, possessing his/her own public and private keys.
(c)
Attacker: the cryptography is assumed to be perfect, and external hostile agent is assumed not existing for fairness property in OMPCS protocols requires protection from each signatory rather than from external attackers. All of the assumption can let us only concentrate on the structure of the protocols.


### 3.2. System Variables

CSP# was proposed as an extension of CSP; it combines high-level modeling operators with shared variables and low-level programming constructs. The idea is to treat sequential terminating programs as atomic events [12].The CSP# model of an OMPCS protocol consists of participants (honest or dishonest), TTP and the communication channel. CSP# mathematical signals were applied to describe the protocols’ participants and the components which combine participants together. The syntax of basic operators is listed in Table1. Where P, Q are processes,e is a name representing an event with an optional sequential program prog, cond is a boolean formula,X is a set of events names, ch is a channel, exp
⁡ is an expression, and x is a variable.Table 1
Syntax of the CSP#.
Stop
Processes do nothing
Skip
Successful termination
P
[
]
Q
General choice
P
[
*
]
External choice
P
〈
〉
Q
Internal choice
P
∣
∣
∣
Q
Interleaving
P
∣
∣
Q
Parallel composition
If (cond){
P
} else {
Q
}
Conditional choice
e
{
p
r
o
g
}
→
P
Event prefixing
P
∖
X
Hiding all occurrences of event inX
[
c
o
n
d
]
P
Guarded process
P
;
Q
Sequential composition
c
h
!
e
x
p
→
P
Channel output
c
h
?
x
→
P
Channel inputUnder the modeling language CSP#, the system variables of protocol model are defined in Table2. Each sending message between signers is modeled using a variable, initialized to 0 and set as k when the successfully sent message level is k. Each sending message between signers and TTP is modeled using a boolean variable, initialized to false and set true when message was sent.Table 2
System variables.
P
r
⁡
_
i
_
j
P
r
⁡
_
i
_
j
=
k, if P
i has successfully sent the k level promise to P
j
P
i
⁡
_
R
e
c
o
v
e
r
y
_
j
P
i
⁡
_
R
e
c
o
v
e
r
y
_
j
_
t
P
i
⁡
_
R
e
c
o
v
e
r
y
_
j
_
t
_
m
P
i sends recovery requirement message to TTP, j is the max level of message P
j has sent to P
i, t is the max level of message P
t has sent to P
i, and m is the max level of message P
t has sent to P
i, and so on
P
i
_
s
t
o
p
P
i quits the protocol
P
i
_
c
o
n
t
a
c
t
e
d
_
T
P
i has sent recovery or abort requirement messages to TTP
P
i
⁡
_
S
j
P
i has successfully received the P
j signed contract
P
i
_
A
b
o
r
t
T
a
k
e
n
P
i sends abort requirement message to TTP
T
_
R
e
s
p
o
n
d
i
TTP has responded to the requirement ofP
i
T
_
R
e
c
o
v
e
r
y
_
s
e
n
d
_
P
i
TTP sends recovery message toP
i
T
_
A
b
o
r
t
_
s
e
n
d
_
P
i
TTP sends abort message toP
i
T
_
F
i
P
i has not sent abort message and TTP will force him/her to abort in certain situation
T
_
S
i
P
i has sent abort message
T
_
h
i
The highest levelP
i has sent to higher signer before it contacts TTP
T
_
l
i
The lowest levelP
i has sent to lower signer before it contacts TTP
T
_
k
i
The highest levelP
i has received from P
j
(
i
<
j
) The highest level P
i has received from all signers m, (
m
,
j
<
i
)


### 3.3. Modeling Protocol

The semantic model is based on the labeled transition system (LTS). An LTS is a three-tupleL
=
(
S
,
S
0
,
R
).(i)
S is set of states. A state can be described by giving value for all valuations in the CSP# model.
(ii)
S
0
∈
S is the set of initial states.
(iii)
R
:
S
×
∑
τ
×
S is the transition relation, ∑
τ is a set of all events, ∑
* is a set of all traces, and a trace is a sequence of events. For every state s
∈
S, there is a state s
′
∈
S such that (
s
,
s
′
)
∈
R. R is process expressions in our CSP# protocol model.A CSP# model configuration is composited of two components(
V
,
P
), where V is a function mapping a variable name to its value and P is a process expression. Then we can get the LTS
=
(
S
,
init, →), where S is the set of reachable system configurations, init is the initial configuration (
V
,
P
), and → is a transition relation.For every signer in protocol, we use a process to describeP
i
H
_
process, which describes how honest signer P
i behaves and the dishonest P
j has a corresponding process P
j
_
process. T
_
process is defined to model T which represents the processes of recovery and abort subprotocols. The protocol is then described as formula (1); P is the set of signatories:
(1)
sys
=
P
i
H
_
Process
∣
∣
∣
P
j
_
process
(
i
,
j
∈
P
)
.


### 3.4. Modeling Weak Fairness

In order to reason protocol model, fairness assertion is described by LTL (linear temporal logic). LTL was proposed by Pnueli in 1977 [13] and is used to verify computer program logic language.LTL is defined by assuming that the atomic formulae are state predicates. Formulae are built up in the usual way according to the following grammar. AP is a collection of atomic propositions of LTL:(a)
for all the atomic propositionsρ
∈
AP, ρ is a LTL formula;
(b)
the constants “true” and “false” are both LTL formulae;
(c)
ifφ, ϕ are two LTL formulae, then ¬
φ, φ
∨
ϕ, φ
∧
ϕ, G
φ, and F
φ are all LTL formulae;
(d)
every LTL formula can be built up by using finite times of the above formation rules.Hereφ and ϕ are two formulae, G reads as “global” (also can be written as [
]), and G
φ means that event φ has to hold on the entire subsequent path. F reads as “finally” (also can be written as <>), F
φ means that event φ eventually has to hold (somewhere on the subsequent path).According to the fairness definition and LTL logic, we assume that only signerP
i is honest, and the description of fairness of signer P
i is given in formula (2). It means that, when the protocol is terminated, if there is a reachable trace τ in which a signer in P
1
,
…
,
P
i
-
1
,
P
i
+
1
,
…
,
P
n can receive P
i’s digital signature S
P
i
(
m
), then there must exist τ
′ which is reachable from τ and can make P
i receive the digital signature of P
1
,
…
,
P
i
-
1
,
P
i
+
1
,
…
,
P
n:
(2)
〈
〉
[
]
(
(
∨
P
i
+
1
·
S
P
i
(
m
)
∨
⋯
∨
P
n
·
S
P
i
(
m
)
)
P
1
·
S
P
i
(
m
)
∨
⋯
∨
P
i
-
1
·
S
P
i
(
m
)
1111111
∨
P
i
+
1
·
S
P
i
(
m
)
∨
⋯
∨
P
n
·
S
P
i
(
m
)
)
1111111
⟶
[
]
〈
〉
(
∧
P
i
·
S
P
i
+
1
(
m
)
∧
⋯
∧
P
i
·
S
P
n
(
m
)
)
P
i
·
S
P
1
(
m
)
∧
⋯
∧
P
i
·
S
P
i
-
1
(
m
)
11111111111111111
∧
P
i
·
S
P
i
+
1
(
m
)
∧
⋯
∧
P
i
·
S
P
n
(
m
)
)
(
(
∨
P
i
+
1
·
S
P
i
(
m
)
∨
⋯
∨
P
n
·
S
P
i
(
m
)
)
P
1
·
S
P
i
(
m
)
∨
⋯
∨
P
i
-
1
·
S
P
i
(
m
)
)
.


### 3.5. State Reduction Algorithm

The model checking method has many advantages, such as, high level automation and exact description ability. But the idea of this method is based on exhausted state space searching. When we use it to verify some concurrent systems, the state space may be increased exponentially. That is the space explosion problem. Towards the space explosion problem, a detailed state reduction algorithm is demonstrated below and the algorithm is shown in Algorithm1.(a)
Deleting states that system cannot reach to decrease the searching time.
(b)
Deleting states that will absolutely lead to fairness which can make the track of attack trace more conveniently.
(c)
Combing transition relations which reach the same next states to compress the state space, that is,A
{
R
}
P and B
{
R
}
P, we can combine the two transition relations into (
A
∨
B
)
{
R
}
P. Here A, B, and P are states and R is transition function. The proof can be found in “Hoare Logic,” rules of consequence.
(d)
Letting the dishonest signers send the highest promises to each other, for the transaction between dishonest signers will not influence the fairness of the honest one. Such behaviors can cut down the number of messages between the dishonest signers and then can reduce the state space.Algorithm 1:The state reduction algorithm.
Procedure  StateReduction(trans)
(1)for  i
←
1  to   length(trans)
(2)do  if    (vaildate(trans[i]) = 1
&
&
exishon(i))∣∣(trans[i].mark = 0)
(3)then  delete(trans[i])
(4)
for   j
←
1  to  length(trans)
(5) do  if   (trans[i].state2 = trans[j].state2) && (i
!
=
j)
(6)then  t
r
a
n
s
[
j
]
.state1
←
trans[i]state1 + trans[j].state1
(7)
delete(trans[i])
(8)
for  i
←
1  to  n
(9)do  for  j
←
1  to  n
(10)do  if  (p
i
,
p
j
∈
d
i
s) && (i
!
=
j)
(11)then  p
_
i
_
j
←
n, p
_
j
_
i
←
n
(12)endtrans
⁡ is an array which stores the transition relations in the OMPCS model, and every transition relation in trans
⁡ contains two states as well as a variable; state 1 is the current state, state 2 is the next state, and trans
⁡.mark is the weight of states. If a state in a protocol model has been reached for m times, the value of mark for such state is m. The variable exishon
(
i
) is a function to judge whether, after P
i contactingT, there also exists an honest signer who has no contract T. validate
(
trans
⁡
[
i
]
)
=
true means that the transition relation trans
⁡
[
i
] contracted T, and T sent a recovery message to reply to it; otherwise, T sent an abort message.Line 1 to line 2 are corresponding to (a) and (b), according to the recovery subprotocols in OMPCS; ifvalidate
=
true and the honest signer have not contracted TTP before, this protocol will be fair. Lines 4 to 7 mean (c); if trans
⁡
[
i
] and trans
⁡
[
j
] have the same next state (state2), trans
⁡
[
i
]
.
state
1 will be combined with trans
⁡
[
j
]
.
state
1, and trans
⁡
[
i
] will be deleted.From lines 8 to 11,n is the number of signers, i, j here are the unique ID for signatories, and d
i
s are the sets for the dishonest signatories. In line 10, if P
i and P
j are dishonest signatories, then they will send the highest promise to each other and it is the pseudocode of (d).


## 3.1. Assumption

Considering the general conditions of OMPCS protocol, assumptions for our fairness analyzing method are as follows.(a)
Channel assumption (lower-case): channels between participants are not trusty; that is to say, the transmitting messages may be delayed and lost. However, channels between participants and the TTP are really reliable; that is, although the transmitting messages may be delayed, they will reach the destination in the limited time.
(b)
Participants of protocols: participants may not be honest, but there is at least one honest among a number of participants. The TTP is always honest, and the honest one will follow protocols. A dishonest one can be legal user, possessing his/her own public and private keys.
(c)
Attacker: the cryptography is assumed to be perfect, and external hostile agent is assumed not existing for fairness property in OMPCS protocols requires protection from each signatory rather than from external attackers. All of the assumption can let us only concentrate on the structure of the protocols.


## 3.2. System Variables

CSP# was proposed as an extension of CSP; it combines high-level modeling operators with shared variables and low-level programming constructs. The idea is to treat sequential terminating programs as atomic events [12].The CSP# model of an OMPCS protocol consists of participants (honest or dishonest), TTP and the communication channel. CSP# mathematical signals were applied to describe the protocols’ participants and the components which combine participants together. The syntax of basic operators is listed in Table1. Where P, Q are processes,e is a name representing an event with an optional sequential program prog, cond is a boolean formula,X is a set of events names, ch is a channel, exp
⁡ is an expression, and x is a variable.Table 1
Syntax of the CSP#.
Stop
Processes do nothing
Skip
Successful termination
P
[
]
Q
General choice
P
[
*
]
External choice
P
〈
〉
Q
Internal choice
P
∣
∣
∣
Q
Interleaving
P
∣
∣
Q
Parallel composition
If (cond){
P
} else {
Q
}
Conditional choice
e
{
p
r
o
g
}
→
P
Event prefixing
P
∖
X
Hiding all occurrences of event inX
[
c
o
n
d
]
P
Guarded process
P
;
Q
Sequential composition
c
h
!
e
x
p
→
P
Channel output
c
h
?
x
→
P
Channel inputUnder the modeling language CSP#, the system variables of protocol model are defined in Table2. Each sending message between signers is modeled using a variable, initialized to 0 and set as k when the successfully sent message level is k. Each sending message between signers and TTP is modeled using a boolean variable, initialized to false and set true when message was sent.Table 2
System variables.
P
r
⁡
_
i
_
j
P
r
⁡
_
i
_
j
=
k, if P
i has successfully sent the k level promise to P
j
P
i
⁡
_
R
e
c
o
v
e
r
y
_
j
P
i
⁡
_
R
e
c
o
v
e
r
y
_
j
_
t
P
i
⁡
_
R
e
c
o
v
e
r
y
_
j
_
t
_
m
P
i sends recovery requirement message to TTP, j is the max level of message P
j has sent to P
i, t is the max level of message P
t has sent to P
i, and m is the max level of message P
t has sent to P
i, and so on
P
i
_
s
t
o
p
P
i quits the protocol
P
i
_
c
o
n
t
a
c
t
e
d
_
T
P
i has sent recovery or abort requirement messages to TTP
P
i
⁡
_
S
j
P
i has successfully received the P
j signed contract
P
i
_
A
b
o
r
t
T
a
k
e
n
P
i sends abort requirement message to TTP
T
_
R
e
s
p
o
n
d
i
TTP has responded to the requirement ofP
i
T
_
R
e
c
o
v
e
r
y
_
s
e
n
d
_
P
i
TTP sends recovery message toP
i
T
_
A
b
o
r
t
_
s
e
n
d
_
P
i
TTP sends abort message toP
i
T
_
F
i
P
i has not sent abort message and TTP will force him/her to abort in certain situation
T
_
S
i
P
i has sent abort message
T
_
h
i
The highest levelP
i has sent to higher signer before it contacts TTP
T
_
l
i
The lowest levelP
i has sent to lower signer before it contacts TTP
T
_
k
i
The highest levelP
i has received from P
j
(
i
<
j
) The highest level P
i has received from all signers m, (
m
,
j
<
i
)


## 3.3. Modeling Protocol

The semantic model is based on the labeled transition system (LTS). An LTS is a three-tupleL
=
(
S
,
S
0
,
R
).(i)
S is set of states. A state can be described by giving value for all valuations in the CSP# model.
(ii)
S
0
∈
S is the set of initial states.
(iii)
R
:
S
×
∑
τ
×
S is the transition relation, ∑
τ is a set of all events, ∑
* is a set of all traces, and a trace is a sequence of events. For every state s
∈
S, there is a state s
′
∈
S such that (
s
,
s
′
)
∈
R. R is process expressions in our CSP# protocol model.A CSP# model configuration is composited of two components(
V
,
P
), where V is a function mapping a variable name to its value and P is a process expression. Then we can get the LTS
=
(
S
,
init, →), where S is the set of reachable system configurations, init is the initial configuration (
V
,
P
), and → is a transition relation.For every signer in protocol, we use a process to describeP
i
H
_
process, which describes how honest signer P
i behaves and the dishonest P
j has a corresponding process P
j
_
process. T
_
process is defined to model T which represents the processes of recovery and abort subprotocols. The protocol is then described as formula (1); P is the set of signatories:
(1)
sys
=
P
i
H
_
Process
∣
∣
∣
P
j
_
process
(
i
,
j
∈
P
)
.


## 3.4. Modeling Weak Fairness

In order to reason protocol model, fairness assertion is described by LTL (linear temporal logic). LTL was proposed by Pnueli in 1977 [13] and is used to verify computer program logic language.LTL is defined by assuming that the atomic formulae are state predicates. Formulae are built up in the usual way according to the following grammar. AP is a collection of atomic propositions of LTL:(a)
for all the atomic propositionsρ
∈
AP, ρ is a LTL formula;
(b)
the constants “true” and “false” are both LTL formulae;
(c)
ifφ, ϕ are two LTL formulae, then ¬
φ, φ
∨
ϕ, φ
∧
ϕ, G
φ, and F
φ are all LTL formulae;
(d)
every LTL formula can be built up by using finite times of the above formation rules.Hereφ and ϕ are two formulae, G reads as “global” (also can be written as [
]), and G
φ means that event φ has to hold on the entire subsequent path. F reads as “finally” (also can be written as <>), F
φ means that event φ eventually has to hold (somewhere on the subsequent path).According to the fairness definition and LTL logic, we assume that only signerP
i is honest, and the description of fairness of signer P
i is given in formula (2). It means that, when the protocol is terminated, if there is a reachable trace τ in which a signer in P
1
,
…
,
P
i
-
1
,
P
i
+
1
,
…
,
P
n can receive P
i’s digital signature S
P
i
(
m
), then there must exist τ
′ which is reachable from τ and can make P
i receive the digital signature of P
1
,
…
,
P
i
-
1
,
P
i
+
1
,
…
,
P
n:
(2)
〈
〉
[
]
(
(
∨
P
i
+
1
·
S
P
i
(
m
)
∨
⋯
∨
P
n
·
S
P
i
(
m
)
)
P
1
·
S
P
i
(
m
)
∨
⋯
∨
P
i
-
1
·
S
P
i
(
m
)
1111111
∨
P
i
+
1
·
S
P
i
(
m
)
∨
⋯
∨
P
n
·
S
P
i
(
m
)
)
1111111
⟶
[
]
〈
〉
(
∧
P
i
·
S
P
i
+
1
(
m
)
∧
⋯
∧
P
i
·
S
P
n
(
m
)
)
P
i
·
S
P
1
(
m
)
∧
⋯
∧
P
i
·
S
P
i
-
1
(
m
)
11111111111111111
∧
P
i
·
S
P
i
+
1
(
m
)
∧
⋯
∧
P
i
·
S
P
n
(
m
)
)
(
(
∨
P
i
+
1
·
S
P
i
(
m
)
∨
⋯
∨
P
n
·
S
P
i
(
m
)
)
P
1
·
S
P
i
(
m
)
∨
⋯
∨
P
i
-
1
·
S
P
i
(
m
)
)
.


## 3.5. State Reduction Algorithm

The model checking method has many advantages, such as, high level automation and exact description ability. But the idea of this method is based on exhausted state space searching. When we use it to verify some concurrent systems, the state space may be increased exponentially. That is the space explosion problem. Towards the space explosion problem, a detailed state reduction algorithm is demonstrated below and the algorithm is shown in Algorithm1.(a)
Deleting states that system cannot reach to decrease the searching time.
(b)
Deleting states that will absolutely lead to fairness which can make the track of attack trace more conveniently.
(c)
Combing transition relations which reach the same next states to compress the state space, that is,A
{
R
}
P and B
{
R
}
P, we can combine the two transition relations into (
A
∨
B
)
{
R
}
P. Here A, B, and P are states and R is transition function. The proof can be found in “Hoare Logic,” rules of consequence.
(d)
Letting the dishonest signers send the highest promises to each other, for the transaction between dishonest signers will not influence the fairness of the honest one. Such behaviors can cut down the number of messages between the dishonest signers and then can reduce the state space.Algorithm 1:The state reduction algorithm.
Procedure  StateReduction(trans)
(1)for  i
←
1  to   length(trans)
(2)do  if    (vaildate(trans[i]) = 1
&
&
exishon(i))∣∣(trans[i].mark = 0)
(3)then  delete(trans[i])
(4)
for   j
←
1  to  length(trans)
(5) do  if   (trans[i].state2 = trans[j].state2) && (i
!
=
j)
(6)then  t
r
a
n
s
[
j
]
.state1
←
trans[i]state1 + trans[j].state1
(7)
delete(trans[i])
(8)
for  i
←
1  to  n
(9)do  for  j
←
1  to  n
(10)do  if  (p
i
,
p
j
∈
d
i
s) && (i
!
=
j)
(11)then  p
_
i
_
j
←
n, p
_
j
_
i
←
n
(12)endtrans
⁡ is an array which stores the transition relations in the OMPCS model, and every transition relation in trans
⁡ contains two states as well as a variable; state 1 is the current state, state 2 is the next state, and trans
⁡.mark is the weight of states. If a state in a protocol model has been reached for m times, the value of mark for such state is m. The variable exishon
(
i
) is a function to judge whether, after P
i contactingT, there also exists an honest signer who has no contract T. validate
(
trans
⁡
[
i
]
)
=
true means that the transition relation trans
⁡
[
i
] contracted T, and T sent a recovery message to reply to it; otherwise, T sent an abort message.Line 1 to line 2 are corresponding to (a) and (b), according to the recovery subprotocols in OMPCS; ifvalidate
=
true and the honest signer have not contracted TTP before, this protocol will be fair. Lines 4 to 7 mean (c); if trans
⁡
[
i
] and trans
⁡
[
j
] have the same next state (state2), trans
⁡
[
i
]
.
state
1 will be combined with trans
⁡
[
j
]
.
state
1, and trans
⁡
[
i
] will be deleted.From lines 8 to 11,n is the number of signers, i, j here are the unique ID for signatories, and d
i
s are the sets for the dishonest signatories. In line 10, if P
i and P
j are dishonest signatories, then they will send the highest promise to each other and it is the pseudocode of (d).


## 4. Case Study

As an OMPCS protocol, the GM protocol was proposed by Garay and Mackenzie in [14]; then in [5] Asokan modified it and proposed the CKS protocol. In this section, the two protocols are modeled and analyzed on the platform PAT [15] and fairness flaws have been discovered.


### 4.1. GM and CKS

Each of the GM and CKS protocols has three subprotocols: main subprotocol, recovery subprotocol, and abort subprotocol. Such protocols use zero-knowledge primitives, private contract signatures [14]. The main subprotocol of the two protocols is the same, and major changes are in the recovery and abort subprotocols.The main subprotocol for n signers is divided inton-level recursions with n-level promises. P
1 sends i-level promise to P
2 which can be denoted as PC
S
P
1
(
(
m
,
i
)
,
P
2
,
T
). The third party is T; if there is nothing wrong in the execution of main subprotocol, T will not be invoked. Conversely, requirement messages will be sent by signers to T to guarantee fairness. For P
i to abort, it will send the abort message to T; for P
i to recover, it will send the corresponding recovery message. The messages are designed so that T can infer the promises that an honest signer would have sent when it launched the recovery subprotocol. For lack of space, we will not describe the two protocols and the details can be found in [6, 14].


### 4.2. Modeling GM Protocol

We have modeled and analyzed the GM protocol for three cases, and here we take the case of four parties for example. Figure2 describes the communications between signers, third party, and channels. We assume that the honest signer is P
1, P
2, P
3, and P
4 are dishonest, and P
2, P
3, and P
4 can collude to cheat P
1. P
1
H_process() was defined as the behavior of P
1 and P
2_process(), P
3_process(), P
4_process(), and T
_
process
(
) as the behaviors of P
2, P
3, P
4, and T. After doing that, the GM protocol was modeled as a parallel system called “sys1H.”Figure 2
Communications between signers, third party, and channels.


#### 4.2.1. Modeling GM Main Subprotocol

Main subprotocol is executed when signers exchange their promises. Whenn
=
4, the main subprotocol has 4 levels (see the OMPCS definition in Section 2) recursions. We use integer variables to describe promises between signers, and boolean variables represent messages between signers and T. The details of the main subprotocol model are shown in Algorithm 2.Algorithm 2:Modeling of four-party GM main subprotocol.
Modeling the behaviors of honest
P
1
in the four-party GM main subprotocol
P1H_process()=
⋯
⋯
//(1) honest P1 sends 1-level promises to P2
[
][!P1_stop &
& !P1_contacted_T &
& Pr_1_4_L==0 &
& Pr_1_3_L==0 &
& Pr_1_2_L==0 &
& Pr_2_1_L==1 &
& Pr_3_1_L==1 &
&
Pr_4_1_L==1]P1sendsp21{Pr_1_2_L=1;}->P1H_process()
//(2) honest P1 sends recovery requirement to T
[
] [!P1_stop &
& !P1_contacted_T &
& Pr_1_4_L==0 &
& Pr_1_3_L==0 &
& Pr_1_2_L==1 &
& Pr_2_1_L==1 &
& Pr_4_1_L==1 &
&
Pr_3_1_L==1]p1recovery111{P1_contacted_T=true; P1_Recovery_1_1_1=true;}->T_process()
Modeling the behaviors of dishonest
P
2
in the four-party GM main subprotocol
P2_process()=
⋯
⋯
//(3)dishonest P2 sends 1-level promise to P1
[
] [!P2_stop && Pr_2_1_L<1] P2sendP32 {Pr_2_1_L=1;}->P2_process()
//(4)dishonest P2 sends recovery requirement to T
[
] [!P2_stop && Pr_4_2_L==1 && Pr_3_2_L==1 && Pr_1_2_L==1]P2recovery111{P2_Recovery_1_1_1=true;}
->T_process()
System definition
sys1H∣=P1H_process() ∣∣∣ P2_process() ∣∣∣ P3_process() ∣∣∣P4_process();The honestP
1 mainly performs two kinds of actions in the main subprotocol, which includes sending promises to other signers and sending requirement to T. They are described in step (
1
) and step (
2
). Step (
1
) models the action of sending 1-level promise, in which we use boolean variables, such as Pr
⁡
_
1
_
3
_
L, to represent the promises exchanging. Setting Pr
⁡
_
1
_
2
_
L
=
1 means P
1 has successfully sent 1-level promise to P
2. Step (
2
) says that if P
1 has not received the correct promises, he can set P
2_Recovery_1_1_1 as true, which represents the action of sending out recovery requirement. Step (
3
) and Step (
4
) describe the malicious behaviors of dishonest P
2. Step (
3
) models that P
2 can send 1-level promise to P
1 and Step (
4
) specifies that P
2 can send recovery requirement to T at a relatively relaxing condition.


#### 4.2.2. Modeling GM Abort and Recovery Subprotocol

Algorithm3 models the actions of the T, that is, the abort and recovery subprotocols. T is a special player that has to be modeled in a particular way. The definition and grammar are the same as the main subprotocol. T_process() maintains two sets, S
(
m
) and F
(
m
), which are initialized as empty. When P
i sends abort message to T, S
(
m
) is set to be S
(
m
)
=
S
(
m
)
∪
{
i
}. Elements inside F
(
m
) are those signers who have not sent abort message to T. Based on the values of S
(
m
) and F
(
m
), the recovery or abort decision will be made by T.Algorithm 3:Modeling of four-party GM abort and recovery subprotocols.
T_process()=
Modeling of the four-party GM abort subprotocol
⋯
⋯
//(1)T agrees with the abort requirement from P2
[
][!T_Respond2 &
& P2_Abort_Send &
& !T_Validated &
& ( T_S4 ∣∣ T_S3)]TabortP21{T_S2=true; T_Abort_Send_P2=true;
T_Respond2=true;}->P2H_process()
//(2)T refuses the abort requirement from P2
[
][!T_Respond2 &
& P2_Abort_Send &
& T_Validated ]TabortP22{T_S2=true; T_Recovery_Send_P2=true;   T_Respond2=true;}-
>P2H_process()
Modeling of the four-party GM recovery subprotocol
⋯
⋯
//(3)T agrees with the recovery requirement from P3
[
] [P3_Recovery_1_3_3 && !T_Respond4 && !T_Respond3 && !T_Respond2 && !T_Respond1]TreocveryP31
{T_Recovery_Send_P3=true; T_Respond3=true; T_Validated=true;}->P3_process()
//(4)T refuses the recovery requirement from P3
[
] [P3_Recovery_1_3_3 && !T_Respond3 && (!T_Respond4 ∣∣ !T_Respond3 ∣∣ !T_Respond2 ∣∣ !T_Respond1)&&
!T_Validated && T_S4]TreocveryP312{T_F1=true;T_F2=true;T_S3=true;T_Abort_Send_P3=true;
T_Respond3=true}->P3_process()The actions ofT can be divided into two parts, the first part describes how T deals with abort request from P
2. T sends out abort token to P
2 if the status is that T
_
Validated is false and (
T
_
S
4
|
|
T
_
S
3
) is true. However, if T
_
Validated is true, this means the recovery message has already been sent. Then the abort request is to be refused. Part two models the behaviors of dealing with recovery requests from P
3; if T
_
Validated is true, the recovery message will be sent. However, conversely, T will make decisions based on the current conditions.


### 4.3. Modeling GM Fairness

The fairness ofP
1 can be divided into two parts. The first is that when GM protocol is finished, if P
1 has not received the contract signed by other signers, then every other signer also will not receive the contract signed by P
1. The remainder is that if any other signers have received the contract signed by P
1, then P
1 must have received the contract signed by other signers as well. So the LTL modeling of P
1’s fairness is illustrated in Algorithm 4.Algorithm 4:Modeling fairness of P
1.
sys1H= P1H_process() ∣∣∣ P2_process() ∣∣∣ P3_process() ∣∣∣P4_process();
#define goals1  (P4_S1 ∣∣ P3_S1 ∣∣ P2_S1);
#define goals2  (P1_S2 && P1_S3 && P1_S4);
#assert sys1H ∣= G ((goals1) -> F(goals2));Goal 1 means that at least one signer inP
2, P
3, and P
4 has received the contract signed by P
1. Meanwhile, goal 2 means that P
1 has received the contract signed by P
2, P
3, and P
4. The fairness of P
1 can be described as sys1H
|
=
G
(
(
goals
1
)
→
F
(
goals
2
)
), which means that, for all the traces of GM modeling system, if there is one trace to make one of P
2, P
3, and P
4 receive the signed contract from P
1, there must exist another trace that can guarantee that P
1 receives the signed contract from P
2, P
3, and P
4.


### 4.4. Modeling CKS Protocol

The model of CKS main subprotocol and the description of fairness remain the same with the GM protocol, so this section will concentrate on the abort and recovery part. The main difference is thatT, when presented with a recovery request, overturns its abort decision if and only if T can infer dishonesty on the part of each of the signers that contracted T in the past. Compared with GM, T in CKS also maintains two integer variables, but the difference is that the variables have different meanings than that in GM.We modeled cases of four and five signers of the CKS protocol and a fairness flaw was found in the case of five. For the sake of contrastive analysis, specifics ofP
2 abort request and P
3_Recovery_1_1_3_3 recovery requirements are shown in Algorithm 5.Algorithm 5:Modeling of five-party CKS abort and recovery subprotocols.
T_process()=
Modeling of the five-party CKS abort subprotocol
⋯
⋯
//(1)T agrees with the abort requirement from P2
[
][!T_Respond2 &
& P2_Abort_Send &
& !T_Validated ]TP2abort1{T_S2=true; T_Abort_Send_P2=true;
T_Respond2=true; T_h2=0; T_l2=1}->P2H_process()
//(2)T refuses the abort requirement from P2
[
][!T_Respond2 &
& P2_Abort_Send &
& T_Validated  ]TP2abort2{T_S2=true; T_Recovery_Send_P2=true;
T_Respond2=true}->P2H_process()
Modeling of the five-party CKS recovery subprotocol
⋯
⋯
//(3)T agrees with the recovery requirement from P3
[
][P3_recovery_1_1_3_3 && !T_Respond5 && !T_Respond4 && !T_Respond3 && !T_Respond2 && !
T_Respond1] P3reco1{T_Recovery_Send_P3=true;T_Respond3=true; T_Validated=true;}->P3_process()
//(4)T refuses the recovery requirement from P3
[
][P3_recovery_1_1_3_3 && !T_Respond3 && (T_Respond5∣∣T_Respond4∣∣T_Respond3∣∣T_Respond2∣∣
T_Respond1)&& !T_Validted && ((T_S5 && T_l5>0 ∣∣T_S4 && T_l4>0 ∣∣ T_S2 && T_h2>2∣∣T_S1 &&
T_h1>2 ))]P3reco3{T_Respond3=true;T_S3=true;T_Abort_Send_P3=true;T_h3=3;T_l3=3}->P3_process()


### 4.5. State Reduction

When modeling GM and CKS protocol, we mitigate the state space explosion problem based on the algorithm proposed in Section3.5. The detailed examples are given as below.(a)
Deleting states which cannot be reached: for instance, in the GM protocol, whenT is dealing with the requirement P
2_Recovery_1_3_2 from P
2, there is a state which requires that!
T
_
S
3
∧
!
T
_
S
4 and two elements in set {
T
_
S
1
,
T
_
S
3
,
T
_
S
4
} should be true. Then a conclusion can be reached that this state is unreachable, for the state constraint must be (
!
T
_
S
3
∧
!
T
_
S
4
)
∧
(
T
_
S
3
∨
T
_
S
4
), which is contradictory. Therefore, we can delete this state.
(b)
Deleting states which will absolutely lead to fairness: when modeling the GM protocol, ifP
4 sends T a recovery requirement P
4_Recovery_3_3_3 in the condition that no one has contacted T before, T will absolutely agree with P
4’s requirement, setting T
_
Validated
=
1. It is obvious to ensure that the fairness can be guaranteed for, in the recovery subprotocol, T cannot overturn the recovery decision. Therefore, this state can be ignored when we are searching for attacking trace.
(c)
Combining transition relations which have the same next states: in the GM protocol, whenT deals with the requirement P
3_Recovery_4_4_4 from P
3, there are two transition relations: one of the current states is T
_
F
3
∧
!
T
_
F
2
∧
!
T
_
F
4 and the other is !
T
_
F
3. However, those two states can reach the same next state; thus, they can be combined into one state (
(
T
_
F
3
∧
!
T
_
F
2
∧
!
T
_
F
4
)
∨
!
T
_
F
3
).
(d)
Letting the dishonest signers send the highest promises to each other: when we model the dishonest signersP
2 and P
3 in the CKS protocol, some of the intermediate states such as Pr
⁡
_
2
_
3
_
L
=
3 and Pr
⁡
_
3
_
2
_
L
=
2 can be deleted, letting P
2 and P
3 send the highest promise to each other directly, Pr
⁡
_
2
_
3
_
L
=
4 and Pr
⁡
_
3
_
2
_
L
=
4.


### 4.6. Analysis

One feature of the OMPCS protocol is that the number of participants can be varied and the structure is not symmetric. That is why the specification ofP
i is different from that of P
j
(
i
≠
j
). A number of CSP# models have been written in PAT for different signers for the GM and CKS protocols. We found that GM protocol cannot satisfy fairness for the case of n
≥
4, because we can verify that the protocol is not fair in case of four, and, in more signatories cases, if there is only one honest, then the dishonest can collaborate to cheat just as they do in the case of 4. The CKS protocol is not fair for the number of signers n
≥
5, the reason is the same for GM.Table3 shows one possible error trace for the GM protocol (P
1 is the honest one and n
=
4). State 0 is the initialized state. In state 1, P
3 contactsT by sending an abort requirement. According to [14],T agrees with this requirement and sends abort message, setting T
_
S
3
=
true. But the dishonest P
3 continues to execute the main subprotocol. Then P
2 contractT with a recovery requirement.T refuses P
2’s requirement based on the abort subprotocol with T
_
F
1
=
true, T
_
S
2
=
true. However, the dishonest P
2 continues to execute the main subprotocol. In the next state P
1 launches a resolve request toT, however T
_
F
1 is true and it indicates thatT will refuse P
1’s requirement and update T
_
S
1
=
true. Then the honest signer P
1 quits the main subprotocol. At last, P
4 sends a recovery requirement. For T
_
S
4 is false, T overturns the previous decision and agrees with P
4’s requirement. Hence the fairness of P
1 are violated. We also found unfairness trace when P
3 or P
2 is the dishonest signer.Table 3
The unfairness trace of the four-party GM protocol.
GM protocol
State 0
State 1
State 2
State 3
State 4
P4__Recovery_3_3_3
False
False
False
False
True
P3__abort
False
True
True
True
True
P2__Recovery_1_1_2
False
False
True
True
True
P1__Recovery_1_3_3
False
False
False
True
True
T_Abort_Send_P4
False
False
False
False
False
T_Recovery_Send_P4
False
False
False
False
True
T_Abort_Send_P3
False
True
True
True
True
T_Abort_Send_P2
False
False
True
True
True
T_Abort_Send_P1
False
False
False
True
True
goals1
False
False
False
False
True
goals2
False
False
False
False
False
Fairness
YES
YES
YES
YES
NOTable4 shows one possible unfairness trace for the CKS protocol (P
3 is the honest one and n
=
5). State 0 is also the initialized state. In step 1, P
5 sends an abort requirement toT.T agrees with this requirement and sends back an abort message with T
_
l
5
=
1, T
_
S
5
=
true. But the dishonest P
5 continues to execute the protocol. In state 2, P
1 contractT with a recovery requirement. T refuses P
1’s requirement and sets T
_
h
1
=
4, T
_
S
1
=
true, the dishonest P
1 continues to execute the main subprotocol. Then P
4 launches a recovery request to T. T refuses P
4’s requirement with an abort message, setting T
_
l
4
=
T
_
h
4
=
5, T
_
S
4
=
true. In the following states, P
2 send recovery messages toT andT will refuse it and update T
_
l
2
=
T
_
h
2
=
5, T
_
S
2
=
true. P
3 sends its signed contract to P
4 and P
5, but the dishonest P
4 and P
5 quits the protocol and P
3 contractsT with recovery requirement.Table 4
The unfairness trace of the five-party CKS protocol.
Revised GM protocol
State 0
State 1
State 2
State 3
State 4
State 5
P5_abort
False
True
True
True
True
True
P4__Recovery_5_4_4_4
False
False
False
True
True
True
P3__Recovery_6_6_5_5
False
False
False
False
False
True
P2__Recovery_5_5_5_5
False
False
False
False
True
True
P1__Recovery_1_4_4_4
False
False
True
True
True
True
T_Abort_Send_P5
False
True
True
True
True
True
T_Abort_Send_P4
False
False
False
True
True
True
T_Abort_Send_P3
False
False
False
False
False
True
T_Abort_Send_P2
False
False
False
False
True
True
T_Abort_Send_P1
False
False
True
True
True
True
goals1
False
False
False
False
False
True
goals2
False
False
False
False
False
False
Fairness
YES
YES
YES
YES
YES
NOHowever, according to [5] and the recovery subprotocol,T computes the value of T
_
h
i and T
_
k
i and finds (
T
_
S
2
)
∧
(
T
_
k
2
≤
T
_
h
2
), and then it makes a decision that it will not overturn the previous decision. Finally,T sends an abort message to P
3; thus, the fairness of P
3 is not guaranteed. The similar error traces can also be found when P
4, P
2, or P
1 is the dishonest one.


### 4.7. Experiment Comparison

In this paper, the fairness for four-party GM protocol and five-party CKS protocol has been verified. There are certain advantages of our method, such as less time and space complexity, more precise semantic, higher degree of automation, and more detailed results. The time and space consuming comparison between our method and the method in [5] is showed in Table 5; the unit for time is second and for memory is KB.Table 5
Experiment comparison.
This paper method
Reference [5] method
Time used
Memory used
Time used
Memory used
GM protocol
n
=
2
0.01
41179
0.050
51228
n
=
3
10.64
72056
38.72
92595
n
=
4
505.21
2479154
—
—
CKS protocol
n
=
2
0.01
39187
0.047
4568
n
=
3
8.29
60145
19.54
86347
n
=
4
552.31
2787336
—
—
n
=
5
1674.05
3105836
—
—We use a common environment for all the tests discussed in this section; the hardware environment for the two methods is the same. For [5], the model checking platform is cmocha and the operating system is Ubuntu. For our method, the model checking platform is PAT3, and the operating system is Windows 7.As Table5 demonstrated, although the problem of protocol fairness verification is a NP problem and the states and time are expected to increase exponentially in theory, our method can get the verification result in certain times in the three and four participants cases of the CKS protocol. Therefore, we can get a conclusion that the reduction algorithm did a good performance as no error trace was found in such cases, and every state in the state space was visited. On the contrary, the method in [5] consumed more time and memory. Specifically, in the four-party occasion, in our experiment environment, this method cannot get verification result in certain hours (we had waited for more than 12 hours). Moreover, this method cannot give explicitly a number of visited states and fairness counterexamples. The main reason is that our method has less system states, higher states compression ratio, and the trace back-track algorithm.


## 4.1. GM and CKS

Each of the GM and CKS protocols has three subprotocols: main subprotocol, recovery subprotocol, and abort subprotocol. Such protocols use zero-knowledge primitives, private contract signatures [14]. The main subprotocol of the two protocols is the same, and major changes are in the recovery and abort subprotocols.The main subprotocol for n signers is divided inton-level recursions with n-level promises. P
1 sends i-level promise to P
2 which can be denoted as PC
S
P
1
(
(
m
,
i
)
,
P
2
,
T
). The third party is T; if there is nothing wrong in the execution of main subprotocol, T will not be invoked. Conversely, requirement messages will be sent by signers to T to guarantee fairness. For P
i to abort, it will send the abort message to T; for P
i to recover, it will send the corresponding recovery message. The messages are designed so that T can infer the promises that an honest signer would have sent when it launched the recovery subprotocol. For lack of space, we will not describe the two protocols and the details can be found in [6, 14].


## 4.2. Modeling GM Protocol

We have modeled and analyzed the GM protocol for three cases, and here we take the case of four parties for example. Figure2 describes the communications between signers, third party, and channels. We assume that the honest signer is P
1, P
2, P
3, and P
4 are dishonest, and P
2, P
3, and P
4 can collude to cheat P
1. P
1
H_process() was defined as the behavior of P
1 and P
2_process(), P
3_process(), P
4_process(), and T
_
process
(
) as the behaviors of P
2, P
3, P
4, and T. After doing that, the GM protocol was modeled as a parallel system called “sys1H.”Figure 2
Communications between signers, third party, and channels.


### 4.2.1. Modeling GM Main Subprotocol

Main subprotocol is executed when signers exchange their promises. Whenn
=
4, the main subprotocol has 4 levels (see the OMPCS definition in Section 2) recursions. We use integer variables to describe promises between signers, and boolean variables represent messages between signers and T. The details of the main subprotocol model are shown in Algorithm 2.Algorithm 2:Modeling of four-party GM main subprotocol.
Modeling the behaviors of honest
P
1
in the four-party GM main subprotocol
P1H_process()=
⋯
⋯
//(1) honest P1 sends 1-level promises to P2
[
][!P1_stop &
& !P1_contacted_T &
& Pr_1_4_L==0 &
& Pr_1_3_L==0 &
& Pr_1_2_L==0 &
& Pr_2_1_L==1 &
& Pr_3_1_L==1 &
&
Pr_4_1_L==1]P1sendsp21{Pr_1_2_L=1;}->P1H_process()
//(2) honest P1 sends recovery requirement to T
[
] [!P1_stop &
& !P1_contacted_T &
& Pr_1_4_L==0 &
& Pr_1_3_L==0 &
& Pr_1_2_L==1 &
& Pr_2_1_L==1 &
& Pr_4_1_L==1 &
&
Pr_3_1_L==1]p1recovery111{P1_contacted_T=true; P1_Recovery_1_1_1=true;}->T_process()
Modeling the behaviors of dishonest
P
2
in the four-party GM main subprotocol
P2_process()=
⋯
⋯
//(3)dishonest P2 sends 1-level promise to P1
[
] [!P2_stop && Pr_2_1_L<1] P2sendP32 {Pr_2_1_L=1;}->P2_process()
//(4)dishonest P2 sends recovery requirement to T
[
] [!P2_stop && Pr_4_2_L==1 && Pr_3_2_L==1 && Pr_1_2_L==1]P2recovery111{P2_Recovery_1_1_1=true;}
->T_process()
System definition
sys1H∣=P1H_process() ∣∣∣ P2_process() ∣∣∣ P3_process() ∣∣∣P4_process();The honestP
1 mainly performs two kinds of actions in the main subprotocol, which includes sending promises to other signers and sending requirement to T. They are described in step (
1
) and step (
2
). Step (
1
) models the action of sending 1-level promise, in which we use boolean variables, such as Pr
⁡
_
1
_
3
_
L, to represent the promises exchanging. Setting Pr
⁡
_
1
_
2
_
L
=
1 means P
1 has successfully sent 1-level promise to P
2. Step (
2
) says that if P
1 has not received the correct promises, he can set P
2_Recovery_1_1_1 as true, which represents the action of sending out recovery requirement. Step (
3
) and Step (
4
) describe the malicious behaviors of dishonest P
2. Step (
3
) models that P
2 can send 1-level promise to P
1 and Step (
4
) specifies that P
2 can send recovery requirement to T at a relatively relaxing condition.


### 4.2.2. Modeling GM Abort and Recovery Subprotocol

Algorithm3 models the actions of the T, that is, the abort and recovery subprotocols. T is a special player that has to be modeled in a particular way. The definition and grammar are the same as the main subprotocol. T_process() maintains two sets, S
(
m
) and F
(
m
), which are initialized as empty. When P
i sends abort message to T, S
(
m
) is set to be S
(
m
)
=
S
(
m
)
∪
{
i
}. Elements inside F
(
m
) are those signers who have not sent abort message to T. Based on the values of S
(
m
) and F
(
m
), the recovery or abort decision will be made by T.Algorithm 3:Modeling of four-party GM abort and recovery subprotocols.
T_process()=
Modeling of the four-party GM abort subprotocol
⋯
⋯
//(1)T agrees with the abort requirement from P2
[
][!T_Respond2 &
& P2_Abort_Send &
& !T_Validated &
& ( T_S4 ∣∣ T_S3)]TabortP21{T_S2=true; T_Abort_Send_P2=true;
T_Respond2=true;}->P2H_process()
//(2)T refuses the abort requirement from P2
[
][!T_Respond2 &
& P2_Abort_Send &
& T_Validated ]TabortP22{T_S2=true; T_Recovery_Send_P2=true;   T_Respond2=true;}-
>P2H_process()
Modeling of the four-party GM recovery subprotocol
⋯
⋯
//(3)T agrees with the recovery requirement from P3
[
] [P3_Recovery_1_3_3 && !T_Respond4 && !T_Respond3 && !T_Respond2 && !T_Respond1]TreocveryP31
{T_Recovery_Send_P3=true; T_Respond3=true; T_Validated=true;}->P3_process()
//(4)T refuses the recovery requirement from P3
[
] [P3_Recovery_1_3_3 && !T_Respond3 && (!T_Respond4 ∣∣ !T_Respond3 ∣∣ !T_Respond2 ∣∣ !T_Respond1)&&
!T_Validated && T_S4]TreocveryP312{T_F1=true;T_F2=true;T_S3=true;T_Abort_Send_P3=true;
T_Respond3=true}->P3_process()The actions ofT can be divided into two parts, the first part describes how T deals with abort request from P
2. T sends out abort token to P
2 if the status is that T
_
Validated is false and (
T
_
S
4
|
|
T
_
S
3
) is true. However, if T
_
Validated is true, this means the recovery message has already been sent. Then the abort request is to be refused. Part two models the behaviors of dealing with recovery requests from P
3; if T
_
Validated is true, the recovery message will be sent. However, conversely, T will make decisions based on the current conditions.


## 4.2.1. Modeling GM Main Subprotocol

Main subprotocol is executed when signers exchange their promises. Whenn
=
4, the main subprotocol has 4 levels (see the OMPCS definition in Section 2) recursions. We use integer variables to describe promises between signers, and boolean variables represent messages between signers and T. The details of the main subprotocol model are shown in Algorithm 2.Algorithm 2:Modeling of four-party GM main subprotocol.
Modeling the behaviors of honest
P
1
in the four-party GM main subprotocol
P1H_process()=
⋯
⋯
//(1) honest P1 sends 1-level promises to P2
[
][!P1_stop &
& !P1_contacted_T &
& Pr_1_4_L==0 &
& Pr_1_3_L==0 &
& Pr_1_2_L==0 &
& Pr_2_1_L==1 &
& Pr_3_1_L==1 &
&
Pr_4_1_L==1]P1sendsp21{Pr_1_2_L=1;}->P1H_process()
//(2) honest P1 sends recovery requirement to T
[
] [!P1_stop &
& !P1_contacted_T &
& Pr_1_4_L==0 &
& Pr_1_3_L==0 &
& Pr_1_2_L==1 &
& Pr_2_1_L==1 &
& Pr_4_1_L==1 &
&
Pr_3_1_L==1]p1recovery111{P1_contacted_T=true; P1_Recovery_1_1_1=true;}->T_process()
Modeling the behaviors of dishonest
P
2
in the four-party GM main subprotocol
P2_process()=
⋯
⋯
//(3)dishonest P2 sends 1-level promise to P1
[
] [!P2_stop && Pr_2_1_L<1] P2sendP32 {Pr_2_1_L=1;}->P2_process()
//(4)dishonest P2 sends recovery requirement to T
[
] [!P2_stop && Pr_4_2_L==1 && Pr_3_2_L==1 && Pr_1_2_L==1]P2recovery111{P2_Recovery_1_1_1=true;}
->T_process()
System definition
sys1H∣=P1H_process() ∣∣∣ P2_process() ∣∣∣ P3_process() ∣∣∣P4_process();The honestP
1 mainly performs two kinds of actions in the main subprotocol, which includes sending promises to other signers and sending requirement to T. They are described in step (
1
) and step (
2
). Step (
1
) models the action of sending 1-level promise, in which we use boolean variables, such as Pr
⁡
_
1
_
3
_
L, to represent the promises exchanging. Setting Pr
⁡
_
1
_
2
_
L
=
1 means P
1 has successfully sent 1-level promise to P
2. Step (
2
) says that if P
1 has not received the correct promises, he can set P
2_Recovery_1_1_1 as true, which represents the action of sending out recovery requirement. Step (
3
) and Step (
4
) describe the malicious behaviors of dishonest P
2. Step (
3
) models that P
2 can send 1-level promise to P
1 and Step (
4
) specifies that P
2 can send recovery requirement to T at a relatively relaxing condition.


## 4.2.2. Modeling GM Abort and Recovery Subprotocol

Algorithm3 models the actions of the T, that is, the abort and recovery subprotocols. T is a special player that has to be modeled in a particular way. The definition and grammar are the same as the main subprotocol. T_process() maintains two sets, S
(
m
) and F
(
m
), which are initialized as empty. When P
i sends abort message to T, S
(
m
) is set to be S
(
m
)
=
S
(
m
)
∪
{
i
}. Elements inside F
(
m
) are those signers who have not sent abort message to T. Based on the values of S
(
m
) and F
(
m
), the recovery or abort decision will be made by T.Algorithm 3:Modeling of four-party GM abort and recovery subprotocols.
T_process()=
Modeling of the four-party GM abort subprotocol
⋯
⋯
//(1)T agrees with the abort requirement from P2
[
][!T_Respond2 &
& P2_Abort_Send &
& !T_Validated &
& ( T_S4 ∣∣ T_S3)]TabortP21{T_S2=true; T_Abort_Send_P2=true;
T_Respond2=true;}->P2H_process()
//(2)T refuses the abort requirement from P2
[
][!T_Respond2 &
& P2_Abort_Send &
& T_Validated ]TabortP22{T_S2=true; T_Recovery_Send_P2=true;   T_Respond2=true;}-
>P2H_process()
Modeling of the four-party GM recovery subprotocol
⋯
⋯
//(3)T agrees with the recovery requirement from P3
[
] [P3_Recovery_1_3_3 && !T_Respond4 && !T_Respond3 && !T_Respond2 && !T_Respond1]TreocveryP31
{T_Recovery_Send_P3=true; T_Respond3=true; T_Validated=true;}->P3_process()
//(4)T refuses the recovery requirement from P3
[
] [P3_Recovery_1_3_3 && !T_Respond3 && (!T_Respond4 ∣∣ !T_Respond3 ∣∣ !T_Respond2 ∣∣ !T_Respond1)&&
!T_Validated && T_S4]TreocveryP312{T_F1=true;T_F2=true;T_S3=true;T_Abort_Send_P3=true;
T_Respond3=true}->P3_process()The actions ofT can be divided into two parts, the first part describes how T deals with abort request from P
2. T sends out abort token to P
2 if the status is that T
_
Validated is false and (
T
_
S
4
|
|
T
_
S
3
) is true. However, if T
_
Validated is true, this means the recovery message has already been sent. Then the abort request is to be refused. Part two models the behaviors of dealing with recovery requests from P
3; if T
_
Validated is true, the recovery message will be sent. However, conversely, T will make decisions based on the current conditions.


## 4.3. Modeling GM Fairness

The fairness ofP
1 can be divided into two parts. The first is that when GM protocol is finished, if P
1 has not received the contract signed by other signers, then every other signer also will not receive the contract signed by P
1. The remainder is that if any other signers have received the contract signed by P
1, then P
1 must have received the contract signed by other signers as well. So the LTL modeling of P
1’s fairness is illustrated in Algorithm 4.Algorithm 4:Modeling fairness of P
1.
sys1H= P1H_process() ∣∣∣ P2_process() ∣∣∣ P3_process() ∣∣∣P4_process();
#define goals1  (P4_S1 ∣∣ P3_S1 ∣∣ P2_S1);
#define goals2  (P1_S2 && P1_S3 && P1_S4);
#assert sys1H ∣= G ((goals1) -> F(goals2));Goal 1 means that at least one signer inP
2, P
3, and P
4 has received the contract signed by P
1. Meanwhile, goal 2 means that P
1 has received the contract signed by P
2, P
3, and P
4. The fairness of P
1 can be described as sys1H
|
=
G
(
(
goals
1
)
→
F
(
goals
2
)
), which means that, for all the traces of GM modeling system, if there is one trace to make one of P
2, P
3, and P
4 receive the signed contract from P
1, there must exist another trace that can guarantee that P
1 receives the signed contract from P
2, P
3, and P
4.


## 4.4. Modeling CKS Protocol

The model of CKS main subprotocol and the description of fairness remain the same with the GM protocol, so this section will concentrate on the abort and recovery part. The main difference is thatT, when presented with a recovery request, overturns its abort decision if and only if T can infer dishonesty on the part of each of the signers that contracted T in the past. Compared with GM, T in CKS also maintains two integer variables, but the difference is that the variables have different meanings than that in GM.We modeled cases of four and five signers of the CKS protocol and a fairness flaw was found in the case of five. For the sake of contrastive analysis, specifics ofP
2 abort request and P
3_Recovery_1_1_3_3 recovery requirements are shown in Algorithm 5.Algorithm 5:Modeling of five-party CKS abort and recovery subprotocols.
T_process()=
Modeling of the five-party CKS abort subprotocol
⋯
⋯
//(1)T agrees with the abort requirement from P2
[
][!T_Respond2 &
& P2_Abort_Send &
& !T_Validated ]TP2abort1{T_S2=true; T_Abort_Send_P2=true;
T_Respond2=true; T_h2=0; T_l2=1}->P2H_process()
//(2)T refuses the abort requirement from P2
[
][!T_Respond2 &
& P2_Abort_Send &
& T_Validated  ]TP2abort2{T_S2=true; T_Recovery_Send_P2=true;
T_Respond2=true}->P2H_process()
Modeling of the five-party CKS recovery subprotocol
⋯
⋯
//(3)T agrees with the recovery requirement from P3
[
][P3_recovery_1_1_3_3 && !T_Respond5 && !T_Respond4 && !T_Respond3 && !T_Respond2 && !
T_Respond1] P3reco1{T_Recovery_Send_P3=true;T_Respond3=true; T_Validated=true;}->P3_process()
//(4)T refuses the recovery requirement from P3
[
][P3_recovery_1_1_3_3 && !T_Respond3 && (T_Respond5∣∣T_Respond4∣∣T_Respond3∣∣T_Respond2∣∣
T_Respond1)&& !T_Validted && ((T_S5 && T_l5>0 ∣∣T_S4 && T_l4>0 ∣∣ T_S2 && T_h2>2∣∣T_S1 &&
T_h1>2 ))]P3reco3{T_Respond3=true;T_S3=true;T_Abort_Send_P3=true;T_h3=3;T_l3=3}->P3_process()


## 4.5. State Reduction

When modeling GM and CKS protocol, we mitigate the state space explosion problem based on the algorithm proposed in Section3.5. The detailed examples are given as below.(a)
Deleting states which cannot be reached: for instance, in the GM protocol, whenT is dealing with the requirement P
2_Recovery_1_3_2 from P
2, there is a state which requires that!
T
_
S
3
∧
!
T
_
S
4 and two elements in set {
T
_
S
1
,
T
_
S
3
,
T
_
S
4
} should be true. Then a conclusion can be reached that this state is unreachable, for the state constraint must be (
!
T
_
S
3
∧
!
T
_
S
4
)
∧
(
T
_
S
3
∨
T
_
S
4
), which is contradictory. Therefore, we can delete this state.
(b)
Deleting states which will absolutely lead to fairness: when modeling the GM protocol, ifP
4 sends T a recovery requirement P
4_Recovery_3_3_3 in the condition that no one has contacted T before, T will absolutely agree with P
4’s requirement, setting T
_
Validated
=
1. It is obvious to ensure that the fairness can be guaranteed for, in the recovery subprotocol, T cannot overturn the recovery decision. Therefore, this state can be ignored when we are searching for attacking trace.
(c)
Combining transition relations which have the same next states: in the GM protocol, whenT deals with the requirement P
3_Recovery_4_4_4 from P
3, there are two transition relations: one of the current states is T
_
F
3
∧
!
T
_
F
2
∧
!
T
_
F
4 and the other is !
T
_
F
3. However, those two states can reach the same next state; thus, they can be combined into one state (
(
T
_
F
3
∧
!
T
_
F
2
∧
!
T
_
F
4
)
∨
!
T
_
F
3
).
(d)
Letting the dishonest signers send the highest promises to each other: when we model the dishonest signersP
2 and P
3 in the CKS protocol, some of the intermediate states such as Pr
⁡
_
2
_
3
_
L
=
3 and Pr
⁡
_
3
_
2
_
L
=
2 can be deleted, letting P
2 and P
3 send the highest promise to each other directly, Pr
⁡
_
2
_
3
_
L
=
4 and Pr
⁡
_
3
_
2
_
L
=
4.


## 4.6. Analysis

One feature of the OMPCS protocol is that the number of participants can be varied and the structure is not symmetric. That is why the specification ofP
i is different from that of P
j
(
i
≠
j
). A number of CSP# models have been written in PAT for different signers for the GM and CKS protocols. We found that GM protocol cannot satisfy fairness for the case of n
≥
4, because we can verify that the protocol is not fair in case of four, and, in more signatories cases, if there is only one honest, then the dishonest can collaborate to cheat just as they do in the case of 4. The CKS protocol is not fair for the number of signers n
≥
5, the reason is the same for GM.Table3 shows one possible error trace for the GM protocol (P
1 is the honest one and n
=
4). State 0 is the initialized state. In state 1, P
3 contactsT by sending an abort requirement. According to [14],T agrees with this requirement and sends abort message, setting T
_
S
3
=
true. But the dishonest P
3 continues to execute the main subprotocol. Then P
2 contractT with a recovery requirement.T refuses P
2’s requirement based on the abort subprotocol with T
_
F
1
=
true, T
_
S
2
=
true. However, the dishonest P
2 continues to execute the main subprotocol. In the next state P
1 launches a resolve request toT, however T
_
F
1 is true and it indicates thatT will refuse P
1’s requirement and update T
_
S
1
=
true. Then the honest signer P
1 quits the main subprotocol. At last, P
4 sends a recovery requirement. For T
_
S
4 is false, T overturns the previous decision and agrees with P
4’s requirement. Hence the fairness of P
1 are violated. We also found unfairness trace when P
3 or P
2 is the dishonest signer.Table 3
The unfairness trace of the four-party GM protocol.
GM protocol
State 0
State 1
State 2
State 3
State 4
P4__Recovery_3_3_3
False
False
False
False
True
P3__abort
False
True
True
True
True
P2__Recovery_1_1_2
False
False
True
True
True
P1__Recovery_1_3_3
False
False
False
True
True
T_Abort_Send_P4
False
False
False
False
False
T_Recovery_Send_P4
False
False
False
False
True
T_Abort_Send_P3
False
True
True
True
True
T_Abort_Send_P2
False
False
True
True
True
T_Abort_Send_P1
False
False
False
True
True
goals1
False
False
False
False
True
goals2
False
False
False
False
False
Fairness
YES
YES
YES
YES
NOTable4 shows one possible unfairness trace for the CKS protocol (P
3 is the honest one and n
=
5). State 0 is also the initialized state. In step 1, P
5 sends an abort requirement toT.T agrees with this requirement and sends back an abort message with T
_
l
5
=
1, T
_
S
5
=
true. But the dishonest P
5 continues to execute the protocol. In state 2, P
1 contractT with a recovery requirement. T refuses P
1’s requirement and sets T
_
h
1
=
4, T
_
S
1
=
true, the dishonest P
1 continues to execute the main subprotocol. Then P
4 launches a recovery request to T. T refuses P
4’s requirement with an abort message, setting T
_
l
4
=
T
_
h
4
=
5, T
_
S
4
=
true. In the following states, P
2 send recovery messages toT andT will refuse it and update T
_
l
2
=
T
_
h
2
=
5, T
_
S
2
=
true. P
3 sends its signed contract to P
4 and P
5, but the dishonest P
4 and P
5 quits the protocol and P
3 contractsT with recovery requirement.Table 4
The unfairness trace of the five-party CKS protocol.
Revised GM protocol
State 0
State 1
State 2
State 3
State 4
State 5
P5_abort
False
True
True
True
True
True
P4__Recovery_5_4_4_4
False
False
False
True
True
True
P3__Recovery_6_6_5_5
False
False
False
False
False
True
P2__Recovery_5_5_5_5
False
False
False
False
True
True
P1__Recovery_1_4_4_4
False
False
True
True
True
True
T_Abort_Send_P5
False
True
True
True
True
True
T_Abort_Send_P4
False
False
False
True
True
True
T_Abort_Send_P3
False
False
False
False
False
True
T_Abort_Send_P2
False
False
False
False
True
True
T_Abort_Send_P1
False
False
True
True
True
True
goals1
False
False
False
False
False
True
goals2
False
False
False
False
False
False
Fairness
YES
YES
YES
YES
YES
NOHowever, according to [5] and the recovery subprotocol,T computes the value of T
_
h
i and T
_
k
i and finds (
T
_
S
2
)
∧
(
T
_
k
2
≤
T
_
h
2
), and then it makes a decision that it will not overturn the previous decision. Finally,T sends an abort message to P
3; thus, the fairness of P
3 is not guaranteed. The similar error traces can also be found when P
4, P
2, or P
1 is the dishonest one.


## 4.7. Experiment Comparison

In this paper, the fairness for four-party GM protocol and five-party CKS protocol has been verified. There are certain advantages of our method, such as less time and space complexity, more precise semantic, higher degree of automation, and more detailed results. The time and space consuming comparison between our method and the method in [5] is showed in Table 5; the unit for time is second and for memory is KB.Table 5
Experiment comparison.
This paper method
Reference [5] method
Time used
Memory used
Time used
Memory used
GM protocol
n
=
2
0.01
41179
0.050
51228
n
=
3
10.64
72056
38.72
92595
n
=
4
505.21
2479154
—
—
CKS protocol
n
=
2
0.01
39187
0.047
4568
n
=
3
8.29
60145
19.54
86347
n
=
4
552.31
2787336
—
—
n
=
5
1674.05
3105836
—
—We use a common environment for all the tests discussed in this section; the hardware environment for the two methods is the same. For [5], the model checking platform is cmocha and the operating system is Ubuntu. For our method, the model checking platform is PAT3, and the operating system is Windows 7.As Table5 demonstrated, although the problem of protocol fairness verification is a NP problem and the states and time are expected to increase exponentially in theory, our method can get the verification result in certain times in the three and four participants cases of the CKS protocol. Therefore, we can get a conclusion that the reduction algorithm did a good performance as no error trace was found in such cases, and every state in the state space was visited. On the contrary, the method in [5] consumed more time and memory. Specifically, in the four-party occasion, in our experiment environment, this method cannot get verification result in certain hours (we had waited for more than 12 hours). Moreover, this method cannot give explicitly a number of visited states and fairness counterexamples. The main reason is that our method has less system states, higher states compression ratio, and the trace back-track algorithm.


## 5. Conclusion and Future Work

Based on modeling language CSP# and linear temporal logic, an efficient method which aims to analyze the fairness of optimistic multiparty contract signing protocols is presented in this paper. In order to demonstrate the feasibility of our method, two examples of the GM and CKS protocol have been described and several fairness attacking traces have been found. Comparisons also have been made in this paper between our method and other traditional methods. And the result shows that our method has certain strengths such as higher automation, less time and space complexity, visualized attacking trace, and better utility.There is no explicit model for any cryptographic primitives in this paper and the attack model is weaker than the original paper. The main challenge is to verify the OMPCS protocols fairness in a more general condition which accounts for cryptographic and a more relaxed communication model. In our next work, we plan to extend the automatic cryptographic protocol verifier ProVerif [16] to suit our fairness verification method.



---

*Source: 983204-2014-06-18.xml*