Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Integer Reasoning Modulo Different Constants in SMT

Elizaveta Pertseva, Alex Ozdemir, Shankara Pailoor, Alp Bassa, Sorawee Porncharoenwase, Işil Dillig, Clark Barrett

TL;DR

This work tackles the challenge of solving multimodular integer constraint systems that arise in cryptographic verification. It introduces a novel refutation framework that partitions constraints by modulus and propagates information across subsystems through lifting to the integers and lowering back to modular spaces, complemented by range analysis and algebraic techniques such as weighted Gröbner bases and integer linear programming to discover shareable lemmas. The approach is implemented in cvc5 and evaluated on cryptographic benchmarks including Montgomery arithmetic and zero-knowledge proofs, where it outperforms state-of-the-art solvers in several categories and yields many unique solutions. The results demonstrate the practical potential of cross-modulus lemma exchange for efficient verification of cryptographic implementations, while also recognizing incompleteness of the lifting methods and suggesting avenues for future improvements, including more complete lifting strategies and dedicated ILP solvers. Overall, the paper presents a principled, modular approach to integer reasoning across constants, with tangible improvements for cryptographic verification workflows.

Abstract

This paper presents a new refutation procedure for multimodular systems of integer constraints that commonly arise when verifying cryptographic protocols. These systems, involving polynomial equalities and disequalities modulo different constants, are challenging for existing solvers due to their inability to exploit multimodular structure. To address this issue, our method partitions constraints by modulus and uses lifting and lowering techniques to share information across subsystems, supported by algebraic tools like weighted Gröbner bases. Our experiments show that the proposed method outperforms existing state-of-the-art solvers in verifying cryptographic implementations related to Montgomery arithmetic and zero-knowledge proofs.

Integer Reasoning Modulo Different Constants in SMT

TL;DR

This work tackles the challenge of solving multimodular integer constraint systems that arise in cryptographic verification. It introduces a novel refutation framework that partitions constraints by modulus and propagates information across subsystems through lifting to the integers and lowering back to modular spaces, complemented by range analysis and algebraic techniques such as weighted Gröbner bases and integer linear programming to discover shareable lemmas. The approach is implemented in cvc5 and evaluated on cryptographic benchmarks including Montgomery arithmetic and zero-knowledge proofs, where it outperforms state-of-the-art solvers in several categories and yields many unique solutions. The results demonstrate the practical potential of cross-modulus lemma exchange for efficient verification of cryptographic implementations, while also recognizing incompleteness of the lifting methods and suggesting avenues for future improvements, including more complete lifting strategies and dedicated ILP solvers. Overall, the paper presents a principled, modular approach to integer reasoning across constants, with tangible improvements for cryptographic verification workflows.

Abstract

This paper presents a new refutation procedure for multimodular systems of integer constraints that commonly arise when verifying cryptographic protocols. These systems, involving polynomial equalities and disequalities modulo different constants, are challenging for existing solvers due to their inability to exploit multimodular structure. To address this issue, our method partitions constraints by modulus and uses lifting and lowering techniques to share information across subsystems, supported by algebraic tools like weighted Gröbner bases. Our experiments show that the proposed method outperforms existing state-of-the-art solvers in verifying cryptographic implementations related to Montgomery arithmetic and zero-knowledge proofs.

Paper Structure

This paper contains 43 sections, 18 theorems, 9 equations, 5 figures, 3 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Motivating Example
  3. Background
  4. Algebra
  5. Sets, Intervals, and Functions
  6. Polynomial Rings
  7. Monomial Orders
  8. Ideals
  9. Gröbner bases
  10. SMT
  11. A Multimodular Logic
  12. Refutation Procedure
  13. Key Ideas
  14. Refutation Calculus
  15. Checking Unsatisfiability
  16. ...and 28 more sections

Key Result

lemma thmcounterlemma

Let $C$ be a multimodular system with bounds $B$ and modulus-$n$ equality subsystem $R^{\approx}_{n}$, with $n\in\mathbb{Z}^{+}$. Then, an equality $e \bmod n \approx 0$ is liftable in $C$ if (1) $\llbracket{e}\rrbracket \in I_n(\llbracket{R^{\approx}_{n}}\rrbracket)$ and (2) $\mathtt{CalcBds}(B, e)

Figures (5)

  • Figure 1: Overview of our refutation procedure. Integer-reasoning interacts with modules for reasoning about equations modulo constants, e.g. (in this figure, modulo 2 and 7).
  • Figure 2: The signature and grammar for $\mathsf{QF\_MIA}$, a fragment of $\mathsf{QF\_NIA}$.
  • Figure 3: Encoding rules for a multimodular system $C$, where $e$ is an expression and $n\in\mathbb{Z}^{+}_{\infty}$.
  • Figure 4: Derivation rules. $e,s$ are expressions, $a\in \mathbb{Z}$, and $n\in\mathbb{Z}^{+}_{\infty}$.
  • Figure 5: Benchmarks solved over time for top 5 solvers: ours ($\mathsf{QF\_MIA}$), z3 ($\mathsf{QF\_NIA}$), cvc5 ($\mathsf{QF\_NIA}$), yices ($\mathsf{QF\_NIA}$), and bitwuzla w/ abstractions ($\mathsf{ QF\_BV}$)

Theorems & Definitions (31)

  • definition thmcounterdefinition: Liftable
  • definition thmcounterdefinition: Lowerable
  • remark thmcounterremark
  • lemma thmcounterlemma
  • lemma thmcounterlemma
  • lemma thmcounterlemma
  • lemma thmcounterlemma
  • theorem thmcountertheorem
  • theorem thmcountertheorem
  • theorem thmcountertheorem
  • ...and 21 more