Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
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_ | 1866916671079317504 |
|---|---|
| author | Kolesar, John Ali, Shan Antonopoulos, Timos Piskac, Ruzica |
| author_facet | Kolesar, John Ali, Shan Antonopoulos, Timos Piskac, Ruzica |
| contents | Zero-knowledge (ZK) protocols enable software developers to provide proofs of their programs' correctness to other parties without revealing the programs themselves. Regular expressions are pervasive in real-world software, and zero-knowledge protocols have been developed in the past for the problem of checking whether an individual string appears in the language of a regular expression, but no existing protocol addresses the more complex PSPACE-complete problem of proving that two regular expressions are equivalent.
We introduce Crepe, the first ZK protocol for encoding regular expression equivalence proofs and also the first ZK protocol to target a PSPACE-complete problem. Crepe uses a custom calculus of proof rules based on regular expression derivatives and coinduction, and we introduce a sound and complete algorithm for generating proofs in our format. We test Crepe on a suite of hundreds of regular expression equivalence proofs. Crepe can validate large proofs in only a few seconds each. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_01198 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge Kolesar, John Ali, Shan Antonopoulos, Timos Piskac, Ruzica Cryptography and Security Logic in Computer Science Zero-knowledge (ZK) protocols enable software developers to provide proofs of their programs' correctness to other parties without revealing the programs themselves. Regular expressions are pervasive in real-world software, and zero-knowledge protocols have been developed in the past for the problem of checking whether an individual string appears in the language of a regular expression, but no existing protocol addresses the more complex PSPACE-complete problem of proving that two regular expressions are equivalent. We introduce Crepe, the first ZK protocol for encoding regular expression equivalence proofs and also the first ZK protocol to target a PSPACE-complete problem. Crepe uses a custom calculus of proof rules based on regular expression derivatives and coinduction, and we introduce a sound and complete algorithm for generating proofs in our format. We test Crepe on a suite of hundreds of regular expression equivalence proofs. Crepe can validate large proofs in only a few seconds each. |
| title | Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge |
| topic | Cryptography and Security Logic in Computer Science |
| url | https://arxiv.org/abs/2504.01198 |