Document Open Access Logo

Formalizing Algorithmic Bounds in the Query Model in EasyCrypt

Authors Alley Stoughton , Carol Chen, Marco Gaboardi, Weihao Qu

PDF
Thumbnail PDF

File

LIPIcs.ITP.2022.30.pdf
  • Filesize: 0.73 MB
  • 21 pages

Document Identifiers

Author Details

Alley Stoughton
  • Boston University, MA, USA
Carol Chen
  • Stuyvesant High School, New York, NY, USA
Marco Gaboardi
  • Boston University, MA, USA
Weihao Qu
  • Boston University, MA, USA

Funding

  • Stoughton, Alley: National Science Foundation Grant No. 1801564.
  • Gaboardi, Marco: National Science Foundation Grant No. 2040249.

Acknowledgements

We would like to thank Mark Bun for numerous helpful discussions. The anonymous referees provided very helpful feedback that helped us improve the paper.

Cite AsGet BibTex

Alley Stoughton, Carol Chen, Marco Gaboardi, and Weihao Qu. Formalizing Algorithmic Bounds in the Query Model in EasyCrypt. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 30:1-30:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ITP.2022.30

Abstract

We use the EasyCrypt proof assistant to formalize the adversarial approach to proving lower bounds for computational problems in the query model. This is done using a lower bound game between an algorithm and adversary, in which the adversary answers the algorithm’s queries in a way that makes the algorithm issue at least the desired number of queries. A complementary upper bound game is used for proving upper bounds of algorithms; here the adversary incrementally and adaptively realizes an algorithm’s input. We prove a natural connection between the lower and upper bound games, and apply our framework to three computational problems, including searching in an ordered list and comparison-based sorting, giving evidence for the generality of our notion of algorithm and the usefulness of our framework.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Models of computation
  • Theory of computation → Design and analysis of algorithms
Keywords
  • query model
  • lower bound
  • upper bound
  • adversary argument
  • EasyCrypt

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Arthur Azevedo De Amorim. Poleiro: Analyzing Sorting Algorithms, 2015. URL: http://poleiro.info/posts/2015-03-25-analyzing-sorting-algorithms.html.
  2. Sepehr Assadi. Advanced Algorithms II: Sublinear Algorithms: Lecture 3, 2020. URL: https://people.cs.rutgers.edu/~sa1497/courses/cs514-s20/lec3.pdf.
  3. Sara Baase and Allen Van Gelder. Computer Algorithms: Introduction to Design and Analysis (third edition). Pearson/Prentice Hall, 2000. Google Scholar
  4. Alexander Bagnall, Samuel Merten, and Gordon Stewart. A library for algorithmic game theory in Ssreflect/Coq. J. Formaliz. Reason., 10(1):67-95, 2017. Google Scholar
  5. Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, and Pierre-Yves Strub. Mechanized proofs of adversarial complexity and application to universal composability. In CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security, Virtual Event, Republic of Korea, November 15-19, 2021, pages 2541-2563. ACM, 2021. Google Scholar
  6. Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, and Pierre-Yves Strub. EasyCrypt: A tutorial. In Foundations of Security Analysis and Design VII, volume 8604 of Lecture Notes in Computer Science, pages 146-166. Springer International Publishing, 2014. Google Scholar
  7. Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. Formal certification of code-based cryptographic proofs. In Zhong Shao and Benjamin C. Pierce, editors, Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009, pages 90-101. ACM, 2009. Google Scholar
  8. Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, and Santiago Zanella Béguelin. Computer-aided security proofs for the working cryptographer. In Proceedings of the 31st Annual Conference on Advances in Cryptology, CRYPTO 2011, pages 71-90. Springer-Verlag, 2011. Google Scholar
  9. David A. Basin, Andreas Lochbihler, and S. Reza Sefidgar. CryptHOL: Game-based proofs in higher-order logic. J. Cryptol., 33(2):494-566, 2020. Google Scholar
  10. Martin Böhm and Bertrand Simon. Discovering and certifying lower bounds for the online bin stretching problem. CoRR, abs/2001.01125, 2020. URL: http://arxiv.org/abs/2001.01125.
  11. Manuel Eberl. Lower bound on comparison-based sorting algorithms. Arch. Formal Proofs, 2017, 2017. URL: https://www.isa-afp.org/entries/Comparison_Sort_Lower_Bound.shtml.
  12. Manuel Eberl. Proving divide and conquer complexities in Isabelle/HOL. J. Autom. Reason., 58(4):483-508, 2017. Google Scholar
  13. Jeff Erickson. Lecture Notes: Adversary Arguments, 2013. URL: https://jeffe.cs.illinois.edu/teaching/algorithms/notes/13-adversary.pdf.
  14. Ruben Gamboa and John Cowles. A mechanical proof of the Cook-Levin theorem. In International Conference on Theorem Proving in Higher Order Logics, pages 99-116. Springer-Verlag, 2004. Google Scholar
  15. Donald E. Knuth. The Art of Computer Programming, Volume III: Sorting and Searching. Addison-Wesley, 1973. Google Scholar
  16. Donald E. Knuth. The Art of Computer Programming, Volume III: Sorting and Searching, 2nd Edition. Addison-Wesley, 1998. Google Scholar
  17. Laura Kovács, Hanna Lachnitt, and Stefan Szeider. Formalizing graph trail properties in Isabelle/HOL. In Christoph Benzmüller and Bruce R. Miller, editors, Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings, volume 12236 of Lecture Notes in Computer Science, pages 190-205. Springer-Verlag, 2020. Google Scholar
  18. Shiri Morshtein, Ran Ettinger, and Shmuel S. Tyszberowicz. Verifying time complexity of binary search using Dafny. In José Proença and Andrei Paskevich, editors, Proceedings of the 6th Workshop on Formal Integrated Development Environment, F-IDE@NFM 2021, Held online, 24-25th May 2021, volume 338 of EPTCS, pages 68-81, 2021. Google Scholar
  19. David Nowak. A framework for game-based security proofs. In Sihan Qing, Hideki Imai, and Guilin Wang, editors, Information and Communications Security, 9th International Conference, ICICS 2007, Zhengzhou, China, December 12-15, 2007, volume 4861 of Lecture Notes in Computer Science, pages 319-333. Springer-Verlag, 2007. Google Scholar
  20. Ulrich Schöpp. A formalised lower bound on undirected graph reachability. In Iliano Cervesato, Helmut Veith, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings, volume 5330 of Lecture Notes in Computer Science, pages 621-635. Springer-Verlag, 2008. Google Scholar
  21. Alley Stoughton and Mayank Varia. Mechanizing the proof of adaptive, information-theoretic security of cryptographic protocols in the random oracle model. In 30th IEEE Computer Security Foundations Symposium, pages 83-99, Santa Barbara, CA, USA, 2017. IEEE Computer Society. URL: https://github.com/alleystoughton/PCR.
  22. Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee, and Jean-Baptiste Tristan. A formal proof of PAC learnability for decision stumps. In Catalin Hritcu and Andrei Popescu, editors, CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021, pages 5-17. ACM, 2021. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact