Woo_and_Lam
// modifie
  A, B, S : principal

  basetype key

  Na, Nb, Kab : key


  shr (principal) : number secret
  everybody knows shr

  A knows A, B
  B knows B, S

  a, b, s : principal
  {
   1. A -> B : A, Na
   2. B -> A : A, Na, B, Nb
   3. A -> B : Na, Nb, {A, B, Na, Nb}_shr(A)
   4. B -> S : {A, B, Na, Nb}_shr(A), {A, B, Na, Nb}_shr(B)
   5. S -> B : {B, Na, Nb, Kab}_shr(A), {A, Na, Nb, Kab}_shr(B)
   6. B -> A : {B, Na, Nb, Kab}_shr(A), {Na, Nb}_Kab
   7. A -> B : {Nb}_Kab
  }  
  
  s1. session *{A, B} A=a, B=b, S=s

  assume secret (shr(A)@s1.S), secret (shr(B)@s1.S)
//       secret (shr(B)@s1.B), secret (shr(A@s1.B))
	 
  claim	*A*G secret (shr(A)@s1.S),
	*A*G secret (shr(B)@s1.S),
	*A*G secret (Kab@s1.S)