💻 computer science

Game Hopping in Lean

Dit artikel introduceert HOPSCOTCH, een Lean 4-framework dat computationeel correcte, op spel gebaseerde cryptografische bewijzen mechaniseert met behulp van een shallow embedding en een state-abstractie-methodologie om complexe beveiligingseigenschappen zoals de GGM-constructie en IND-CCA-beveiliging formeel te verifiëren.

Oorspronkelijke auteurs: Stefan Dziembowski, Grzegorz Fabiański, Daniele Micciancio, Rafał{} Stefański

Gepubliceerd 2026-08-07

📖 8 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Stefan Dziembowski, Grzegorz Fabiański, Daniele Micciancio, Rafał{} Stefański

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een meester-slotenmaker bent die wil bewijzen dat je nieuwe kluis onbreekbaar is. Je zegt niet alleen: "Hij is sterk!" Je moet een reeks stappen laten zien: "Als je dit kleine slotje niet kunt breken, kun je de deur niet breken; als je de deur niet kunt breken, kun je de kluis niet breken." Dit is hoe moderne cryptografie werkt. Experts gebruiken "spelletjes" om de beveiliging te testen, waarbij een hacker probeert een geheim te raden, en de veiligheid van een systeem wordt bewezen door aan te tonen dat het breken ervan net zo moeilijk is als het oplossen van een bekende, onmogelijke puzzel. Maar hier komt de crux bij: deze bewijzen met de hand leveren is als proberen een kaartenhuis in balans te houden tijdens een orkaan. Het is gemakkelijk om een kleine fout te maken, een subtiele opening te missen, of de controle te verliezen door de complexiteit, en als je één stap mist, stort het hele bewijs in. Daarom zoeken wetenschappers naar een manier om een computer elke kaart te laten controleren, om ervoor te zorgen dat het kaartenhuis overeind blijft.

Dit is waar het papier om de hoek komt kijken. De auteurs hebben een digitale werkplaats gebouwd genaamd HOPSCOTCH (een speelse naam voor een spel van huppelen) binnen een krachtig computerprogramma genaamd Lean 4. Zie HOPSCOTCH als een super slimme, robotachtige corrector die niet alleen je wiskunde controleert; hij begrijpt het verhaal van het beveiligingsbewijs. In plaats van cryptografen te dwingen in een vreemde, beperkte taal te schrijven, laat HOPSCOTCH hen bewijzen schrijven met dezelfde instrumenten die ze voor al hun andere wiskunde gebruiken. Het verandert het "game-hopping"-proces — het springen van het ene beveiligingsscenario naar het volgende — in een helder, stapsgewijs object dat de computer kan inspecteren, verifiëren en zelfs kan automatiseren. De auteurs hebben niet alleen het hulpmiddel gebouwd; ze hebben het succesvol gebruikt om de veiligheid van verschillende beroemde encryptiemethoden te bewijzen, inclus_of een complexe constructie genaamd GGM, waarmee ze laten zien dat deze "robotachtige corrector" complexe cryptografische uitdagingen uit de echte wereld aankan zonder in de war te raken.

Het Grote Plaatje: Waarom we een Correctierobot Nodig Hebben

In de wereld van digitale beveiliging vertrouwen we op "bewijsbare veiligheid". Dit betekent dat we niet alleen hopen dat onze codes veilig zijn; we proberen het te bewijzen. De standaardmanier om dit te doen is de "game-based" benadering. Stel je een beveiligingsbewaker (het systeem) en een inbreker (de tegenstander) voor. De bewaker heeft een geheim, en de inbreker probeert het te raden. Om te bewijzen dat de bewaker veilig is, zeggen we niet alleen "hij is goed." We creëren een reeks "spelletjes" of scenario's.

Het Echte Spel: De inbreker probeert het werkelijke systeem te breken.
De Sprong (The Hop): We stellen ons een iets ander spel voor dat bijna hetzelfde is, maar makkelijker te analyseren. We bewijzen dat als de inbreker het Echte Spel kan winnen, hij ook dit nieuwe, iets andere spel kan winnen.
De Keten: We blijven van het ene spel naar het andere springen, waarbij we de regels telkens een klein beetje veranderen, totdat we een definitief spel bereiken dat overduidelijk onmogelijk te winnen is (zoals een miljoen keer achter elkaar een muntje goed raden).

