A proof complexity perspective on effectively zero-knowledge proofs

Sintesi Tecnica: Una Prospettiva dalla Complessità della Dimostrazione sugli Approvanti a Conoscenza Effettivamente Nulla

Enunciato del Problema
Il saggio affronta il concetto di approvanti a conoscenza effettivamente nulla (zero-knowledge, ZK), una variante introdotta da Ilango [4] che si basa su idee della logica matematica. La formulazione originale di Ilango evitava le standard nozioni logiche (come teorie, dimostrabilità e coerenza) a favore di simulazioni algoritmiche. Il saggio identifica un limite specifico nella definizione di Ilango: la proprietà che una dimostrazione sia "indistinguibile dal vero" è incorporata direttamente nella definizione dell'approvante piuttosto che essere derivata come una conseguenza. Inoltre, la costruzione degli approvanti ZK effettivi si basa su congetture sia dalla crittografia che dalla complessità della dimostrazione, specificamente riguardo l'esistenza di tautologie proposizionali difficili per specifici sistemi di dimostrazione. Il saggio mira a riformulare questo concetto utilizzando il linguaggio della logica e della complessità della dimostrazione per fornire prove di esistenza più semplici e per chiarire la relazione tra la definizione dell'approvante e la proprietà di "indistinguibilità".

Metodologia
L'autore utilizza il framework della complessità della dimostrazione e dell'aritmetica limitata, utilizzando specificamente teorie capaci di ragionare su computazioni e dimostrazioni (come $S^1_2$ e $S_2$). La metodologia prevede:

1. Riformulazione Logica: Sostituzione delle simulazioni algoritmiche con teorie formali $T$ e le loro estensioni $T^*$. L'approvante è definito rispetto a una teoria $T$, e la proprietà ZK è caratterizzata dalla non esistenza di brevi dimostrazioni all'interno di $T$ per la non esistenza di un simulatore.
2. Modello della Teoria dell'Aritmetica: Le dimostrazioni utilizzano modelli non standard dell'aritmetica e il "principio di overspill". Nello specifico, il saggio si avvale di un teorema di K.-Pudlák [13] che collega la non esistenza di brevi dimostrazioni proposizionali in un sistema di dimostrazione $P(T)$ alla esistenza di estensioni di modelli di aritmetica limitata dove certe formule sono soddisfacibili.
3. Generatori di Complessità della Dimostrazione: Nella sezione finale, il saggio esplora la trasformazione degli approvanti ZK effettivi in approvanti a conoscenza nulla "genuini". Ciò viene ottenuto sostituendo la sequenza di tautologie difficili $\Psi$ con generatori di complessità della dimostrazione. La costruzione assume l'esistenza di "demi-bits" (un tipo di generatore difficile definito da Rudich [16]) e permette all'approvante e al verificatore di condividere una stringa casuale comune.

Contributi Chiave e Risultati

• Riformulazione dell'Approvante: Il saggio definisce un approvante $Prover[A, B, \Psi]$ rispetto a una teoria $T$. La proprietà ZK è definita non dalla immediata esistenza di un simulatore, ma dalla condizione che per ogni dimensione polinomiale $d$, la teoria $T$ non possa dimostrare (con dimostrazioni di dimensione super-polinomiale) che non esiste un simulatore di dimensione $n^d$.
• Derivazione di "Indistinguibilità dal Vero": Un risultato primario (Teorema 2.4) dimostra che la proprietà di essere "indistinguibile dal vero" è una conseguenza della definizione ZK rispetto a una teoria, piuttosto che un prerequisito. Se un'enunciazione $S(n)$ è dimostrabile in $T$ come conseguenza della esistenza di un simulatore, e l'approvante è ZK rispetto a $T$, allora $S(n)$ deve essere vera per tutti i casi tranne che per un numero finito di $n$. Questo contrasta con la definizione di Ilango dove ciò era parte dei requisiti assiomatici dell'approvante.
• Prova di Esistenza (Teorema 2.2): Il saggio dimostra che se $A, B$ formano uno schema Non-Interactive Witness Indistinguishable (NIWI) e la sequenza di tautologie $\Psi$ è difficile per il sistema di dimostrazione $P(T^*)$, allora l'approvante costruito è ZK rispetto a $T$. La prova utilizza modelli non standard per mostrare che l'esistenza di un simulatore è coerente con la teoria, impedendo così brevi dimostrazioni della sua non esistenza.
• Trasformazione in ZK Genuino (Sezione 3): Il saggio mostra che il concetto di ZK effettivo può essere convertito in standard approvanti a conoscenza nulla (dove un simulatore esiste effettivamente) sotto specifiche assunzioni. Utilizzando generatori di complessità della dimostrazione derivati da "demi-bits" e permettendo alle parti di condividere una stringa casuale comune, la difficoltà delle formule sottostanti può essere garantita uniformemente. Ciò evita la necessità che l'approvante e il verificatore si fidino di una specifica sequenza di tautologie senza verifica.

Significato e Rivendicazioni
Il saggio sostiene di offrire una "prova semplice" dell'esistenza e delle proprietà chiave degli approvanti a conoscenza effettivamente nulla sfruttando la struttura logica della complessità della dimostrazione. La sua significatività risiede in:

1. Chiarezza Concettuale: Chiarisce i fondamenti logici degli approvanti ZK effettivi, mostrando che la proprietà di "indistinguibilità dal vero" è una conseguenza derivabile dalla definizione dell'approvante rispetto a una teoria.
2. Collegamento tra Logica e Crittografia: Collega esplicitamente la nozione crittografica di indistinguibilità della testimonianza con la nozione logica di estensioni di modelli e la non esistenza di brevi dimostrazioni.
3. Percorso verso lo ZK Standard: Delinea un percorso teorico per trasformare questi approvanti condizionali, basati sulla logica, in approvanti a conoscenza nulla standard, subordinatamente all'esistenza di generatori difficili di complessità della dimostrazione (specificamente i "demi-bits") e all'uso di una stringa casuale comune.

L'autore rimane modesto riguardo alla costruzione delle sequenze difficili stesse, notando che, sebbene esistano congetture (ad esempio, riguardo l'esistenza di generatori difficili per tutti i sistemi di dimostrazione), una prova che una specifica costruzione funzioni rimane un problema aperto nella complessità della dimostrazione. Il saggio funge da raffinamento teorico e da ponte tra la formulazione logica dello ZK e le definizioni crittografiche standard.