FVQKD: verifica formale della sicurezza della distribuzione quantistica delle chiavi in Rocq

Abstract degli autori

La distribuzione quantistica delle chiavi (QKD), la cui sicurezza deriva dalla meccanica quantistica anziché da ipotesi computazionali, sta entrando nella fase di standardizzazione e di adozione commerciale. Eppure le sue garanzie di sicurezza si fondano su dimostrazioni tecnicamente delicate, verificate a mano. La verifica formale colma questa lacuna, offrendo una duplice garanzia: sicurezza incondizionata basata su principi fisici e dimostrazioni verificate da una macchina per escludere errori di ragionamento. Presentiamo FVQKD, una libreria Rocq per la verifica automatica delle dimostrazioni di sicurezza della QKD. Il suo primo risultato è una dimostrazione completa, dall’inizio alla fine e verificata da una macchina, della sicurezza composabile di BB84 per chiavi di lunghezza finita. La formalizzazione ricostruisce dai principi fondamentali l’intero apparato necessario alla dimostrazione, compresi il quadro delle entropie lisce, la relazione di incertezza entropica e il Quantum Leftover Hash Lemma. Porta alla luce condizioni necessarie che l’argomentazione pubblicata lascia implicite, una delle quali rivela un ramo mancante nella dimostrazione, e fonda il limite della teoria dell’informazione su una semantica formale dell’esecuzione del protocollo, assente nell’analisi svolta su carta. La dimostrazione non ricorre in alcun punto ad admit e si basa soltanto sul kernel di Rocq e su assiomi fondazionali standard. Per quanto ne sappiamo, è la prima verifica formale completa, dall’inizio alla fine, di una dimostrazione di sicurezza della QKD. Basato su MathComp, MathComp-Analysis e CoqQ, il lavoro mette a disposizione un’infrastruttura per l’informazione quantistica progettata per essere riutilizzata in varianti più ampie della QKD e in applicazioni della crittografia quantistica.