/*
 * This the Otway-Rees Protocol (see Clark/Jacob, 6.3.2),  
 * using message tags to protect against the type flaw attack.
 * The protocol allows the server S to generate a session key Kab for use 
 * by A and B. 
 *
 *   A -> B : Rid, A, B, { msg1 (Na,Rid,A,B) }Kas
 *   B -> S : Rid, A, B, { msg1 (Na,Rid,A,B) }Kas, { msg2 (Nb,Rid,A,B) }Kbs
 *   S -> B : Rid, { msg4(Na,Kab) }Kas, { msg3(Nb,Kab) }Kbs
 *   B -> A : Rid, { msg4(Na,Kab) }Kas
 *
 * Compare this protocol to Abadi and Needham's simplification, 
 * which we verify in or-simplified.cry. In comparison to the simplified
 * version, the original contains a freshly generated run identifier Rid.
 * The inclusion of the run identifier and the encryption of msg1 and msg2
 * gives A the additional guarantee that B has been contacted as part of 
 * the protocol run Rid. 
 *
 * The type analysis of the protocol exposes various redundancies: For
 * instance, it is not necessary to send Rid as cleartext in the second,
 * third and fourth message. Moreover, the inclusion of A in msg1 is 
 * redundant, as is the inclusion of B in msg2. 
 *
 * Christian Haack, v1.1.0 2004/09/22
 */

/*
 * Include the standard prelude
 */

import prelude;

/*
 * Words used in correspondence assertions.
 */

public providing : Word;
public to : Word;
public in : Word;
public challenge : Word;
public response : Word;
public acknowledging : Word;
public being : Word;
public contacted : Word;
public as : Word;
public part : Word; 
public of : Word;
public run : Word;

/*
 * Nonce types.
 */

type ChallengeAToS ( a:Any, b:Any, rid:Any )
= SoshChall( !begun(b acknowledging to a being contacted as part of run rid) );

type ResponseSToA ( s:Any, a:Any, kab:Any, na:Any )
  = SoshResp ( begun(s providing kab to a in response to challenge na) );

type ChallengeBToS
  = SoshChall ();

type ResponseSToB ( s:Any, b:Any, kab:Any, nb:Any )
  = SoshResp ( begun(s providing kab to b in response to challenge nb) );

/*
 * The message patterns.
 */

pattern Msg1 (a:Any, s:Any) 
  = ( na:ChallengeAToS(a,b,rid), rid:Un, _, b:Host );
// This pattern shows that Alice's name is not really needed in msg1.

pattern Msg2 (b:Any, s:Any)
  = ( nb:ChallengeBToS, rid:Un, a:Un, _ )
    [ !begun(b acknowledging to a being contacted as part of run rid) ];
// This pattern shows that Bob's name is not really needed in msg1.

pattern Msg3 (b:Any, s:Any)
  = ( nb:ResponseSToB(s,b,kab,nb), kab:Private );

pattern Msg4 (a:Any, s:Any)
  = ( na:ResponseSToA(s,a,kab,na), kab:Private );

/* 
 * The tag types.
 */

tag msg1(Msg1(a,s)) : Auth (a:Any,s:Any);
tag msg2(Msg2(b,s)) : Auth (b:Any,s:Any);
tag msg3(Msg3(b,s)) : Auth (b:Any,s:Any);
tag msg4(Msg4(a,s)) : Auth (a:Any,s:Any);

/*
 * 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 (rid : Public);	
  new ( nonceA : ChallengeAToS(a,b,rid) );	
  output socket is ( rid, a, b, { msg1(nonceA,rid,a,b) }kas );
  input socket is ( rid, { msg4(nonceA,kab:Private) }kas ) 
    [ begun(s providing kab to a in response to challenge nonceA),
      !begun(b acknowledging to a being contacted as part of run rid) ];
  end(s providing kab to a in response to challenge nonceA);
  end(b acknowledging to a being contacted as part of run rid);
}

/*
 * The responder.
 */

server Responder
  (b:Host, s:Server, kbs:SharedKey(b,s)) 
  at b is (socketA:Socket) 
{
  input socketA is (rid:Un, a:Un, b, ticketS:Un);	
  establish Intermediary at s is (socketS:Socket);
  new (nonceB : ChallengeBToS);
  begin! (b acknowledging to a being contacted as part of run rid);
  output socketS is (rid, ticketS, { msg2(nonceB,rid,a,b) }kbs);
  input socketS is ( rid, ticketA:Un, { msg3(nonceB,kab:Private) }kbs )
    [ begun(s providing kab to b in response to challenge nonceB) ];
  end(s providing kab to b in response to challenge nonceB);
  output socketA is (rid,ticketA);

}  

/*
 * The intermediary.
 */

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

  input socket is (rid:Un,a:Un,b:Un,requestA:Un,requestB:Un);
  let kas:SharedKey(a,s) = lkupKey(a,s);
  let kbs:SharedKey(b,s) = lkupKey(b,s);
  match requestA is { msg1(nonceA:ChallengeAToS(a,b,rid), rid, a, b) }kas; 
  match requestB is { msg2(nonceB:ChallengeBToS, rid, a, b) }kbs
    [ !begun(b acknowledging to a being contacted as part of run rid) ];
  new (kab:SharedKey(a,b));
  begin (s providing kab to a in response to challenge nonceA);
  begin (s providing kab to b in response to challenge nonceB);
  output socket is ( { msg4(nonceA,kab) }kas, { msg3(nonceB,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:53