VARIANT:
two-pass unilateral authentication

PURPOSE:
Authentication of a client to a server. This protocol models a situation
in which the server wants to verify the client identity and starts the session. The client answers by sending his digital signature.  

REFERENCE:

 

MODELER:

 

ALICE_BOB: 

 1. B -> A : Rb, Text1
 2. A -> B : {PKa,A}inv(PKs), Ra,Rb, B, Text2,{Ra,Rb,B,Text1}inv(PKa)
 

PROBLEMS:
1
 

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.

 


HLPSL: 

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

  local  State     : nat,
         Pka       : public_key,
         Rb        : text,
         Ra, Text2 : text

  init State := 0



  transition

   1. State = 0
      /\ Rec(start)
      =|>
      State' := 1 
      /\ Rb' := new()
      /\ Snd(Rb'.ctext1)

   2. State = 1
      /\ Rec(Pka'.A.{Pka'.A}_inv(Pks).Ra'.Rb.B.Text2'.
                    {Ra'.Rb.B.ctext1}_inv(Pka'))  
      =|> 
      State' := 2 
      /\ request(B,A,ra,Ra')

end role




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

  local  State     : nat,
         Ra        : text,
         Rb, Text1 : text

  init State := 0



  transition

   1. State = 0
      /\ Rec(Rb'.Text1')
      =|> 
      State' := 2 
      /\ Ra' := new()
      /\ Snd(Pka.A.{Pka.A}_inv(Pks).Ra'.Rb'.B.ctext2.
                   {Ra'.Rb'.B.Text1'}_inv(Pka))
      /\ witness(A,B,ra,Ra')


end role




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

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

          iso2_Init(B,A,Pks,SB,RB)
       /\ iso2_Resp(A,B,Pka,Pks,SA,RA)

end role




role environment() def=

  const  ctext1,ctext2 : text,
         ra            : protocol_id,
         a,b,i         : agent, 
         pkb,pks,pki   : public_key
  
  intruder_knowledge={i,a,b,pks,pki,inv(pki),ctext1,ctext2,
                      {pki.i}_inv(pks)}   

  composition

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

end role




goal

   %ISO2_Init  authenticates ISO2_Resp on ra
   authentication_on ra % addressess G1 and G2

end goal




environment()