Regular PapersNo Access

MODELLING AND ANALYSIS OF PKI-BASED SYSTEMS USING PROCESS CALCULI

BENJAMIN AZIZ

Department of Computing, Imperial College London, 180 Queen's Gate, London, SW7 2AZ, United Kingdom

Search for more papers by this author

and

GEOFF HAMILTON

School of Computing, Dublin City University, Dublin 9, Ireland

Search for more papers by this author

https://doi.org/10.1142/S0129054107004851Cited by:3 (Source: Crossref)

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.

References

Martín Abadi and Andrew Gordon, A calculus for cryptographic protocols: The spi calculus, Proceedings of the 4th ACM Conference on Computer and Communications Security (ACM Press, 1997) pp. 36–47. Google Scholar
Samson Abramsky, Information and Computation 92(2), 161 (1991), DOI: 10.1006/inco.1991.9999. Crossref, Web of Science, Google Scholar
B. Aziz. A Static Analysis Framework for Security Properties in Mobile and Cryptographic Systems. PhD thesis, School of Computing, Dublin City University, Dublin, Ireland, 2003 . Google Scholar
Benjamin Aziz, A semiring-based quantitative analysis of mobile systems, Proceedings of the 3rd International Workshop on Software Verification and Validation, Electronic Notes in Theoretical Computer Science 157 (Elsevier, 2005) pp. 3–21. Google Scholar
Benjamin Aziz, David Gray and Geoff Hamilton, A static analysis of pki-based systems, Proceedings of the 9th Italian Conference on Theoretical Computer Science, Lecture Notes in Computer Science 3701 (Springer Verlag, 2005) pp. 51–65. Google Scholar
Benjamin Aziz, Geoff Hamilton and David Gray, Journal of Logic and Algebraic Programming 64(2), 285 (2005), DOI: 10.1016/j.jlap.2004.09.006. Crossref, Web of Science, Google Scholar
Hanane El Bakkali and Bahia Idrissi Kaitouni, A predicate calculus logic for the pki trust model analysis, Proceedings of the IEEE International Symposium on Network Computing and Applications (IEEE Computer Society, 2001) pp. 368–371. Google Scholar
Chiara Bodeiet al., Automatic validation of protocol narration, Proceedings of the 16th IEEE Computer Security Foundations Workshop (IEEE Computer Society, 2003) pp. 126–140. Google Scholar
Chiara Bodeiet al., Information and Computation 168(1), 68 (2001), DOI: 10.1006/inco.2000.3020. Crossref, Web of Science, Google Scholar
Ahmed Bouajjani, Javier Esparza and Oded Maler, Reachability analysis of push-down automata: Application to model-checking, Proceedings of the 8th International Conference on Concurrency Theory, Lecture Notes in Computer Science 1243, eds. Antoni W. Mazurkiewicz and Jzef Winkowski (Springer Verlag, 1997) pp. 135–150. Google Scholar
Iliano Cervesato, The dolev-yao intruder is the most powerful attacker, Proceedings of the 16th Annual Symposium on Logic in Computer Science, ed. J. Halpern (IEEE Computer Society Press, 2001) pp. 246–265. Google Scholar
Danny Dolev and A. Yao, On the security of public key protocols, Proceedings of the 22nd Annual Symposium on Foundations of Computer Science (1981) pp. 350–357. Google Scholar
C. M. Ellison, B. Frantz, B. Lampson, R. L. Rivest, B. M. Thomas, and T. Ylonen. Spki certificate theory. RFC 2693, September 1999 . Google Scholar
Javier Esparzaet al., Efficient algorithms for model checking pushdown systems, Proceedings of the 12th International Conference on Computer-Aided Verification, Lecture Notes in Computer Science 1855, eds. E. Allen Emerson and A. Prasad Sistla (Springer Verlag, 2000) pp. 232–247. Google Scholar
Andrew Gordon, Nominal calculi for security and mobility, Proceedings of the DARPA Workshop on Foundations for Secure Mobile Code, eds. D. Volpano, C. Irvine and G. Smith (US Naval Postgraduate School, 1997) pp. 10–14. Google Scholar
M. J. C. Gordon and T. F. Melham , Introduction to HOL ( Cambridge University Press , Cambridge, UK , 1993 ) . Google Scholar
David Gray , Benjamin Aziz and Geoff Hamilton , Spiky: A nominal calculus for modelling protocols that use pkis , Proceedings of the International Workshop on Security Analysis of Systems: Formalism and Tools ( 2004 ) . Google Scholar
Steffen M. Hansen, Jakob Skriver and Hanne Riis Nielson, Using static analysis to validate the saml single sign-on protocol, Proceedings of the 2005 workshop on Issues in the theory of security (ACM Press, 2005) pp. 27–40. Google Scholar
C. A. R. Hoare, Communications of the ACM 21(8), 666 (1978), DOI: 10.1145/359576.359585. Crossref, Web of Science, Google Scholar
Somesh Jha and Thomas W. Reps, Analysis of spki/sdsi certificates using model checking, Proceedings of the 15th IEEE Computer Security Foundations Workshop (IEEE Computer Society, 2002) pp. 129–147. Google Scholar
T. Ksiyatrakul, S. Older, and S.-K. Chin. Formal analysis of x.509 certificates. Technical Report TR DII 08/01, Universit degli studi di Siena, 2001 . Google Scholar
Eve Maler, Prateek Mishra, and Rob Philpott. Assertions and protocol for the oasis security assertion markup language, version 1.1 edition. Technical Report oasis-sstc-saml-core-1.1, OASIS, September 2003 . Google Scholar
Eve Maler, Prateek Mishra, and Rob Philpott. Bindings and proles for the oasis security assertion markup language, version 1.1 edition. Technical Report sstc-saml-bindings-1.1-cs-01, OASIS, May 2003 . Google Scholar
Robin Milner , Communicating and Mobile Systems: The Pi-Calculus ( Cambridge University Press , 1999 ) . Google Scholar
Robin Milner, Joachim Parrow and David Walker, Information and Computation 100(1), 1 (1992), DOI: 10.1016/0890-5401(92)90008-4. Crossref, Web of Science, Google Scholar
Flemming Nielson and Hanne Riis Nielson , Electronic Notes in Theoretical Computer Science 10 , eds. Andrew Pitts , Andrew Gordon and Carolyn Talcott ( Elsevier Science Publishers , 2000 ) . Google Scholar
Flemming Nielson, Hanne Riis Nielson and Renè Rydhof Hansen, Theoretical Computer Science 283(1), 381 (2002), DOI: 10.1016/S0304-3975(01)00140-2. Crossref, Web of Science, Google Scholar
Gordon Plotkin, SIAM Journal on Computing 5(3), 452 (1976), DOI: 10.1137/0205035. Crossref, Web of Science, Google Scholar
P. Y. A. Ryan and S. A. Schnieder , Modelling and Analysis of Security Protocols ( Addison-Weslley , 2001 ) . Google Scholar
Davide Sangiorgi and David Walker , The Pi-Calculus - A Theory of Mobile Processes ( Cambridge University Press , Cambridge, UK , 2001 ) . Google Scholar
Ian Stark, A fully abstract domain model for the π-calculus, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (IEEE Computer Society, 1996) pp. 36–42. Google Scholar
Alan M. Turing, Proceedings of the London Mathematical Society 42, 230 (1937). Web of Science, Google Scholar
CCITT Rec. X.509. ISO/IEC 9594–8:1994 information technology - open systems interconnection - the directory: Authentication framework, 1994 . Google Scholar