Abstract
Modularity has been seen to be very useful in system development. Unfortunately, many security properties proposed in the literature are not composable (in contrast to other system properties), which is required to reason about them in a modular way. We present work supporting modular development of secure systems by showing a standard notion of secrecy to be composable wrt. the standard composition in the specification framework Focus (extended with cryptographic primitives). Additionally, the property is preserved under the standard refinement. We consider more fine-grained conditions useful in modular verification of secrecy. Keywords. Network security, cryptographic protocols, secrecy, modularity, composability, refinement, formal specification, computer aided software engineering.
This work was supported by the Studienstiftung des deutschen Volkes and the Computing Laboratory.
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.
Similar content being viewed by others
References
Abadi, M.: Security protocols and their properties. In: Bauer, F. and Stein-brueggen, R., (eds.): Foundations of Secure Computation. IOS Press, 2000
Abadi, M. and Gordon, A.D.: A calculus for cryptographic protocols: The spificalculus. Information and Computation, 148(1):1–70 (January 1999)
Abadi, M. and Jan Jürjens: Formal eavesdropping and its computational interpretation, 2000. Submitted
Apostolopoulos, V., Peris, V., and Saha, D.: Transport layer security: How much does it really cost? In: Conference on Computer Communications (IEEE Infocom). New York (March 1999)
Broy, M. and Stølen, K.: Specification and Development of Interactive Systems. Springer (2000) (to be published)
Cardelli, L., Ghelli, G., and Gordon, A.: Secrecy and group creation. In: CONCUR 2000. (2000) 365–379
Dolev, D. and Yao, A.: On the security of public key protocols. IEEE Transactions on Information Theory, 29(2):198–208 (1983)
Huber, F., Molterer, S., Rausch, A., Schätz, B., Sihling, M., and Slotosch, O.: Tool supported Specification and Simulation of Distributed Systems. In: International Symposium on Software Engineering for Parallel and Distributed Systems. (1998) 155–164
Jan Jürjens: Secure information flow for concurrent processes. In: CONCUR 2000 (11th International Conference on Concurrency Theory), Vol. 1877 of LNCS. Pennsylvania, Springer (2000) 395–409
Jan Jürjens: Object-oriented modelling of audit security for smart-card payment schemes. In: Paradinas, P., (ed.): IFIP/SEC 2001 — 16th International Conference on Information Security, Paris, (11–13 June 2001) Kluwer
Jan Jürjens: Secrecy-preserving refinement. In: Formal Methods Europe (International Symposium), LNCS. Springer (2001)
Jan Jürjens: Towards development of secure systems using UML. In: Huffmann, H., (ed.): Fundamental Approaches to Software Engineering (FASE/ETAPS, International Conference), LNCS. Springer (2001)
Jan Jürjens and Guido Wimmel: Specification-based testing of firewalls. Submitted (2001)
Lotz, V.: Threat scenarios as a means to formally develop secure systems. Journal of Computer Security 5 (1997) 31–67
McLean, J.: A general theory of composition for a class of “possibilistic” properties. IEEE Transactions on Software Engineering, 22(1):53–67 (1996)
Meadows, C.: Using traces based on procedure calls to reason about composability. In: IEEE Symposium on Security and Privacy. (1992)
Meadows, C.: Applying the dependability paradigm to computer security. In: New Security Paradigms Workshop. (1995)
Meadows, C.: Formal verification of cryptographic protocols: A survey. In: Asiacrypt 96. (1996)
Meadows, C.: Open issues in formal methods for cryptographic protocol analysis. In: DISCEX. IEEE (2000)
Millen, J.: Hookup security for synchronous machines. In: Computer Security Foundations Workshop III. IEEE Computer Society (1990)
Pitzmann, B.: Higher cryptographic protocols, 1998. Lecture Notes, Universität des Saarlandes
Pohl, H. and Weck G., (eds.): Internationale Sicherheitskriterien. Oldenbourg Verlag (1993)
Ryan, P. and Schneider, S.: Process algebra and non-interference. In: IEEE Computer Security Foundations Workshop. (1999)
Sewell, P. and Vitek, J.: Secure composition of untrusted code: Wrappers and causality types. In: CSFW. (2000)
Varadharajan, V.: Hook-up property for information flow secure nets. In: CSFW. (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jürjens, J. (2001). Composability of Secrecy. In: Gorodetski, V.I., Skormin, V.A., Popyack, L.J. (eds) Information Assurance in Computer Networks. MMM-ACNS 2001. Lecture Notes in Computer Science, vol 2052. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45116-1_6
Download citation
DOI: https://doi.org/10.1007/3-540-45116-1_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42103-0
Online ISBN: 978-3-540-45116-7
eBook Packages: Springer Book Archive