/*
 * This protocol is the result of Needham and Schroeder's fix to the original 
 * Needham-Schroeder protocol to avoid the key compromise attack. The 
 * original Needham-Schroeder protocol is in ns.cry.
 *
 * The protocol allows the server S to generate a session key Kab for use 
 * by A and B.
 *
 *   A -> B : A
 *   B -> A : { msg2 (A, Nb0) }Kbs
 *   A -> S : A, B, Na, { msg2 (A, Nb0) }Kbs
 *   S -> A : { msg4 (Na, B, Kab, { msg5 (Kab, Nb0, A) }Kbs) }Kas
 *   A -> B : { msg5 (Kab, Nb0, A) }Kbs
 *   B -> A : { msg6 (Nb1) }Kab
 *   A -> B : { msg7 (Nb1) }Kab
 *
 * Alan Jeffrey, v0.0.2 2001/02/26
 * Christian Haack, modified for v1.1.0 2004/09/14
 * 
 */

/*
 * Include the standard prelude
 */

import prelude;

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

/*
 * Nonce types.
 */

type Challenge = PoshChall ();

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

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

type ResponseAToB ( a:Host, b:Host, kab:SharedKey(a,b,kab) )
  = PoshResp ( begun(a acknowledging reception of kab to b) );

/* 
 * Message patterns.
 */

pattern Msg2 = (Un,Challenge);

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

pattern Msg5 ( b:Un, s:Server, kbs:SharedKey(b,s,kbs) )
  = ( kab : SharedKey(a,b,kab),  
      nonceB0 : ResponseSToB(a,b,s,kab),
      a : Un );   

pattern Msg6 ( a:Un, b:Host, kab:SharedKey(a,b,kab) ) 
  = Challenge [ !begun(b acknowledging reception of kab to a) ];

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

/* 
 * Message tags.
 */

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

/*
 * The responder.
 */

server Responder
  (b:Host, s:Server, kbs:SharedKey(b,s,kbs)) 
  at b is (socket : Socket) 
{
  input socket is (a:Un);
  new (nonceB0 : Challenge);
  output socket is { msg2(a,nonceB0) }kbs; 
  input socket is { msg5(kab:SharedKey(a,b,kab), nonceB0, a) }kbs
    [ begun(s providing session key kab to b for a) ];
  end (s providing session key kab to b for a);    
  begin! (b acknowledging reception of kab to a);
  new (nonceB1 : Challenge);
  output socket is { msg6(nonceB1) }kab;
  input socket is { msg7(nonceB1) }kab
    [ begun(a acknowledging reception of kab to b) ];
  end(a acknowledging reception of kab to b);
}

/*
 * The intermediary.
 */

server Intermediary (s:Server) at s is (socket : Socket) 
{
  input socket is (a:Un,b:Un,nonceA:Challenge,ctext:Un);
  let kas:SharedKey(a,s,kas) = lkupKey (a,s);
  let kbs:SharedKey(b,s,kbs) = lkupKey (b,s);
  match ctext is { msg2 (a, nonceB0:Challenge) }kbs;
  new (kab : SharedKey(a,b,kab));
  begin(s providing session key kab to a for b);
  begin(s providing session key kab to b for a);
  output socket is { msg4(nonceA, b, kab, { msg5(kab,nonceB0,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