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

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

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

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

intruder_knowledge
 alice,bob,kb;

goal
  secrecy_of Secret [A,B];