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