Advertisement

Journal of Automated Reasoning

, Volume 56, Issue 1, pp 49–94 | Cite as

Automated Proofs of Block Cipher Modes of Operation

  • Martin Gagné
  • Pascal Lafourcade
  • Yassine Lakhnech
  • Reihaneh Safavi-Naini
Article
  • 129 Downloads

Abstract

We present a Hoare logic for proving semantic security and determining exact security bounds of a block cipher mode of operation. We propose a simple yet expressive programming language to specify encryption modes, semantic functions for each command (statement) in the language, an assertion language that allows to state predicates and axioms, and rules to propagate the predicates through the commands of a program. We also provide heuristics for finding loop invariants that are necessary for the application of our rule on for-loops. This enables us to prove the security of protocols that take arbitrary length messages as input. We implemented a prototype that uses this logic to automatically prove the security of block cipher modes of operation. This prototype can prove the security of many standard modes of operation, such as Cipher Block Chaining (CBC), Cipher FeedBack mode (CFB), Output FeedBack (OFB), and CounTeR mode (CTR).

Keywords

Automated verification Hoare logic Provable cryptography Symmetric encryption Block cipher 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Barthe, G., Crespo, J.M., Grégoire, B., Kunz, C., Lakhnech, Y., Schmidt, B., Zanella-Béguelin, S.: Fully automated analysis of padding-based encryption in the computational model. In: Proceedings of the 20th ACM Conference on Computer and Communications Security, (CCS’13) (2013)Google Scholar
  2. 2.
    Bellare, M., Desai, A., Jokipii, E., Rogaway, P.: A concrete security treatment of symmetric encryption. Ann. IEEE Symp. Found. Comput. Sci. 0, 394 (1997)Google Scholar
  3. 3.
    Barthe, G., Daubignard, M., Kapron, B.M., Lakhnech, Y., Laporte, V.: On the equality of probabilistic terms. In: Clarke, E.M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers, volume 6355 of Lecture Notes in Computer Science, pp 46–63. Springer (2010)Google Scholar
  4. 4.
    Barthe, G., Daubignard, M., Kapron, B., Lakhnech, Y.: Computational indistinguishability logic. In: Proceedings of the 17th ACM conference on Computer and communications security, CCS ’10, pp 375–386. ACM (2010)Google Scholar
  5. 5.
    Barthe, G., Grégoire, B., Heraud, S., Béguelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: Rogaway, P. (ed.) CRYPTO, volume 6841 of Lecture Notes in Computer Science, pp 71–90. Springer (2011)Google Scholar
  6. 6.
    Barthe, G., Grégoire, B., Lakhnech, Y., Béguelin, S.Z.: Beyond provable security verifiable ind-cca security of oaep. In: CT-RSA, Lecture Notes in Computer Science, pp 180–196. Springer (2011)Google Scholar
  7. 7.
    Bellare, M., Kilian, J., Rogaway, P.: The security of the cipher block chaining message authentication code. J. Comput. Syst. Sci. 61(3), 362–399 (2000)MATHMathSciNetCrossRefGoogle Scholar
  8. 8.
    Blanchet, B., Pointcheval, D.: Automated security proofs with sequences of games. In: Dwork, C. (ed.) CRYPTO, volume 4117 of Lecture Notes in Computer Science, pp 537–554. Springer (2006)Google Scholar
  9. 9.
    Bellare, M., Rogaway, P., Wagner, D.: The EAX mode of operation. In: Roy, B.K., Meier, W. (eds.) FSE, volume 3017 of Lecture Notes in Computer Science, pp 389–407. Springer (2004)Google Scholar
  10. 10.
    Courant, J., Daubignard, M., Ene, C., Lafourcade, P., Lahknech, Y.: Towards automated proofs for asymmetric encryption schemes in the random oracle model. In: Proceedings of the 15th ACM Conference on Computer and Communications Security, (CCS’08), p 2008, Alexandria, USAGoogle Scholar
  11. 11.
    Courant, J., Ene, C., Lakhnech, Y.: Computationally sound typing for non-interference: The case of deterministic encryption. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science, 27th International Conference, New Delhi, India, December 12-14, 2007, Proceedings, volume 4855 of Lecture Notes in Computer Science, pp 364–375. Springer (2007)Google Scholar
  12. 12.
    Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Kenneth Zadeck, F.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451–490 (1991)CrossRefGoogle Scholar
  13. 13.
    Chakraborty, D., Nandi, M.: An improved security bound for HCTR. In: Fast Software Encryption: 15th International Workshop, FSE 2008, Lausanne, Switzerland, February 10-13, 2008, Revised Selected Papers, pp 289–302. Springer-Verlag, Berlin, Heidelberg (2008)Google Scholar
  14. 14.
    Chakraborty, D., Sarkar, P.: A new mode of encryption providing a tweakable strong pseudo-random permutation. In: Robshaw, M.J.B. (ed.) FSE, volume 4047 of Lecture Notes in Computer Science, pp 293–309. Springer (2006)Google Scholar
  15. 15.
    Chakraborty, D., Palash, S.HCH: A new tweakable enciphering scheme using the hash-counter-hash approach. IEEE Trans. Inf. Theory 54(4), 1683–1699 (2008)MATHCrossRefGoogle Scholar
  16. 16.
    Desai, A.: New paradigms for constructing symmetric encryption schemes secure against chosen-ciphertext attack. In: CRYPTO ’00: Proceedings of the 20th Annual International Cryptology Conference on Advances in Cryptology, pp 394–412. Springer-Verlag, London, UK (2000)Google Scholar
  17. 17.
    Ehrsam, W.F., Meyer, C.H.W., Smith, J.L., Tuchman, W.L.: Message verification and transmission error detection by block chaining. US Patent 4074066 (1976)Google Scholar
  18. 18.
    Gagné, M., Lafourcade, P., Lakhnech, Y.: Automated security proofs for almost-universal hash for mac verification. In: Crampton, J., Jajodia, S., Mayes, K. (eds.) ESORICS, volume 8134 of Lecture Notes in Computer Science, pp 291–308. Springer (2013)Google Scholar
  19. 19.
    Gagné, M., Lafourcade, P., Lakhnech, Y., Safavi-Naini, R.: Prototype implementation of hoare logic. Available at http://sancy.univ-bpclermont.fr/~lafourcade/Tools/
  20. 20.
    Gagné, M., Lafourcade, P., Lakhnech, Y., Safavi-Naini, R.: Automated proofs for encryption modes. In: 13th Annual Asian Computing Science Conference Focusing on Information Security and Privacy: Theory and Practice (ASIAN’09), volume 5913 of LNCS, pp 39–53 (2009)Google Scholar
  21. 21.
    Gagné, M., Lafourcade, P., Lakhnech, Y., Safavi-Naini, R., Lafourcade, P.: Automated verification of block cipher modes of operation, an improved method. In: García-Alfaro, J. (ed.) FPS, volume 6888 of Lecture Notes in Computer Science, pp 23–31. Springer (2011)Google Scholar
  22. 22.
    Halevi, S.: EME*: Extending EME to handle arbitrary-length messages with associated data. In: Canteaut, A., Viswanathan, K. (eds.) Progress in Cryptology - INDOCRYPT 2004, 5th International Conference on Cryptology in India, Chennai, India, December 20-22, 2004, Proceedings, volume 3348 of Lecture Notes in Computer Science, pp 315–327. Springer (2004)Google Scholar
  23. 23.
    Halevi, S.: Invertible universal hashing and the tet encryption mode. In: Menezes, A. (ed.) CRYPTO, volume 4622 of Lecture Notes in Computer Science, pp 412–429. Springer (2007)Google Scholar
  24. 24.
    Halevi, S., Rogaway, P.: A tweakable enciphering mode. In: Boneh, D. (ed.) CRYPTO, volume 2729 of Lecture Notes in Computer Science, pp 482–499. Springer (2003)Google Scholar
  25. 25.
    Halevi, S., Rogaway, P.: A parallelizable enciphering mode. In: Okamoto, T. (ed.) CT-RSA, volume 2964 of Lecture Notes in Computer Science, pp 292–304. Springer (2004)Google Scholar
  26. 26.
    Jutla, C.S.: Encryption modes with almost free message integrity. In: EUROCRYPT ’01: Proceedings of the International Conference on the Theory and Application of Cryptographic Techniques, pp 529–544. Springer-Verlag, London, UK (2001)Google Scholar
  27. 27.
    Jaulmes, É., Joux, A., Valette, F.: On the security of randomized CBC-MAC beyond the birthday paradox limit - a new construction. In: Fast Software Encryption 02, Lecture Notes in Computer Science, pp 237–251. Springer-Verlag (2001)Google Scholar
  28. 28.
    Liskov, M., Rivest, R.L., Wagner, D.: Tweakable block ciphers. In: CRYPTO ’02: Proceedings of the 22nd Annual International Cryptology Conference on Advances in Cryptology, pp 31–46. Springer-Verlag, London, UK (2002)Google Scholar
  29. 29.
    McGrew, D.A., Fluhrer, S.R., Miri, A., Wiener, M.J.: The security of the extended codebook (xcb) mode of operation. In: Adams, C.M. (ed.) Selected Areas in Cryptography, volume 4876 of Lecture Notes in Computer Science, pp 311–327. Springer (2007)Google Scholar
  30. 30.
    Malozemoff, A.J., Katz, J., Green, M.D.: Automated analysis and synthesis of block-cipher modes of operation. In: IEEE 27th Computer Security Foundations Symposium, CSF 2014, Vienna, Austria, 19-22 July, 2014, pp 140–152. IEEE (2014)Google Scholar
  31. 31.
    McGrew, D.A., Viega, J.: The security and performance of the galois/counter mode (GCM) of operation. In: Canteaut, A., Viswanathan, K. (eds.) INDOCRYPT, volume 3348 of Lecture Notes in Computer Science, pp 343–355. Springer (2004)Google Scholar
  32. 32.
    Wang, P., Feng, D., Wu, W.: On the security of tweakable modes of operation: TBC and TAE. In: Zhou, J., Lopez, J., Deng, R.H., Bao, F. (eds.) ISC, volume 3650 of Lecture Notes in Computer Science, pp 274–287. Springer (2005)Google Scholar

Copyright information

© Springer Science+Business Media Dordrecht 2015

Authors and Affiliations

  1. 1.Wheaton CollegeNortonUSA
  2. 2.LIMOSUniversité Clermont AuvergneClermont-FerrandFrance
  3. 3.Université Joseph Fourier (Grenoble 1), CNRSGrenobleFrance
  4. 4.University of CalgaryCalgaryCanada

Personalised recommendations