Abstract
We consider compositional properties of reactive systems that are secure in a cryptographic sense. We follow the well-known simulatability approach of modern cryptography, i.e., the specification is an ideal system and a real system should in some sense simulate this ideal one. We show that if a system consists of a polynomial number of arbitrary ideal subsystems such that each of them has a secure implementation in the sense of blackbox simulatability, then one can securely replace all ideal subsystems with their respective secure counterparts without destroying the blackbox simulatability relation. We further prove our theorem for universal simulatability by showing that blackbox simulatability implies universal simulatability under reasonable assumptions. We show all our results with concrete security.
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
Abadi, M., Lamport, L.: Conjoining specifications. ACM Transactions on Programming Languages and Systems 17(3), 507–534 (1995)
Backes, M., Jacobi, C.: Cryptographically sound and machine-assisted verification of security protocols. In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol. 2607, pp. 675–686. Springer, Heidelberg (2003)
Backes, M., Pfitzmann, B.: Computational probabilistic non-interference. In: Gollmann, D., Karjoth, G., Waidner, M. (eds.) ESORICS 2002. LNCS, vol. 2502, pp. 1–23. Springer, Heidelberg (2002)
Backes, M., Pfitzmann, B.: Intransitive non-interference for cryptographic purposes. In: Proc. 24th IEEE Symposium on Security & Privacy, pp. 140–152 (2003)
Backes, M., Pfitzmann, B., Steiner, M., Waidner, M.: Polynomial fairness and liveness. In: Proc. 15th IEEE Computer Security Foundations Workshop (CSFW), pp. 160–174 (2002)
Beaver, D.: Secure multiparty protocols and zero knowledge proof systems tolerating a faulty minority. Journal of Cryptology 4(2), 75–122 (1991)
Bellare, M., Kilian, J., Rogaway, P.: The security of cipher block chaining. In: Desmedt, Y.G. (ed.) CRYPTO 1994. LNCS, vol. 839, pp. 341–358. Springer, Heidelberg (1994)
Bellare, M., Rogaway, P.: Optimal asymmetric encryption. In: De Santis, A. (ed.) EUROCRYPT 1994. LNCS, vol. 950, pp. 92–111. Springer, Heidelberg (1995)
Canetti, R.: Security and composition of multiparty cryptographic protocols. Journal of Cryptology 3(1), 143–202 (2000)
Canetti, R.: Universally composable security: A new paradigm for cryptographic protocols. In: Proc. 42nd IEEE Symposium on Foundations of Computer Science (FOCS), pp. 136–145 (2001); Extended version in Cryptology ePrint Archive, Report 2000/67, http://eprint.iacr.org/
Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: Secure protocol composition (extended abstract). In: Proc. 1st ACM Workshop on Formal Methods in Security Engineering (FMSE), pp. 11–23 (2003)
Goldreich, O.: Foundations of Cryptography: Basic Tools. Cambridge University Press, Cambridge (2001)
Goldreich, O., Micali, S., Wigderson, A.: How to play any mental game – or – a completeness theorem for protocols with honest majority. In: Proc. 19th Annual ACM Symposium on Theory of Computing (STOC), pp. 218–229 (1987)
Goldwasser, S., Levin, L.: Fair computation of general functions in presence of immoral majority. In: Menezes, A., Vanstone, S.A. (eds.) CRYPTO 1990. LNCS, vol. 537, pp. 77–93. Springer, Heidelberg (1991)
Goldwasser, S., Micali, S.: Probabilistic encryption. Journal of Computer and System Sciences 28, 270–299 (1984)
Hirt, M., Maurer, U.: Player simulation and general adversary structures in perfect multiparty computation. Journal of Cryptology 13(1), 31–60 (2000)
Hoare, C.A.R.: Communicating Sequential Processes. International Series in Computer Science. Prentice Hall, Hemel Hempstead (1985)
Johnson, D.M., Javier Thayer, F.: Security and the composition of machines. In: Proc. 1st IEEE Computer Security Foundations Workshop (CSFW), pp. 72–89 (1988)
Lincoln, P., Mitchell, J., Mitchell, M., Scedrov, A.: A probabilistic poly-time framework for protocol analysis. In: Proc. 5th ACM Conference on Computer and Communications Security, pp. 112–121 (1998)
Lincoln, P., Mitchell, J., Mitchell, M., Scedrov, A.: Probabilistic polynomial-time equivalence and security analysis. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 776–793. Springer, Heidelberg (1999)
Lynch, N.: Distributed Algorithms. Morgan Kaufmann Publishers, San Francisco (1996)
Mantel, H.: On the composition of secure systems. In: Proc. 23rd IEEE Symposium on Security & Privacy, pp. 88–101 (2002)
McCullough, D.: Specifications for multi-level security and a hook-up property. In: Proc. 8th IEEE Symposium on Security & Privacy, pp. 161–166 (1987)
McCullough, D.: A hookup theorem for multilevel security. IEEE Transactions on Software Engineering 16(6), 563–568 (1990)
McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: Proc. 15th IEEE Symposium on Security & Privacy, pp. 79–93 (1994)
McLean, J.: A general theory of composition for a class of “possibilistic” security properties. IEEE Transactions on Software Engineering 22(1), 53–67 (1996)
Micali, S., Rogaway, P.: Secure computation. In: Feigenbaum, J. (ed.) CRYPTO 1991. LNCS, vol. 576, pp. 392–404. Springer, Heidelberg (1992)
Misra, J., Chandy, K.M.: Proofs of network of processes. IEEE Transactions on Software Engineering 7(4), 417–426 (1981)
Pfitzmann, B., Waidner, M.: A general framework for formal notions of “secure” systems. Research Report 11/94, University of Hildesheim (April 1994), http://www.semper.org/sirene/lit/abstr94.html/#PfWa_94
Pfitzmann, B., Waidner, M.: Composition and integrity preservation of secure reactive systems. In: Proc. 7th ACM Conference on Computer and Communications Security, pp. 245–254 (2000); Extended version (with Matthias Schunter) IBM Research Report RZ 3206 (May 2000), http://www.semper.org/sirene/publ/PfSW1_00ReactSimulIBM.ps.gz
Pfitzmann, B., Waidner, M.: A model for asynchronous reactive systems and its application to secure message transmission. In: Proc. 22nd IEEE Symposium on Security & Privacy, pp. 184–200 (2001); Extended version in Cryptology ePrint Archive, Report 2000/066, http://eprint.iacr.org/
Widom, J., Gries, D., Schneider, F.B.: Trace-based network proof systems: Expressiveness and completeness. ACM Transactions on Programming Languages and Systems 14(3), 396–416 (1992)
Yao, A.C.: Protocols for secure computations. In: Proc. 23rd IEEE Symposium on Foundations of Computer Science (FOCS), pp. 160–164 (1982)
Yao, A.C.: Theory and applications of trapdoor functions. In: Proc. 23rd IEEE Symposium on Foundations of Computer Science (FOCS), pp. 80–91 (1982)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Backes, M., Pfitzmann, B., Waidner, M. (2004). A General Composition Theorem for Secure Reactive Systems. In: Naor, M. (eds) Theory of Cryptography. TCC 2004. Lecture Notes in Computer Science, vol 2951. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24638-1_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-24638-1_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21000-9
Online ISBN: 978-3-540-24638-1
eBook Packages: Springer Book Archive