Formal Verification Techniques for Cryptographic Protocols in Addressing Security and Efficiency in Post Quantum Computing Paradigms

Ahana A Majeed

Authors

Ahana A Majeed USA Author

Keywords:

Formal verification, cryptographic protocols, post-quantum cryptography, quantum computing, security, efficiency

Abstract

The rapid evolution of quantum computing threatens to undermine traditional cryptographic protocols, necessitating the adoption of post-quantum cryptography (PQC). This paper explores formal verification techniques for cryptographic protocols to ensure both security and efficiency in the post-quantum era. We analyze existing methodologies, focusing on their ability to model, verify, and validate PQC algorithms and protocols. Leveraging a literature review of prominent research, we evaluate the effectiveness of formal verification frameworks, highlighting gaps and potential future directions. Our findings underscore the importance of integrating automated tools and frameworks to strengthen cryptographic resilience against quantum adversaries.

References

Lowe, Gavin. "Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR." Tools and Algorithms for the Construction and Analysis of Systems, 1996.

Paulson, Lawrence C. "The Inductive Approach to Verifying Cryptographic Protocols." Journal of Computer Security, vol. 6, no. 1, 1998, pp. 85–128.

Blanchet, Bruno. "An Efficient Cryptographic Protocol Verifier Based on Prolog Rules." Proceedings of the 14th IEEE Computer Security Foundations Workshop, 2001, pp. 82–96.

Alkim, Erdem, Léo Ducas, Thomas Pöppelmann, and Peter Schwabe. "Post-Quantum Key Exchange: A New Hope." USENIX Security Symposium, 2016, pp. 327–343.

Barthe, Gilles, Adrien Koutsos, and Pierre-Yves Strub. "Towards Computational Verification of Lattice-Based Cryptographic Constructions." Proceedings of CCS, 2019, pp. 485–502.

Unruh, Dominique. "Quantum Proofs of Knowledge." Advances in Cryptology – EUROCRYPT, 2014, pp. 135–152.

Shor, Peter W. "Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer." SIAM Journal on Computing, vol. 26, no. 5, 1997, pp. 1484–1509.

Grover, Lov K. "A Fast Quantum Mechanical Algorithm for Database Search." Proceedings of the 28th Annual ACM Symposium on Theory of Computing, 1996, pp. 212–219.

Goldwasser, Shafi, Silvio Micali, and Ronald Rivest. "A Digital Signature Scheme Secure Against Adaptive Chosen-Message Attacks." SIAM Journal on Computing, vol. 17, no. 2, 1988, pp. 281–308.

Boneh, Dan, and Victor Shoup. A Graduate Course in Applied Cryptography. Draft Version 0.5, 2020.

Bernstein, Daniel J., and Tanja Lange. "Post-Quantum Cryptography." Nature, vol. 549, no. 7671, 2017, pp. 188–194.

Campbell, Peter S., Michael Groves, and Dan Shepherd. "Soliloquy: A Cautionary Tale." International Workshop on Post-Quantum Cryptography, 2017, pp. 65–79.

Gutoski, Gus, and John Watrous. "Toward a General Theory of Quantum Games." Proceedings of the Thirty-Ninth Annual ACM Symposium on Theory of Computing (STOC), 2007, pp. 565–574.

Peikert, Chris. "A Decade of Lattice Cryptography." Foundations and Trends in Theoretical Computer Science, vol. 10, no. 4, 2016, pp. 283–424.