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 the Otway-Rees Protocol (see Clark/Jacob, 6.3.2), * using message tags to protect against the type flaw attack. * The protocol allows the server S to generate a session key Kab for use * by A and B. * * A -> B : Rid, A, B, { msg1 (Na,Rid,A,B) }Kas * B -> S : Rid, A, B, { msg1 (Na,Rid,A,B) }Kas, { msg2 (Nb,Rid,A,B) }Kbs * S -> B : Rid, { msg4(Na,Kab) }Kas, { msg3(Nb,Kab) }Kbs * B -> A : Rid, { msg4(Na,Kab) }Kas * * Compare this protocol to Abadi and Needham's simplification, * which we verify in or-simplified.cry. In comparison to the simplified * version, the original contains a freshly generated run identifier Rid. * The inclusion of the run identifier and the encryption of msg1 and msg2 * gives A the additional guarantee that B has been contacted as part of * the protocol run Rid. * * The type analysis of the protocol exposes various redundancies: For * instance, it is not necessary to send Rid as cleartext in the second, * third and fourth message. Moreover, the inclusion of A in msg1 is * redundant, as is the inclusion of B in msg2. * * Christian Haack, v1.1.0 2004/09/22 */
/* * Include the standard prelude */
import prelude;
/* * Words used in correspondence assertions. */
public providing : Word; public to : Word; public in : Word; public challenge : Word; public response : Word; public acknowledging : Word; public being : Word; public contacted : Word; public as : Word; public part : Word; public of : Word; public run : Word;
/* * Nonce types. */
type ChallengeAToS ( a:Any, b:Any, rid:Any ) = SoshChall( !begun(b acknowledging to a being contacted as part of run rid) ); type ResponseSToA ( s:Any, a:Any, kab:Any, na:Any ) = SoshResp ( begun(s providing kab to a in response to challenge na) ); type ChallengeBToS = SoshChall (); type ResponseSToB ( s:Any, b:Any, kab:Any, nb:Any ) = SoshResp ( begun(s providing kab to b in response to challenge nb) );
/* * The message patterns. */
pattern Msg1 (a:Any, s:Any) = ( na:ChallengeAToS(a,b,rid), rid:Un, _, b:Host );
// This pattern shows that Alice's name is not really needed in msg1.
pattern Msg2 (b:Any, s:Any) = ( nb:ChallengeBToS, rid:Un, a:Un, _ ) [ !begun(b acknowledging to a being contacted as part of run rid) ];
// This pattern shows that Bob's name is not really needed in msg1.
pattern Msg3 (b:Any, s:Any) = ( nb:ResponseSToB(s,b,kab,nb), kab:Private ); pattern Msg4 (a:Any, s:Any) = ( na:ResponseSToA(s,a,kab,na), kab:Private );
/* * The tag types. */
tag msg1(Msg1(a,s)) : Auth (a:Any,s:Any); tag msg2(Msg2(b,s)) : Auth (b:Any,s:Any); tag msg3(Msg3(b,s)) : Auth (b:Any,s:Any); tag msg4(Msg4(a,s)) : Auth (a:Any,s: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) : 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 (rid : Public); new ( nonceA : ChallengeAToS(a,b,rid) ); output socket is ( rid, a, b, { msg1(nonceA,rid,a,b) }kas ); input socket is ( rid, { msg4(nonceA,kab:Private) }kas ) [ begun(s providing kab to a in response to challenge nonceA), !begun(b acknowledging to a being contacted as part of run rid) ]; end(s providing kab to a in response to challenge nonceA); end(b acknowledging to a being contacted as part of run rid); }
/* * The responder. */
server Responder (b:Host, s:Server, kbs:SharedKey(b,s)) at b is (socketA:Socket) { input socketA is (rid:Un, a:Un, b, ticketS:Un); establish Intermediary at s is (socketS:Socket); new (nonceB : ChallengeBToS); begin! (b acknowledging to a being contacted as part of run rid); output socketS is (rid, ticketS, { msg2(nonceB,rid,a,b) }kbs); input socketS is ( rid, ticketA:Un, { msg3(nonceB,kab:Private) }kbs ) [ begun(s providing kab to b in response to challenge nonceB) ]; end(s providing kab to b in response to challenge nonceB); output socketA is (rid,ticketA); }
/* * The intermediary. */
server Intermediary (s:Server) at s is (socket:Socket) { input socket is (rid:Un,a:Un,b:Un,requestA:Un,requestB:Un); let kas:SharedKey(a,s) = lkupKey(a,s); let kbs:SharedKey(b,s) = lkupKey(b,s); match requestA is { msg1(nonceA:ChallengeAToS(a,b,rid), rid, a, b) }kas; match requestB is { msg2(nonceB:ChallengeBToS, rid, a, b) }kbs [ !begun(b acknowledging to a being contacted as part of run rid) ]; new (kab:SharedKey(a,b)); begin (s providing kab to a in response to challenge nonceA); begin (s providing kab to b in response to challenge nonceB); output socket is ( { msg4(nonceA,kab) }kas, { msg3(nonceB,kab) }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