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.