Abstract
We develop principles and rules for achieving secrecy properties in security protocols. Our approach is based on traditional classification techniques, and extends those techniques to handle concurrent processes that use shared-key cryptography. The rules have the form of typing rules for a basic concurrent language with cryptographic primitives, the spi calculus. They guarantee that, if a protocol typechecks, then it does not leak its secret inputs.
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi calculus. In Proceedings of the Fourth ACM Conference on Computer and Communications Security, pages 36–47, 1997.
M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi calculus. Technical Report 414, University of Cambridge Computer Laboratory, January 1997. Extended version of both [AG97a] and [AG97c].
M. Abadi and A. D. Gordon. Reasoning about cryptographic protocols in the spi calculus. To appear in the Proceedings of CONCUR'97, 1997.
M. Abadi and R. Needham. Prudent engineering practice for cryptographic protocols. IEEE Transactions on Software Engineering, 22(1):6–15, January 1996.
M. Burrows, M. Abadi, and R. M. Needham. A logic of authentication. Proceedings of the Royal Society of London A, 426:233–271, 1989. A preliminary version appeared as Digital Equipment Corporation Systems Research Center report No. 39, February 1989.
M. Boreale and R. De Nicola. Testing equivalence for mobile processes. Information and Computation, 120(2):279–303, August 1995.
M. Bellare and P. Rogaway. Provably secure session key distribution: The three party case. In Proceedings of the 27th Annual ACM Symposium on Theory of Computing, 1995.
D. E. Denning. Cryptography and Data Security. Addison-Wesley, Reading, Mass., 1982.
Data encryption standard. Fed. Inform. Processing Standards Pub. 46, National Bureau of Standards, Washington DC, January 1977.
R. De Nicola and M. C. B. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34:83–133, 1984.
M. Gasser. Building a Secure Computer System. Van Nostrand Reinhold Company Inc., New York, 1988.
T. Lindholm and F. Yellin. The Java Virtual Machine Specification. Addison-Wesley, 1996.
R. Milner. The polyadic π-calculus: a tutorial. Technical Report ECSLFCS-91-180, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, UK, October 1991. Appeared in Logic and Algebra of Specification, F. L. Bauer, W. Brauer, and H. Schwichtenberg, eds., Springer-Verlag, 1993.
R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, parts I and II. Information and Computation, pages 1–40 and 41–77, September 1992.
G. Necula. Proof-carrying code. In Proceedings of the 24th ACM Symposium on Principles of Programming Languages, pages 106–119, 1997.
R. M. Needham and M. D. Schroeder. Using encryption for authentication in large networks of computers. Communications of the ACM, 21(12):993–999, December 1978.
B. Pierce and D. Sangiorgi. Typing and subtyping for mobile processes. Mathematical Structures in Computer Science, 6(5):409–453, October 1996.
B. Schneier. Applied Cryptography: Protocols, Algorithms, and Source Code in C. John Wiley & Sons, Inc., second edition, 1996.
D. Volpano, G. Sinith, and C. Irvine. A sound type system for secure flow analysis. Journal of Computer Security, 4(3):1–21, 1996.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abadi, M. (1997). Secrecy by typing in security protocols. In: Abadi, M., Ito, T. (eds) Theoretical Aspects of Computer Software. TACS 1997. Lecture Notes in Computer Science, vol 1281. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014571
Download citation
DOI: https://doi.org/10.1007/BFb0014571
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63388-4
Online ISBN: 978-3-540-69530-1
eBook Packages: Springer Book Archive