A proof complexity perspective on effectively zero-knowledge proofs

Technische Samenvatting: Een Bewijskomplexiteitperspectief op Effectief Zero-Knowledge Bewijzen

Probleemstelling
Het artikel behandelt het concept van "effectief zero-knowledge" (ZK) bewijzen, een variant geïntroduceerd door Ilango [4] die steunt op ideeën uit de mathematische logica. De oorspronkelijke formulering van Ilango vermeed standaard logische begrippen (zoals theorieën, bewijsbaarheid en consistentie) ten gunste van algoritmische simulaties. Het artikel identificeert een specifieke beperking in de definitie van Ilango: de eigenschap dat een bewijs "ononderscheidbaar van waar" is, is direct in de definitie van de bewijzer (prover) ingebed in plaats van er een gevolg van te zijn. Bovendien rust de constructie van effectief ZK-bewijzen op vermoedens uit zowel de cryptografie als de bewijskomplexiteit, met name met betrekking tot het bestaan van harde propositionele tautologieën voor specifieke bewijssystemen. Het artikel streeft ernaar dit concept te herformuleren met behulp van de taal van de logica en bewijskomplexiteit om eenvoudigere bewijzen van existentie te leveren en om de relatie tussen de definitie van de bewijzer en de "ononderscheidbaarheidseigenschap" te verhelderen.

Methodologie
De auteur maakt gebruik van het kader van bewijskomplexiteit en begrensde rekenkunde (bounded arithmetic), waarbij specifiek gebruik wordt gemaakt van theorieën die in staat zijn om te redeneren over berekeningen en bewijzen (zoals $S^1_2$ en $S_2$). De methodologie omvat:

1. Logische Herformulering: Het vervangen van algoritmische simulaties door formele theorieën $T$ en hun uitbreidingen $T^*$. De bewijzer wordt gedefinieerd relatief aan een theorie $T$, en de ZK-eigenschap wordt gekarakteriseerd door het niet-bestaan van korte bewijzen binnen $T$ voor het niet-bestaan van een simulator.
2. Modeltheorie van Rekenkunde: De bewijzen maken gebruik van niet-standaard modellen van rekenkunde en het "overspill-principe". Specifiek leunt het artikel op een stelling van K.-Pudlák [13] die het niet-bestaan van korte propositionele bewijzen in een bewijssysteem $P(T)$ koppelt aan de existentie van uitbreidingen van modellen van begrensde rekenkunde waar bepaalde formules bevredigbaar zijn.
3. Bewijskomplexiteitsgeneratoren: In de laatste sectie onderzoekt het artikel het transformeren van effectief ZK-bewijzen naar "echte" zero-knowledge bewijzen. Dit wordt bereikt door de sequentie van harde tautologieën $\Psi$ te vervangen door bewijskomplexiteitsgeneratoren. De constructie gaat uit van het bestaan van "demi-bits" (een type harde generator gedefinieerd door Rudich [16]) en staat toe dat de bewijzer en de verifieerder een gemeenschappelijke willekeurige reeks (common random string) delen.

Belangrijkste Bijdragen en Resultaten

• Herformulering van de Bewijzer: Het artikel definieert een bewijzer $Prover[A, B, \Psi]$ relatief aan een theorie $T$. De ZK-eigenschap wordt niet gedefinieerd door het onmiddellijke bestaan van een simulator, maar door de voorwaarde dat voor elke polynoomgrootte $d$, de theorie $T$ niet kan bewijzen (met bewijzen van super-polynomiale grootte) dat er geen simulator van grootte $n^d$ bestaat.
• Afleiding van "Ononderscheidbaarheid van Waar": Een primair resultaat (Theorem 2.4) toont aan dat de eigenschap van "ononderscheidbaar van waar" een gevolg is van de ZK-definitie relatief aan een theorie, in plaats van een vereiste. Als een bewering $S(n)$ in $T$ bewijsbaar is als een gevolg van het bestaan van een simulator, en de bewijzer is ZK relatief aan $T$, dan moet $S(n)$ waar zijn voor alle behalve een eindig aantal $n$. Dit staat in contrast met de definitie van Ilango, waar dit deel uitmaakte van de axiomatische vereisten van de bewijzer.
• Existentiebewijs (Theorem 2.2): Het artikel bewijst dat indien $A, B$ een Non-Interactive Witness Indistinguishable (NIWI) schema vormen en de sequentie van tautologieën $\Psi$ hard is voor het bewijssysteem $P(T^*)$, de geconstrueerde bewijzer ZK is relatief aan $T$. Het bewijs maakt gebruik van niet-standaard modellen om aan te tonen dat het bestaan van een simulator consistent is met de theorie, waardoor korte bewijzen van het niet-bestaan ervan worden voorkomen.
• Transformatie naar Echte ZK (Sectie 3): Het artikel laat zien dat het concept van effectief ZK kan worden omgezet in standaard zero-knowledge bewijzen (waarbij een simulator daadwerkelijk bestaat) onder specifieke aannames. Door gebruik te maken van bewijskomplexiteitsgeneratoren afgeleid van "demi-bits" en door beide partijen een gemeenschappelijke willekeurige reeks te laten delen, kan de hardheid van de onderliggende formules uniform worden gegarandeerd. Dit omzeilt de noodzaak voor de bewijzer en verifieerder om een specifieke sequentie van tautologieën te vertrouwen zonder verificatie.

Betekenis en Claims
Het artikel beweert een "eenvoudig bewijs" te bieden voor de existentie en de belangrijkste eigenschappen van effectief zero-knowledge bewijzen door gebruik te maken van de logische structuur van bewijskomplexiteit. De betekenis ligt in:

1. Conceptuele Helderheid: Het verheldert de logische fundamenten van effectief ZK-bewijzen, door aan te tonen dat de "ononderscheidbaarheid van waar"-eigenschap een afleidbaar gevolg is van de definitie van de bewijzer relatief aan een theorie.
2. Bruggen Slaan tussen Logica en Cryptografie: Het verbindt expliciet het cryptografische begrip van witness indistinguishability met het logische begrip van modeluitbreidingen en het niet-bestaan van korte bewijzen.
3. Pad naar Standaard ZK: Het schetst een theoretisch pad om deze conditionele, op logica gebaseerde bewijzen te transformeren naar standaard zero-knowledge bewijzen, afhankelijk van het bestaan van harde bewijskomplexiteitsgeneratoren (specifiek demi-bits) en het gebruik van een gemeenschappelijke willekeurige reeks.

De auteur blijft bescheiden over de constructie van de harde sequenties zelf, waarbij wordt opgemerkt dat hoewel er vermoedens bestaan (bijv. over het bestaan van generatoren die hard zijn voor alle bewijssystemen), een bewijs dat een specifieke constructie werkt een openstaand probleem blijft in de bewijskomplexiteit. Het artikel dient als een theoretische verfijning en een brug tussen de logische formulering van ZK en standaard cryptografische definities.