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:

Paul Hankes Drielsma, ETH Zürich
Sebastian Mödersheim, ETH Zürich

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:

In order to avoid that the model becomes infinite merely because the trusted server must always listen for new requests, we limit the number of requests that T can answer.

PROBLEMS:

strong authentication on no
strong authentication on nr
secrecy of no_secret

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()