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 is Abadi and Needham's simplification of the Otway-Rees * protocol (compare to or.cry). The analysis below shows that * the protocol can be further simplified by omitting the principal * names A in message 4 and B in message 3. * * A -> B : A, B, Na * B -> S : A, B, Na, Nb * S -> B : { msg4(Na,Kab,A,B) }Kas, { msg3(Nb,Kab,A,B) }Kbs * B -> A : { msg4(Na,Kab,A,B) }Kas * * Alan Jeffrey, v0.0.1 2001/02/26 * Christian Haack, modified for v1.1.0 2004/09/10 */
/* * Include the standard prelude */
import prelude;
/* * Words used in correspondence assertions. */
public providing : Word; public to : Word; public for : Word;
/* * Nonce types. */
type Challenge = PoshChall (); type ResponseToA ( s:Server, a:Any, b:Any, kab:SharedKey(a,b) ) = PoshResp ( begun(s providing kab to a for b) ); type ResponseToB ( s:Server, a:Any, b:Any, kab:SharedKey(a,b) ) = PoshResp ( begun(s providing kab to b for a) );
/* * The message patterns. */
pattern Msg3 (b:Any, s:Server) = ( kab : SharedKey(a,b), nonce:ResponseToB(s,a,b,kab), a:Un, _ );
// This pattern shows that Bob's name is not really needed in msg3.
pattern Msg4 (a:Any, s:Server) = ( kab:SharedKey(a,b), nonce:ResponseToA(s,a,b,kab), _, b:Un );
// This pattern shows that Alice's name is not really needed in msg4.
/* * The tag types. */
tag msg3(Msg3(b,s)) : Auth (b:Un,s:Server); tag msg4(Msg4(a,s)) : Auth (a:Un,s:Server);
/* * 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) : SharedKey(p,q);
/* * The initiator. */
client Initiator (a:Host, b:Host, s:Server, kas:SharedKey(a,s)) at a is { establish Responder at b is (socket:Socket); new (nonceA:Challenge); output socket is (a,b,nonceA); input socket is { msg4(kab:SharedKey(a,b),nonceA,a,b) }kas [ begun(s providing kab to a for b) ]; end(s providing kab to a for b); }
/* * The responder. */
server Responder (b:Host, s:Server, kbs:SharedKey(b,s)) at b is (socketA:Socket) { input socketA is (a:Un,b,nonceA:Challenge); establish Intermediary at s is (socketS:Socket); new (nonceB:Challenge); output socketS is (a,b,nonceA,nonceB); input socketS is ( ticketA:Un, { msg3(kab:SharedKey(a,b),nonceB,a,b) }kbs ) [ begun(s providing kab to b for a) ]; output socketA is ticketA; end (s providing kab to b for a); }
/* * The intermediary. */
server Intermediary (s:Server) at s is (socket:Socket) { input socket is (a:Un,b:Un,nonceA:Challenge,nonceB:Challenge); let kas:SharedKey(a,s) = lkupKey(a,s); let kbs:SharedKey(b,s) = lkupKey(b,s); new (kab:SharedKey(a,b)); begin (s providing kab to a for b); begin (s providing kab to b for a); output socket is ({ msg4(kab,nonceA,a,b) }kas, { msg3(kab,nonceB,a,b) }kbs); }
/* * 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