protocol proto4;
identifiers
A,B	: user;
Secret	: number;
Kab	: symmetric_key;

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

knowledge
A	: B,Kab;
B	: A,Kab;

session_instances
 [A:alice,B:bob,Kab:kab];

intruder_knowledge
 alice,bob;

goal
  secrecy_of Secret [A,B];