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 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 pattems 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. © 2005 by International Federation for Information Processing.
CITATION STYLE
Haack, C., & Jeffrey, A. (2005). Pattern-matching spi-calculush. In IFIP Advances in Information and Communication Technology (Vol. 173, pp. 55–70). Springer New York LLC. https://doi.org/10.1007/0-387-24098-5_5
Mendeley helps you to discover research relevant for your work.