Modelling and analysis of PKI-based systems using process calculi

Benjamin Aziz*, Geoff Hamilton

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review


In this paper, 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.

Original languageEnglish
Pages (from-to)593-618
Number of pages26
JournalInternational Journal of Foundations of Computer Science
Issue number3
Publication statusPublished - 1 Jun 2007


Dive into the research topics of 'Modelling and analysis of PKI-based systems using process calculi'. Together they form a unique fingerprint.

Cite this