/*********************************************************************/
/*                         Time-stamp: <13-01-2005 Mikael Buchholtz> */
/*                                                                   */
/* BBF1 - server-based key establishment using symmetric keys        */
/*                                                                   */
/* R. K. Bauer,  T. A. Berson, and R. J. Feiertag: A Key             */
/* Distribution Protocol Using Event Markers, ACM Transactions on    */
/* Computer Systems, 1(3), p 249 - 255, 1983.                        */
/*                                                                   */
/* Note: content of message 2 and message 3 has been rearranged      */
/*                                                                   */
/* Scenario: bi-directional key establishment                        */
/*                                                                   */
/* Attack: A starts a session with B (1.x) and                       */
/*         B starts a session with A (2.x)                           */
/*                                                                   */
/* 1.1  A     -> B     : A, NA1                                      */
/* 1.2  B     -> M(S)  : A, NA1, B, NB1                              */
/* 2.1  B     -> A     : B, NB2                                      */
/* 2.2  A     -> M(S)  : B, NB2, A, NA2                              */
/* 1.2' M(S)  -> S     : A, NA2, B, NB1                              */
/* 1.3  S     -> M(B)  : {KAB, A, NB1}:KB, {KAB, B, NA2}:KA          */
/* 1.3' M(S)  -> M(B)  : {KAB, A, NB1}:KB, garbage                   */
/* 2.3' M(S)  -> M(B)  : {KAB, B, NA2}:KA, garbage                   */
/*                                                                   */
/* At this point A and B shares the key KAB but the both believe     */
/* that it was from the session they themselves started.             */
/*********************************************************************/

let X subset NATURAL1 in
let Y subset NATURAL1 in

/* Long term keys */
(new_{i in X union Y} KS_{i})
(

/* Principal I_{i} */
(|_{i in X} 

      /* Initiating a session with principal I_{j} */
      |_{j in Y} !(new na_{i,j}) 
	          <I_{i}, na_{i,j}>.
                  (; xa_{i,j}).
		  decrypt xa_{i,j} as {I_{j}, na_{i,j}; xk_{i,j}}:KS_{i} 
                                      [at a_{i,j} orig {s2_{i,j}}] in 0)
|

/* Principal I_{j} */
(|_{j in Y} 
      /* Responding to a session from principal I_{i} */
       |_{i in X} !(I_{i}; yn_{i,j}).
                   (new nb_{i,j})
                   <I_{i}, I_{j}, yn_{i,j}, nb_{i,j}>.
		   (; yb_{i,j}, ya_{i,j}).
                   decrypt yb_{i,j} as {I_{i}, nb_{i,j}; yk_{i,j}}:KS_{j} 
		                       [at b_{i,j} orig {s1_{i,j}}] in
		   <ya_{i,j}>.0)
|

/* Server catering for session between I_{i} and I_{j} */
(|_{i in X} |_{j in Y} !(I_{i}, I_{j}; za_{i,j}, zb_{i,j}).
                        (new K_{i,j})
                        <{I_{i}, zb_{i,j}, K_{i,j}}:KS_{j} 
                         [at s1_{i,j} dest {b_{i,j}}],
			 {I_{j}, za_{i,j}, K_{i,j}}:KS_{i} 
                         [at s2_{i,j} dest {a_{i,j}}]>.0)
)