Abstract
Soundness of symbolic security with respect to computational security was originally investigated from the point of cryptographic protocol design. However, there has been an emerging interest in applying it to the automatic generation and verification of cryptographic algorithms. This creates a challenge, since it requires reasoning about low-level primitives like exclusive-or whose actual behavior may be inconsistent with any possible symbolic behavior.
In this paper we consider symbolic and computational soundness of cryptographic algorithms defined in terms of block ciphers and exclusive-or. We present a class of algorithms in which security is defined in terms of IND$-CPA-security, that is, security against an adaptive chosen plaintext adversary’s distinguishing the output of the cryptosystem from a random string. We develop conditions for symbolic security and show that they imply computational security. As a result of this, we are able to identify a class of cryptosystems to which results such as Unruh’s [25] on the impossibility of computationally sound exclusive-or do not apply, in the sense that symbolic security implies computational security against an adaptive adversary. We also show how our results apply to a practical class of cryptosystems: cryptographic modes of operation.
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
Similar content being viewed by others
Notes
- 1.
I am grateful to an anonymous reviewer for this example.
- 2.
We write symbolic terms in bold and computational terms in italic to make it easier to distinguish between the two.
- 3.
The term comes from"mode of operation".
- 4.
We could indeed define histories as frames, but since in this work we have no need of the main feature of frames (that they are substitutions) we choose a simpler option.
- 5.
I am grateful to Christopher Lynch for this example.
References
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proceedings of POPL 2001, pp. 104–115. ACM (2001)
Abadi, M., Rogaway, P.: Reconciling two views of cryptography. In: van Leeuwen, J., Watanabe, O., Hagiya, M., Mosses, P.D., Ito, T. (eds.) TCS 2000. LNCS, vol. 1872, pp. 3–22. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-44929-9_1
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Backes, M., Pfitzmann, B.: A cryptographically sound security proof of the Needham-Schroeder-Lowe public-key protocol. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 1–12. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-24597-1_1
Bard, G.V.: Blockwise-adaptive chosen-plaintext attack and online modes of encryption. In: Galbraith, S.D. (ed.) Cryptography and Coding 2007. LNCS, vol. 4887, pp. 129–151. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-77272-9_9
Barthe, G., et al.: Fully automated analysis of padding-based encryption in the computational model. In: ACM Conference on Computer and Communications Security (2013)
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, pp. 652–663. Springer, Heidelberg (2005). https://doi.org/10.1007/11523468_53
Bellare, M., Rogaway, P.: The security of triple encryption and a framework for code-based game-playing proofs. In: Vaudenay, S. (ed.) EUROCRYPT 2006. LNCS, vol. 4004, pp. 409–426. Springer, Heidelberg (2006). https://doi.org/10.1007/11761679_25
Bresson, E., Lakhnech, Y., Mazaré, L., Warinschi, B.: A generalization of DDH with applications to protocol analysis and computational soundness. In: Menezes, A. (ed.) CRYPTO 2007. LNCS, vol. 4622, pp. 482–499. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74143-5_27
Campbell, C.: Design and specification of cryptographic capabilities. IEEE Commun. Soc. Mag. 16(6), 15–19 (1978)
Carmer, B., Rosulek, M.: Linicrypt: a model for practical cryptography. In: Robshaw, M., Katz, J. (eds.) CRYPTO 2016. LNCS, vol. 9816, pp. 416–445. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-53015-3_15
Dolev, D., Yao, A.C.-C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198–207 (1983)
Ehrsam, W.F., Meyer, C.H., Smith, J.L., Tuchman, W.L.: Message verification and transmission error detection by block chaining, US Patent 4,074,066, 14 February 1978
Gagné, M., Lafourcade, P., Lakhnech, Y., Safavi-Naini, R.: Automated proofs of block cipher modes of operation. J. Autom. Reason. 56(1), 49–94 (2016). https://doi.org/10.1007/s10817-015-9341-5
Gligor, V.D., Donescu, P., Katz, J.: On message integrity in symmetric encryption. In: 1st NIST Workshop on AES Modes of Operation (2000)
Halevi, S.: An observation regarding Jutla’s modes of operation. IACR Cryptol. ePrint Arch. 2001:15 (2001)
Hoang, V.T., Katz, J., Malozemoff, A.J.: Automated analysis and synthesis of authenticated encryption schemes. In: Proceedings of 22nd ACM CCS, pp. 84–95 (2015)
Joux, A., Martinet, G., Valette, F.: Blockwise-adaptive attackers revisiting the (in)security of some provably secure encryption modes: CBC, GEM, IACBC. In: Yung, M. (ed.) CRYPTO 2002. LNCS, vol. 2442, pp. 17–30. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45708-9_2
Knudsen, L.R.: Block chaining modes of operation. In: Proceedings of Symmetric Key Block Cipher Modes of Operation Workshop (2000)
Kremer, S., Mazaré, L.: Adaptive soundness of static equivalence. In: Biskup, J., López, J. (eds.) ESORICS 2007. LNCS, vol. 4734, pp. 610–625. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74835-9_40
Lin, H., et al.: Algorithmic problems in the symbolic approach to the verification of automatically synthesized cryptosystems. In: Konev, B., Reger, G. (eds.) FroCoS 2021. LNCS, vol. 12941, pp. 253–270. Springer, Heidelberg (2021). https://doi.org/10.1007/978-3-030-86205-3_14
Malozemoff, A.J., Katz, J., Green, M.D.: Automated analysis and synthesis of block-cipher modes of operation. In: 2014 IEEE 27th Computer Security Foundations Symposium (CSF), pp. 140–152. IEEE (2014)
McQuoid, I., Swope, T., Rosulek, M.: Characterizing collision and second-preimage resistance in Linicrypt. In: Hofheinz, D., Rosen, A. (eds.) TCC 2019. LNCS, vol. 11891, pp. 451–470. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-36030-6_18
Micciancio, D., Warinschi, B.: Soundness of formal encryption in the presence of active adversaries. In: Naor, M. (ed.) TCC 2004. LNCS, vol. 2951, pp. 133–151. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24638-1_8
Unruh, D.: The impossibility of computationally sound XOR. IACR Cryptology ePrint Archive, 2010:389 (2010)
Acknowledgements
I am grateful to Jonathan Katz for helpful comments on earlier versions of this paper, as well as for the comments of many anonymous reviewers. I am also grateful the fruitful discussions I have had with fellow members of the CryptoSolve group, including Wei Du, Serdar Erbatur, Hai Lin, Christopher Lynch, Andrew Marshall, Paliath Narendran, Danielle Radosta, Veena Ravishankar, Brandon Rozek, and Luis Rovera. Any problems that remain with this paper are of course my own responsibility. This work was funded by ONR Code 311.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Meadows, C. (2021). Moving the Bar on Computationally Sound Exclusive-Or. In: Bertino, E., Shulman, H., Waidner, M. (eds) Computer Security – ESORICS 2021. ESORICS 2021. Lecture Notes in Computer Science(), vol 12973. Springer, Cham. https://doi.org/10.1007/978-3-030-88428-4_14
Download citation
DOI: https://doi.org/10.1007/978-3-030-88428-4_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-88427-7
Online ISBN: 978-3-030-88428-4
eBook Packages: Computer ScienceComputer Science (R0)