Modelling and Analysis of PKI-Based Systems Using Process Calculi

In this technical report, we present a process algebra aimed at modelling PKI-based systems. The new language, SPIKY, extends the spi-calculus by adding primitives for the retrieval of certified/uncertified public keys as well as private keys belonging to users of the PKI-based system. SPIKY also formalises the notion of process ownership by PKI users, which is necessary in controlling the semantics of the key retrieval capabilities. We also construct a static analysis for SPIKY that captures the property of term substitutions resulting from message-passing and PKI/cryptographic operations. This analysis is shown to be safe and computable. Finally, we use the analysis to define the term secrecy and peer participation properties for a couple of examples of authentication protocols.

• Type: Journal
• Year: 2007
• Where: IJFCS
• Authors: Benjamin Aziz, Geoff Hamilton
• Keywords: IJFCS 2007, Key Retrieval Capabilities, PKI-based Systems, Technical Report