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

Pattern Matching

In Cryptyc, patterns are of the form msg or msg[assertions], where msg is a message with type annotations on some or all of its variables. An assertion, typically, is of the form begun(text) or !begun(text), indicating that a begin(text) or begin!(text) marker has previously been executed. Assertions may also be type assertions of the form msg : type. Examples for patterns are:

  • { MTag(msg : Public) }SKey

  • (msg : Public) [ !begun(Alice sending msg to Bob) ]

  • msg [ !begun(Alice sending msg to Bob), msg : Public ]

In order to explain pattern matching, we translate patterns to an alternative form that separates the three important pattern components: the binder, the message and the assertion set. After this translation, patterns have the form { binder . msg | assertions } . The msg component now contains no more type annotations --- type assertions all get moved to the assertions component. The binder collects all variables that were type-annotated before the translation. Here are the results of translating the three example patterns:

  • { msg . {MTag(msg)}SKey | msg : Public }

  • { msg . msg | !begun(Alice sending msg to Bob), msg : Public ]

  • { . msg | !begun(Alice sending msg to Bob), msg : Public }

We can now explain pattern matching: A message msg0 matches the pattern { binder . msg | assertions } iff it is obtained from msg by instantiating the binder such that the assertions are derivable under the matching instantiation.

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: Wed Nov 10 12:27:58 2004