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

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

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

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

intruder_knowledge
 alice,bob,ka;

goal
  secrecy_of Secret [A,B];