PROTOCOL:
ASW Fair Exchange Protocol

VARIANT:
original

PURPOSE:

The ASW protocol, presented by Asokan, Shoup, and Waidner in [ASW], is an optimistic fair exchange protocol for contract signing intended to enable two parties to commit themselves to a previously agreed upon contractual text. A trusted third party (T3P) is involved only if dispute resolution is required (hence the term optimistic, which differentiates this approach from others in which an online trusted party is involved in every exchange). In resolving disputes, the T3P issues either a \emph{replacement contract} asserting that he recognises the contract in question as valid, or an abort token asserting that he has never issued, and will never issue, a replacement contract. An important requirement of the protocol is that the intruder cannot block messages between an honest agent and the T3P forever.  

REFERENCE:

[PHD:ZEB:04:ASW,ASW]  

MODELER:

 

ALICE_BOB:

In ASW, the parties are generally called the originator O, the responder R, and the trusted third party T. Their respective public keys are labelled Vo, Vr, and Vt. We denote with Text1 the contractual text that O and R wish to sign. Finally, No and Nr are the respective nonces of O and R. The constant aborted is used to indicate that the originator wishes to abort the attached contract. The Aborted and Resolved sets are maintained by the trusted server to keep track of what contracts have been aborted and for which contracts replacements have been issued.

  The Exchange Subprotocol
  1. O -> R : me1 = {Vo.Vr.T.Text1.h(No)}_inv(Vo)
  2. R -> O : me2 = {me1.h(Nr)}_inv(Vr)
  3. O -> R : No
  4. R -> O : Nr
  The Abort Subprotocol
  1. O -> T: ma1 = {aborted.me1}_inv(Vo)
  2. T -> O: ma2 = if Resolved(me1) then {me1.me2}_inv(Vt)
                   else {aborted.ma1}_inv(Vt); Aborted(ma1) := true
  Resolve Subprotocol
  1. O -> T: mr1 = me1.me2
  2. T -> O: mr2 = if Aborted(me1) then {aborted.me1}_inv(Vt)
                   else {me1.me2}_inv(Vt) ; Resolved(me1) := true

 

LIMITATIONS:

Issues abstracted from:

 

PROBLEMS:
3
 

ATTACKS:
None

 

NOTES:

This specification reflects the protocol in its original form and led to the discovery of the attack presented in Section 5 of [PHD:ZEB:04:ASW]. In that paper, the authors show how the fair exchange security goal of ASW can be reduced, via a meta-reasoning step, to a secrecy goal. In particular, they show that this goal is achieved for the originator, if he is assured that, whenever he aborts a contract exchange and receives an abort token, then the actual contract remains secret. In this specification, we declare the originator's nonce (or "secret committment") to be secret, as it is required for any valid standard contract. The security goals required to detect the attack are not included in this variant, as they are quite complex. See the "abort token attack" variant.  


HLPSL:

