/*
 * This is a simple mutual authentication protocol
 * where Alice and Bob authenticate themselves to each other.
 * This is the `ISO Symmetric Key Three-Pass Mutual Authentication'
 * protocol from Clark and Jacob (1997) with the non-secret messages
 * removed, and the messages reordered to deal with dependent records.
 *
 * B -> A : Nb
 * A -> B : { MsgA, B, Na, Nb }Kab   // Note that B is redundant here
 * B -> A : { MsgB, Na, Nb }Kab      // Note that Nb is redundant here
 *
 * Alan Jeffrey, v0.0.1 2001/02/22
 */

/*
 * Include the standard prelude
 */

import oldprelude;

/*
 * This file declares a server Responder and a client Initiator.
 */

public Responder : Server;
public Initiator : Client;

/*
 * Words used in the nonce
 */

public sent : Word;
public for : Word;

/*
 * The types of the nonce and keys.
 */

type NonceA (msgB : Payload) = Nonce (end (Initiator for Bob sent msgB));
type NonceB (msgA : Payload) = Nonce (end (Responder for Alice sent msgA));

type Msg2 = Struct (msgA : Payload, b : Host, nonceA : Challenge, nonceB' : NonceB (msgA));
type Msg3 = Struct (msgB : Payload, nonceA' : NonceA (msgB), nonceB : Challenge);

type MutualMsg = Union (msg2 : Msg2, msg3 : Msg3);

type MutualKey = Key (MutualMsg);

/*
 * The key shared between Alice and Bob.
 */

private SKey : MutualKey;

/*
 * The responder.
 */

server Responder at Alice is (socket : Socket) {

  input socket is (nonceB : Challenge);
  new (msgA : Payload);
  new (nonceA : Challenge);
  begin (Responder for Alice sent msgA);
  cast nonceB is (nonceB' : NonceB (msgA));
  output socket is ({ msg2 (msgA, Bob, nonceA, nonceB') }SKey);
  input socket is ({ msg3 (msgB : Payload, nonceA' : NonceA (msgB), nonceB) }SKey);
  check nonceA is nonceA';
  end (Initiator for Bob sent msgB);

}

/*
 * The initiator.
 */

client Initiator at Bob is {

  establish Responder at Alice is (socket : Socket);
  new (msgB : Payload);
  new (nonceB : Challenge);
  begin (Initiator for Bob sent msgB);
  output socket is (nonceB);
  input socket is ({ msg2(msgA : Payload, Bob, nonceA : Challenge, nonceB' : NonceB (msgA)) }SKey);
  check nonceB is nonceB';
  cast nonceA is (nonceA' : NonceA (msgB));
  output socket is ({ msg3(msgB, nonceA', nonceB) }SKey);
  end (Responder for Alice sent msgA);

}

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