/*
 * 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! 
 *
 * See andrewrpc.cry for a fixed version.
 *
 * Alan Jeffrey, v0.0.1 2001/02/22
 * Christian Haack, modified for v1.1.0 2004/09/09
 */

/*
 * 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:Un, 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:Un, b:Host, sessionKey:SharedKey(a,b), sessionNonce:Challenge )
= 
( ResponseToA(a,b,sessionKey,sessionNonce), Challenge );

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

pattern Msg4(a:Host,b:Host) = ( SharedKey(a,b), Challenge );

/*
 * The tag types.
 */

tag msg1(Msg1) : Auth(a:Host,b:Host);
tag msg2(Msg2(a,b)) : Auth(a:Un,b:Host);
tag msg3(Msg3(a,b)) : Auth(a:Host,b:Host);
tag msg4(Msg4(a,b)) : Auth(a:Un,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(nonceA,nonceB:Challenge) }kab;
  output socket is { msg3(nonceB) }kab;
  input socket is { msg4(
    sessionKey:SharedKey(a,b), 
    sessionNonce:Challenge 
  ) };
  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(nonceA,nonceB) }kab;
  input socket is { msg3(nonceB) }kab [ begun(a contacting b) ];
  out socket is { msg4(sessionKey,sessionNonce) };	
  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