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.
|