Actor Network Procedures as Psi-calculi for Security Ceremonies
This is an incremental contribution for researchers in formal methods and security, focusing on theoretical connections between existing formalisms.
This work tackles the problem of relating actor network procedures (ANP), a graphical formalism for security ceremonies, to the psi-calculi framework by providing a semantics for ANP through psi-calculi and developing a graphical language for a psi-calculus instance. The result is a deeper formalization and representation of ANP, though no concrete numbers are provided.
The actor network procedures of Pavlovic and Meadows are a recent graphical formalism developed for describing security ceremonies and for reasoning about their security properties. The present work studies the relations of the actor network procedures (ANP) to the recent psi-calculi framework. Psi-calculi is a parametric formalism where calculi like spi- or applied-pi are found as instances. Psi-calculi are operational and largely non-graphical, but have strong foundation based on the theory of nominal sets and process algebras. One purpose of the present work is to give a semantics to ANP through psi-calculi. Another aim was to give a graphical language for a psi-calculus instance for security ceremonies. At the same time, this work provides more insight into the details of the ANPs formalization and the graphical representation.