/*
 * This is a version of Carlsen's Secret Key Initiator Protocol,
 * as presented in section 6.3.7 of the Clark/Jacob survey.
 *
 *   A -> B : A, Na
 *   B -> S : A, Na, B, Nb1
 *   S -> B : { msg3b(A, Kab, Nb1) }Kbs, { msg3a(B, Kab, Na) }Kas
 *   B -> A : { msg3a(B, Kab, Na) }Kas, { msg4(Na) }Kab, Nb2
 *   A -> B : { msg5(Nb2) }Kab
 *
 * The first three messages and the first half of the fourth are 
 * exactly as Abadi and Needham's simplification of the Otway-Rees
 * protocol (see or-simplified.cry). What follows are acknowledgments 
 * that A and B have actually received Kab. Bob acknowledges to Alice
 * by sending {msg4(Na)}Kab, and Alice acknowledges to Bob by sending 
 * {msg5(Nb2)}Kab. 
 *
 * Alan Jeffrey, v0.0.2 2001/03/10
 * 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 for : Word;
public acknowledging : Word;
public receipt : Word;
public of : Word;
public to : Word;

/*
 * The nonce types.
 */

type Challenge = PoshChall ();

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

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

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

/*
 * The message patterns.
 */

pattern Msg3b (b:Un,s:Server)
  = ( kab:SharedKey(a,b,kab), nonce:ResponseSToB(s,a,b,kab), a:Un);

pattern Msg3a (a:Un,s:Server)
  = ( kab:SharedKey(a,b,kab), nonce:ResponseSToA(s,a,b,kab), b:Un );

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

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

/* 
 * The tag types.
 */

tag msg3a (Msg3a(b,s)) : Auth(b:Un, s:Server, k:SharedKey(b,s,k));
tag msg3b (Msg3b(a,s)) : Auth(a:Un, s:Server, k:SharedKey(a,s,k));
tag msg4 (Msg4(a,b,k)) : Auth(a:Un, b:Server, k:SharedKey(a,b,k)); 
tag msg5 (Msg5(a,b,k)) : Auth(a:Host, b:Server, k:SharedKey(a,b,k)); 

/*
 * 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,b,nonceA);
  input socket is { msg3a(kab:SharedKey(a,b,kab), nonceA, b) }kas 
    [ begun(s providing kab to a for b) ];
  end(s providing kab to a for b);
  input socket is ( {msg4(nonceA)}kab, nonceB2:Challenge )
    [ !begun(b acknowledging receipt of kab to a) ];
  end(b acknowledging receipt of kab to a); 
  begin(a acknowledging receipt of kab to b);
  output socket is { msg5(nonceB2) }kab;		  
}

/*
 * The responder.
 */

server Responder
  (b:Host, s:Server, kbs:SharedKey(b,s,kbs)) 
  at b is (socket:Socket) 
{
  input socket 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, 
    { msg3b(kab:SharedKey(a,b,kab), nonceB, a) }kbs 
  ) [ begun(s providing kab to b for a) ];
  end (s providing kab to b for a);
  begin!(b acknowledging receipt of kab to a);
  new (nonceB2:Public);
  output socket is ( ticketA, {msg4(nonceA) }kab, nonceB2 );
  input socket is { msg5(nonceB2) }kab
    [ begun(a acknowledging receipt of kab to b) ];
  end(a acknowledging receipt of kab to b); 

}

/*
 * 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,kas) = lkupKey(a,s);
  let kbs:SharedKey(b,s,kbs) = lkupKey(b,s);	
  new (kab:SharedKey(a,b,kab));
  begin (s providing kab to a for b);
  begin (s providing kab to b for a);
  output socket is (
    { msg3a(kab,nonceA,b) }kas,
    { msg3b(kab,nonceB,a) }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