/* Woo and Lam protocol for BSW */

declarations {
   Channel Cas, Cbs;
   Principal A, B, S; 
   Nonce Nb; 
   Formula phi;
   Message X; 
}

assumptions { 
   /* A1  */  in(A, r(Cas)); 
   /* A2  */  in(S, r(Cas)); 
   /* A3  */  believes(A, equals(w(Cas), {A, S})); 
   /* A4  */  believes(S, equals(w(Cas), {A, S})); 
   /* A5  */  in(B, r(Cbs)); 
   /* A6  */  in(S, r(Cbs)); 
   /* A7  */  believes(B, equals(w(Cbs), {B, S})); 
   /* A8  */  believes(S, equals(w(Cbs), {B, S})); 
   /* A9  */  believes(A, implies(recentlySaid(S, phi), believes(S, phi))); 
   /* A10 */  believes(A, implies(believes(S, said(B, X)), said(B, X)));
   /* A11 */  believes(B, implies(recentlySaid(S, phi),believes(S, phi))); 
   /* A12 */  believes(B, implies(believes(S, said(A, X)), said(A, X)));
   /* A13 */  believes(B, fresh(Nb));

}

protocol {
   /* 1 A -> B : A               */    sees(B, A);
   /* 2 B -> A : Nb              */    sees(A, Nb);
   /* 3 A -> B : {Nb}Kab         */    seesOnChannel(B, Cas, Nb);
   /* 4 B -> S : {A, {Nb}Kas}Kbs */    seesOnChannel(S, Cbs,(A, Cas(Nb)));
   /* 5 S -> B : {Nb}Kbs         */    seesOnChannel(B, Cbs, Nb);
}

goals { 
   /* G1 */ believes(B, recentlySaid(A, (B, Nb)));
   /* G2 */ believes(B, recentlySaid(S, Nb));
}