Andrew D. Gordon
Microsoft Research

Christian Haack
Radboud University

Alan Jeffrey
Bell Labs

Cryptographic Protocol Type Checker

Introduction

Applet

Examples

Download

Research Papers

Changelog

To Do List

/* * A simple nonce challenge. * This is a "Public-Out-Signed-Home" (POSH) nonce. * POSH nonces are similar to Guttman's incoming tests. * * A -> B : A * B -> A : N * A -> B : {| msg(N,text,B) |}sA * * where * N : nonce * msg : a message tag * sA : Alice's private signing key * * Alan Jeffrey v0.0.2 2001/02/22 * Christian Haack, modified for v1.1.0 2004/11/03 */
/* * Include the standard prelude */
import prelude;
/* * Words used in correspondence assertions. */
public sending : Word; public to : Word;
/* * Nonce types. */
type Challenge = PoshChall (); type Response (a:Host,b:Host,text:Public) = PoshResp ( begun(a sending text to b) );
/* * The message pattern. */
pattern Msg (a:Host) = ( nA:Response(a,b,text), text:Public, b:Host );
/* * The message tag. */
tag msg (Msg(a)) : Auth<a:Host>;
/* * We assume that two principals are able to securely lookup the required * authentication keys. We formally express this by assuming the existence * of a secure lookup function of the following dependent function type: */
fun lkupAuthKey (p:Any) : AuthKey(p);
/* * The sender, who receives a nonce challenge from the receiver, * generates a new message, begins the appropriate session, * then tags and encrypts the text with the authorizing nonce, * then sends the ciphertext. */
client Sender (a:Host, b:Host, sA:SignKey(a)) at a is { establish Receiver at b is (socket : Socket); output socket is a; input socket is (nonce : Challenge); new (text : Public); begin(a sending text to b); output socket is {| msg(nonce,text,b) |}sA; }
/* * The receiver, who issues the nonce challenge, * gets back the response, checks the nonce is the one issued, * and ends the session. */
server Receiver (b:Host) at b is (socket : Socket) { input socket is (a:Un); new (nonce : Challenge); output socket is nonce; let sA:AuthKey(a) = lkupAuthKey (a); input socket is {| msg(nonce, text:Public, b) |}sA^-1 [ begun(a sending text to b) ]; end(a sending text to 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