/*
 * This is the simple example discussed in the Introduction at intro.html.
 *
 * Christian Haack, v.1.1.0 2004/11/08
 */

import prelude;

public sending : Word;
public to : Word;

private SKey : SharedKey (Alice,Bob);

pattern Msg (a:Host, b:Host)
  = ( msg : Public ) [ !begun (a sending msg to b) ];

tag MTag (Msg(a,b)) : Auth(a:Host, b:Host);

client Sender at Alice is {
  establish Receiver at Bob is (socket : Socket);
  new (msg : Public);
  begin! (Alice sending msg to Bob);
  output socket is { MTag(msg) }SKey;
}

server Receiver at Bob is (socket : Socket) {
  input socket is { MTag(msg:Public) }SKey;
  end (Alice sending msg to Bob);
}

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