Quantum Cryptography and Autoformalization in Lean

In de wereld van veilige communicatie zijn de meest vertrouwde sloten niet gemaakt van staal, maar van de fundamentele wetten van de fysica. Dit is het domein van quantum key distribution (kwantumtoetsverdeling), een methode waarbij twee personen, traditioneel Alice en Bob genoemd, een gedeelde geheime code genereren om hun berichten te beschermen. In tegenstelling tot traditionele encryptie, die steunt op de moeilijkheid van het oplossen van complexe wiskundige problemen, steunt deze aanpak op het feit dat het meten van een minuscuul lichtdeeltje, of een foton, onvermijdelijk verandert. Als een derde partij, een meeluisteraar genaamd Eve, probeert mee te luisteren, laat zij een detecteerbaar spoor van haar interferentie achter. Decennialang hebben wetenschappers protocollen ontwikkeld om deze sleutels te creëren, maar het bewijzen dat deze systemen werkelijk veilig zijn, is een fragiel proces geweest. De bewijzen vertrouwden vaak op een keten van wiskundige argumenten die aan elkaar waren genaaid uit verschillende artikelen, elk met een eigen reeks aannames. Als één schakel in die keten enigszins niet overeenkwam met een andere, of als een verborgen aanname werd over het hoofd gezien, kon de gehele beveiligingsgarantie in gevaar komen zonder dat iemand het merkte.

Een team onderzoekers aan het Massachusetts Institute of Technology heeft deze kwetsbaarheid nu aangepakt door een beveiligingsbewijs vanaf de grond op te bouberen met behulp van een computerprogramma dat ontworpen is om wiskundige logica te controleren. Ze richtten zich op een specifieke, veelgebruikte methode genaamd het BB84-protocol, dat paren verstrengelde deeltjes gebruikt om sleutels te genereren. In plaats van te vertrouwen op een mens om te verifiëren of elke stap van de logica standhoudt, hebben zij het volledige beveiligingsargument vertaald naar een formele taal die een computer kan lezen en met absolute precisie kan verifiëren. Het resultaat is een door een machine gecontroleerd bewijs dat geen ruimte laat voor verborgen hiaten of niet-overeenstemmende aannames. Het bevestigt dat het protocol veilig blijft, zelfs wanneer het aantal uitgewikkelde deeltjes beperkt is, een veelvoorkomende realiteit in de praktijk die de beveiligingsinschattingen vaak verzwakt. Bovendien werd hetzelfde computersysteem dat het bewijs verifieerde, gebruikt om een nieuwe, strakkere wiskundige grens te ontdekken, die de eindige-omvang-straf (finite-size penalty) op de sleutelrate vermindert.

De onderzoekers begonnen met het creëren van een digitale taal binnen het computersysteem die de regels van lokale operaties en klassieke communicatie strikt afdwingt. In de context van kwantumcryptografie betekent dit dat de computer ervoor zorgt dat Alice en Bob alleen acties kunnen uitvoeren op hun eigen deeltjes en alleen informatie kunnen delen via publieke kanalen, zonder magisch toegang te krijgen tot elkaars privédata. Deze taal fungeert als een vangrail die het soort logische fouten voorkomt dat menselijke beoordelaars kan passeren. Bijvoorbeeld, in eerdere pogingen om deze bewijzen te formaliseren, stelde een kunstmatige intelligentie-agent ooit een methode voor waarbij de uiteindelijke sleutel werd gecreëerd door reeksen te combineren die geen van beide partijen daadwerkelijk bezat. De strikte regels van de computer markeerden dit onmiddellijk als onmogelijk, waardoor het team gedwongen werd hun aanpak te verfijnen. Door het protocol stap voor stap binnen deze beperkte omgeving op te bouwen, verzekerde het team dat het uiteindelijke beveiligingstheorema exact het fysieke proces beschreef dat zij beoogden te beschermen.

Zodra het protocol was geconstrueerd, vroeg het team de computer om de beveiliging ervan te verifiëren tegen een krachtig type aanval, bekend als een coherente aanval, waarbij een meeluisteraar met alle deeltjes tegelijkertijd interageert in plaats van één voor één. De computer controleerde elke logische stap, van de initiële meting van de deeltjes tot de laatste stappen van foutcorrectie en privacyversterking. Het bevestigde dat het protocol veilig is, wat betekent dat als het systeem niet wordt afgebroken, de resulterende sleutel ononderscheidbaar is van een perfecte, willekeurige geheime sleutel, zelfs voor een meeluisteraar met onbeperkte rekenkracht. Cruciaal is dat het bewijs rekening hield met het feit dat real-world systemen werken met een eindig aantal deeltjes, niet met een oneindige stroom. Dit eindige-omvang-effect dwingt wetenschappers meestal om overdreven conservatief te zijn en meer potentieel sleutelmateriaal weg te gooien om de veiligheid te garanderen. Het nieuwe bewijs bood echter een precieze berekening van hoeveel sleutelmateriaal veilig behouden kan worden, wat de straf opgelegd door deze eindige limieten vermindert.

In een verrassende wending gebruikten de onderzoekers dezelfde computerpijplijn niet alleen om hun werk te verifiëren, maar ook om het te verbeteren. Terwijl het systeem de logica controleerde, hielp het het team bij het identificeren van een strakkere grens op de variantie van de conditionele entropie die wordt gebruikt om de beveiliging van deze systemen in te schatten. De bestaande formule was te ruim, wat leidde tot een onnodige reductie in de lengte van de geheime sleutel. Het team, geleid door het vermogen van de computer om verschillende wiskundige grenzen te testen en te vergelijken, leidde een nieuwe, scherpere ongelijkheid af. Deze nieuwe grens is strakker, waardoor het systeem sleutels kan genereren met een verminderde eindige-omvang-straf vergeleken met wat de oude formule zou hebben toegestaan, zonder de beveiliging op te offeren. Deze ontdekking was geen gok, maar een rigoureus wiskundig resultaat dat de computer als waar heeft geverifieerd, wat aantoont dat formele bewijsengines meer kunnen dan alleen werk controleren—ze kunnen wetenschappelijke ontdekking actief versnellen door betere oplossingen voor oude problemen te vinden.

Het werk dient ook als een sjabloon voor hoe toekomstige cryptografische systemen gevalideerd moeten worden. Door de onderliggende bibliotheek van definities en stellingen als open source vrij te geven, hebben de onderzoekers een herbruikbare toolkit aan de gemeenschap verstrekt. Deze bibliotheek bevat de formele definities van kwantumtoestanden, kanalen en de specifieke taal voor het beschrijven van protocollen, waardoor andere wetenschappers op dit fundament kunnen voortbouwen. Dit betekent dat toekomstige bewijzen voor andere kwantumprotocollen, of zelfs voor andere gebieden van de kwantuminformatiewetenschap, met dezelfde mate van striktheid kunnen worden geconstrueerd. Het team heeft aangetoond dat door menselijk inzicht te combineren met de onverbiddelijke precisie van machine-gecontroleerde logica, het mogelijk is om de verborgen onzekerheden te elimineren die het veld al lang teisteren. Het resultaat is een nieuwe standaard voor beveiligingsargumenten, waarbij het vertrouwen in een kwantumsleutel niet slechts een bewering van een onderzoeker is, maar een feit dat door een machine is geverifieerd.