PROTOCOL:
ISO1 Public Key Unilateral Authentication Protocol

VARIANT:
one-pass unilateral authentication

PURPOSE:
A client authenticates himself to a server by sending a digital signature.
 

REFERENCE:

 

MODELER:

 

ALICE_BOB:

   1. A -> B : {PKa,A}inv(PKs), Na, B, Text,{Na,B,Text}inv(PKa)
 
 

PROBLEMS:
1
 

CLASSIFICATION:
G1, G2
 

ATTACKS:

The intruder can attack this protocol by simple eavesdropping and replaying the digital signatures.
 i     -> (a,6) : start
 (a,6) -> i     : pka,a,{pka,a}inv(pks),na(a,6),b,ctext,
                  {na(a,6),b,ctext}inv(pka)
 i     -> (b,4) : pka,a,{pka,a}inv(pks),na(a,6),b,ctext,
                  {na(a,6),b,ctext}inv(pka)
 i     -> (b,7) : pka,a,{pka,a}inv(pks),na(a,6),b,ctext,
                  {na(a,6),b,ctext}inv(pka)
 
 

NOTES:

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

If one would like to use the same server public key for each session, then permutation on Pks should be avoided.

 



HLPSL:

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

 local  State: nat,
        Na   : text

 init  State := 0



 transition

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

end role


role iso1_Resp (A, B: agent, Pks : public_key, Rec : channel(dy)) played_by B def= local State : nat, Pka : public_key, Na, Text : text init State := 0 transition 1. State = 0 /\ Rec(Pka'.A.{Pka'.A}_inv(Pks).Na'.B.Text'.{Na'.B.Text'}_inv(Pka')) =|> State' := 1 /\ request(B,A,na,Na') end role
role session (A, B : agent, Pka : public_key, Pks : public_key) def= local SA, RA, RB: channel (dy) const na : protocol_id composition iso1_Init(A,B,Pka,Pks,SA,RA) /\ iso1_Resp(A,B,Pks,RB) end role
role environment() def= const ctext : text, a, b : agent, pka, pks : public_key intruder_knowledge={a,b,pks,pka} composition session(a,b,pka,pks) /\ session(a,b,pka,pks) end role
goal %ISO1_Resp authenticates ISO1_Init on na authentication_on na % addressess G1 and G2 end goal
environment()