protocol NeedhamSchroederPublicKey;
identifiers
A,B 		: user;
Na,Nb 		: number;
KPa,KPb 	: public_key;

messages
1. A -> B 	: {Na, A}KPb
2. B -> A 	: {Na, Nb}KPa
3. A -> B 	: {Nb}KPb

knowledge
A	: A,B,KPa,KPb;
B	: A,B,KPa,KPb;

session_instances
 [A:alice,B:bob,KPa:ka,KPb:kb];

goal
 A authenticates B on Na;

 -> 

role Alice (A, B: agent,             
             KPa, KPb: public_key,      
             SND, RCV: channel (dy)) 
    played_by A def=
    transition  
   
    0.  State  = 0 /\ RCV(start) =|> 
        State':= 2 /\ Na' := new() /\ SND({Na'.A}_KPb)
                   /\ secret(Na',na,{A,B}) 
    ...

 role Bob(A, B: agent,      
          KPa, KPb: public_key,      
          SND, RCV: channel (dy))
    ...

role Alice (A, B: agent,             
             KPa, KPb: public_key,      
             SND, RCV: channel (dy)) 
    played_by A def=
    transition  
   
    0.  State  = 0 /\ RCV(start) =|> 
        State':= 2 /\ Na' := new() /\ SND({Na'.A}_KPb)
                   /\ secret(Na',na,{A,B}) 
    ...

 role Bob(A, B: agent,      
          KPa, KPb: public_key,      
          SND, RCV: channel (dy))
    ...

 ->