Abstract
We advocate here the use of two authentication primitives we recently propose in a calculus for distributed systems, as a further instrument for programmers interested in authentication. These primitives offer a way of abstracting from various specifications of authentication and obtaining idealized protocols “secure by construction”. We can consequently prove that a cryptographic protocol is the correct implementation of the corresponding abstract protocol; when the proof fails, reasoning on the abstract specification may drive to the correct implementation.
Work partially supported by EU-project DEGAS (IST-2001-32072) and by Progetto MIUR Metodi Formali per la Sicurezza (MEFISTO).
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
Abadi, M., Gordon, A.D.: A Calculus for Cryptographic Protocols: The Spi Calculus. Information and Computation 148(1), 1–70 (1999)
Abadi, M.: Secrecy by Typing In Security protocols. Journal of the ACM 5(46), 18–36 (1999)
Abadi, M., Fournet, C., Gonthier, G.: Authentication Primitives and their compilation. In: Proceedings of Principles of Programming Languages (POPL 2000), pp. 302–315. ACM Press, New York (2000)
Bodei, C., Degano, P., Focardi, R., Priami, C.: Primitives for Authentication in Process Algebras. Theoretical Computer Science 283(2), 271–304 (2002)
Bodei, C., Degano, P., Priami, C.: Names of the π-Calculus Agents Handled Locally. Theoretical Computer Science 253(2), 155–184 (2001)
Bodei, C., Degano, P., Focardi, R., Priami, C.: Authentication via Localized Names. In: Proceedings of the 12th Computer Security Foundation Workshop (CSFW12), pp. 98–110. IEEE Press, Los Alamitos (1999)
Boreale, M., De Nicola, R.: Testing equivalence for mobile processes. Information and Computation 120(2), 279–303 (1995)
Burrows, M., Abadi, M., Needham, R.: A Logic of Authentication. ACM Transactions on Computer Systems, 18–36 (February 1990)
National Bureau of Standards. Data Encryption Standard (DES). FIPS Publication 46 (1977)
De Nicola, R., Hennessy, M.C.B.: Testing equivalence for processes. Theoretical Computer Science 34, 83–133 (1984)
Durante, A., Focardi, R., Gorrieri, R.: A Compiler for Analysing Cryptographic Protocols Using Non-Interference. ACM Transactions on Software Engineering and Methodology 9(4), 488–528 (2000)
Degano, P., Priami, C.: Enhanced Operational Semantics: A Tool for Describing and Analysing Concurrent Systems. To appear in ACM Computing Surveys
Degano, P., Priami, C.: Non Interleaving Semantics for Mobile Processes. Theoretical Computer Science 216, 237–270 (1999)
Fábrega, F.J.T., Herzog, J.C., Guttman, J.D.: Strand spaces: Why is a security protocol correct? In: Proceedings of the 1998 IEEE Symposium on Security and Privacy, pp. 160–171. IEEE Press, Los Alamitos (1998)
Focardi, R., Gorrieri, R., Martinelli, F.: Message authentication through non-interference. In: Rus, T. (ed.) AMAST 2000. LNCS, vol. 1816, pp. 258–272. Springer, Heidelberg (2000)
Focardi, R., Gorrieri, R., Martinelli, F.: Non Interference for the Analysis of Cryptographic Protocols. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, p. 354. Springer, Heidelberg (2000)
Focardi, R., Martinelli, F.: A Uniform Approach for the Definition of Security Properties. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 794–813. Springer, Heidelberg (1999)
Focardi, R., Ghelli, A., Gorrieri, R.: Using Non Interference for the Analysis of Security Protocols. In: Proceedings of the DIMACS Workshop on Design and Formal Verification of Security Protocols, DIMACS Center, Rutgers University (1997)
Thayer, R., Doraswamy, N., Glenn, R.: RFC 2411: IP security document roadmap (November 1998)
International Organization for Standardization. Information technology – Security techniques – Entity authentication mechanism; Part 1: General model. ISO/IEC 9798–1, Second Edition (September 1991)
Lowe, G.: A Hierarchy of Authentication Specification. In: Proceedings of the 10th Computer Security Foundation Workshop (CSFW10). IEEE Press, Los Alamitos (1997)
Lowe, G.: Breaking and Fixing the Needham-Schroeder Public-key Protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 146–166. Springer, Heidelberg (1996)
Kemmerer, R., Meadows, C., Millen, J.: Three systems for cryptographic protocol analysis. J. Cryptology 7(2), 79–130 (1994)
Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes (I and II). Information and Computation 100(1), 1–77 (1992)
Mitchell, J.C., Mitchell, M., Stern, U.: Automated Analysis of Cryptographic Protocols Using Murφ. In: Proceedings of the 1997 IEEE Symposium on Research in Security and Privacy, pp. 141–153. IEEE Computer Society Press, Los Alamitos (1997)
Sangiorgi, D.: Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD Thesis. University of Edinburgh (1992)
Schneider, S.: Verifying authentication protocols in CSP. IEEE Transactions on Software Engineering 24(9) (September 1998)
Schneier, B.: Applied Cryptography, 2nd edn. John Wiley & Sons, Inc., Chichester (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bodei, C., Degano, P., Focardi, R., Priami, C. (2003). Authentication Primitives for Protocol Specifications. In: Malyshkin, V.E. (eds) Parallel Computing Technologies. PaCT 2003. Lecture Notes in Computer Science, vol 2763. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45145-7_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-45145-7_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40673-0
Online ISBN: 978-3-540-45145-7
eBook Packages: Springer Book Archive