Proceedings of the Workshop on Computation: Theory and Practice (WCTP 2025)

<Previous Article In Volume
Next Article In Volume>

Formal Verification of Pohlig-Hellman Algorithm for Computing Discrete Logarithms with Coq

Authors
Jeremiah Daniel A. Regalario1, *, Marc Emanuel N. Dela Paz2, Meluisa D. Montealto3, Nicole Coleen V. Santos4, Alfonso B. Labao5
1Numerical Analysis and Scientific Computing Research Group, Institute of Mathematics, College of Science, University of the Philippines Diliman, Quezon City, 1101, Philippines
2Logic and Computability Laboratory, Department of Computer Science, College of Engineering, University of the Philippines Diliman, Quezon City, 1101, Philippines
3Institute of Mathematics, College of Science, University of the Philippines Diliman, Quezon City, 1101, Philippines
4Logic and Computability Laboratory, Institute of Mathematics, College of Science, University of the Philippines Diliman, Quezon City, 1101, Philippines
5Department of Computer Science, College of Engineering, University of the Philippines Diliman, Quezon City, 1101, Philippines
*Corresponding author. Email: jaregalario@up.edu.ph
Corresponding Author
Jeremiah Daniel A. Regalario
Available Online 30 April 2026.
DOI
10.2991/978-94-6239-638-8_8How to use a DOI?
Keywords
discrete logarithm; Pohlig–Hellman algorithm; Coq formalization; cyclic groups; Chinese Remainder Theorem; cryptography
Abstract

With the discrete logarithm problem (DLP) underpinning many modern cryptographic protocols, ensuring the correctness of algorithms that solve DLP is crucial for digital security. In this work, we present a machine-checked formalization of the Pohlig–Hellman algorithm in the Coq proof assistant. We introduce an abstract  FiniteCyclic Group class to model cyclic groups of known order  Z p × , then invoke key number-theoretic results (Fundamental Theorem of Arithmetic, Fermat’s Little Theorem, and the Chinese Remainder Theorem) as axioms to reconstruct the Pohlig-Hellman index factorization approach. Our proof shows that, given a generator and any group element, Coq’s CRT solver and a discrete black box log oracle in prime power subgroups combine to recover the unique exponent satisfying  g x = h . This development not only demonstrates how Coq can faithfully capture nontrivial cryptographic reasoning.

Copyright
© 2026 The Author(s)
Open Access
Open Access This chapter is licensed under the terms of the Creative Commons Attribution-NonCommercial 4.0 International License (http://creativecommons.org/licenses/by-nc/4.0/), which permits any noncommercial use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

Download article (PDF)

<Previous Article In Volume
Next Article In Volume>
Volume Title
Proceedings of the Workshop on Computation: Theory and Practice (WCTP 2025)
Series
Atlantis Highlights in Computer Sciences
Publication Date
30 April 2026
ISBN
978-94-6239-638-8
ISSN
2589-4900
DOI
10.2991/978-94-6239-638-8_8How to use a DOI?
Copyright
© 2026 The Author(s)
Open Access
Open Access This chapter is licensed under the terms of the Creative Commons Attribution-NonCommercial 4.0 International License (http://creativecommons.org/licenses/by-nc/4.0/), which permits any noncommercial use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

Cite this article

risenwbib
TY  - CONF
AU  - Jeremiah Daniel A. Regalario
AU  - Marc Emanuel N. Dela Paz
AU  - Meluisa D. Montealto
AU  - Nicole Coleen V. Santos
AU  - Alfonso B. Labao
PY  - 2026
DA  - 2026/04/30
TI  - Formal Verification of Pohlig-Hellman Algorithm for Computing Discrete Logarithms with Coq
BT  - Proceedings of the  Workshop on Computation: Theory and Practice (WCTP 2025)
PB  - Atlantis Press
SP  - 97
EP  - 117
SN  - 2589-4900
UR  - https://doi.org/10.2991/978-94-6239-638-8_8
DO  - 10.2991/978-94-6239-638-8_8
ID  - Regalario2026
ER  -