Abstract
We consider the problem of implementing a security protocol in such a manner that secrecy of sensitive data is not jeopardized. Implementation is assumed to take place in the context of an API that provides standard cryptography and communication services. Given a dependency specification, stating how API methods can produce and consume secret information, we propose an information flow property based on the idea of invariance under perturbation, relating observable changes in output to corresponding changes in input. Besides the information flowcondition itself, the main contributions of the paper are results relating the admissibility property to a direct flow property in the special case of programs which branch on secrets only in cases permitted by the dependency rules. These results are used to derive an unwinding-like theorem, reducing a behavioral correctness check (strong bisimulation) to an invariant.
This material is based uponwork partially supported by the European Office ofAerospace Research and Development, Air Force Office of Scientific Research, Air Force Research Laboratory, under Contract No. F61775-01-C0006, and by the European IST project VerifiCard.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
M. Abadi and A. D. Gordon. A Bisimulation Method for Cryptographic Protocols. Nordic Journal of Computing, 5(4):267–303, 1998.
M. Bellare, J. Garay, R. Hauser, A. Herzberg, H. Krawczyk, M. Steiner, G. Tsudik, and M. Waidner. iKP-a family of secure electronic payment protocols. In First USENIX Workshop on Electronic Commerce, May 1995.
E. S. Cohen. Information Transmission in Sequential Programs. In R. A. DeMillo, D. P. Dobkin, A. K. Jones, and R. J. Lipton, editors, Foundations of Secure Computation, pages 297–335. Academic Press, 1978.
M. Dam and P. Giambiagi. Confidentiality for Mobile Code: The case of a simple payment protocol. In Proceedings of 13th IEEE Computer Security Foundations Workshop, 2000.
R. Focardi and R. Gorrieri. A Classification of Security Properties for Process Algebras. Journal of Computer Security, 3(1):5–33, 1995.
P. Giambiagi and M. Dam. On the Secure Implementation of Security Protocols. Full version, available from http://www.sics.se/fdt/publications/gd03-secImpl-full.pdf, 2003.
A. W. Roscoe and M. H. Goldsmith. What is Intransitive Noninterference? In Proceedings of 12th IEEE Computer Security Foundations Workshop, 1999.
A. Sabelfeld and A. C. Myers. Language-Based Information-Flow Security. IEEE Journal on Selected Areas in Communications, 21(1), 2003.
A. Sabelfeld and D. Sands.APER Model of Secure Information Flowin Sequential Programs. Higher-Order and Symbolic Computation, 14(1), 2001.
D. Volpano. Secure Introduction of One-Way Functions. In Proceedings of 13th IEEE Computer Security Foundations Workshop, 2000.
D. Volpano, G. Smith, and C. Irvine. A Sound Type System for Secure FlowAnalysis. Journal of Computer Security, 4(3):167–187, 1996.
S. Zdancewic and A. Myers. Robust Declassification. In Proceedings of 14th IEEE Computer Security Foundations Workshop, 2001.
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
Giambiagi, P., Dam, M. (2003). On the Secure Implementation of Security Protocols. In: Degano, P. (eds) Programming Languages and Systems. ESOP 2003. Lecture Notes in Computer Science, vol 2618. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36575-3_11
Download citation
DOI: https://doi.org/10.1007/3-540-36575-3_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00886-6
Online ISBN: 978-3-540-36575-4
eBook Packages: Springer Book Archive