VARIANT:
three-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 a confirmation of the successful authentication is sent by the initiator.  

REFERENCE:

 

MODELER:

 

ALICE_BOB: 

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

PROBLEMS:
2
 

CLASSIFICATION:
G1, G2
 

ATTACKS:
None
 

NOTES:

inv(PKs) is the private key of the server C; {PKa,A}inv(PKs) is the certificate of agent A, and
{PKb,B}inv(PKs) is the certificate of agent B.

 


HLPSL: 

role iso4_Init ( A,B: agent,
                 Pkb,Pks: public_key, 
                 Snd,Rec: channel(dy))
played_by B
def=

  local  State         : nat,
         Pka           : public_key,
         Nb            : text,
         Na,Text2,Text3: text

  const ctext1,ctext4,ctext5: text

  init State := 0 



  transition

   1. State = 0
      /\ Rec(start) 
      =|> 
      State' := 1
      /\ Nb' := new() 
      /\ Snd(Nb'.ctext1) 
      /\ witness(B,A,nb,Nb')

   2. State = 1
      /\ Rec(Pka'.A.{Pka'.A}_inv(Pks).Na'.Nb.B.Text3'.
             {Na'.Nb.B.Text2'}_inv(Pka'))
      =|> 
      State' := 2
      /\ Snd(Pkb.B.{Pkb.B}_inv(Pks).Nb.Na'.A.ctext5.{Nb.Na'.A.ctext4}_inv(Pkb))

      /\ request(B,A,na,Na')

end role




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

  local  State               : nat,
         Pkb                 : public_key,
         Na                  : text,
         Nb,Text1,Text4,Text5: text

  const ctext2,ctext3: text

  init State := 0



  transition

   1. State = 0
      /\ Rec(Nb'.Text1') 
      =|>
      State' := 1
      /\ Na' := new()
      /\ Snd(Pka.A.{Pka.A}_inv(Pks).
             Na'.Nb'.B.ctext3.{Na'.Nb'.B.ctext2}_inv(Pka))
      /\ witness(A,B,na,Na')

   2. State = 1
      /\ Rec(Pkb'.B.{Pkb'.B}_inv(Pks).
             Nb.Na.A.Text5'.{Nb.Na.A.Text4'}_inv(Pkb'))
      =|> 
      State' := 2
      /\ request(A,B,nb,Nb)

end role




role session (A,B:agent,
              Pka,Pkb,Pks: public_key) def=       

  local SA,RA,SB,RB: channel (dy)

  composition

          iso4_Init(A,B,Pkb,Pks,SA,RA)
       /\ iso4_Resp(B,A,Pka,Pks,SB,RB)

end role




role environment() def=

 const na, nb             : protocol_id,
       a, b, i            : agent,
       pka, pkb, pks, pki : public_key

 intruder_knowledge={a,b,pki,inv(pki),pks,
                     ctext1,ctext4,ctext5,{pki.i}_inv(pks),  
                     ctext2,ctext3,{pki.i}_inv(pks)}         

 composition

        session(a,b,pka,pkb,pks)
     /\ session(a,i,pka,pki,pks)
     /\ session(i,b,pki,pkb,pks)


end role




goal

   %ISO4_Resp authenticates ISO4_Init on nb
   authentication_on nb % addressess G1 and G2

   %ISO4_Init authenticates ISO4_Resp on na
   authentication_on na % addressess G1 and G2

end goal




environment()