/*
 * This is a variant of the Yahalom Protocol, using message tags to 
 * secure against type flaw attacks. The protocol allows the server S 
 * to generate a session key Kab for use by A and B. The protocol (once 
 * we add message tags) is:
 *
 *   A -> B : A, Na
 *   B -> S : B, { msg2 (A, Na, Nb) }Kbs
 *   S -> A : { msg3(B, Kab, Na, Nb) }Kas, { msg4a(A, Kab) }Kbs
 *   A -> B : { msg4a(A, Kab) }Kbs, { msg4b(Nb) }Kab
 *
 * This protocol has been proven correct (for instance, by Guttman in the
 * strand space model, and by Paulson), even in the presence of key 
 * compromise. Whether this correct protocol type-checks, depends on the 
 * how we write the correspondence specifications.
 * 
 * If we require the correspondence "providing Kab to B for A" to end
 * before message 4b gets decrypted, then the protocol does not type-check. 
 * Ending the correspondence at this point guarantees that the decryption 
 * key for 4b is new.
 *
 * On the other hand, if we require the correspondence to end after 
 * message 4b has been decrypted, then the protocol type-checks. However, 
 * in this case, Kab is used to decrypt message 4b, although at this point our 
 * specifications do not guarantee that Kab is new.
 * 
 * Compare this discussion to the discussion of the Needham-Schroder
 * protocol in ns.cry. 
 *
 * Interestingly, the Yahalom protocol is safe even against key compromise.
 *
 * See yahalom-modified.cry for a modification of Yahalom that type-checks,
 * even if we end the correspondence for Kab before using Kab.
 *
 * Note that this protocol doesn't obey the usual client-server discipline: 
 * we have a cycle where Alice contacts Bob, who contacts Sam, who contacts 
 * Alice again.  When Sam contacts Alice, he needs to do it using the same 
 * connection as Bob, which means Bob has to pass the socket connection on 
 * to Sam. 
 *
 * Alan Jeffrey, v0.0.2 2001/02/26
 * Christian Haack, modified, 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;

/*
 * Nonce types.
 */

type Challenge = PoshChall ();

type ResponseBToA (a:Any, b:Any, na:Any)
  = PoshResp ( begun(b acknowledging reception of na to a) );

type ResponseSToA (a:Any, b:Any, kab:SharedKey(a,b,kab), na:Any) 
  = PoshResp ( begun(providing kab to a for b),
	       begun(providing kab to b for a),
	       begun(b acknowledging reception of na to a) );

type ResponseSToB (a:Any, b:Any, kab:SharedKey(a,b,kab)) 
  = PoshResp ( begun(providing kab to b for a),
	       begun(a acknowledging reception of kab to b) );

/*
 * Message patterns.
 */

pattern Msg2 (b:Host) 
  = ( a:Un, 
      nonceA:ResponseBToA(a,b,nonceA), 
      Challenge );

pattern Msg3 (a:Un)
  = ( b : Un, 
      kab : SharedKey(a,b,kab), 
      nonceA : ResponseSToA(a,b,kab,nonceA),
      Challenge );

pattern Msg4a (b:Un)
  = ( a:Un, kab:SharedKey(a,b,kab) ); 

pattern Msg4b (a:Host, b:Host, kab:SharedKey(a,b,kab)) 
  = ( nonceB : ResponseSToB(a,b,kab) );

/* 
 * Message tags.
 */

tag msg2(Msg2(b)) : Auth(b:Host, s:Server, kbs:SharedKey(b,s,kbs));  
tag msg3(Msg3(a)) : Auth(a:Un, s:Server, kas:SharedKey(a,s,kas));
tag msg4a(Msg4a(b)) : Auth(b:Un, s:Server, kbs:SharedKey(b,s,kbs));
tag msg4b(Msg4b(a,b,kab)) : Auth(a:Host, b:Host, kab:SharedKey(a,b,kab));

/*
 * We assume that two principals are able to securely lookup their shared 
 * longterm keys. We formally express this by assuming the existence 
 * of a secure lookup function of the following dependent function type:
 */

fun lkupKey (p:Any,q:Any) : (k:SharedKey(p,q,k));

/*
 * The initiator.
 */

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

/*
 * The responder.
 */

server Responder
  (b:Host, s:Server, kbs:SharedKey(b,s,kbs)) 
  at b is (socketA : Socket) 
{
  input socketA is (a : Un, nonceA : Challenge);
  establish Intermediary at s is (socketS : Socket);
  new (nonceB : Challenge);
  begin (b acknowledging reception of nonceA 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, { msg2 (a, nonceA, nonceB) }kbs, socketA);
  // The next message should come from Alice.
  input socketA is (
    { msg4a (a, kab:SharedKey(a,b,kab)) }kbs,
    ctext : Un
  );
  end (providing kab to b for a);       // LINE END1
  match ctext is { msg4b(nonceB) }kab;  // LINE DECRYPT
  //end (providing kab to b for a);     // LINE END2
  end (a acknowledging reception of kab to b);

  // If we comment out LINE END1 and instead insert LINE END2, then the 
  // protocol type-checks. However, that change is "unsafe" because, then, 
  // in LINE DECRYPT we use decryption key kab, although the correspondence
  // assertions do not tell us that kab is new.
  // 
  // This protocol happens to be safe, even in the presence of possible 
  // key compromise, but that requires an additional argument, which is not 
  // a consequence of type safety.
}

/*
 * The intermediary.
 */

server Intermediary (s:Server) at s is (socketB : Socket) 
{
  input socketB is (b:Un, request:Un, socketA:Socket);
  let kbs:SharedKey(b,s,kbs) = lkupKey (b,s);
  match request is { msg2 (
    a:Un, nonceA:ResponseBToA(a,b,nonceA), nonceB:Challenge
  ) }kbs;
  let kas:SharedKey(a,s,kas) = lkupKey (a,s); 
  new (kab : SharedKey(a,b,kab));
  begin (providing kab to a for b);
  begin (providing kab to b for a);
  output socketA is (
    { msg3 (b, kab, nonceA, nonceB) }kas,
    { msg4a (a, kab) }kbs
  );
}

/*
 * That's all folks.
 */

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: 2005-12-14 06:33:52