Abstract
In this paper, we introduce a framework composed of a syntax and its compositional Petri net semantics, for the specification and verification of properties (like authentication) of security protocols. The protocol agents (e.g., an initiator, a responder, a server, a trusted third party, ...) are formalized as roles, each of them having a predefined behavior depending on their global and also local knowledge (including for instance public, private and shared keys), and may interact in a potentially hostile environment.
The main characteristics of our framework, is that it makes explicit, structured and formal, the usually implicit information necessary to analyse the protocol, for instance the public and private context of execution. The roles and the environment are expressed using SPL processes and compositionally translated into high-level Petri nets, while the context specifying the global and local knowledge of the participants in the protocol is used to generate the corresponding initial marking (with respect to the studied property). Finally, this representation is used to analyse the protocol properties, applying techniques of simulation and model-checking on Petri nets. The complete approach is illustrated on the case study of the Kao-Chow authentication protocol.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Armando, A., et al.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005)
Abadi, M., Blanchet, B.: Analyzing security protocols with secrecy types and logic programs. Journal of the ACM 52(1) (2005)
Abadi, M., Gordon, A.: A calculus for cryptographic protocols. In: The Spi calculus. ACM Conference on Computers and Communication Security. ACM Press, New York (1997)
Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). Journal of Cryptology 15(2) (2002)
Al-Azzoni, I., Down, D.G., Khedri, R.: Modelling and verification of cryptographic protocols using coloured Petri nets and Design/CPN. Nordic Journal of Computing 12(3) (2005)
Best, E., Devillers, R., Koutny, M.: Petri Net Algebra. In: EATCS Monographs on TCS. Springer, Heidelberg (2001)
Best, E., Fra̧czak, W., Hopkins, R.P., Klaudel, H., Pelz, E.: M-nets: an algebra of high level Petri nets, with an application to the semantics of concurrent programming languages. Acta Informatica 35 (1998)
Blanchet, B.: A computationally sound mechanized prover for security protocols. In: IEEE Symposium on Security and Privacy (2006)
Bouroulet, R., Klaudel, H., Pelz, E.: A semantics of Security Protocol Language (SPL) using a class of composable high-level Petri nets. In: ACSD 2004. IEEE Computer Society, Los Alamitos (2004)
Bouroulet, R., Klaudel, H., Pelz, E.: Modelling and verification of authentication using enhanced net semantics of SPL (Security Protocol Language). In: ACSD 2006. IEEE Computer Society, Los Alamitos (2006)
Christensen, S., Hansen, N.D.: Coloured Petri Nets Extended with Place Capacities, Test Arcs and Inhibitor Arcs. In: Ajmone Marsan, M. (ed.) ICATPN 1993. LNCS, vol. 691. Springer, Heidelberg (1993)
Clark, J., Jacob, J.: A survey of authentication protocol literature: Version 1.0 (1997), http://www.cs.york.ac.uk/jac/papers/drareview.ps.gz
Cortier, V., Warinschi, B.: Computationally sound, automated proofs for security protocols. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 157–171. Springer, Heidelberg (2005)
Crazzolara, F., Winskel, G.: Events in security protocols. In: ACM Conf on Computer and Communications Security. ACM Press, New York (2001)
Denker, G., Millen, J.: CAPSL Integrated Protocol Environment. In: DISCEX 2000. IEEE Computer Society, Los Alamitos (2000)
Dill, D.L., Drexler, A.J., Hu, A.J., Han Yang, C.: Protocol Verification as a Hardware Design Aid. In: IEEE International Conference on Computer Design: VLSI in Computers and Processors (1992)
Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory IT-29 12 (1983)
Donovan, B., Norris, P., Lowe, G.: Analyzing a library of security protocols using Casper and FDR. In: Workshop on Formal Methods and Security Protocols (1999)
Evangelista, S.: High Level Petri Nets Analysis with Helena. In: Ciardo, G., Darondeau, P. (eds.) ICATPN 2005. LNCS, vol. 3536, pp. 455–464. Springer, Heidelberg (2005), http://helena.cnam.fr/
Gordon, A., Jeffrey, A.: Authenticity by Typing for Security Protocols. In: IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos (2001)
Kao, I.-L., Chow, R.: An efficient and secure authentication protocol using uncertified keys. In: Operating Systems Review, vol. 29(3), ACM Press, New York (1995)
Kremer, S., Raskin, J.-F.: A Game-Based Verification of Non-Repudiation and Fair Exchange Protocols. Journal of Computer Security 11(3) (2003)
Lowe, G.: An attack on the Needham-Schroeder public key authentication protocol. Information Processing Letters 56(3) (1995)
Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using (FDR). In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055. Springer, Heidelberg (1996)
Meadows, C.: Formal Methods for Cryptographic Protocol Analysis: Emerging Issues and Trends. IEEE Journal on Selected Areas in Communication 21(1) (2003)
Milner, R.: Communicating and mobile systems: The π-calculus. Cambridge University Press, Cambridge (1999)
Mitchell, J.C., Mitchell, M., Stern, U.: Automated Analysis of Cryptographic Protocols Using Murϕ. In: IEEE Symposium on Security and Privacy. IEEE Computer Society Press, Los Alamitos (1997)
Needham, R.M., Schroeder, M.D.: Using Encrypton for Authentication in Large Networks of Computers. Comm. of the ACM 21(12) (1978)
Nieh, B.B., Tavares, S.E.: Modelling and Analyzing Cryptographic Protocols Using Petri Nets. In: Zheng, Y., Seberry, J. (eds.) AUSCRYPT 1992. LNCS, vol. 718. Springer, Heidelberg (1993)
Rivest, R.L., Shamir, A., Adleman, L.: A method for obtaining digital signatures and public-key cryptosystem. Comm. of the ACM 21(2) (1978)
Schneier, B.: Applied Cryptography. Wiley, Chichester (1996)
Thayer, F., Herzog, J.C., Guttman, J.D.: Strand Spaces: Why is a Security Protocol Correct? In: IEEE Symposium on Security and Privacy (1998)
Song, D.: Athena: A new efficient automatic checker for security protocol analysis. In: CSFW 1999. IEEE Computer Society Press, Los Alamitos (1999)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bouroulet, R., Devillers, R., Klaudel, H., Pelz, E., Pommereau, F. (2008). Modeling and Analysis of Security Protocols Using Role Based Specifications and Petri Nets. In: van Hee, K.M., Valk, R. (eds) Applications and Theory of Petri Nets. PETRI NETS 2008. Lecture Notes in Computer Science, vol 5062. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68746-7_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-68746-7_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68745-0
Online ISBN: 978-3-540-68746-7
eBook Packages: Computer ScienceComputer Science (R0)