~/talk

Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge

Talkat OOPSLA 2025 · 2025-10-16..10-18· [cryptography]
links:none on file
name:Shan Ali
links:none on file
links:none on file
links:none on file
slides:none on file

Crepe is a zero-knowledge protocol that encodes full regular-expression equivalence proofs (PSPACE-complete) using a custom calculus based on coinduction and derivatives, converts a derivative-search trace into a sound and complete proof tree, and validates committed proof steps on a proof VM with multiplexed rule-checkers. Evaluation generates proofs for 7,353 equivalent regex pairs (72 hit a 10-minute timeout) and shows large proofs validate in only a few seconds under the default multiplexing; Crepe hides values with commitments and trades speed versus security across multiplexing modes.

AI-written summary · about

  1. 0:00Introduction
  2. 1:25Zero knowledge regex equivalence
  3. 3:28Proof format and co-induction
  4. 7:05Proof generation and validation
  5. 9:11CREPE performance evaluation
  6. 10:55Related work and future
  7. 11:56Conclusion and Q&A
~/search
type to search 6,249 conferences, 138,987 speakers and 185,172 talks
~/help
cmdctrl k
search every conference, speaker and series
/
focus the filter search
h
home
c
conferences
s
speakers
e
series
t
light / dark — the status bar button does the same
?
this help
esc
close this, then clear every filter — or just the search, while you are typing in it

Ignored while you are typing. Pages without a filter rail have no search to focus.