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

/* * An acknowledgment using a nonce. * This is a "Secret-Out-Public-Home" (SOPH) nonce. * SOPH nonces are similar to Guttman's outgoing tests. * * Alice sends a text and a nonce N to Bob. * Bob returns N, in order to acknowledge the receipt of the text. * * A -> B : {| msg(A,text,N) |}pB * B -> A : N * * where * N : a nonce * msg : a message tag * pB : Bob's public encryption key * * Christian Haack, v1.1.0 2004/10/25 */
/* * Include the standard prelude */
import prelude;
/* * Words used in correspondence assertions. */
public acknowledging : Word; public receipt : Word; public of : Word; public to : Word;
/* * Nonce types. */
type Challenge (a:Any, b:Any, text:Any) = SophChall ( begun(b acknowledging receipt of text to a) ); type Response = SophResp ( );
/* * Message pattern. */
pattern Msg (b:Host) = ( a:Host, text:Private, n:Challenge(a,b,text) );
/* * Message tag. */
tag msg (Msg(b)) : Auth(b:Host);
/* * The initiator. */
client Initiator (a:Host, b:Host, pB:PublicKey(b)) at a is { establish Responder at b is (socket : Socket); new (text : Private); new (n : Challenge(a,b,text)); output socket is {| msg(a,text,n) |}pB; input socket is n [ begun(b acknowledging receipt of text to a) ]; end(b acknowledging receipt of text to a); }
/* * The responder. */
server Responder (b:Host, pB:PrivateKey(b)) at b is (socket : Socket) { input socket is {| msg(a:Un, text:Tainted, n:Challenge(a,b,text)) |}pB^-1; begin(b acknowledging receipt of text to a); output socket is n; }
/* * 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:52