Message Authentication through Non Interference

  • Riccardo Focardi
  • Roberto Gorrieri
  • Fabio Martinelli
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1816)


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].


Authentication Protocol Security Protocol Hostile Environment Security Property Message Authentication 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    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.Google Scholar
  2. [2]
    M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi calculus. Information and Computation, 148(1):1–70, 1999.zbMATHCrossRefMathSciNetGoogle Scholar
  3. [3]
    M. Burrows, M. Abadi, and R. Needham. “A Logic of Authentication”. Proc. of the Royal Society of London, 426:233–271, 1989.zbMATHMathSciNetCrossRefGoogle Scholar
  4. [4]
    C. Bodei, P. Degano, R. Focardi, and C. Priami. Authentication via localized names. In Proc. of CSFW’99, pages 98–110. IEEE press, 1999.Google Scholar
  5. [5]
    R. De Nicola and M. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34:83–133, 1984.zbMATHCrossRefMathSciNetGoogle Scholar
  6. [6]
    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.Google Scholar
  7. [7]
    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.Google Scholar
  8. [8]
    R. Focardi and R. Gorrieri. A classification of security properties for process algebras. Journal of Computer Security, 3(1):5–33, 1994/1995.Google Scholar
  9. [9]
    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.CrossRefGoogle Scholar
  10. [10]
    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.Google Scholar
  11. [11]
    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.Google Scholar
  12. [12]
    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.Google Scholar
  13. [13]
    G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In Proc. of TACAS’96, pages 146–166. LNCS 1055, 1996.Google Scholar
  14. [14]
    G. Lowe. A hierarchy of authentication specification. In Proc. of the 10th Computer Security Foundation Workshop, pages 31–43. IEEE press, 1997.Google Scholar
  15. [15]
    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.Google Scholar
  16. [16]
    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.Google Scholar
  17. [17]
    F. Martinelli. Languages for description and analysis of authentication protocols. In Proc. of ICTCS’98, pages 304–315. World Scientific, 1998.Google Scholar
  18. [18]
    F. Martinelli. Partial model checking and theorem proving for ensuring security properties. In Proc. of CSFW’98, pages 44–52. IEEE press, 1998.Google Scholar
  19. [19]
    R. Milner. Communication and Concurrency. Prentice-Hall, 1989.Google Scholar
  20. [20]
    P. Y. A. Ryan and S. Schneider. Process algebra and non-interference. In Proc. of CSFW’99, pages 214–227. IEEE press, 1999.Google Scholar
  21. [21]
    S. Schneider. Formal analysis of a non-repudiation protocol. In Proc. of CSFW’98, pages 54–65. IEEE Press, 1998.Google Scholar
  22. [22]
    S. Schneider. Verifying authentication protocols in CSP. IEEE Transactions on Software Engineering, 24(9), September 1998.Google Scholar
  23. [23]
    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.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Riccardo Focardi
    • 1
  • Roberto Gorrieri
    • 2
  • Fabio Martinelli
    • 3
  1. 1.Dipartimento di InformaticaUniversità Ca’ Foscari di VeneziaItaly
  2. 2.Dipartimento di Scienze dell’InformazioneUniversità di BolognaItaly
  3. 3.Istituto per le Applicazioni Telematiche C.N.R.PisaItaly

Personalised recommendations