protocol WL;
identifiers
A, B, S 	: user;
Nb 		: number;
Kas, Kbs	: symmetric_key;

messages
1. A -> B 	: A
2. B -> A 	: Nb
3. A -> B 	: {Nb}Kas
4. B -> S 	: {{Nb}Kas,A}Kbs
5. S -> B 	: {Nb}Kbs

knowledge
A	: A,B,S,Kas;
B	: A,B,S,Kbs;
S	: A,B,S,Kas,Kbs;

session_instances
 [A:alice,B:bob,S:server,Kas:kas,Kbs:kbs]
 [A:i,B:bob,S:server,Kas:kis,Kbs:kbs]
 [A:alice,B:i,S:server,Kas:kas,Kbs:kis]
 [A:bob,B:alice,S:server,Kas:kbs,Kbs:kas];

intruder_knowledge
 alice, bob, server, kis;

goal
  B authenticates A on Nb;