protocol proto3;
identifiers
A,B		: user;
Na,Secret	: number;
Ka,Kb		: public_key;

messages
1. A -> B : {A,Na}Kb
1. B -> A : {A,B,Na,Secret}Ka

knowledge
A	: B,Ka,Kb;
B	: A,Ka,Kb;

session_instances
 [A:alice,B:bob,Ka:ka,Kb:kb];

intruder_knowledge
 alice,bob,ka,kb;

goal
  secrecy_of Secret [A,B];