>
Analysis
of optimistic
multi-party contract signing
Rohit Chadha1,2,
Steve Kremer3,4, Andre Scedrov1
1University
of Pennsylvania
2University
of Sussex
3Universit茅
Libre de Bruxelles
4Birmingham
University
Digital Contract
signing
Use digital signatures
to sign a contract over a network
Contract text
is already agreed upon
Special instance
of fair exchange protocols
Important issue for
secure electronic commerce
Naive 2-party example
:
A 00/font> B : SigA (contract)
B 00/sub> A : SigB (contract)
Digital Contract
signing
Use digital signatures
to sign a contract over a network
Special instance
of fair exchange protocols
Important issue for
secure electronic commerce
Naive 2-party example
:
A 00/font> B : SigA (contract)
B 00/sub> A : 00/sub>
Bob may be
malicious and not send his signature
Asymmetry : someone must be the first to
send his signature
Properties
of Contract Signing
Fairness
If A can get B00
signature, then B can get A00 signature, and vice-versa
Timeliness
Avoids that a
participant gets stuck
Advantage
A participant
has an advantage if
it has a strategy
to complete the exchange
and it has a strategy
to abort the exchange
Abuse-freeness (provable
advantage)
Avoids that a
participant can prove to an external party that it has the power to
choose the outcome of the protocol
Evolution of
contract signing
Randomized protocols
Trusted
Party intervenes
Use trusted party
as a delivery authority
May cause a bottleneck
00/font>
Trusted Party intervenes
only in case of problem (optimistic
approach)
More complex, and
more error-prone 00/font>
In 1980, Even & Yacobi showed
that no
fair deterministic contract signing protocol exists without the participation
of a trusted party.
Formal methods
& contract signing
[Shmatikov, Mitchell,
2000]
Model-checker
Murphi
invariant checking
[Chadha, Kanovich,
Scedrov, 2001]
Specification in
MSR
inductive proofs
[Kremer, Raskin, 2002]
Model-checker Mocha
ATL (temporal logic
with game semantics)
[Chadha, Mitchell,
Scedrov, Shmatikov 2003]
general results (protocol
independent) on advantage
00/font>
Only 2-party contract signing protocols have been
studied
Topologies
Unlike for 2-party
protocols, the different instances of fair exchange protocols differ
significantly in the multi-party case
1-to-many
non-repudiation
and certified e-mail
ring topology
barter
full graph
contract signing
1
n
3
2
...
1
n
3
2
...
1
n
3
2
...
Contract signing
requires the most complicated protocols
Multi-party
contract signing
n participants
want to sign a contract
Properties for a
honest participant must hold against any
coalition of dishonest participants,
i.e., against up to n-1 dishonest participants
Every participant
must receive the signature of all other participants (topology is a full graph)
Multi-party
protocols
Astonishingly few
so far
[Asokan, Baum-Waidner,
Schunter, Waidner, T.R. 1998]
Optimistic
synchronous multi-party contract signing
[Baum-Waidner,
Waidner, T.R. 1998 & ICALP 2000]
Optimistic
asynchronous multi-party contract signing
[Garay,
MacKenzie, DISC 1999]
Optimistic
asynchronous multi-party contract signing
[Baum-Waidner, Waidner,
ICALP 2001]
Optimistic
asynchronous multi-party contract signing with reduced number of rounds
Protocol model
All participants
are players
2
versions of each player
described using guarded commands
honest : follow the protocol
dishonest : may send messages out of order and
continue the main protocol after contacting the trusted party
Messages are immediately available
for reading
Only structural flaws
are considered
no modelling of
the cryptographic primitives
Mocha cannot handle
parametric specifications
Small C++ programs for the GM protocol and the BW protocol,
that generate the Mocha specification for a given number of participants
The model-checker
Mocha
Guarded
commands
describing the protocol
ATL formula
Mocha
ATS
Model-Checking
YES
NO
C++ program
The BW protocol [Baum, Waidner, ICALP
2000]
Rather simple protocol,
with symmetric behaviour of each participant
T can overturn aborts
We used Mocha to
verify fairness for n=2,005, but no flaw was found
The basic protocol
does not aim to provide abuse-freeness
Non-standard definition
of contract
a special protocol
for verifying the validity of a contract is defined
GM protocol [Garay, MacKenzie, DISC
1999]
Recursive description of the protocol
The protocol is divided
into n levels
In each protocol
level specific promises are used
Promises are implemented
using private
contract signatures (convertible
designated verifier signatures)
The i-level protocol
is triggered when Pi receives
1-level promises from Pi+1 through
Pn
In i-level protocol
participants Pi through P1 exchange
i-level promises
They
agree on the contract with promises
(not signatures)
Pi
through P1 close higher level protocols
After the n-level
protocol actual signatures are exchanged
GM main protocol
for Pi
Pi Pi-1 ... P1
Distribute
1-level promises
(i-1)
level protocol
Collect
(i-1) level promises
Exchange
i-level promises
GM main prot.
(4 participants)
P4
P3
P2
P1
otherwise
stop
otherwise
stop
otherwise
stop
1-level
promise
1-level
promise
1-level
promise
1-level
promise
1-level
promise
1-level
promise
GM main prot.
(4 participants)
P4
P3
P2
P1
otherwise
abort
1-level
promise
2-level
promise
2-level
promise
2-level
promise
2-level
promise
otherwise
recover
otherwise
recover
otherwise
recover
GM main prot.
(4 participants)
P4
P3
P2
P1
3-level
promise
otherwise
recover
otherwise
recover
3-level
promise
3-level
promise
otherwise
recover
3-level
promise
otherwise
recover
otherwise
recover
3-level
promise
3-level
promise
3-level
promise
3-level
promise
3-level
promise
GM main prot.
(4 participants)
P4
P3
P2
P1
otherwise
recover
otherwise
recover
4-level
promise
4-level
promise
4-level
promise
4-level
promise
4-level
promise
4-level
promise
otherwise
recover
otherwise
recover
4-level
promise
4-level
promise
4-level
promise
otherwise
recover
4-level
promise
4-level
promise
4-level
promise
otherwise
recover
GM main prot.
(4 participants)
P4
P3
P2
P1
otherwise
recover
otherwise
recover
Signature
Signature
Signature
otherwise
recover
otherwise
recover
otherwise
recover
Signature
Signature
Signature
otherwise
recover
Signature
Signature
Signature
Signature
Signature
Signature
GM abort and
resolve for Pi
To
abort, Pi sends to T
SPi(m,Pi,(P1,
... ,Pn), abort)
To
resolve, Pi sends to T
SPi
({PCSPj(m,kj), Pi, T} (j 00/sub> {1... n}\{i}),SPi(m,1)
where
if j>i, kj is the maximum level of a promise received from
Pj on m
if j<i, kj
is the maximum level of promises received from each of the participants
Pj' , with j'< i
GM protocol
for T
Each participant
may contact T only
once
T replies with a resolved contract or an abort token
T may overturn an abort, but never a resolve
T maintains the following
information for each contract to decide when to overturn an abort
validated: a boolean
indicating whether the contract has been validated or not
S: the set of indices
of parties that have aborted
F: set of indices
of parties which helps T to decide when to overturn an abort
An attack on
abuse-freeness
Note that P1
cannot abort
Abort responses
include the participants that have aborted
If P1
receives an abort from T it must have
send a resolve request
Use T as an
oracle :
When
T receives a resolve request T verifies
all promises and, by answering to P1,
provides evidence that all participants
have started the protocol
An attack on
abuse-freeness (2)
Consider the protocol
instance where n=3
Using Mocha, we show
that abuse-freeness does not hold for a honest P3
P1
and P2 have a strategy to reach a state where
P1 has
an abort reply and
P1 and P2
have a strategy to obtain P300 signature
honest P3
does not have a strategy to obtain P100 and P200 signature
An attack on
abuse-freeness (3)
At the beginning
P2 aborts
P1 tries to
resolve, but gets an abort reply from T, which it can show to Charlie
At that point
P1 and P2 can choose the outcome
stop the
protocol : P3 is not able to overturn the abort
complete the
protocol in an optimistic way
Easy fix: make
abort replies to different participants indistinguishable
An attack on
fairness
The first attack
was discovered when noticing an error in the proof
Consider the protocol
instance where n=4
Using Mocha, we show
that fairness does not hold for a honest P2
There
exists a path such that
P1, P3
and P4 have P200 signature
there exists
a path such that P2 does not obtain all other signatures
Similar attacks
can be shown against P1 and P3
Using Mocha
we did not discover any attack on fairness for
n=3
An attack on
fairness (2)
P1,
P3 and P4 collude against P2
P3
aborts at the beginning
T adds P3 to S
P1
resolves, but T responds with an abort
T
adds P1 to S and P2 to F
P2
tries to recover, but as P2 is in F,
T responds with an abort
P4
resolves and T overturns the abort
An attack on
fairness (3)
More generally the
attack scenarios are as follows
dishonest Pk1
aborts but continues the protocol
dishonest Pk2
tries to recover but does not succeed
as
a side-effect it adds one or several
participants to the set F
honest
Pk3 tries to recover but does not succeed
dishonest Pk4
recovers and overturns the abort
Another attack
on fairness
P4
and P1 dishonest
Dishonest P4
aborts
Dishonest P3
tries to recover but does not succeed
as
a side-effect adds to P1 the set F
Honest
P1 has to recover, but fails
Honest P2
has to recover and overturns
Correcting
the GM protocol
Major revisions required
Getting the decision to
overturn abort correct
Recovery protocol and T00
protocol changed
Central idea in the revision
Abort overturned if and only
if T infers that each signer that contacted it in the past has been
dishonest
Idea borrowed from Baum-Waidner
protocol
Mocha did not discover any
attacks for both 3 and 4 signers
Revised GM
protocol
Recovery messages modified
so that T can infer the highest-level promises that an honest signer
would have sent when the recovery was launched
Leads to a smaller number
of possible resolve requests
T maintains the list S of
signers who have contacted T in the past and received an abort
For each signer Pi
in S,T maintains two integer variables
hi
: highest level promise that an honest
Pi would have sent to any higher
indexed signers before contacting
T
li
: highest level promise that an honest
Pi would have sent to any lower
indexed signers before contacting
T
Protocol for
T
If T ever replies with a signed
contract, then T responds with the contract for any further request
If the first request to T
is a resolve request, then T sends back a signed contract
If the first request is an
abort request, then T aborts the contract. T may overturn this abort
decision in future.
T maintains the abort if it
cannot deduce that a signer in the list S is dishonest
T
overturns the abort if it can deduce
that all the signers in S have behaved
dishonestly
T deduces that a signer
Pi in S is dishonest when contacted
by Pj if
j>i
and Pi presents to T a k-level promise
from Pi such that k>hi , or
j<i and Pi
presents to T a k-level promise from
Pi such that k>li
Conclusion
First formal analysis
of multi-party contract signing protocols
Using the model-checker
Mocha and the logic ATL instances of two protocols have been verified
Two new attacks have
been discovered in the GM protocol
Abuse-freeness
can be broken using side information given by T: easy to fix
Fairness can be broken
when n > 3: requires major changes to be fixed
Future work
Extend strand space
formalism to model fair exchange protocols
derive Mocha specifications
directly from strands
correctness proofs
when no attack is found
Extend the analysis
to a more complete model
Dolev-Yao-like intruder
Parametric verification
Study different topologies,
e.g. ring topologies in fair exchange
Extend general results
on advantage, presented in [Chadha,
Mitchell, Scedrov, Shmatikov 2003]
to multi-party protocols
GM main prot.
(4 participants)
P4
P3
P2
P1
1-level
promise
1-level
promise
3-level
promise
1-level
promise
2-level
promise
2-level
promise
2-level
promise
3-level
promise
3-level
promise
3-level
promise
3-level
promise
4-level
promise
4-level
promise
4-level
promise
4-level
promise
4-level
promise
Signature
Signature
Signature
GM main protocol
for Pi (detailed)
Pi
1-level
promise from j (n 00/sub> j < i)
Otherwise, stop
1-level promise to j (i
< j 00/sub> 1)
agreement of Pi...P1
i-1-level promise to j
(i < j 00/sub> 1)
i-level promise to j (i
< j 00/sub> 1)
i-level promise from j
(i < j 00/sub> 1)
i-level promise to i+1
Otherwise, abort
Otherwise, resolve
i-level promise from i+1
Otherwise, resolve
i+1-level promise to j
(i < j 00/sub> 1)
i+1-level promise from
j (i < j 00/sub> 1)
Otherwise, resolve
i+1-level promise to j
(i < j 00/sub> i+2)
i+2-level promise from
j (i+2 00/sub> j < i)
Otherwise, resolve
...
Otherwise, resolve
n+1-level promise from
j (n 00/sub> j < i)
and signatures
n+1-level promise to j
( j 00/sub> i)
and signatures
download Analysis of optimistic multi-party contract signing
