VARIANT:
fixed version with weak authentication

PURPOSE:
Sender invariance (authentication assuming that the first message is not tampered with)
 

REFERENCE:
http://www.ietf.org/internet-drafts/draft-bradner-pbk-frame-06.txt
 

MODELER:

 

ALICE_BOB: 

  A -> B: A, PK_A, hash(PK_A)
  A -> B: {***tag1***,Msg}inv(PK_A), hash(PK_A)
  B -> A: Nonce
  A -> B: {***tag2***,Nonce}inv(PK_A)

 

PROBLEMS:
1
 

ATTACKS:
None
 

NOTES:

Same as before, but specifying only weak authentication.

 


HLPSL: 

role alice (A,B        : agent,
            SND,RCV    : channel(dy),
            Hash       : hash_func,
            PK_A       : public_key,
            Tag1,Tag2  : text)
played_by A
def=

  local
    State      : nat,
    Msg        : text,
    Nonce      : text

  init State := 0

  transition

 1. State  = 0 /\ RCV(start) =|>
    State':= 2 /\ Msg' := new()
               /\ SND(B.{Tag1.Msg'}_inv(PK_A).Hash(PK_A))
               /\ witness(A,A,msg,Msg')

 3. State  = 2 /\ RCV(Nonce') =|>
    State':= 4 /\ SND({Tag2.Nonce'}_inv(PK_A))

end role




role bob (B,A        : agent,
          SND,RCV    : channel(dy),
          Hash       : hash_func,
          PK_A       : public_key,
          Tag1,Tag2  : text)
played_by B
def=

  local
    State      : nat,
    Nonce      : text,
    Msg        : text

  init State := 1

  transition

 1. State  = 1 /\ RCV(B.{Tag1.Msg'}_inv(PK_A).Hash(PK_A)) =|>
    State':= 5 /\ Nonce' := new()
               /\ SND(Nonce')

 3. State  = 5 /\ RCV({Tag2.Nonce}_inv(PK_A)) =|>
    State':= 7 /\ wrequest(A,A,msg,Msg)
         
end role




role session(A,B        : agent,
             Hash       : hash_func,
             PK_A       : public_key,
             Tag1,Tag2        : text)
def=

  local SND,RCV,SNDA,RCVA  : channel (dy)

  composition

     alice(A,B,SND,RCV,Hash,PK_A,Tag1,Tag2)
  /\ bob(B,A,SND,RCV,Hash,PK_A,Tag1,Tag2)

end role




role environment()
def=

  const
    a,b            : agent,
    f              : hash_func,
    msg            : protocol_id,
    pk_a,pk_b,pk_i : public_key,
    tag1,tag2      : text

  intruder_knowledge = {a,b,f,pk_a,pk_b,pk_i,inv(pk_i)}

  composition
     session(a,b,f,pk_a,tag1,tag2)
  /\ session(b,a,f,pk_b,tag1,tag2)
  /\ session(i,b,f,pk_i,tag1,tag2)
  /\ session(a,i,f,pk_a,tag1,tag2)

end role




goal

  % Sender Invariance (G16)
  weak_authentication_on msg

end goal




environment()