Quantum Cryptography and Autoformalization in Lean

Nel mondo della comunicazione sicura, le serrature più affidabili non sono fatte di acciaio, ma delle leggi fondamentali della fisica. Questo è il regno della distribuzione quantistica delle chiavi, un metodo in cui due persone, tradizionalmente chiamate Alice e Bob, generano un codice segreto condiviso per proteggere i loro messaggi. A differenza della crittografia tradizionale, che si basa sulla difficoltà di risolvere complessi problemi matematici, questo approccio si basa sul fatto che misurare una minuscola particella di luce, o un fotone, la cambia inevitabilmente. Se una terza parte, un intercettatore di nome Eve, tenta di ascoltare, lascia una traccia rilevabile del suo intervento. Per decenni, gli scienziati hanno sviluppato protocolli per creare queste chiavi, ma dimostrare che questi sistemi siano veramente sicuri è stato un processo fragile. Le prove si basavano spesso su una catena di argomentazioni matematiche cucite insieme da diversi articoli, ognuno con il proprio set di assunzioni. Se un anello di quella catena era leggermente disallineato con un altro, o se un'assunzione nascosta era stata trascurata, l'intera garanzia di sicurezza poteva essere compromessa senza che nessuno se ne accorgesse.

Un team di ricercatori del Massachusetts Institute of Technology ha affrontato questa fragilità costruendo una prova di sicurezza partendo da zero utilizzando un programma informatico progettato per controllare la logica matematica. Si sono concentrati su un metodo specifico e ampiamente utilizzato chiamato protocollo BB84, che utilizza coppie di particelle entangled per generare chiavi. Invece di fidarsi di un essere umano per verificare che ogni passaggio della logica regga, hanno tradotto l'intero argomento di sicurezza in un linguaggio formale che un computer possa leggere e verificare con assoluta precisione. Il risultato è una prova verificata dalla macchina che non lascia spazio a lacune nascoste o assunzioni discordanti. Essa conferma che il protocollo rimane sicuro anche quando il numero di particelle scambiate è limitato, un vincolo comune nel mondo reale che spesso indebolisce le stime di sicurezza. Inoltre, lo stesso sistema informatico che ha verificato la prova è stato utilizzato per scoprire un nuovo limite matematico più stretto, che riduce la penalità della dimensione finita sul tasso di chiave.

I ricercatori hanno iniziato creando un linguaggio digitale all'interno del sistema informatico che imponga rigorosamente le regole delle operazioni locali e della comunicazione classica. Nel contesto della crittografia quantistica, ciò significa che il computer assicura che Alice e Bob possano eseguire solo azioni sulle proprie particelle e possano condividere informazioni solo attraverso canali pubblici, senza mai accedere magicamente ai dati privati l'uno dell'altro. Questo linguaggio funge da guardrail, impedendo il tipo di errori logici che possono sfuggire ai revisori umani. Ad esempio, in precedenti tentativi di formalizzare queste prove, un agente di intelligenza artificiale propose una volta un metodo in cui la chiave finale veniva creata combinando stringhe che nessuna delle due parti possedeva effettivamente. Le regole rigide del computer segnalarono immediatamente l'impossibilità di ciò, costringendo il team a perfezionare il proprio approccio. Costruendo il protocollo passo dopo passo all'interno di questo ambiente vincolato, il team ha garantito che il teorema di sicurezza finale descrivesse esattamente il processo fisico che intendevano proteggere.

Una volta costruito il protocollo, il team ha chiesto al computer di verificare la sua sicurezza contro un tipo potente di attacco noto come attacco coerente, in cui un intercettatore interagisce con tutte le particelle simultaneamente anziché una alla volta. Il computer ha controllato ogni passaggio logico, dalla misurazione iniziale delle particelle fino ai passaggi finali di correzione degli errori e amplificazione della privacy. Ha confermato che il protocollo è sicuro, il che significa che, se il sistema non abortisce, la chiave risultante è indistinguibile da una chiave segreta perfetta e casuale, anche per un intercettatore con potenza di calcolo illimitata. Fondamentalmente, la prova ha tenuto conto del fatto che i sistemi reali operano con un numero finito di particelle, non con un flusso infinito. Questo effetto della dimensione finita solitamente costringe gli scienziati a essere eccessivamente conservativi, scartando più materiale di chiave potenziale per garantire la sicurezza. La nuova prova, tuttavia, ha fornito un calcolo preciso di quanto materiale di chiave possa essere mantenuto in sicurezza, riducendo la penalità imposta da questi limiti finiti.

In una svolta sorprendente, i ricercatori hanno utilizzato lo stesso sistema informatico non solo per verificare il proprio lavoro, ma per migliorarlo. Mentre il sistema controllava la logica, ha aiutato il team a identificare un limite più stretto sulla varianza dell'entropia condizionale utilizzata per stimare la sicurezza di questi sistemi. La formula esistente era troppo larga, portando a una riduzione non necessaria della lunghezza della chiave segreta. Il team, guidato dalla capacità del computer di testare e confrontare diversi limiti matematici, ha derivato una nuova disuguaglianza più precisa. Questo nuovo limite è più stretto, permettendo al sistema di generare chiavi con una penalità della dimensione finita ridotta rispetto a quanto avrebbe permesso la vecchia formula, senza sacrificare la sicurezza. Questa scoperta non è stata un indovino, ma un risultato matematico rigoroso che il computer ha verificato come vero, dimostrando che i motori di prova formale possono fare di più che controllare il lavoro: possono attivamente accelerare la scoperta scientifica trovando soluzioni migliori a vecchi problemi.

Il lavoro funge anche da modello per come dovrebbero essere validati i futuri sistemi crittografici. Rilasciando la libreria sottostante di definizioni e teoremi come open source, i ricercatori hanno fornito un toolkit riutilizzabile per la comunità. Questa libreria include le definizioni formali di stati quantistici, canali e il linguaggio specifico per descrivere i protocolli, consentendo ad altri scienziati di costruire su questa base. Ciò significa che le future prove per diversi protocolli quantistici, o anche per altre aree della scienza dell'informazione quantistica, possono essere costruite con lo stesso livello di rigore. Il team ha dimostrato che combinando l'intuizione umana con la implacabile precisione della logica verificata dalla macchina, è possibile eliminare le incertezze nascoste che hanno a lungo afflitto il campo. Il risultato è un nuovo standard per gli argomenti di sicurezza, in cui l'affidabilità di una chiave quantistica non è solo un'affermazione fatta da un ricercatore, ma un fatto verificato da una macchina.