Analysis of a Fair Exchange Protocol

0 comments

file time: 2008-02-16

filetype:ppt

Click Here To Download...

>  

Analysis of  
a Fair Exchange Protocol 

Vitaly Shmatikov    John Mitchell

Stanford University 

 

Agreement in Hostile Environment 

Cannot trust the communication channel Cannot trust the other party in the protocol Trusted third party may exist Last resort: use only if something goes wrong  

Contract Signing 

Both parties want to sign the contract Neither wants to commit first   
 

Immunity

deal

 

Fairness 

If A cannot obtain a contract,

then B should not be able to

obtain a contract, either 

(and vice versa) 

Example (Alice buys a house from Bob)

              If Alice cannot obtain a deed for the property,

              Bob should not be able to collect Alice00 money

 

Accountability 

If trusted party T misbehaves,

then honest party should be

able to prove T00 misbehavior 

Example (Alice buys a house from Bob)

              If escrow service gives Bob Alice00 money without

              giving Alice the deed, Alice should be able to prove

              to a judge that escrow service is cheating

 

Formal Protocol Analysis 

Intruder

Model 

Analysis

Tool 

Formal

Protocol 

Informal

Protocol

Description 

Gee whiz.

Looks OK

  to me.

 

                    Murj            [Dill et al.] 

Describe finite-state system State variables with initial values Transition rules Communication by shared variables Scalable: choose system size parameters Specify correctness condition Automatic exhaustive state enumeration Hash table to avoid repeating states

Success with research, industrial protocol verification

 

Optimistic Contract Signing 

A 

B 

m1  =  sigA (PKA, PKB, T, text, hash(RA)) 

m2  =  sigB (m1, hash(RB)) 

m3  =  RA 

m4  =  RB 
 

[Asokan, Shoup, Waidner] 

m1, RA, m2, RB

Contract from normal execution  
Contract issued by third party  
Abort token issued by third party  

Several Forms of Contract 

m1, RA, m2, RB 

sigT (m1, m2) 

sigT (abort, a1)

 

Role of Trusted Third Party 

T can issue an abort token

Promise not to resolve the protocol in the future

T can issue a replacement contract

Proof that both parties are committed

T decides whether to abort or resolve on the first-come-first-serve basis  
T only gets involved if requested by A or B  

Abort Subprotocol 

A 

          ??? 

B 

Network 

T 

a1=sigA(abort,m1) 

a2 

resolved?

    Yes:  a2 = sigT (m1, m2)

     No:   aborted := true

              a2 = sigT (abort, a1) 

   m1 = sigA (00hash(RA)) 

sigT (m1, m2) 

sigT (abort, a1) 

OR

 

Resolve Subprotocol 

B 

A 

Net 

T 

r1 = m1, m2 

aborted?

    Yes:  r2 = sigT (abort, a1)

     No:   resolved := true

              r2 = sigT (m1, m2) 

r2 

m1 = sigA (00hash(RA)) 

m3 = RA 

m2 = sigB (00hash(RB)) 

sigT (m1, m2) 

sigT (abort, a1) 

OR 

???

 

Race Condition 

B 

A 

m1  =  sigA (PKA, PKB, T, text, hash(RB)) 

m2  =  sigB (m1, hash(RB)) 

T 

a1 = sigA (abort, m1) 

r1 = m1, m2

 

Attack 

A 

r2 = sigT (m1, m2) 

m1  =  sigA (... hash(RA)) 

m2  =  sigB (m1, hash(RB)) 
 

m3  =  RA 

T 

r1 = m1, m2 

secret  QB, m2 

sigT (m1, m2) 

m1, RA, m2, QB 

contracts are

inconsistent!

 

Later ... 

sigA (PKA, PKA, T, text, hash(RA)) 

B 

Replay Attack 

Intruder causes B

to commit to old

contract with A 

sigB (m1, hash(QB)) 

RA 

QB 

A 

B 

RA 

sigA (00hash(RA)) 

RB 

sigB (...  hash(RB))

 

           sigA (     , hash(RB)) 

Repairing the Protocol 

A 

B 

m1  =  sigA (PKA, PKB, T, text, hash(RA)) 

m2  =  sigB (m1, hash(RB)) 

m3  =            RA 

m4  =  RB 

m1, RA, m2, RB

 

Another Property: Abuse-Freeness 

No party should be able to prove

that it can solely determine

the outcome of the protocol 

Example (Alice buys a house from Bob)

              Bob should not be able to show Alice00 offer to

              Cynthia so that he can convince Cynthia to pay more

 

Conclusions 

Fair exchange protocols are subtle Correctness conditions are hard to formalize Unusual constraints on communication channels Several interdependent subprotocols Many cases and interleavings Finite-state tools are useful for case analysis

   download Analysis of a Fair Exchange Protocol