Symbolic Synthesis of Indifferentiability Attacks
Abstract
We propose automated methods for synthesising attacks against indifferentiability, a powerful simulation-based notion of security commonly used to reason about symmetric-key constructions. Our methods are inspired from symbolic cryptography which is popular to reason about, e.g., cryptographic protocols. For that, we introduce a core programming language for algebraic distinguishers and study the class of universal distinguishers, who win the indifferentiability game against every simulator; then, we show that the universality of algebraic distinguishers can be reduced to solving systems of algebraic, deducibility and static-equivalence constraints.
Our approach is implemented in a tool, AutoDiff, which solves these constraint systems, and applies heuristics to automate the cryptanalysis (i.e., to search automatically for universal distinguishers). We evaluate the tool with many non-trivial attacks from the literature on Feistel networks and Even-Mansour blockciphers among others. Our tool is able to check the validity these attacks, and in many cases to synthesise them without guidance. To our knowledge, AutoDiff is the first practical tool for indifferentiability attacks.
Supplementary Material
Indifferentiability is a popular standard for characterising the security of symmetric encryption schemes due its convenient compositionality properties. It is however also more complex than classical indistinguishability notions (IND-CPA, IND-CCA...) by being a simulation-based notion, resulting in historical flaws in proofs of complex constructions. Even verifying that an attack code violates indifferentiability is actually a non-trivial task. Our contribution develops proof techniques, support and automation for this notion. We provide a reduction of differentiability to a form of algebraic constraints, that are simpler to solve and already benefit from several decidability results in the literature. We then use this result to implement a heuristics synthesising attacks against indifferentiability and experiment it on various classical constructions.
- Download
- 47.72 MB
References
[1]
Martín Abadi, Bruno Blanchet, and Cédric Fournet. 2017. The applied pi calculus: Mobile values, new names, and secure communication. Journal of the ACM (JACM) (2017).
[2]
Mart'i n Abadi and Vé ronique Cortier. 2006. Deciding knowledge in security protocols under equational theories. Theor. Comput. Sci., Vol. 367, 1-2 (2006), 2--32. https://doi.org/10.1016/j.tcs.2006.08.032
[3]
Martín Abadi and Phillip Rogaway. 2007. Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption). J. Cryptol., Vol. 20, 3 (2007), 395. https://doi.org/10.1007/s00145-007-0203-0
[4]
Miguel Ambrona, Gilles Barthe, Romain Gay, and Hoeteck Wee. 2017. Attribute-Based Encryption in the Generic Group Model: Automated Proofs and New Constructions. In ACM CCS 2017: 24th Conference on Computer and Communications Security, Bhavani M. Thuraisingham, David Evans, Tal Malkin, and Dongyan Xu (Eds.). ACM Press, Dallas, TX, USA, 647--664. https://doi.org/10.1145/3133956.3134088
[5]
Miguel Ambrona, Gilles Barthe, and Benedikt Schmidt. 2016. Automated Unbounded Analysis of Cryptographic Constructions in the Generic Group Model. In Advances in Cryptology -- EUROCRYPT 2016, Part II (Lecture Notes in Computer Science, Vol. 9666), Marc Fischlin and Jean-Sé bastien Coron (Eds.). Springer, Heidelberg, Germany, Vienna, Austria, 822--851. https://doi.org/10.1007/978-3-662-49896-5_29
[6]
Mathilde Arnaud, Véronique Cortier, and Stéphanie Delaune. 2007. Combining Algorithms for Deciding Knowledge in Security Protocols. In Frontiers of Combining Systems, Boris Konev and Frank Wolter (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 103--117.
[7]
Manuel Barbosa and Pooya Farshim. 2015. The Related-Key Analysis of Feistel Constructions. In Fast Software Encryption -- FSE 2014 (Lecture Notes in Computer Science, Vol. 8540), Carlos Cid and Christian Rechberger (Eds.). Springer, Heidelberg, Germany, London, UK, 265--284. https://doi.org/10.1007/978-3-662-46706-0_14
[8]
Manuel Barbosa and Pooya Farshim. 2018. Indifferentiable Authenticated Encryption. In Advances in Cryptology -- CRYPTO 2018, Part I (Lecture Notes in Computer Science, Vol. 10991), Hovav Shacham and Alexandra Boldyreva (Eds.). Springer, Heidelberg, Germany, Santa Barbara, CA, USA, 187--220. https://doi.org/10.1007/978-3-319-96884-1_7
[9]
Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Benedikt Schmidt, and Santiago Zanella Béguelin. 2013. Fully automated analysis of padding-based encryption in the computational model. In ACM CCS 2013: 20th Conference on Computer and Communications Security, Ahmad-Reza Sadeghi, Virgil D. Gligor, and Moti Yung (Eds.). ACM Press, Berlin, Germany, 1247--1260. https://doi.org/10.1145/2508859.2516663
[10]
Gilles Barthe, Edvard Fagerholm, Dario Fiore, John C. Mitchell, Andre Scedrov, and Benedikt Schmidt. 2014. Automated Analysis of Cryptographic Assumptions in Generic Group Models. In Advances in Cryptology -- CRYPTO 2014, Part I (Lecture Notes in Computer Science, Vol. 8616), Juan A. Garay and Rosario Gennaro (Eds.). Springer, Heidelberg, Germany, Santa Barbara, CA, USA, 95--112. https://doi.org/10.1007/978-3-662-44371-2_6
[11]
Gilles Barthe, Xiong Fan, Joshua Gancher, Benjamin Grégoire, Charlie Jacomme, and Elaine Shi. 2018. Symbolic Proofs for Lattice-Based Cryptography. In ACM CCS 2018: 25th Conference on Computer and Communications Security, David Lie, Mohammad Mannan, Michael Backes, and XiaoFeng Wang (Eds.). ACM Press, Toronto, ON, Canada, 538--555. https://doi.org/10.1145/3243734.3243825
[12]
Gilles Barthe, Benjamin Grégoire, and Benedikt Schmidt. 2015. Automated Proofs of Pairing-Based Cryptography. In ACM CCS 2015: 22nd Conference on Computer and Communications Security, Indrajit Ray, Ninghui Li, and Christopher Kruegel (Eds.). ACM Press, Denver, CO, USA, 1156--1168. https://doi.org/10.1145/2810103.2813697
[13]
Gilles Barthe, Benjamin Grégoire, Charlie Jacomme, Steve Kremer, and Pierre-Yves Strub. 2019. Symbolic methods in computational cryptography proofs. In 31st IEEE Computer Security Foundations Symposium (CSF).
[14]
David Basin, Jannik Dreier, Lucca Hirschi, Savs a Radomirovic, Ralf Sasse, and Vincent Stettler. 2018. A formal analysis of 5G authentication. In ACM Conference on Computer and Communications Security (CCS).
[15]
Mathieu Baudet. 2007. Sécurité des protocoles cryptographiques: aspects logiques et calculatoires. Ph.D. Dissertation. École normale supérieure de Cachan.
[16]
Mathieu Baudet, Véronique Cortier, and Steve Kremer. 2009. Computationally sound implementations of equational theories against passive adversaries. Information and Computation, Vol. 207, 4 (2009), 496--520.
[17]
Mihir Bellare and Phillip Rogaway. 1994. Optimal asymmetric encryption. In Workshop on the Theory and Application of of Cryptographic Techniques.
[18]
Guido Bertoni, Joan Daemen, Michael Peeters, and Gilles Van Assche. 2008. On the indifferentiability of the sponge construction. In Annual International Conference on the Theory and Applications of Cryptographic Techniques (EuroCrypt).
[19]
Karthikeyan Bhargavan, Bruno Blanchet, and Nadim Kobeissi. 2017. Verified models and reference implementations for the TLS 1.3 standard candidate. In IEEE Symposium on Security and Privacy (S&P).
[20]
John Black, Phillip Rogaway, and Thomas Shrimpton. 2002. Black-Box Analysis of the Block-Cipher-Based Hash-Function Constructions from PGV. In Advances in Cryptology -- CRYPTO 2002 (Lecture Notes in Computer Science, Vol. 2442), Moti Yung (Ed.). Springer, Heidelberg, Germany, Santa Barbara, CA, USA, 320--335. https://doi.org/10.1007/3-540-45708-9_21
[21]
Dan Boneh, Xavier Boyen, and Eu-Jin Goh. 2005. Hierarchical Identity Based Encryption with Constant Size Ciphertext. In Advances in Cryptology -- EUROCRYPT 2005 (Lecture Notes in Computer Science, Vol. 3494), Ronald Cramer (Ed.). Springer, Heidelberg, Germany, Aarhus, Denmark, 440--456. https://doi.org/10.1007/11426639_26
[22]
Charles Bouillaguet, Patrick Derbez, and Pierre-Alain Fouque. 2011. Automatic Search of Attacks on Round-Reduced AES and Applications. In Advances in Cryptology -- CRYPTO 2011 (Lecture Notes in Computer Science, Vol. 6841), Phillip Rogaway (Ed.). Springer, Heidelberg, Germany, Santa Barbara, CA, USA, 169--187. https://doi.org/10.1007/978-3-642-22792-9_10
[23]
Johannes Buchmann, Andrei Pyshkin, and Ralf-Philipp Weinmann. 2006. A Zero-Dimensional Gröbner Basis for AES-128. In Fast Software Encryption -- FSE 2006 (Lecture Notes in Computer Science, Vol. 4047), Matthew J. B. Robshaw (Ed.). Springer, Heidelberg, Germany, Graz, Austria, 78--88. https://doi.org/10.1007/11799313_6
[24]
Sergiu Bursuc, Hubert Comon-Lundh, and Stéphanie Delaune. 2007. Associative-Commutative Deducibility Constraints. In STACS 2007, Wolfgang Thomas and Pascal Weil (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 634--645.
[25]
Vincent Cheval, Hubert Comon-Lundh, and Stéphanie Delaune. 2011. Trace equivalence decision: Negative tests and non-determinism. In ACM conference on Computer and communications security (CCS.
[26]
Vincent Cheval, Véronique Cortier, and Stéphanie Delaune. 2013. Deciding equivalence-based properties using constraint solving. Theoretical Computer Science (2013).
[27]
Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. 2018. DEEPSEC: Deciding equivalence properties in security protocols theory and practice. In IEEE Symposium on Security and Privacy (S&P).
[28]
Yannick Chevalier and Michael Rusinowitch. 2010. Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures. Theoretical Computer Science (2010).
[29]
cS tefan Ciobâcua, Stéphanie Delaune, and Steve Kremer. 2012. Computing knowledge in security protocols under convergent equational theories. Journal of Automated Reasoning (2012).
[30]
Hubert Comon-Lundh and Véronique Cortier. 2008. Computational soundness of observational equivalence. In ACM conference on Computer and communications security (CCS).
[31]
Jean-Sébastien Coron, Thomas Holenstein, Robin Künzler, Jacques Patarin, Yannick Seurin, and Stefano Tessaro. 2016. How to Build an Ideal Cipher: The Indifferentiability of the Feistel Construction. Journal of Cryptology, Vol. 29, 1 (01 Jan 2016), 61--114. https://doi.org/10.1007/s00145-014-9189-6
[32]
Jean-Sébastien Coron, Jacques Patarin, and Yannick Seurin. 2008. The Random Oracle Model and the Ideal Cipher Model Are Equivalent. In Advances in Cryptology -- CRYPTO 2008 (Lecture Notes in Computer Science, Vol. 5157), David Wagner (Ed.). Springer, Heidelberg, Germany, Santa Barbara, CA, USA, 1--20. https://doi.org/10.1007/978-3-540-85174-5_1
[33]
Véronique Cortier and Stéphanie Delaune. 2012. Decidability and combination results for two notions of knowledge in security protocols. Journal of Automated Reasoning, Vol. 48, 4 (2012), 441--487.
[34]
Véronique Cortier, Steve Kremer, and Bogdan Warinschi. 2011. A survey of symbolic methods in computational analysis of cryptographic systems. Journal of Automated Reasoning (2011).
[35]
Judicaël Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade, and Yassine Lakhnech. 2008. Towards automated proofs for asymmetric encryption schemes in the random oracle model. In ACM CCS 2008: 15th Conference on Computer and Communications Security, Peng Ning, Paul F. Syverson, and Somesh Jha (Eds.). ACM Press, Alexandria, Virginia, USA, 371--380. https://doi.org/10.1145/1455770.1455817
[36]
Nicolas Courtois. 2003. Fast Algebraic Attacks on Stream Ciphers with Linear Feedback. In Advances in Cryptology -- CRYPTO 2003 (Lecture Notes in Computer Science, Vol. 2729), Dan Boneh (Ed.). Springer, Heidelberg, Germany, Santa Barbara, CA, USA, 176--194. https://doi.org/10.1007/978-3-540-45146-4_11
[37]
Nicolas Courtois and Willi Meier. 2003. Algebraic Attacks on Stream Ciphers with Linear Feedback. In Advances in Cryptology -- EUROCRYPT 2003 (Lecture Notes in Computer Science, Vol. 2656), Eli Biham (Ed.). Springer, Heidelberg, Germany, Warsaw, Poland, 345--359. https://doi.org/10.1007/3-540-39200-9_21
[38]
Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott, and Thyla van der Merwe. 2017. A comprehensive symbolic analysis of TLS 1.3. In ACM Conference on Computer and Communications Security (CCS).
[39]
Yuanxi Dai, Yannick Seurin, John P. Steinberger, and Aishwarya Thiruvengadam. 2017. Indifferentiability of Iterated Even-Mansour Ciphers with Non-idealized Key-Schedules: Five Rounds Are Necessary and Sufficient. In Advances in Cryptology -- CRYPTO 2017, Part III (Lecture Notes in Computer Science, Vol. 10403), Jonathan Katz and Hovav Shacham (Eds.). Springer, Heidelberg, Germany, Santa Barbara, CA, USA, 524--555. https://doi.org/10.1007/978-3-319-63697-9_18
[40]
Yuanxi Dai and John P. Steinberger. 2016. Indifferentiability of 8-Round Feistel Networks. In Advances in Cryptology -- CRYPTO 2016, Part I (Lecture Notes in Computer Science, Vol. 9814), Matthew Robshaw and Jonathan Katz (Eds.). Springer, Heidelberg, Germany, Santa Barbara, CA, USA, 95--120. https://doi.org/10.1007/978-3-662-53018-4_4
[41]
Stéphanie Delaune, Steve Kremer, and Daniel Pasaila. 2012. Security protocols, constraint systems, and group theories. In International Joint Conference on Automated Reasoning (IJCAR).
[42]
Stéphanie Delaune, Pascal Lafourcade, Denis Lugiez, and Ralf Treinen. 2008. Symbolic protocol analysis for monoidal equational theories. Information and Computation (2008).
[43]
Patrick Derbez and Pierre-Alain Fouque. 2016. Automatic Search of Meet-in-the-Middle and Impossible Differential Attacks. In Advances in Cryptology -- CRYPTO 2016, Part II (Lecture Notes in Computer Science, Vol. 9815), Matthew Robshaw and Jonathan Katz (Eds.). Springer, Heidelberg, Germany, Santa Barbara, CA, USA, 157--184. https://doi.org/10.1007/978-3-662-53008-5_6
[44]
Yevgeniy Dodis, Martijn Stam, John P. Steinberger, and Tianren Liu. 2016. Indifferentiability of Confusion-Diffusion Networks. In Advances in Cryptology -- EUROCRYPT 2016, Part II (Lecture Notes in Computer Science, Vol. 9666), Marc Fischlin and Jean-Sé bastien Coron (Eds.). Springer, Heidelberg, Germany, Vienna, Austria, 679--704. https://doi.org/10.1007/978-3-662-49896-5_24
[45]
D. Dolev and A.C. Yao. 1981. On the Security of Public Key Protocols. In Symposium on Foundations of Computer Science (FOCS).
[46]
Shimon Even and Yishay Mansour. 1997. A construction of a cipher from a single pseudorandom permutation. Journal of cryptology (1997).
[47]
H. Feistel. 1973. Cryptography and Computer Privacy. Scientific American. https://books.google.es/books?id=Y0BenQEACAAJ
[48]
Eiichiro Fujisaki, Tatsuaki Okamoto, David Pointcheval, and Jacques Stern. 2001. RSA-OAEP is secure under the RSA assumption. In Annual International Cryptology Conference (CRYPTO).
[49]
Viet Tung Hoang, Jonathan Katz, and Alex J. Malozemoff. 2015. Automated Analysis and Synthesis of Authenticated Encryption Schemes. In ACM CCS 2015: 22nd Conference on Computer and Communications Security, Indrajit Ray, Ninghui Li, and Christopher Kruegel (Eds.). ACM Press, Denver, CO, USA, 84--95. https://doi.org/10.1145/2810103.2813636
[50]
Thomas Holenstein, Robin Kü nzler, and Stefano Tessaro. 2010. Equivalence of the Random Oracle Model and the Ideal Cipher Model, Revisited. CoRR, Vol. abs/1011.1264 (2010).
[51]
Charlie Jacomme and Steve Kremer. 2021. An extensive formal analysis of multi-factor authentication protocols. ACM Transactions on Privacy and Security (TOPS) (2021).
[52]
John Kelsey and Tadayoshi Kohno. 2006. Herding hash functions and the Nostradamus attack. In Annual International Conference on the Theory and Applications of Cryptographic Techniques (EUROCRYPT). Springer.
[53]
Steve Kremer and Laurent Mazaré. 2007. Adaptive soundness of static equivalence. In European Symposium on Research in Computer Security (ESORICS.
[54]
Rodolphe Lampe and Yannick Seurin. 2013. How to Construct an Ideal Cipher from a Small Set of Public Permutations. In Advances in Cryptology -- ASIACRYPT 2013, Part I (Lecture Notes in Computer Science, Vol. 8269), Kazue Sako and Palash Sarkar (Eds.). Springer, Heidelberg, Germany, Bengalore, India, 444--463. https://doi.org/10.1007/978-3-642-42033-7_23
[55]
Gaëtan Leurent. 2012. Analysis of Differential Attacks in ARX Constructions. In Advances in Cryptology -- ASIACRYPT 2012 (Lecture Notes in Computer Science, Vol. 7658), Xiaoyun Wang and Kazue Sako (Eds.). Springer, Heidelberg, Germany, Beijing, China, 226--243. https://doi.org/10.1007/978-3-642-34961-4_15
[56]
Alex J. Malozemoff, Jonathan Katz, and Matthew D. Green. 2014. Automated Analysis and Synthesis of Block-Cipher Modes of Operation. In CSF 2014: IEEE 27st Computer Security Foundations Symposium, Anupam Datta and Cedric Fournet (Eds.). IEEE Computer Society Press, Vienna, Austria, 140--152. https://doi.org/10.1109/CSF.2014.18
[57]
Ueli M. Maurer. 2005. Abstract Models of Computation in Cryptography (Invited Paper). In 10th IMA International Conference on Cryptography and Coding (Lecture Notes in Computer Science, Vol. 3796), Nigel P. Smart (Ed.). Springer, Heidelberg, Germany, Cirencester, UK, 1--12.
[58]
Ueli M. Maurer, Renato Renner, and Clemens Holenstein. 2004. Indifferentiability, Impossibility Results on Reductions, and Applications to the Random Oracle Methodology. In TCC 2004: 1st Theory of Cryptography Conference (Lecture Notes in Computer Science, Vol. 2951), Moni Naor (Ed.). Springer, Heidelberg, Germany, Cambridge, MA, USA, 21--39. https://doi.org/10.1007/978-3-540-24638-1_2
[59]
Catherine Meadows. 2020. Symbolic and Computational Reasoning About Cryptographic Modes of Operation. Cryptology ePrint Archive, Report 2020/142. https://eprint.iacr.org/2020/794.
[60]
V. I. Nechaev. 1994. Complexity of a Determinate Algorithm for the Discrete Logarithm. Mathematical Notes, Vol. 55, 2 (1994), 165--172.
[61]
Bart Preneel, René Govaerts, and Joos Vandewalle. 1994. Hash Functions Based on Block Ciphers: A Synthetic Approach. In Advances in Cryptology -- CRYPTO'93 (Lecture Notes in Computer Science, Vol. 773), Douglas R. Stinson (Ed.). Springer, Heidelberg, Germany, Santa Barbara, CA, USA, 368--378. https://doi.org/10.1007/3-540-48329-2_31
[62]
Thomas Ristenpart, Hovav Shacham, and Thomas Shrimpton. 2011. Careful with Composition: Limitations of the Indifferentiability Framework. In Advances in Cryptology -- EUROCRYPT 2011 (Lecture Notes in Computer Science, Vol. 6632), Kenneth G. Paterson (Ed.). Springer, Heidelberg, Germany, Tallinn, Estonia, 487--506. https://doi.org/10.1007/978-3-642-20465-4_27
[63]
Danping Shi, Siwei Sun, Patrick Derbez, Yosuke Todo, Bing Sun, and Lei Hu. 2018. Programming the Demirci-Selc cuk Meet-in-the-Middle Attack with Constraints. In Advances in Cryptology -- ASIACRYPT 2018, Part II (Lecture Notes in Computer Science, Vol. 11273), Thomas Peyrin and Steven Galbraith (Eds.). Springer, Heidelberg, Germany, Brisbane, Queensland, Australia, 3--34. https://doi.org/10.1007/978-3-030-03329-3_1
[64]
Victor Shoup. 1997. Lower Bounds for Discrete Logarithms and Related Problems. In Advances in Cryptology -- EUROCRYPT'97 (Lecture Notes in Computer Science, Vol. 1233), Walter Fumy (Ed.). Springer, Heidelberg, Germany, Konstanz, Germany, 256--266. https://doi.org/10.1007/3-540-69053-0_18
[65]
Dominique Unruh. 2010. The impossibility of computationally sound XOR. IACR Cryptol. ePrint Arch. (2010).
Index Terms
- Symbolic Synthesis of Indifferentiability Attacks
Recommendations
A synthetic indifferentiability analysis of some block-cipher-based hash functions
At ASIACRYPT'06 , Chang et al. analyzed the indifferentiability of some popular hash functions based on block ciphers, namely, the twenty collision resistant PGV, the MDC2 and the PBGV hash functions, etc. In particular, two indifferentiable attacks ...
Improved indifferentiability security bound for the JH mode
Indifferentiability security of a hash mode of operation guarantees the mode's resistance against all generic attacks. It is also useful to establish the security of protocols that use hash functions as random functions. The JH hash function was one of ...
Sequential Indifferentiability of Confusion-Diffusion Networks
Progress in Cryptology – INDOCRYPT 2021AbstractA large proportion of modern symmetric cryptographic building blocks are designed using the Substitution-Permutation Networks (SPNs), or more generally, Shannon’s confusion-diffusion paradigm. To justify its theoretical soundness, Dodis et al. (...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
May 2022
1291 pages
ISBN:9781450391405
DOI:10.1145/3488932
- General Chairs:
- Yuji Suga,
- Kouichi Sakurai,
- Program Chairs:
- Xuhua Ding,
- Kazue Sako
Copyright © 2022 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 30 May 2022
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
ASIA CCS '22
Sponsor:
ASIA CCS '22: ACM Asia Conference on Computer and Communications Security
May 30 - June 3, 2022
Nagasaki, Japan
Acceptance Rates
Overall Acceptance Rate 418 of 2,322 submissions, 18%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 254Total Downloads
- Downloads (Last 12 months)120
- Downloads (Last 6 weeks)24
Reflects downloads up to 16 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in