The open archive for STFC research publications

Full Record Details

Persistent URL http://purl.org/net/epubs/work/41590
Record Status Checked
Record Id 41590
Title Modelling and analysis of PKI-based systems using process calculi
Abstract 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.
Organisation CCLRC
Keywords Engineering , Security , PKI , Process Algebra , Static Analysis
Funding Information
Related Research Object(s):
Licence Information:
Language English (EN)
Type Details URI(s) Local file(s) Year
Journal Article Int. Jnl Found. Comp. Sci. 18, no. 3 (2007): 593-618. doi:10.1142/S0129054107004851 2007
Report Imperial College London Technical Reports 2006/14. 2006. http://www.doc.ic…icalreports/2006/#14 2006