TY - JOUR
T1 - Modelling and analysis of PKI-based systems using process calculi
AU - Aziz, Benjamin
AU - Hamilton, Geoff
PY - 2007/6/1
Y1 - 2007/6/1
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=34249734226&partnerID=8YFLogxK
U2 - 10.1142/S0129054107004851
DO - 10.1142/S0129054107004851
M3 - Article
AN - SCOPUS:34249734226
VL - 18
SP - 593
EP - 618
JO - International Journal of Foundations of Computer Science
JF - International Journal of Foundations of Computer Science
SN - 0129-0541
IS - 3
ER -