/*
 * This is Abadi and Needham's simplification of the Otway-Rees 
 * protocol (compare to or.cry). The analysis below shows that
 * the protocol can be further simplified by omitting the principal
 * names A in message 4 and B in message 3.
 *
 *   A -> B : A, B, Na
 *   B -> S : A, B, Na, Nb
 *   S -> B : { msg4(Na,Kab,A,B) }Kas, { msg3(Nb,Kab,A,B) }Kbs
 *   B -> A : { msg4(Na,Kab,A,B) }Kas
 *
 * Alan Jeffrey, v0.0.1 2001/02/26
 * Christian Haack, modified for v1.1.0 2004/09/10
 */

/*
 * Include the standard prelude
 */

import prelude;

/*
 * Words used in correspondence assertions.
 */

public providing : Word;
public to : Word;
public for : Word;

/*
 * Nonce types.
 */

type Challenge = PoshChall ();

type ResponseToA ( s:Server, a:Any, b:Any, kab:SharedKey(a,b) )
  = PoshResp ( begun(s providing kab to a for b) );

type ResponseToB ( s:Server, a:Any, b:Any, kab:SharedKey(a,b) )
  = PoshResp ( begun(s providing kab to b for a) );

/*
 * The message patterns.
 */

pattern Msg3 (b:Any, s:Server)
  = ( kab : SharedKey(a,b), nonce:ResponseToB(s,a,b,kab), a:Un, _ );
// This pattern shows that Bob's name is not really needed in msg3. 

pattern Msg4 (a:Any, s:Server)
  = ( kab:SharedKey(a,b), nonce:ResponseToA(s,a,b,kab), _, b:Un );
// This pattern shows that Alice's name is not really needed in msg4.

/* 
 * The tag types.
 */

tag msg3(Msg3(b,s)) : Auth (b:Un,s:Server);
tag msg4(Msg4(a,s)) : Auth (a:Un,s:Server);

/*
 * 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) : SharedKey(p,q);

/*
 * The initiator.
 */

client Initiator
  (a:Host, b:Host, s:Server, kas:SharedKey(a,s)) 
  at a is 
{
  establish Responder at b is (socket:Socket);
  new (nonceA:Challenge);	
  output socket is (a,b,nonceA);
  input socket is { msg4(kab:SharedKey(a,b),nonceA,a,b) }kas 
    [ begun(s providing kab to a for b) ];
  end(s providing kab to a for b);	  

}

/*
 * The responder.
 */

server Responder
  (b:Host, s:Server, kbs:SharedKey(b,s)) 
  at b is (socketA:Socket) 
{
  input socketA is (a:Un,b,nonceA:Challenge);
  establish Intermediary at s is (socketS:Socket);
  new (nonceB:Challenge);
  output socketS is (a,b,nonceA,nonceB);
  input socketS is ( 
    ticketA:Un, 
    { msg3(kab:SharedKey(a,b),nonceB,a,b) }kbs 
  ) [ begun(s providing kab to b for a) ];
  output socketA is ticketA;
  end (s providing kab to b for a);
}

/*
 * The intermediary.
 */

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

  input socket is (a:Un,b:Un,nonceA:Challenge,nonceB:Challenge);
  let kas:SharedKey(a,s) = lkupKey(a,s);
  let kbs:SharedKey(b,s) = lkupKey(b,s);
  new (kab:SharedKey(a,b));
  begin (s providing kab to a for b);
  begin (s providing kab to b for a);
  output socket is ({ msg4(kab,nonceA,a,b) }kas, { msg3(kab,nonceB,a,b) }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:53