VARIANT:
two-pass mutual authentication

PURPOSE:
Two parties authenticate each other. Aim of the Mutual authentication
is to make sure to each of the parties of the other's identity. In this protocol authentication should be achieved by a single encrypted message sent from each party.  

REFERENCE:

 

MODELER:

 

ALICE_BOB:

 1. A -> B : PKa,A,{PKa,A}inv(PKs), Na, B, Text2,{Na,B,Text1}inv(PKa)
 2. B -> A : PKb,B,{PKb,B}inv(PKs), Nb, A, Text4,{Nb,A,Text3}inv(PKb)
 
 

PROBLEMS:
2
 

CLASSIFICATION:
G1, G2
 

ATTACKS:

The intruder can attack this protocol by simple eavesdropping and replaying the messages.
 i     -> (a,6) : start
 (a,6) -> i     : pka,a,{pka,a}inv(pks),na(a,6),b,ctext2,
                  {na(a,6),b,ctext1}inv(pka)
 i     -> (b,9) : start
 (b,9) -> i     : pkb,b,{pkb,b}inv(pks),na(b,9),a,ctext2,
                  {na(b,9),a,ctext1}inv(pkb)
 i     -> (a,6) : pkb,b,{pkb,b}inv(pks),na(b,9),a,ctext2,
                  {na(b,9),a,ctext1}inv(pkb)
 
 

NOTES:

 



HLPSL:

role iso3_Init( A, B     : agent,       
                Pka, Pks : public_key,
                Snd, Rcv : channel(dy))
played_by A
def=

  local  State             : nat,
         Na                : text,
         Nb, Text3, Text4  : text,
         Pkb               : public_key

  init State := 0 



  transition

   1. State = 0
      /\ Rcv(start)
      =|> 
      State' := 1
      /\ Na' := new()
      /\ Snd(Pka.A.{Pka.A}_inv(Pks).Na'.B.ctext2.{Na'.B.ctext1}_inv(Pka)) 
      /\ witness(A,B,na,Na')

   2. State = 1 
      /\ Rcv(Pkb'.B.{Pkb'.B}_inv(Pks).Nb'.A.Text4'.{Nb'.A.Text3'}_inv(Pkb'))
      =|> 
      State' := 2
      /\ wrequest(A,B,nb,Nb')

end role


role iso3_Resp (B, A : agent, Pkb, Pks : public_key, Snd, Rcv : channel(dy)) played_by B def= local State : nat, Nb : text, Na,Text1,Text2 : text, Pka : public_key init State := 0 transition 1. State = 0 /\ Rcv(Pka'.A.{Pka'.A}_inv(Pks).Na'.B.Text2'.{Na'.B.Text1'}_inv(Pka')) =|> State' := 1 /\ Nb' := new() /\ Snd(Pkb.B.{Pkb.B}_inv(Pks).Nb'.A.ctext4.{Nb'.A.ctext3}_inv(Pkb)) /\ witness(B,A,nb,Nb') /\ wrequest(B,A,na,Na') end role
role session (A, B : agent, Pka, Pkb : public_key, Pks : public_key) def= local SA, RA, SB, RB: channel (dy) composition iso3_Init(A,B,Pka,Pks,SA,RA) /\ iso3_Resp(B,A,Pkb,Pks,SB,RB) end role
role environment() def= const ctext1, ctext2, ctext3, ctext4 : text, na, nb : protocol_id, a, b : agent, pka, pkb, pks, pki : public_key intruder_knowledge={a,b,pks,pki,inv(pki)} composition session(a,b,pka,pkb,pks) /\ session(a,b,pka,pkb,pks) /\ session(b,a,pkb,pka,pks) end role
goal %ISO3_Init weakly authenticates ISO3_Resp on nb weak_authentication_on nb % addressess G1 and G2 %ISO3_Resp weakly authenticates ISO3_Init on na weak_authentication_on na % addressess G1 and G2 end goal
environment()