role orig(O, R, T    : agent,
          Text       : text,
          Vo, Vr, Vt : public_key) played_by O def=

 local S      : nat,
       No, Nr : text,
       SND, RCV   : channel (dy)

 init S := 0

 transition

 % Exchange subprotocol
 1. S = 0 /\ RCV(start) 
    =|>
    S' := 1 /\ No' := new()
    /\ SND({Vo.Vr.T.Text.h(No')}_inv(Vo))
    /\ witness(O,R,no,No'.Text)

 2. S = 1 /\ RCV({{Vo.Vr.T.Text.h(No)}_inv(Vo).h(Nr')}_inv(Vr)) 
    =|>
    S' := 2 /\ SND(No)

 3. S = 2 /\ RCV(Nr) 
    =|>
    S' := 3 /\ request(O,R,nr,Nr.Text)

 % Abort subprotocol
 4. S = 1 /\ RCV(timeout)
    =|>
    S' := 5 
    /\ SND({aborted.{Vo.Vr.T.Text.h(No)}_inv(Vo)}_inv(Vo))
    /\ secret(No,no_secret,{O})

 5. S = 5 
    /\ RCV({ aborted.
            {aborted.{Vo.Vr.T.Text.h(No)}_inv(Vo)}_inv(Vo)}_inv(Vt))
    =|>
    S' := 6 

 6. S = 5 
    /\ RCV({ {Vo.Vr.T.Text.h(No)}_inv(Vo).
            {{Vo.Vr.T.Text.h(No)}_inv(Vo).h(Nr')}_inv(Vr)}_inv(Vt))
    =|> 
    S' := 7

 % Resolve subprotocol
 7. S = 2 /\ RCV(resolve) 
    =|>
    S' := 8 
    /\ SND( {Vo.Vr.T.Text.h(No)}_inv(Vo).
           {{Vo.Vr.T.Text.h(No)}_inv(Vo).h(Nr)}_inv(Vr))




 8. S = 8 /\ RCV({ aborted.
                  {aborted.{Vo.Vr.T.Text.h(No)}_inv(Vo)}_inv(Vo)}_inv(Vt))
    =|> 
    S' := 9

 9. S = 8 /\ RCV({ {Vo.Vr.T.Text.h(No)}_inv(Vo).
                  {{Vo.Vr.T.Text.h(No)}_inv(Vo).h(Nr)}_inv(Vr)}_inv(Vt))
    =|>
    S' := 10 /\ request(O,R,nr,Nr.Text)

end role


role resp(O, R, T : agent, Text : text, Vo, Vr, Vt : public_key) played_by R def= local S : nat, No, Nr : text, SND, RCV : channel (dy) init S := 0 transition % Exchange subprotocol 1. S = 0 /\ RCV({Vo.Vr.T.Text.h(No')}_inv(Vo)) =|> S' := 1 /\ Nr' := new() /\ SND({{Vo.Vr.T.Text.h(No')}_inv(Vo).h(Nr')}_inv(Vr)) /\ witness(R,O,nr,Nr'.Text) 2. S = 1 /\ RCV(No) =|> S' := 2 /\ SND(Nr) /\ request(R,O,no,No.Text) % Resolve subprotocol 3. S = 1 /\ RCV(resolve) =|> S' := 3 /\ SND( {Vo.Vr.T.Text.h(No)}_inv(Vo). {{Vo.Vr.T.Text.h(No)}_inv(Vo).h(Nr)}_inv(Vr)) 8. S = 3 /\ RCV({ aborted. {aborted.{Vo.Vr.T.Text.h(No)}_inv(Vo)}_inv(Vo)}_inv(Vt)) =|> S' := 4 9. S = 3 /\ RCV({ {Vo.Vr.T.Text.h(No)}_inv(Vo). {{Vo.Vr.T.Text.h(No)}_inv(Vo).h(Nr)}_inv(Vr)}_inv(Vt)) =|> S' := 5 /\ request(R,O,no,No.Text) end role
role server(T : agent, Vt : public_key, AList : (message.message) set, RList : (message.message) set) played_by T def= local S : nat, Vo, Vr : public_key, Text : text, No, Nr : text, Count, X : message, SND, RCV : channel (dy) init S := 0 %% The Count variable specifies how many requests %% the trusted server can answer. One request is %% possible per application of "succ" /\ Count := succ(t) transition % Respond to an abort request 1. S = 0 /\ RCV({aborted.{Vo'.Vr'.T.Text'.h(No')}_inv(Vo')}_inv(Vo')) /\ in(( {Vo'.Vr'.T.Text'.h(No')}_inv(Vo'). {{Vo'.Vr'.T.Text'.h(No')}_inv(Vo').h(Nr')}_inv(Vr')), RList) /\ Count = succ(X') =|> S' := 0 /\ SND({ {Vo'.Vr'.T.Text'.h(No')}_inv(Vo'). {{Vo'.Vr'.T.Text'.h(No')}_inv(Vo').h(Nr')}_inv(Vr')}_inv(Vt)) /\ Count' := X' 2. S = 0 /\ RCV({aborted.{Vo'.Vr'.T.Text'.h(No')}_inv(Vo')}_inv(Vo')) /\ not(in(( {Vo'.Vr'.T.Text'.h(No')}_inv(Vo'). {{Vo'.Vr'.T.Text'.h(No')}_inv(Vo').h(Nr')}_inv(Vr')), RList)) /\ Count = succ(X') =|> S' := 0 /\ SND({ aborted. {aborted.{Vo'.Vr'.T.Text'.h(No')}_inv(Vo')}_inv(Vo')}_inv(Vt)) /\ AList' := cons(( {Vo'.Vr'.T.Text'.h(No')}_inv(Vo'). {aborted. {Vo'.Vr'.T.Text'.h(No')}_inv(Vo')}_inv(Vo')), AList) /\ Count' := X' % Respond to a resolve request 3. S = 0 /\ RCV({Vo'.Vr'.T.Text'.h(No')}_inv(Vo'). {{Vo'.Vr'.T.Text'.h(No')}_inv(Vo').h(Nr')}_inv(Vr')) /\ in(( {Vo'.Vr'.T.Text'.h(No')}_inv(Vo'). {aborted. {Vo'.Vr'.T.Text'.h(No')}_inv(Vo')}_inv(Vo')), AList) /\ Count = succ(X') =|> S' := 0 /\ SND({ aborted. {aborted.{Vo'.Vr'.T.Text'.h(No')}_inv(Vo')}_inv(Vo')}_inv(Vt)) /\ Count' := X' 4. S = 0 /\ RCV( {Vo'.Vr'.T.Text'.h(No')}_inv(Vo'). {{Vo'.Vr'.T.Text'.h(No')}_inv(Vo').h(Nr')}_inv(Vr')) /\ not(in(( {Vo'.Vr'.T.Text'.h(No')}_inv(Vo'). {aborted. {Vo'.Vr'.T.Text'.h(No')}_inv(Vo')}_inv(Vo')), AList)) /\ Count = succ(X') =|> S' := 0 /\ SND({ {Vo'.Vr'.T.Text'.h(No')}_inv(Vo'). {{Vo'.Vr'.T.Text'.h(No')}_inv(Vo').h(Nr')}_inv(Vr')}_inv(Vt)) /\ RList' := cons(( {Vo'.Vr'.T.Text'.h(No')}_inv(Vo'). {{Vo'.Vr'.T.Text'.h(No')}_inv(Vo').h(Nr')}_inv(Vr')), RList) /\ Count' := X' end role
role session(O, R, T : agent, Vo, Vr, Vt : public_key, Text : text) def= composition orig(O,R,T,Text,Vo,Vr,Vt) /\ resp(O,R,T,Text,Vo,Vr,Vt) end role
role environment() def= local AList, RList : (message.message) set const succ : hash_func, no, nr, no_secret : protocol_id, o, r, t, ref : agent, vo, vr, vt, ki : public_key, aborted, timeout, resolve, text1 : text, h : hash_func init AList := {} /\ RList := {} intruder_knowledge = {aborted, timeout, resolve, text1, o, r, t, vo, vr, vt, ki, inv(ki), h } composition session(o,r,t,vo,vr,vt,text1) /\ % session(i,r,t,ki,vr,vt,text1) /\ % session(i,r,t,ki,vr,vt,text1) /\ server(t,vt,AList,RList) end role
goal % Entity authentication (G1) % Message authentication (G2) % Replay protection (G3) % Accountability (G17) % Proof of origin (G18) % Proof of delivery (G19) authentication_on no authentication_on nr % Expressing fair exchange via observer (not described in D6.1) secrecy_of no_secret % R has no advantage over O end goal environment()