protocol DiffieHellman;
identifiers
A,B		: user;
G,Na,Nb,Secret	: number;

messages
1. A -> B 	: G^Na
2. B -> A	: G^Nb
3. A -> B	: {Secret}((G^Na)^Nb)

knowledge
A	: G,B;
B	: G,A;

session_instances
  [A:alice,B:bob,G:g]
% [A:marcel,B:roger,G:g]
; 

intruder_knowledge
 g,alice,bob;

goal
 secrecy_of Secret [A,B];