Abstract
The composition of security definitions is a subtle issue. As most security protocols use a combination of security primitives, it is important to have general results that allow to combine such definitions. We present here a general result of composition for security criteria (i.e. security requirements). This result can be applied to deduce security of a criterion from security of one of its sub-criterion and an indistinguishability criterion. To illustrate our result, we introduce joint security for asymmetric and symmetric cryptography and prove that it is equivalent to classical security assumptions for both the asymmetric and symmetric encryption schemes. Using this, we give a modular proof of computational soundness of symbolic encryption. This result holds in the case of an adaptive adversary which can use both asymmetric and symmetric encryption.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abadi, M., Jürjens, J.: Formal eavesdropping and its computational interpretation. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, pp. 82–94. Springer, Heidelberg (2001)
Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). In: IFIP TCS 2000. IFIP International Conference on Theoretical Computer Science, Sendai, Japan, Springer, Berlin (2000)
Bellare, M., Boldyreva, A., Micali, S.: Public-key encryption in a multi-user setting: Security proofs and improvements. In: Preneel, B. (ed.) EUROCRYPT 2000. LNCS, vol. 1807, pp. 259–274. Springer, Heidelberg (2000)
Baudet, M., Cortier, V., Kremer, S.: Computationally sound implementations of equational theories against passive adversaries. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, Springer, Heidelberg (2005)
Blanchet, B.: A computationally sound mechanized prover for security protocols. In: IEEE Symposium on Security and Privacy, Oakland, California (May 2006)
Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations. In: Proceedings of the 10th ACM conference on Computer and communication security, pp. 220–230 (2003)
Bellare, M., Rogaway, P.: The game-playing technique. Cryptology ePrint Archive, Report 2004/331 (2004), http://eprint.iacr.org/
Cousot, P.: Methods and Logics for Proving Programs. In: Handbook of Theoretical Computer Science, vol. B: Formal Methods and Semantics, pp. 841–994. Elsevier Science Publishers B.V., Amsterdam (1990)
Cortier, V., Warinschi, B.: Computationally sound, automated proofs for security protocols. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, Springer, Heidelberg (2005)
Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)
Goldwasser, S., Micali, S.: Probabilistic encryption. Journal of Computer and System Sciences 28(2), 270–299 (1984)
Janvier, R., Lakhnech, Y., Mazaré, L.: Completing the picture: Soundness of formal encryption in the presence of active adversaries. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, Springer, Heidelberg (2005)
Mazaré, L.: Computational Soundness of Symbolic Models for Cryptographic Protocols. PhD thesis, INPG, Grenoble, October 2006 (to appear)
Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems. Springer, Heidelberg (1992)
Micciancio, D., Panjwani, S.: Adaptive security of symbolic encryption. In: Kilian, J. (ed.) TCC 2005. LNCS, vol. 3378, pp. 169–187. Springer, Heidelberg (2005)
Micciancio, D., Warinschi, B.: Soundness of formal encryption in the presence of active adversaries. In: Proceedings of the Theory of Cryptography Conference, pp. 133–151. Springer, Heidelberg (2004)
Shoup, V.: Sequences of games: a tool for taming complexity in security proofs (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Daubignard, M., Janvier, R., Lakhnech, Y., Mazaré, L. (2007). Game-Based Criterion Partition Applied to Computational Soundness of Adaptive Security. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds) Formal Aspects in Security and Trust. FAST 2006. Lecture Notes in Computer Science, vol 4691. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75227-1_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-75227-1_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75226-4
Online ISBN: 978-3-540-75227-1
eBook Packages: Computer ScienceComputer Science (R0)