Hader, T., Kaufmann, D., & Kovacs, L. (2023). SMT Solving over Finite Field Arithmetic. In R. Piscac & A. Voronkov (Eds.), Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 238–256). https://doi.org/10.29007/4n6w
E192-04 - Forschungsbereich Formal Methods in Systems Engineering E056-10 - Fachbereich SecInt-Secure and Intelligent Human-Centric Digital Technologies
-
Erschienen in:
Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
-
Band:
94
-
Datum (veröffentlicht):
Jun-2023
-
Veranstaltungsname:
24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
en
Veranstaltungszeitraum:
4-Jun-2023 - 9-Jun-2023
-
Veranstaltungsort:
Kolumbien
-
Umfang:
19
-
Keywords:
SMT Solving; Finite Fields; Polynomial Arithmetic
en
Abstract:
Non-linear polynomial systems over finite fields are used to model functional behavior of cryptosystems, with applications in system security, computer cryptography, and post- quantum cryptography. Solving polynomial systems is also one of the most difficult problems in mathematics. In this paper, we propose an automated reasoning procedure for deciding the satisfiability of a system of non-linear equations over finite fields. We introduce zero decomposition techniques to prove that polynomial constraints over finite fields yield finite basis explanation functions. We use these explanation functions in model constructing satisfiability solving, allowing us to equip a CDCL-style search procedure with tailored theory reasoning in SMT solving over finite fields. We implemented our approach and provide a novel and effective reasoning prototype for non-linear arithmetic over finite fields.
en
Projekttitel:
Automated Reasoning with Theories and Induction for Software Technologies: ERC Consolidator Grant 2020 (European Commission)