Yahalom
  A, B, S :       principal
  Na, Nb :        number
  Kas, Kbs, Kab : key
  A knows A, B, S, Kas
  B knows B, S, Kbs
  S knows S, A, B, Kas, Kbs 
  {
   1. A -> B : A, Na
   2. B -> S : B, { A, Na, Nb }_Kbs
   3. S -> A : { B, Kab, Na, Nb }_Kas, { A, Kab }_Kbs
   4. A -> B : { A, Kab }_Kbs, { Nb }_Kab
  }        
// claim Secret(Kab),
//       Agreement(A,B,Nb,Nb),
//       Agreement(A,B,Kab,Kab)