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

/* * This example is from section 6.1.5., "Using Non-Reversible Functions", * of the Clark/Jacob survey. In message 2, Alice sends a fresh session * key to Bob. In message 3, Bob acknowledges its receipt. * * B -> A : B,Nb * A -> B : Na, { msg2( hash(Nb), K) }Kab * B -> A : { hash( msg3(Na) ) }K * * where * Nb : a nonce generated by Bob * Na : a nonce generated by Alice * Kab : Alice and Bob's shared longterm key * msg2, msg3 : message tags * * We have omitted data that is irrelevant to our desired safety properties. * Moreover, we have omitted the unnecessary encryption of Na in message 2. * * Christian Haack, v1.1.0, 2004/11/05 */
/* * Include the standard prelude */
import prelude;
/* * Words used in correspondences. */
public sending : Word; public to : Word; public acknowledging : Word; public receipt : Word; public of : Word;
/* * Nonce types. */
type Challenge = PoshChall(); type ResponseAToB (a:Any, b:Any, k:Any) = PoshResp ( begun(a sending k to b) ); type ResponseBToA (a:Any, b:Any, k:Any) = PoshResp ( begun(b acknowledging to a receipt of k) );
/* * Message patterns. */
pattern Msg2 (a:Any, b:Any) = ( hash ( n:ResponseAToB(a,b,k) ), k:SharedKey(a,b,k) ); pattern Msg3 (a:Any, b:Any, k:Any) = ResponseBToA(a,b,k);
/* * Tag types. */
tag msg2 (Msg2(a,b)) : Auth (a:Any,b:Any,k:Any); tag msg3 (Msg3(a,b,k)) : Auth (a:Any,b:Any,k:Any);
/* * We assume that two 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 (p:Any,q:Any) : (k:SharedKey(p,q,k));
/* * The initiator. */
client Initiator (b:Host, a:Host, kab:SharedKey(a,b,kab)) at b is { establish Responder at a is (socket : Socket); new (nb : Challenge); output socket is (b,nb); input socket is (na:Challenge, { msg2( hash(nb), k:SharedKey(a,b,k) ) }kab ) [ begun (a sending k to b) ]; end (a sending k to b); begin (b acknowledging to a receipt of k); output socket is { hash( msg3(na) ) }k; }
/* * The responder. */
server Responder (a:Host) at a is (socket : Socket) { input socket is (b:Un, nb:Challenge); new (k : SharedKey(a,b,k)); new (na : Challenge); let kab : SharedKey(a,b,kab) = lkupKey (a,b); begin (a sending k to b); output socket is (na, { msg2( hash(nb), k ) }kab); input socket is { hash( msg3(na) ) }k [ begun (b acknowledging to a receipt of k) ]; end (b acknowledging to a receipt of k); }
/* * 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