/*
 * In their BAN logic article, Burrows, Abadi and Needham propose the 
 * following modification of the Yahalom protocol. (See yahalom.cry for
 * the unmodified Yahalom.) As an advantage, they mention that this
 * protocol is easier to analyze because it does not use an uncertified
 * key.  
 *
 *   A -> B : A, Na
 *   B -> S : B, Nb, { msg2 (A, Na) }Kbs
 *   S -> A : Nb, { msg3(B, Kab, Na) }Kas, { msg4a(A, Kab, Nb) }Kbs
 *   A -> B : { msg4a(A, Kab, Nb) }Kbs, { msg4b(Nb) }Kab
 *
 * The main difference to the original Yahalom protocol is that 
 * the original does not include Nb in message 4a. Moreover, the 
 * original includes Nb in the ciphertexts in messages 2 and 3. In the 
 * modified version, this is no longer necessary. 
 *
 * Alan Jeffrey, v0.0.2 2001/02/26
 * Christian Haack, modified for v1.1.0, 2004/09/15
 */

/*
 * Include the standard prelude
 */

import prelude;

/*
 * Words used in correspondence assertions.
 */

public providing : Word;
public acknowledging : Word;
public reception : Word;
public to : Word;
public for : Word;
public of : Word;

/* Challenge type. */
type Challenge = PoshChall ();

/* Response types for na. */
type ResponseBToA (a:Public, b:Public, na:Any) 
  = PoshResp ( begun(b acknowledging reception of na to a) );
type ResponseSToA (a:Public, b:Public, s:Public, kab:SharedKey(a,b,kab), na:Any) 
  = PoshResp ( begun(s providing kab to a for b),
               begun(b acknowledging reception of na to a) );

/* Response type for nb. */
type ResponseSToB (a:Public, b:Public, s:Public, kab:SharedKey(a,b,kab)) 
  = PoshResp ( begun(s providing kab to b for a) );

/* Message patterns. */
pattern Msg2 (b:Public) 
  = ( a:Public, 
      nA:ResponseBToA(a,b,nA) );
pattern Msg3 (a:Public, s:Public)
  = ( b:Public, 
      kab:SharedKey(a,b,kab), 
      nA:ResponseSToA(a,b,s,kab,nA) );
pattern Msg4a (b:Public, s:Public)
  = ( a:Public, 
      kab:SharedKey(a,b,kab), 
      nB:ResponseSToB(a,b,s,kab) ); 
pattern Msg4b (a:Public, b:Public, kab:SharedKey(a,b,kab)) 
  = Any [ !begun(a acknowledging reception of kab to b) ];

/* Message tags. */
tag msg2 (Msg2(b)) : Auth (b:Public, s:Public, kbs:SharedKey(b,s,kbs));
tag msg3 (Msg3(a,s)) : Auth (a:Public, s:Public, kas:SharedKey(a,s,kas));
tag msg4a (Msg4a(b,s)) : Auth (b:Public, s:Public, kbs:SharedKey(b,s,kbs));
tag msg4b (Msg4b(a,b,kab)) : Auth (a:Public, b:Public, kab:SharedKey(a,b,kab));


client Initiator
  (a:Public, b:Public, s:Public, kas:SharedKey(a,s,kas)) 
  at a is 
{
  establish Responder at b is (socket : Socket);
  new (nA : Challenge);
  output socket is (a,nA);
  // This next message is meant to come from Sam, even
  // though the socket was opened as going to Bob.  
  input socket is (
    nB : Challenge, 
    { msg3(b, kab:SharedKey(a,b,kab), nA) }kas,
    ticketB:Un
  ) [ begun(s providing kab to a for b),
      begun(b acknowledging reception of nA to a) ];
  end(s providing kab to a for b);
  end(b acknowledging reception of nA to a);
  begin!(a acknowledging reception of kab to b);
  // Next we're back to sending to Bob on this socket.
  output socket is (ticketB, { msg4b(nB) }kab );
}

server Responder
  (a:Public, b:Public, s:Public, kbs:SharedKey(b,s,kbs)) 
  at b is (socketA : Socket) 
{
  input socketA is (a, nA : Challenge);
  establish Intermediary at s is (socketS : Socket);
  new (nB : Challenge);
  begin (b acknowledging reception of nA to a);	
  // Note that in the next output we have to include the socket connection to
  // Alice, otherwise Sam has no way to contact Alice.
  output socketS is (b, nB, { msg2 (a, nA) }kbs, socketA);
  // The next message should come from Alice.
  input socketA is (
    { msg4a(a, kab:SharedKey(a,b,kab), nB) }kbs,
    { msg4b(nB) }kab
  ) [ begun(s providing kab to b for a),
      !begun(a acknowledging reception of kab to b) ];
  end(s providing kab to b for a);       
  end(a acknowledging reception of kab to b);
}

server Intermediary (s:Public, a:Public, kas:SharedKey(a,s,kas), b:Public, kbs:SharedKey(b,s,kbs)) at s is (socketB : Socket) {
  input socketB is (b, nB:Challenge, { msg2(a, nA:ResponseBToA(a,b,nA)) }kbs, socketA:Socket);
  new (kab:SharedKey(a,b,kab));
  begin(s providing kab to a for b);
  begin(s providing kab to b for a);
  output socketA is ( { msg3(b,kab,nA) }kas, { msg4a(a,kab,nB) }kbs );
}

Cryptyc implementation Copyright © 2001-2004, Alan Jeffrey and Christian Haack
Technical reports Copyright © 2000-2004 Microsoft Research, Alan Jeffrey and Christian Haack
This material is partly based upon work supported by the National Science Foundation under Grant No. 0208549.
Last modified: 2006-02-20 06:31:11