Language, Semantics, and Methods for Cryptographic Protocols

  • Federico Crazzolara
  • Glynn Winskel

Abstract

In this report we present a process language for security protocols together
with an operational semantics and an alternative semantics in terms of sets
of events. The denotation of process is a set of events, and as each event specifies
a set of pre- and postconditions, this denotation can be viewed as a Petri net.
This Petri-net semantics has a strong relation to both Paulson's inductive set
of rules [Pau98] and strand spaces [THG98c]. By means of an example we
illustrate how the Petri-net semantics can be used to prove properties such as
secrecy and authentication.
Published
2000-08-01
How to Cite
Crazzolara, F., & Winskel, G. (2000). Language, Semantics, and Methods for Cryptographic Protocols. BRICS Report Series, 7(18). https://doi.org/10.7146/brics.v7i18.20145