/*********************************************************************/
/*                         Time-stamp: <20-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                        */
/*                                                                   */
/* Fix: order of content in first encryption altered                 */
/*********************************************************************/

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 {nb_{i,j}, I_{i}; 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})
                        <{zb_{i,j}, I_{i}, 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)
)