×

Typing correspondence assertions for communication protocols. (English) Zbl 1023.68006

Summary: Woo and Lam propose correspondence assertions for specifying authenticity properties of security protocols. Prior work on checking correspondence assertions depends on model-checking and is limited to finite-state systems. We propose a dependent type and effect system for checking correspondence assertions. Since it is based on type-checking, our method is not limited to finite-state systems. This paper presents our system in the simple and general setting of the \(pi\)-calculus. We show how to type-check correctness properties of example communication protocols based on secure channels. In a related paper, we extend our system to the more complex and specific setting of checking cryptographic protocols based on encrypted messages sent over insecure channels.

MSC:

68M12 Network protocols
68P25 Data encryption (aspects in computer science)

Software:

Automath; PIPER
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abadi, M.; Gordon, A. D., A calculus for cryptographic protocolsthe spi calculus, Inform., Comput., 148, 1-70 (1999) · Zbl 0924.68073
[2] Barendregt, H., Lambda calculi with types, (Abramsky, S.; Gabbay, D. M.; Maibaum, T. S.E., Handbook of Logic in Computer Science, Vol. II (1992), Oxford University Press: Oxford University Press Oxford) · Zbl 0445.03005
[3] Berry, G.; Boudol, G., The chemical abstract machine, Theoret. Comput. Sci., 96, 1, 217-248 (1992) · Zbl 0747.68013
[4] S. Chaki, S.R. Rajamani, J. Rehof, Types as models: model checking message-passing programs, in: 29th ACM Symp. on Principles of Programming Languages (POPL’02), 2002, pp. 45-57.; S. Chaki, S.R. Rajamani, J. Rehof, Types as models: model checking message-passing programs, in: 29th ACM Symp. on Principles of Programming Languages (POPL’02), 2002, pp. 45-57. · Zbl 1323.68365
[5] E. Clarke, W. Marrero, Using formal methods for analyzing security. Available at http://www.cs.cmu.edu/ marrero/abstract.html; E. Clarke, W. Marrero, Using formal methods for analyzing security. Available at http://www.cs.cmu.edu/ marrero/abstract.html
[6] K. Crary, D. Walker, G. Morrisett, Typed memory management in a calculus of capabilities, in: A. Aiken (Ed.), 26th ACM Symp. on Principles of Programming Languages (POPL’99), 1999, pp. 262-275.; K. Crary, D. Walker, G. Morrisett, Typed memory management in a calculus of capabilities, in: A. Aiken (Ed.), 26th ACM Symp. on Principles of Programming Languages (POPL’99), 1999, pp. 262-275.
[7] Dal Zilio, S.; Gordon, A. D., Region analysis and a \(π\)-calculus with groups, J. Funct. Programm., 12, 229-292 (2002) · Zbl 1005.68041
[8] Flanagan, C.; Abadi, M., Object types against races, (Baeten, J. C.M.; Mauw, S., CONCUR’99: Concurrency Theory. CONCUR’99: Concurrency Theory, Lectures Notes in Computer Science, Vol. 1664 (1999), Springer: Springer Berlin), 288-303
[9] A.D. Gordon, A. Jeffrey, Authenticity by typing for security protocols, in: 14th IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, Silver Spring, MD, 2001, pp. 145-159. An extended version appears as Microsoft Research Technical Report MSR-TR-2001-49, May 2001.; A.D. Gordon, A. Jeffrey, Authenticity by typing for security protocols, in: 14th IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, Silver Spring, MD, 2001, pp. 145-159. An extended version appears as Microsoft Research Technical Report MSR-TR-2001-49, May 2001.
[10] A.D. Gordon, A. Jeffrey, Typing correspondence assertions for communication protocols, in: Mathematical Foundations of Programming Semantics 17, Electronic Notes in Theoretical Computer Science, Vol. 45, Elsevier, Amsterdam, 2001, pp. 99-120, Preliminary Proceedings, BRICS Notes Series NS-01-2, BRICS, University of Aarhus, May 2001. An extended version appears as Microsoft Research Technical Report MSR-TR-2001-48, May 2001.; A.D. Gordon, A. Jeffrey, Typing correspondence assertions for communication protocols, in: Mathematical Foundations of Programming Semantics 17, Electronic Notes in Theoretical Computer Science, Vol. 45, Elsevier, Amsterdam, 2001, pp. 99-120, Preliminary Proceedings, BRICS Notes Series NS-01-2, BRICS, University of Aarhus, May 2001. An extended version appears as Microsoft Research Technical Report MSR-TR-2001-48, May 2001.
[11] A.D. Gordon, A. Jeffrey, Types and effects for asymmetric cryptographic protocols, in: 15th IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, Silver Spring, MD, 2002, to appear.; A.D. Gordon, A. Jeffrey, Types and effects for asymmetric cryptographic protocols, in: 15th IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, Silver Spring, MD, 2002, to appear.
[12] D.K. Gifford, J.M. Lucassen, Integrating functional and imperative programming, in: ACM Conference on Lisp and Functional Programming, 1986, pp. 28-38.; D.K. Gifford, J.M. Lucassen, Integrating functional and imperative programming, in: ACM Conference on Lisp and Functional Programming, 1986, pp. 28-38.
[13] M. Hennessy, J. Riely, Resource access control in systems of mobile agents, in: Third Internat. Workshop on High-Level Concurrent Languages (HLCL’98), Electronic Notes in Theoretical Computer Science, Vol. 16(3), Elsevier, Amsterdam, 1998.; M. Hennessy, J. Riely, Resource access control in systems of mobile agents, in: Third Internat. Workshop on High-Level Concurrent Languages (HLCL’98), Electronic Notes in Theoretical Computer Science, Vol. 16(3), Elsevier, Amsterdam, 1998. · Zbl 0917.68047
[14] Honda, K.; Vasconcelos, V.; Kubo, M., Language primitives and type discipline for structured communication-based programming, (European Symp. on Programming (ESOP’98). European Symp. on Programming (ESOP’98), Lectures Notes in Computer Science, Vol. 1381 (1998), Springer: Springer Berlin), 122-128
[15] Honda, K.; Vasconcelos, V.; Yoshida, N., Secure information flow as typed process behaviour, (European Symp. on Programming (ESOP’00). European Symp. on Programming (ESOP’00), Lectures Notes in Computer Science, Vol. 1782 (2000), Springer: Springer Berlin), 180-199 · Zbl 0960.68126
[16] A. Igarashi, N. Kobayashi, A generic type system for the pi calculus, in: 28th ACM Symp. on Principles of Programming Languages (POPL’01), 2001, pp. 128-141.; A. Igarashi, N. Kobayashi, A generic type system for the pi calculus, in: 28th ACM Symp. on Principles of Programming Languages (POPL’01), 2001, pp. 128-141. · Zbl 1323.68410
[17] Kobayashi, N., A partially deadlock-free typed process calculus, ACM Trans. Programm. Languages Syst., 20, 436-482 (1998)
[18] Lowe, G., A hierarchy of authentication specifications, (10th Computer Security Foundations Workshop (1995), IEEE Computer Society Press: IEEE Computer Society Press Silver Spring, MD), 31-43
[19] J.M. Lucassen, Types and effects, towards the integration of functional and imperative programming. Ph.D. Thesis, MIT Press, Cambridge, MA, 1987; Available as Technical Report MIT/LCS/TR-408, MIT Laboratory for Computer Science.; J.M. Lucassen, Types and effects, towards the integration of functional and imperative programming. Ph.D. Thesis, MIT Press, Cambridge, MA, 1987; Available as Technical Report MIT/LCS/TR-408, MIT Laboratory for Computer Science.
[20] W. Marrero, E.M. Clarke, S. Jha, Model checking for security protocols, in: DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997. Preliminary version appears as Technical Report TR-CMU-CS-97-139, Carnegie Mellon University, May 1997.; W. Marrero, E.M. Clarke, S. Jha, Model checking for security protocols, in: DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997. Preliminary version appears as Technical Report TR-CMU-CS-97-139, Carnegie Mellon University, May 1997.
[21] Milner, R., Communicating and Mobile Systems: the \(π\)-Calculus (1999), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0942.68002
[22] H.R. Nielson, F. Nielson, Higher-order concurrent programs with finite communication topology,in: 21st ACM Symp. on Principles of Programming Languages (POPL’94), 1994, pp. 84-97.; H.R. Nielson, F. Nielson, Higher-order concurrent programs with finite communication topology,in: 21st ACM Symp. on Principles of Programming Languages (POPL’94), 1994, pp. 84-97.
[23] Nielson, F.; Riis Nielson, H., From CML to process algebras, (CONCUR 93—Concurrency Theory. CONCUR 93—Concurrency Theory, Lecture Notes in Computer Science, Vol. 715 (1993), Springer: Springer Berlin), 493-508
[24] Nordström, B.; Petersson, K.; Smith, J., Programming in Martin-Löf’s Type Theory: An Introduction (1990), Oxford University Press: Oxford University Press Oxford · Zbl 0744.03029
[25] Pierce, B.; Sangiorgi, D., Typing and subtyping for mobile processes, Math. Struct. Comput. Sci., 6, 5, 409-454 (1996) · Zbl 0861.68030
[26] C. Skalka, S. Smith, Static enforcement of security with types, in: P. Wadler (Ed.), Internat. Conf. on Functional Programming (ICFP’00), 2000, pp. 34-45.; C. Skalka, S. Smith, Static enforcement of security with types, in: P. Wadler (Ed.), Internat. Conf. on Functional Programming (ICFP’00), 2000, pp. 34-45.
[27] Takeuchi, K.; Honda, K.; Kubo, M., An interaction-based language and its typing system, (Sixth European Conf. on Parallel Languages and Architecture (PARLE’94). Sixth European Conf. on Parallel Languages and Architecture (PARLE’94), Lecture Notes in Computer Science, Vol. 817 (1994), Springer: Springer Berlin), 398-413
[28] J.-P. Talpin, Aspects théoretiques et pratiques de l’inférence de types et d’effets, Thése de doctorat, Université Paris VI and Ecole des Mines de Paris, May 1993.; J.-P. Talpin, Aspects théoretiques et pratiques de l’inférence de types et d’effets, Thése de doctorat, Université Paris VI and Ecole des Mines de Paris, May 1993.
[29] Tofte, M.; Talpin, J.-P., Region-based memory management, Inform. Comput., 132, 2, 109-176 (1997) · Zbl 0876.68027
[30] T.Y.C. Woo, S.S. Lam, A semantic model for authentication protocols, in: IEEE Symp. on Security and Privacy, 1993, pp. 178-194.; T.Y.C. Woo, S.S. Lam, A semantic model for authentication protocols, in: IEEE Symp. on Security and Privacy, 1993, pp. 178-194.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.