/*
 * This is a variant of the Needham-Schroeder Symmetric Key Protocol,
 * using message tags rather than nonce arithmetic.  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 -> S : A, B, Na
 *   S -> A : { msg2(Na, B, Kab, { msg3(Kab, A) }Kbs) }Kas
 *   A -> B : { msg3(Kab, A) }Kbs
 *   B -> A : { msg4(Nb) }Kab
 *   A -> B : { msg5(Nb) }Kab
 *
 * This protocol is flawed if one takes into account the possibility
 * of key compromise (see for example Clark and Jacob, 1997):
 * Message 3 is vulnerable to replay. As a result, an attacker
 * can impersonate A and trick B into accepting a compromised key.
 *
 * On the other hand, under the idealistic assumption that keys can't
 * be compromised, this protocol is safe.
 * 
 * Whether this 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 4, then the protocol does not type-check. Ending the
 * correspondence at this point guarantees that the key for encrypting 
 * and decrypting messages 4 and 5 is new.  
 *	
 * On the other hand, if we require the correspondence to end after 
 * message 5, then the protocol type-checks. However, in this case, Kab is
 * used to encrypt and decrypt messages 4 and 5, although at this point our 
 * specifications do not guarantee that Kab is new. 
 *
 * A fix for the key-compromise attack, as proposed by Needham and Schroeder,
 * is presented in ns-modified.cry.
 *
 * Alan Jeffrey, v0.0.2 2001/02/25
 * Christian Haack, modified for v.1.1.0 2004/09/13
 */

/*
 * Include the standard prelude
 */

import prelude;

public providing : Word;
public session : Word;
public key : Word;
public to : Word;
public for : Word;

/*
 * Nonce types.
 */

type Challenge = PoshChall ();

type ResponseSToA ( a:Un, b:Un, kab:SharedKey(a,b,kab) ) 
  = PoshResp ( begun(providing session key kab to a for b),
	       begun(providing session key kab to b for a) );

type ResponseAToB ( a:Host, b:Host, kab:SharedKey(a,b,kab) ) 
  = PoshResp ( begun(providing session key kab to b for a) );

/* 
 * Message patterns.
 */

pattern Msg2 ( a:Un, s:Server, kas:SharedKey(a,s,kas) ) 
  = ( nonceA : ResponseSToA(a,b,kab),
      b : Un,
      kab : SharedKey(a,b,kab),
      ticket : Un );

pattern Msg3 ( b:Un, s:Server, kbs:SharedKey(b,s,kbs) )
  = ( kab : SharedKey(a,b,kab), a : Un );   

pattern Msg4 ( a:Un, b:Host, kab:SharedKey(a,b,kab) ) 
  = Challenge;

pattern Msg5 ( a:Host, b:Host, kab:SharedKey(a,b,kab) ) 
  = ResponseAToB(a,b,kab);

/* 
 * Message tags.
 */

tag msg2(Msg2(a,s,kas)) : Auth(a:Un, s:Server, kas:SharedKey(a,s,kas));
tag msg3(Msg3(b,s,kbs)) : Auth(b:Un, s:Server, kbs:SharedKey(b,s,kbs));
tag msg4(Msg4(a,b,kab)) : Auth(a:Un, b:Host, kab:SharedKey(a,b,kab));
tag msg5(Msg5(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 Intermediary at s is (socketS : Socket);
  new (nonceA : Challenge);
  output socketS is (a, b, nonceA);
  input socketS is { msg2(nonceA, b, kab:SharedKey(a,b,kab), ticket:Un) }kas 
    [ begun(providing session key kab to a for b),
      begun(providing session key kab to b for a) ];
  end(providing session key kab to a for b);
  establish Responder at b is (socketB : Socket);
  output socketB is ticket;
  input socketB is { msg4 (nonceB:Challenge) }kab;
  output socketB is { msg5(nonceB) }kab;

}

/*
 * The responder.
 */

server Responder
  (b:Host, s:Server, kbs:SharedKey(b,s,kbs)) 
  at b is (socket : Socket) 
{
  input socket is { msg3(kab:SharedKey(a,b,kab), a:Un) }kbs;
  new (nonceB : Challenge);
  end (providing session key kab to b for a);       // line b3
  output socket is { msg4(nonceB) }kab;             // line b4
  input socket is { msg5(nonceB) }kab;              // line b5
  //end (providing session key kab to b for a);     // line b6

  // If we comment out line b3 and uncomment line b6, instead, 
  // then the protocol type-checks. But then our spec does not 
  // guarantee that key kab used in lines b4 and b5 is new.

}

/*
 * The intermediary.
 */

server Intermediary (s:Server) at s is (socket : Socket) {

  input socket is (a:Un, b:Un, nonceA:Challenge);
  let kas:SharedKey(a,s,kas) = lkupKey (a,s);
  let kbs:SharedKey(b,s,kbs) = lkupKey (b,s);
  new (kab : SharedKey(a,b,kab));
  begin(providing session key kab to a for b);
  begin(providing session key kab to b for a);
  output socket is { msg2(nonceA, b, kab, { msg3(kab,a) }kbs) }kas;
  
}

/*
 * 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:53