Non-linear SMT-reasoning over finite fields

Abstract

Nichtlineare Polynome über endliche Körper haben zahlreiche Anwendungen in der Kryptographie, da sie schwer zu lösen sind. In dieser Arbeit befassen wir uns mit diesem Problem und präsentieren eine automatische Entscheidungsprozedur für die Erfüllbarkeit von Systemen nichtlinearer Polynome über endliche Körper. Unser Ansatz besteht aus einer Conflict-Driven Clause Learning (CDCL) Suchprozedur die bereits erfolgreich für Systeme nichtlinearer Polynome über die reellen Zahlen verwendet wurde. Wir zeigen, dass eine solche Prozedur auch für Systeme von Polynomen über endliche Körper verwendet werden kann. Neben der Suchprozedur selbst präsentieren wir zwei verschiedene Ansätze zum Verarbeiten der Polynome basierend auf der Eliminationstheorie und Gröbnerbasen. Wir vergleichen unseren Ansatz mit aktuellen Lösungsverfahren und beurteilen unsere Ergebnisse.

Non-linear polynomial systems over finite fields are widely found in cryptography, as they are known to be hard to solve. In this thesis, we address this challenge and propose an automated reasoning procedure for deciding the satisfiability of a system on non-linear equations over finite fields. Our approach performs a Conflict-Driven Clause Learning (CDCL) style search, which has been successfully applied to deciding satisfiability of non-linear arithmetic constraints in the past. We show that CDCL can be utilized for the problem of solving non-linear polynomial systems and present the search procedure as well as two different theory solving back-end approaches utilizing elimination theory as well as Gröbner bases. In addition, we are comparing our approach to state-of-the-art procedures and give an evaluation of the results.