Als we kunnen bewijzen dat elke enkele "sprong" veilig is, dan is de hele keten veilig. Dit wordt een "game-hopping bewijs" genoemd.

Het probleem is dat mensen hier niet goed in zijn om het perfect te doen. Deze bewijzen zijn lang, rommelig en vol met minuscule details. Een enkel gemist detail kan het hele bewijs onjuist maken, en het systeem onveilig. Jarenlang hebben onderzoekers geprobeerd speciale computertools te bouwen om deze bewijzen te controleren, maar deze tools spreken vaak een andere taal dan de wiskundigen. Ze zijn als een vertaler die alleen "Beveiliging" spreekt maar niet "Wiskunde", waardoor experts gedwongen worden hun ideeën heen en weer te vertalen, wat traag en foutgevoelig is.

Enter HOPSCOTCH: De Universele Vertaler

De auteurs van dit artikel, Stefan Dziembowski, Grzegor Fabiański, Daniele Micciancio en Rafał Stefański, besloten een brug te bouwen. Ze creëerden HOPSCOTCH, een framework binnen Lean 4, een populair computerprogramma dat wordt gebruikt om wiskundige bewijzen te verifiëren.

Hier is de magie van HOPSCOTCH:

Geen Nieuwe Taal: In tegen tegenstelling tot andere tools die je dwingen een nieuwe, beperkte manier van coderen te leren, laat HOPSCOTCH je bewijzen schrijven met standaard Lean. Het is alsof je een chef toestaat om te koken met zijn eigen favoriete messen in plaats van hem te dwingen met plastic messen te werken.
Bewijzen als Objecten: In HOPSCOTCH is een bewijs niet zomaar een hoop tekst. Het is een gestructureerd object, zoals een Lego-model. Elke "hop" in het spel is een specifieke Lego-steen. Je kunt ze aan elkaar klikken, en de computer controleert of ze perfect passen. Als je probeert twee stenen te verbinden die niet bij elkaar passen, zegt de computer: "Nee, dat werkt niet."
De "Abstractie"-truc: Een van de moeilijkste delen van deze bewijzen is aantonen dat twee verschillend uitziende systemen zich exact hetzelfde gedragen. HOPSCOTCH gebruikt een slimme truc genaamd "state abstraction" (toestandsabstractie). Stel je voor dat je twee robots hebt. De een heeft een rommelig intern bedradingsschema, en de ander heeft een net schema. HOPSCOTCH stelt je in staat om een kaart (een abstractiefunctie) te tekenen die laat zien hoe de rommelige draden overeenkomen met de nette draden. Als de kaart correct is, weet de computer dat de robots identiek gedrag vertonen, zelfs als ze er van binnen anders uitzien.

Wat Ze Eigenlijk Deden en Vonden

De auteurs hebben het hulpmiddel niet alleen gebouwd; ze hebben het op de proef gesteld. Ze gebruikten HOPSCOTCH om de veiligheid van vier belangrijke cryptografische concepten formeel te verifiëren:

Encrypt-then-MAC: Een methode om berichten zowel geheim als bestand tegen manipulatie te maken. Ze bewezen dat als de onderliggende encryptie en de "tagging" (MAC) veilig zijn, het geheel veilig is tegen zelfs de slimste hackers.
ElGamal Encryptie: Een beroemde manier om geheime berichten te verzenden met behulp van publieke sleutels. Ze lieten zien hoe je de veiligheid ervan kunt bewijzen op basis van een moeilijk wiskundig probleem genaamd de Decisional Diffie-Hellman (DDH) assumptie.
One-Time Secrecy naar IND-CPA: Ze bewezen dat als een systeem veilig is voor een enkele boodschap, het veilig kan worden gemaakt voor vele boodschappen, een cruciale stap bij het bouwen van robuuste encryptie.
De GGM Constructie: Dit is de grote klapper. De GGM-methode zet een eenvoudige willekeurige getallengenerator om in een complexe "pseudorandom function" (een nep-willekeurige getallengenerator die echt lijkt). Eerdere computerbewijzen konden alleen zeer ondiepe versies aan (zoals een boom met 3 stappen). De auteurs gebruikten HOPSCOTCH om de veiligheid van GGM te bewijzen voor niet-constante diepte, wat betekent dat het werkt voor bomen van elke grootte. Naar hun weten is dit de eerste keer dat een algemeen bruikbare computer-proof assistant succesvol deze specifieke, complexe constructie heeft geverifieerd.

