/*
 * This is a variant of the Andrew Secure RPC Protocol
 * from Clark and Jacob (1997), using message tags rather
 * than nonce arithmetic.  The protocol is used to exchange
 * a session key SK and a session nonce SN.  The original protocol is:
 *
 * A -> B : A, { msg1(Na) }Kab
 * B -> A : { msg2(Na, Nb) }Kab
 * A -> B : { msg3(Nb) }Kab
 * B -> A : { msg4(SK, SN) }Kab
 *
 * This protocol is flawed, not to mention rather redundant: a
 * 3-way handshake is being used for nonce challenges, which are
 * then ignored in the final message! We can fix this by merging 
 * messages 2 and 4 into one message:
 *
 * A -> B : A, { msg1(Na) }Kab
 * B -> A : { msg2(SK, SN, Na, Nb) }Kab
 * A -> B : { msg3(Nb) }Kab
 *
 * Alan Jeffrey, v0.0.1 2001/02/22
 * Christian Haack, modified for v1.1.0 2004/09/08
 */

/*
 * Include the standard prelude
 */

import prelude;

/*
 * Words used in the correspondence assertions.
 */

public contacting : Word;
public generating : Word;
public and : Word;
public for : Word;

/*
 * The nonce types.
 */

type Challenge = SoshChall();

type ResponseToA( 
  a:Host, b:Host, sessionKey:SharedKey(a,b), sessionNonce:Challenge )
= 
SoshResp( 
  begun(b generating sessionKey and sessionNonce for a),
  fresh(sessionNonce:Challenge) );

type ResponseToB(a:Host,b:Host) = SoshResp ( begun(a contacting b) );

/* 
 * The message patterns.
 */

pattern Msg1 = Challenge;

pattern Msg2(a:Host,b:Host) = ( 
  sessionKey : SharedKey(a,b),
  sessionNonce : Challenge, 
  nonceA : ResponseToA(a,b,sessionKey,sessionNonce), 
  nonceB : Challenge 
);

pattern Msg3(a:Host,b:Host) = ResponseToB(a,b);

/*
 * The tag types.
 */

tag msg1(Msg1) : Auth(a:Host,b:Host);
tag msg2(Msg2(a,b)) : Auth(a:Host,b:Host);
tag msg3(Msg3(a,b)) : Auth(a:Host,b:Host);


/*
 * We assume that 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(a:Any,b:Any) : SharedKey(a,b);

/*
 * The initiator.
 */

client Initiator (a:Host, b:Host, kab:SharedKey(a,b)) at a is 
{ 
  establish responder at b is (socket:Socket);
  begin(a contacting b);
  new (nonceA : Challenge);
  output socket is (a, { msg1(nonceA) }kab);
  input socket is { msg2(
    sessionKey : SharedKey(a,b), 
    sessionNonce : Challenge, 
    nonceA, 
    nonceB : Challenge
  ) }kab [ begun(b generating sessionKey and sessionNonce for a),
           fresh(sessionNonce:Challenge) ];
  output socket is { msg3(nonceB) }kab;
  end(b generating sessionKey and sessionNonce for a);
}

/*
 * The responder.
 */

server Responder(b:Host) at b is (socket:Socket) 
{
  input socket is (a:Un,ctext:Un);
  let kab:SharedKey(a,b) = lkupKey(a,b);
  match ctext is { msg1(nonceA:Challenge) }kab;   
  new (nonceB:Challenge);
  new (sessionKey:SharedKey(a,b));
  new (sessionNonce:Challenge);
  begin(b generating sessionKey and sessionNonce for a);
  output socket is { msg2(sessionKey,sessionNonce,nonceA,nonceB) }kab;
  input socket is { msg3(nonceB) }kab [ begun(a contacting b) ];
  end(a contacting b);
}

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