Integer Reasoning Modulo Different Constants in SMT
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918027951341568 |
|---|---|
| author | Pertseva, Elizaveta Ozdemir, Alex Pailoor, Shankara Bassa, Alp Porncharoenwase, Sorawee Dillig, Işil Barrett, Clark |
| author_facet | Pertseva, Elizaveta Ozdemir, Alex Pailoor, Shankara Bassa, Alp Porncharoenwase, Sorawee Dillig, Işil Barrett, Clark |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_14998 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Integer Reasoning Modulo Different Constants in SMT Pertseva, Elizaveta Ozdemir, Alex Pailoor, Shankara Bassa, Alp Porncharoenwase, Sorawee Dillig, Işil Barrett, Clark Logic in Computer Science 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. |
| title | Integer Reasoning Modulo Different Constants in SMT |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2505.14998 |