Hoe Ze Het Deden (De "Game" Mechanica)

Het artikel legt uit dat HOPSCOTCH werkt door het bewijs af te breken in specifieke stappen, of "constructors":

Observationele Equivalentie: Bewijzen dat twee spelletjes er voor een buitenstaander hetzelfde uitzien.
Reducties: Laten zien dat als je Spel A kunt breken, je ook Spel B kunt breken.
Hybride Sequenties: Het aan elkaar ketenen van vele kleine stappen.

Het framework bevat "tactics" (geautomatiseerde helpers) die proberen deze stappen voor je op te lossen. Als je bijvoorbeeld moet bewijzen dat twee oracles (de spelsystemen) hetzelfde zijn, kan de computer automatisch proberen een "state abstraction" kaart te vinden. Als dat niet lukt, laat de computer de stap over aan de mens, maar behoudt de computer de structuur zodat de mens precies weet waar hij zich bevindt.

De auteurs bewezen ook een "computationele geldigheidstelling" (computational soundness theorem). Dit is een chique manier om te zeggen: "Als de computer zegt dat dit bewijs geldig is, dan is het ook daadwerkelijk geldig in de echte wereld." Ze lieten zien dat voor elk bewijsobject dat HOPSCOTCH creëert, je wiskundig precies kunt berekenen hoeveel "voordeel" (advantage) een hacker zou hebben, gebaseerd op de assumpties die in het bewijs worden gebruikt. Dit zorgt ervoor dat de computer niet alleen een spelletje met zichzelf speelt; het geeft een reële, concrete veiligheidsgarantie.

De Kern van het Verhaal

Het artikel concludeert dat HOPSCOTCH erin slaagt de kloof te overbruggen tussen het gemak van gespecialiseerde beveiligingstools en de kracht van algemene wiskundige assistenten. Het stelt cryptografen in staat om bewijzen te schrijven die gemakkelijker te lezen, gemakkelijker te controleren en minder foutgevoelig zijn voor menselijke fouten. Hoewel de auteurs toegeven dat de computer nog niet controleert of de "hacker" snel genoeg draait (een technisch detail genaamd polynomiale tijd), hebben ze de basis gelegd voor volledig geautomatiseerde, betrouwbare beveiligingsbewijzen.

Ze geven ook een hint naar de toekomst: met deze gestructureerde bewijsobjecten zou het binnenkort mogelijk kunnen zijn om AI te gebruiken om te helpen deze bewijzen automatisch te schrijven, of om het systeem uit te breiden om zelfs complexere scenario's aan te pakken die te maken hebben met "slechte gebeurtenissen" en waarschijnlijkheid. Maar voor nu is de belangrijkste prestatie duidelijk: ze hebben een betrouwbare, flexibele en krachtige manier gebouwd om computers te laten helpen bewijzen dat onze digitale geheimen veilig zijn.

=== SAMENVATTING ===

Technische Samenvatting: Game Hopping in Lean

Probleemstelling

Moderne cryptografie leunt zwaar op het paradigma van bewijsbare veiligheid, die doorgaans wordt geformaliseerd via computationele game-gebaseerde definities. In dit kader wordt veiligheid vastgesteld door een reeks "game hops" (of hybride argumenten) te construeren die het voordeel van een tegenstander terugbrengen naar bekende harde computationele problemen. Echter, handmatige game-gebaseerde bewijzen zijn berucht foutgevoelig, monolithisch complex en gevoelig voor subtiele hiaten.

Hoewel domeinspecifieke tools zoals EasyCrypt en CryptoVerif succesvol grote klassen van deze reducties hebben geautomatiseerd, opereren zij buiten algemene interactieve stellingbewijzers. Dit dwingt ontwikkelaars tot een keuze: de geautomatiseerde eenvoud van gespecialiseerde tools versus de fundamentele expressiviteit en betrouwbaarheid van algemene stellingbewijzers zoals Lean. Bestaande algemene frameworks missen vaak de specifieke structurele ondersteuning die nodig is om de expliciete stappen van een game-hopping argument als eerste-orde objecten te representeren.

