Pattern-Matching Spi-Calculus
Cryptographic protocols often make use of nested cryptographic
primitives, for example signed message digests, or encrypted signed
messages. Gordon and Jeffrey's prior work on types for authenticity
did not allow for such nested cryptography. In this work, we present
the \emph{pattern-matching spi-calculus}, which is an obvious extension
of the spi-calculus to include pattern-matching as primitive. The
novelty of the language is in the accompanying type system, which uses
the same language of patterns to describe complex data dependencies
which cannot be described using prior type systems. We show
that any appropriately typed process is guaranteed to satisfy
a strong robust safety property.