Integer Reasoning Modulo Different Constants in SMT

TL;DR

This paper introduces a novel refutation procedure for multimodular integer constraints in SMT, improving verification of cryptographic protocols by exploiting algebraic structure and sharing information across modules.

Contribution

It proposes a new method that partitions constraints by modulus and uses lifting/lowering techniques with algebraic tools to enhance SMT solving for cryptography.

Findings

Outperforms existing solvers in cryptographic verification tasks

Effective in verifying Montgomery arithmetic and zero-knowledge proofs

Leverages algebraic structures for improved reasoning

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\"obner 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.