Methodologie: Het HOPSCOTCH-framework

De auteurs presenteren HOPSCOTCH, een Lean 4-framework ontworpen om computationeel geloofwaardige, game-gebaseerde cryptografische bewijzen te mechaniseren. Het framework overbrugt de kloof tussen gespecialiseerde automatisering en algemene verificatie via de volgende methodologische pijlers:

1. Shallow Embedding en Oracle Indistinguishability

HOPSCOTCH maakt gebruik van een shallow embedding: oracles, reducties en tegenstanders worden gedefinieerd als gewone Lean-functies en types in plaats van een aparte domeinspecifieke taal.

Veiligheidsdefinities: Veiligheidsconcepten worden uitgedrukt als ononderscheidbaarheid tussen stateful probabilistische oracles. Een oracle wordt gemodelleerd als een stateful procedure die queries beantwoordt, gerepresenteerd met behulp van de RState monad (StateT over Probability Mass Functions).
Reducties: Oracle-reducties worden gemodelleerd als abstracte berekeningen (OracleComp) die een onderliggend oracle kunnen bevragen terwijl ze hun eigen staat behouden. Compositie wordt afgehandeld via een simulateQ-operatie, aangeduid met de ruit-notatie ( $R \diamond O$ ).

2. Expliciete Bewijsobjecten

In tegenstelling tot standaard Lean-bewijzen, die vaak ongestructureerde scripts zijn, is een HOPSCOTCH-bewijs een expliciet formeel object van het type IndistinguishabilityI. De constructoren van dit inductieve type komen direct overeen met de stappen van een game-hopping argument:

obsEq: Hops gebaseerd op observationele equivalentie (semantische identiteit).
reduction: Hops verkregen door een oracle-reductie toe te passen op beide zijden van een ononderscheidbaarheidsverklaring.
assumption: Hops gerechtvaardigd door een cryptografische aanname (een paar ononderscheidbare oracles).
symm en trans: Structurele regels voor symmetrie en transitiviteit.
longSequence: Een constructor voor hybride argumenten waarbij de lengte van de sequentie afhangt van parameters (bijv. de veiligheidsparameter $\kappa$ of query-bounds), in plaats van vast te staan.

3. Observationele Equivalentie via Abstractie

Om te bewijzen dat twee oracles observationeel equivalent zijn (d.w.z. ononderscheidbaar door elke waarnemer), maakt HOPSCOTCH gebruik van een state-abstractiemethodologie. In plaats van te vertrouwen op complexe relationele programmalogica, levert de gebruiker een abstractiefunctie die de staat van het ene oracle in kaart brengt naar de staat van het andere oracle.

Deterministische Abstractie: Een functie $f: S_1 \to S_2$ die initiële staten behoudt en commuteert met query-transities.
Randomized Abstractie: Een functie $f: S_1 \to \text{PMF}(S_2)$ die probabilistische staatstransformaties afhandelt, zoals het vervangen van eager sampling door deferred sampling.
Deze aanpak ondersteunt veelvoorkomende bewijspatronen zoals het vergeten van irrelevante staat, het introduceren van redundante staat en het herschikken van staat.

4. Automatisering en Tactics

Het framework bevat domeinspecifieke tactics, primair game_hopping, die de constructie van bewijsobjecten automatiseert.

De tactic accepteert een lijst met tussenliggende oracles en genereert subgoals voor aangrenzende hops.
Het probeert deze subgoals automatisch op te lossen door reductiepatronen te herkennen of state-abstractie lemmas toe te passen.
Indien automatisering faalt, kan de gebruiker handmatig de abstractiefunctie leveren met behulp van by_abstraction of by_rand_abstraction.

5. Computationele Soundness

Het framework bewijst een algemene computationele soundness theorem. Dit theorem interpreteert het expliciete bewijsobject door concrete reducties te construeren tegen de aannames die in het bewijs worden gebruikt.

