Abstract
Authentication is a slippery security property that has been formally defined only recently; among the recent definitions, a rather interesting one has been proposed for the spi-calculus in [1, 2]. On the other hand, in a recent paper [10], we have proved that many existing security properties can be seen uniformly as specific instances of a general scheme based on the idea of non interference. The purpose of this paper is to show that, under reasonable assumptions, also spi-authentication can be recast in this general framework, by showing that it is equivalent to the non interference property called NDC of [8, 9].
Work partially supported by MURST Progetto “Certificazione automatica di programmi mediante interpretazione astratta” and Progetto “Teoria della Concorrenza, Linguaggi di Ordine Superiore e Strutture di Tipi”; CNR Progetto “Modelli e Metodi per la Matematica e l’Ingegneria”; CSP Progetto “ISA: Isp Secured trAnsactions”.
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
M. Abadi and A. D. Gordon. Reasoning about cryptographic protocols in the spi calculus. In Proc. of CONCUR’97, pages 59–73. LNCS 1243, 1997.
M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi calculus. Information and Computation, 148(1):1–70, 1999.
M. Burrows, M. Abadi, and R. Needham. “A Logic of Authentication”. Proc. of the Royal Society of London, 426:233–271, 1989.
C. Bodei, P. Degano, R. Focardi, and C. Priami. Authentication via localized names. In Proc. of CSFW’99, pages 98–110. IEEE press, 1999.
R. De Nicola and M. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34:83–133, 1984.
A. Durante, R. Focardi, and R. Gorrieri. CVS: A compiler for the analysis of cryptographic protocols. In Proc. of CSFW’99, pages 203–212. IEEE press, 1999.
R. Focardi, A. Ghelli, and R. Gorrieri. Using non interference for the analysis of security protocols. In Proc. of DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997.
R. Focardi and R. Gorrieri. A classification of security properties for process algebras. Journal of Computer Security, 3(1):5–33, 1994/1995.
R. Focardi and R. Gorrieri. The compositional security checker: A tool for the verification of information flow security properties. IEEE Transactions on Software Engineering, 23(9):550–571, 1997.
R. Focardi and F. Martinelli. A uniform approach for the definition of security properties. In Proc. of World Congress on Formal Methods (FM’99), pages 794–813. Springer, LNCS 1708, 1999.
J. A. Goguen and J. Meseguer. Security policy and security models. In Proc. of the 1982 Symposium on Security and Privacy, pages 11–20. IEEE Press, 1982.
D. Gollmann. What do we mean by entity authentication? In Proc. of Symposium in Research in Security and Privacy, pages 46–54. IEEE Press, 1996.
G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In Proc. of TACAS’96, pages 146–166. LNCS 1055, 1996.
G. Lowe. A hierarchy of authentication specification. In Proc. of the 10th Computer Security Foundation Workshop, pages 31–43. IEEE press, 1997.
D. Marchignoli and F. Martinelli. Automatic verification of cryptographic protocols through compositional analysis techniques. In Proc. of TACAS’99, volume 1579 of LNCS, pages 148–163, 1999.
W. Marrero, E. Clarke, and S. Jha. A model checker for authentication protocols. In Proc. of DIMACS Workshop on Design and Formal Verification of Security Protocols. Rutgers University, Sep. 1997.
F. Martinelli. Languages for description and analysis of authentication protocols. In Proc. of ICTCS’98, pages 304–315. World Scientific, 1998.
F. Martinelli. Partial model checking and theorem proving for ensuring security properties. In Proc. of CSFW’98, pages 44–52. IEEE press, 1998.
R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
P. Y. A. Ryan and S. Schneider. Process algebra and non-interference. In Proc. of CSFW’99, pages 214–227. IEEE press, 1999.
S. Schneider. Formal analysis of a non-repudiation protocol. In Proc. of CSFW’98, pages 54–65. IEEE Press, 1998.
S. Schneider. Verifying authentication protocols in CSP. IEEE Transactions on Software Engineering, 24(9), September 1998.
J. T. Wittbold and D. M. Johnson. “Information Flow in Nondeterministic Systems”. In Proc. of the 1990 IEEE Symposium on Research in Security and Privacy, pages 144–161. IEEE Computer Society Press, 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Focardi, R., Gorrieri, R., Martinelli, F. (2000). Message Authentication through Non Interference . In: Rus, T. (eds) Algebraic Methodology and Software Technology. AMAST 2000. Lecture Notes in Computer Science, vol 1816. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45499-3_20
Download citation
DOI: https://doi.org/10.1007/3-540-45499-3_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67530-3
Online ISBN: 978-3-540-45499-1
eBook Packages: Springer Book Archive