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 a version of Carlsen's Secret Key Initiator Protocol, * as presented in section 6.3.7 of the Clark/Jacob survey. * * A -> B : A, Na * B -> S : A, Na, B, Nb1 * S -> B : { msg3b(A, Kab, Nb1) }Kbs, { msg3a(B, Kab, Na) }Kas * B -> A : { msg3a(B, Kab, Na) }Kas, { msg4(Na) }Kab, Nb2 * A -> B : { msg5(Nb2) }Kab * * The first three messages and the first half of the fourth are * exactly as Abadi and Needham's simplification of the Otway-Rees * protocol (see or-simplified.cry). What follows are acknowledgments * that A and B have actually received Kab. Bob acknowledges to Alice * by sending {msg4(Na)}Kab, and Alice acknowledges to Bob by sending * {msg5(Nb2)}Kab. * * Alan Jeffrey, v0.0.2 2001/03/10 * 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 for : Word; public acknowledging : Word; public receipt : Word; public of : Word; public to : Word;
/* * The nonce types. */
type Challenge = PoshChall (); type ResponseSToA ( s:Server, a:Un, b:Un, kab:SharedKey(a,b,kab) ) = PoshResp ( begun(s providing kab to a for b) ); type ResponseSToB ( s:Server, a:Un, b:Un, kab:SharedKey(a,b,kab) ) = PoshResp ( begun(s providing kab to b for a) ); type ResponseAToB ( a:Host, b:Host, kab:SharedKey(a,b,kab) ) = PoshResp ( begun(a acknowledging receipt of kab to b) );
/* * The message patterns. */
pattern Msg3b (b:Un,s:Server) = ( kab:SharedKey(a,b,kab), nonce:ResponseSToB(s,a,b,kab), a:Un); pattern Msg3a (a:Un,s:Server) = ( kab:SharedKey(a,b,kab), nonce:ResponseSToA(s,a,b,kab), b:Un ); pattern Msg4 (a:Un,b:Host,kab:SharedKey(a,b,kab)) = Un [ !begun(b acknowledging receipt of kab to a) ]; pattern Msg5 (a:Host,b:Host,kab:SharedKey(a,b,kab)) = ResponseAToB(a,b,kab);
/* * The tag types. */
tag msg3a (Msg3a(b,s)) : Auth(b:Un, s:Server, k:SharedKey(b,s,k)); tag msg3b (Msg3b(a,s)) : Auth(a:Un, s:Server, k:SharedKey(a,s,k)); tag msg4 (Msg4(a,b,k)) : Auth(a:Un, b:Server, k:SharedKey(a,b,k)); tag msg5 (Msg5(a,b,k)) : Auth(a:Host, b:Server, k:SharedKey(a,b,k));
/* * 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 (a:Host, b:Host, s:Server, kas:SharedKey(a,s,kas)) at a is { establish Responder at b is (socket:Socket); new (nonceA:Challenge); output socket is (a,b,nonceA); input socket is { msg3a(kab:SharedKey(a,b,kab), nonceA, b) }kas [ begun(s providing kab to a for b) ]; end(s providing kab to a for b); input socket is ( {msg4(nonceA)}kab, nonceB2:Challenge ) [ !begun(b acknowledging receipt of kab to a) ]; end(b acknowledging receipt of kab to a); begin(a acknowledging receipt of kab to b); output socket is { msg5(nonceB2) }kab; }
/* * The responder. */
server Responder (b:Host, s:Server, kbs:SharedKey(b,s,kbs)) at b is (socket:Socket) { input socket 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, { msg3b(kab:SharedKey(a,b,kab), nonceB, a) }kbs ) [ begun(s providing kab to b for a) ]; end (s providing kab to b for a); begin!(b acknowledging receipt of kab to a); new (nonceB2:Public); output socket is ( ticketA, {msg4(nonceA) }kab, nonceB2 ); input socket is { msg5(nonceB2) }kab [ begun(a acknowledging receipt of kab to b) ]; end(a acknowledging receipt of kab to b); }
/* * 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,kas) = lkupKey(a,s); let kbs:SharedKey(b,s,kbs) = lkupKey(b,s); new (kab:SharedKey(a,b,kab)); begin (s providing kab to a for b); begin (s providing kab to b for a); output socket is ( { msg3a(kab,nonceA,b) }kas, { msg3b(kab,nonceB,a) }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