Voor elke distinguisher tegen de eind-oracles, construeert het theorem een distinguisher voor elke aanname die in het bewijs wordt gebruikt.
Het leidt een concrete bovengrens af voor het oorspronkelijke voordeel als een som van de voordelen tegen de aannames, gewogen door het aantal keren dat elke aanname wordt gebruikt (rekening houdend met symmetrie-omkeringen).
Het framework formaliseert de polynomiale tijdcomplexiteit niet formeel binnen Lean; in plaats daarvan vertrouwt het op concrete veiligheidsbounds en externe verificatie van het polynomiale karakter van de geconstrueerde reducties.

Belangrijkste Bijdragen en Resultaten

Het paper demonstreert het nut van HOPSCOTCH door verschillende representatieve cryptografische bewijzen te formaliseren:

IND-RAND naar IND-CPA: Een formeel bewijs dat real-or-random veiligheid ononderscheidbaarheid onder een chosen-plaintext attack impliceert, wat het gebruik van oracle-reducties en observationele equivalentie illustreert.
Encrypt-then-MAC: Een bewijs van IND-CCA veiligheid voor de Encrypt-then-MAC constructie. Deze casestudy benadrukt het gebruik van reshuffling abstracties (het herverpakken van staat) en redundancy introductions (bewijzen van equivalentie wanneer staatvelden worden gedupliceerd).
ElGamal Encryption: Een bewijs van veiligheid gebaseerd op de Decisional Diffie-Hellman (DDH) aanname. Deze casestudy maakt gebruik van forgetting irrelevant information en deferred randomness (deferred vs. eager sampling) abstracties, naast groepsspecifieke vereenvoudigingslemata.
One-Time Secrecy naar IND-CPA: Een bewijs dat one-time secrecy publieke-sleutel IND-CPA veiligheid impliceert. Dit maakt gebruik van bounded observational equivalence en long sequences waarbij de lengte van het hybride argument afhankelijk is van de adversary's query bound.
GGM Pseudorandom Function Constructie: Een formalisering van de GGM-constructie die een PRG transformeert naar een PRF.
- Dit bewijs bevat een hybride sequentie van lengte $\kappa$ (de veiligheidsparameter).
- Het past de deferred-randomness idiom toe op volledige caches van willekeurige labels in plaats van enkelvoudige waarden.
- Significantie: Naar weten van de auteurs is dit het eerste gemachinisde bewijs van de GGM-constructie voor niet-constante diepte in een algemene stellingbewijzer (vorig werk door CryptoZoo formaliseerde diepte 3).

Significantie en Claims

De auteurs beweren dat HOPSCOTCH erin slaagt de kloof te overbruggen tussen gespecialiseerde game-hopping tools en algemene stellingbewijzers. De significantie ligt in:

Fundamentele Betrouwbaarheid: Door gebruik te maken van de Lean-kernel en het volledige Mathlib-ecosysteem (inclusief finite-group theory), garandeert het framework dat bewijzen geworteld zijn in een vertrouwde basis, in tegen tegenstelling tot domeinspecifieke tools die vertrouwen op aangepaste checkers.
Expliciete Structuur: Het representeren van bewijzen als expliciete objecten maakt betere inspectie, automatisering en de afleiding van concrete veiligheidsbounds mogelijk die het gebruik van aannames bijhouden.
Expressiviteit: Het framework ondersteunt parameter-afhankelijke hybride argumenten en complexe staatstransformaties (via randomized abstraction) die moeilijk te modelleren zijn in andere systemen.
Automatisering: De combinatie van expliciete bewijsobjecten en domeinspecifieke tactics vermindert boilerplate, waardoor formele bewijzen korter en leesbaarder worden terwijl de kracht van algemene automatisering behouden blijft.

Het paper concludeert dat hoewel het nog niet volledig de asymptotische polynomiale tijdcomplexiteit formaliseert (dit als een externe conditie laat), de concrete veiligheidsbounds die door het soundness theorem worden geleverd, voldoende zijn om standaard asymptotische begrippen te herstellen onder redelijke externe aannames. De auteurs beschouwen het framework als een veelbelovend doelwit voor toekomstige machine-assisted bewijsgeneratie en de integratie van error-bounded transities.