💻 computer science

CrypFormBench: Benchmarking Formal Analysis Capability of Large Language Models for Cryptographic Schemes

Dit artikel introduceert CrypFormBench, een uitgebreide benchmark bestaande uit 700 instanties verspreid over 677 cryptografische schema's en 7 formele verificatietalen, om de huidige beperkingen van grote taalmodellen bij het genereren en corrigeren van formele beveiligingsbewijzen te evalueren en te onthullen, terwijl praktische strategieën worden geboden om hun prestaties te verbeteren.

Oorspronkelijke auteurs: Zhaoxuan Li, Qionglu Zhang, Hengyuan Liu, Xiaoyan Gu, Xianhui Lu, Hongbo Liu, Bingzheng Wang, Haihui Fan, Ziming Zhao, Rui Zhang, Li Zhou

Gepubliceerd 2026-06-25

📖 6 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Zhaoxuan Li, Qionglu Zhang, Hengyuan Liu, Xiaoyan Gu, Xianhui Lu, Hongbo Liu, Bingzheng Wang, Haihui Fan, Ziming Zhao, Rui Zhang, Li Zhou

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

Het Grote Plaatje: Het "Vertaler"-probleem

Stel je voor dat je een meesterarchitect bent die ongelooflijk veilige kluizen ontwerpt (cryptografische schema's). Je schrijft je blauwdrukken in gewoon Engels zodat iedereen het plan kan begrijpen. Echter, om deze kluizen daadwerkelijk te bouwen en te testen op zwakheden, moet je die Engelse blauwdrukken vertalen naar een zeer strikte, eeuwenoude en complexe taal die alleen specifieke, hoogtechnologische beveiligingsrobots (formele verificatietools zoals Scyther of Tamarin) begrijpen.

Deze vertaling is moeilijk. Het vereist een menselijke expert die zowel de kluisontwerpen als de strikte taal van de robot begrijpt. Als je één klein kommaatje mist of het verkeerde woord gebruikt, wijst de robot de blauwdruk af, of erger nog, hij bouwt een kluis die veilig lijkt maar een verborgen achterdeur heeft.

De Vraag: Kunnen Large Language Models (LLM's)—de AI-chatbots die we vandaag de dag gebruiken—als deze expert-vertalers fungeren? Kunnen ze een gewone Engelse beschrijving van een beveiligingsprotocol nemen en direct de perfecte, foutloze code schrijven voor de beveiligingsrobots?

Het Antwoord (volgens dit paper): Nog niet helemaal. Ze worden beter in lezen en repareren, maar ze worstelen nog steeds met het schrijven vanaf nul.

De Oplossing: CrypFormBench (De "Sportschool" voor AI)

Om precies uit te zoeken hoe goed deze AI-vertalers zijn, hebben de onderzoekers een enorme testomgeving gebouwd genaamd CrypFormBench (of C.F.B.).

Beschouw dit als een sportschool met 700 verschillende trainingsstations.

De Apparatuur: Ze hebben 700 echte beveiligingsprotocollen verzameld (zoals de protocollen die worden gebruikt in je telefoon, bankieren of het internet).
De Talen: Ze hebben deze protocollen vertaald naar 7 verschillende "robottalen" (formele talen zoals SPDL, HLPSL, EasyCrypt, etc.).
De Tests: Ze vroegen de AI niet alleen om code te schrijven. Ze testten vijf specifieke vaardigheden:
1. Interpretatie: "Hier is een robotcode; leg het aan mij uit in het Engels." (Lezen)
2. Generatie: "Hier is een Engelse beschrijving; schrijf de robotcode." (Schrijven vanaf nul)
3. Aanvulling: "Hier is een robotcode met gaten in; vul de lege plekken in." (Het werk van anderen gedeeltelijk herstellen)
4. Transformatie: "Hier is de code in Taal A; herschrijf het in Taal B." (Vertalen tussen robots)
5. Correctie: "Deze robotcode bevat een fout; los het op." (Debuggen)

De Resultaten: Het Rapportcijfer van de AI

De onderzoekers hebben 9 van de slimste beschikbare AI-modellen getest (waaronder GPT-4o, Claude-3.5 en DeepSeek). Dit is wat ze vonden:

1. De Vaardigheid "Goed in Lezen" (Interpretatie & Aanvulling)

Analogie: Stel je een student voor die heel goed is in het lezen van een tekstboek en de ontbrekende woorden in een zin kan invullen omdat de context al aanwezig is.
Resultaat: De AI's waren verrassend goed in dit. Wanneer ze een codegedeelte kregen met enkele ontbrekende delen, of gevraagd werd om uit te leggen wat een stuk code doet, presteerden ze erg goed. Ze begrepen de "grammatica" van de beveiligingstalen.

2. De Vaardigheid "Slecht in Schrijven" (Generatie & Transformatie)

Analogie: Stel je nu voor dat je diezelfde student vraagt om een heel nieuw tekstboek vanaf nul te schrijven, of om een boek van Frans naar Japans te vertalen zonder woordenboek. Ze beginnen te hallucineren, verzinnen regels of vergeten de strikte grammatica.
Resultaat: Hier faalden de AI's.
- Generatie: Wanneer de AI werd gevraagd een volledig beveiligingsprotocol te schrijven op basis van een gewone Engelse beschrijving, produceerden de meeste AI's code die de robots niet eens konden uitvoeren. Het was alsof er een zin werd geschreven met een kapotte syntaxis.
- Transformatie: Wanneer ze werden gevraagd om code van de ene robottaal naar de andere te vertalen, raakten de AI's vaak in de war. Ze mengden de regels van de twee talen door elkaar, waardoor er een "Frankenstein"-code ontstond die in geen van beide talen werkte.
- De Score: Zelfs de beste AI (Claude-3.5) scoorde slechts 48,7 van de 100. Dit betekent dat minder dan de helft van hun pogingen daadwerkelijk bruikbaar was voor de beveiligingstools.

3. De Vaardigheid "Repareren" (Correctie)

Analogie: Als je de student een zin geeft met een duidelijke typefout (bijv. "recieve" in plaats van "receive"), kunnen ze die gemakkelijk herstellen. Maar als de zin grammaticaal correct is maar logisch gezien fout zit (bijv. "De kluis staat open voor iedereen, maar hij is veilig"), dan worstelen ze om de logische fout te vinden.
Resultaat: De AI's waren goed in het oplossen van eenvoudige syntactische fouten (typefouten). Echter, ze hadden moeite met "semantische" fouten—het repareren van de logica van het beveiligingsprotocol zelf.

Waarom is dit zo moeilijk?

Het paper legt uit dat deze "robottalen" niet lijken op Python of Java. Ze zijn extreem strikt.

De "Eén Fout" Regel: Bij normaal programmeren kan het zijn dat de computer gewoon klaagt als je een puntkomma vergeet. In deze beveiligingstalen kan één ontbrekend woord de hele betekenis van het beveiligingsbewijs veranderen, waardoor een veilige kluis onveilig lijkt, of andersom.
Het "Context" Probleem: Deze protocollen hangen vaak af van lange ketens van gebeurtenissen (bijv. "Als Alice een bericht stuurt in stap 1, moet Bob in stap 2 reageren, maar alleen als hij nog geen bericht van stap 0 heeft gezien"). AI's raken vaak de draad kwijt in deze lange ketens.

Wat kunnen we doen? (De "Steunwieltjes")

Het paper suggereert dat hoewel we nog niet op AI's kunnen vertrouwen om het hele werk alleen te doen, we ze wel als assistenten kunnen gebruiken als we ze de juiste hulp geven:

Few-Shot Prompting: In plaats van alleen te zeggen "Schrijf dit", laat je de AI eerst drie voorbeelden zien van hoe je het schrijft. Dit werkt als een spiekbriefje.
Pass@K: Vraag de AI om de code 5 keer te proberen te schrijven, en kies vervolgens de beste versie. Dit vergroot de kans op een werkende versie.
Human-in-the-Loop: Gebruik de AI om de code te ontwerpen, maar laat een menselijke expert de code controleren voordat de beveiligingsrobot deze uitvoert.

De Kernboodschap

Het paper concludeert dat Large Language Models momenteel uitstekende onderzoeksassistenten zijn voor het begrijpen en repareren van beveiligingscode, maar dat ze nog geen betrouwbare architecten zijn voor het bouwen van nieuwe beveiligingsprotocollen vanaf nul.

Ze kunnen je helpen de handleiding te lezen en je typefouten te corrigeren, maar je hebt nog steeds een menselijke expert nodig om te garanderen dat de kluis daadwerkelijk veilig is voordat je de sleutels overhandigt. De benchmark (CrypFormBench) is nu beschikbaar voor andere onderzoekers om nieuwe AI-modellen tegen deze strikte standaarden te testen.

Technische Samenvatting: CrypFormBench

1. Probleemstelling

Handmatige formele analyse van cryptografische schema's is arbeidsintensief en vereist diepgaande expertise in zowel cryptografie als formele specificatietalen. Hoewel geautomatiseerde tools zoals Scyther, Tamarin, CryptoVerif en EasyCrypt bestaan, vertrouwen zij nog steeds op experts om de logica van een schema te abstraheren naar gespecialiseerde, foutgevoelige formele talen (bijv. HLPSL, SPDL, toegepaste $\pi$ -calculus). Large Language Models (LLMs) bieden een potentiële oplossing voor het automatiseren van de afleiding van formele specificaties uit natuurlijke taal. Hun effectiviteit in dit domein blijft echter onverkend vanwege het ontbreken van gestandaardiseerde evaluatiemethodologieën.

Bestaande benchmarks zijn ontoereikend omdat ze vaak:

Alleen symbolische veiligheid ondersteunen en computationele veiligheid verwaarlozen.
Een beperkte schaal dekken (bijv. ~18 protocollen) en diverse dreigingsmodellen of geavanceerde primitieven (bijv. Zero-Knowledge, Post-Quantum) uitsluiten.
Een gebrek hebben aan een verenigd framework om LLM's te evalueren over meerdere formele verifier-talen en taaktypen (generatie, transformatie, correctie).

2. Methodologie: CrypFormBench (C.F.B)

De auteurs introduceren CrypFormBench, een uitgebreide benchmark ontworpen om de capaciteiten van LLM's in formele cryptografische analyse te evalueren. De methodologie bestaat uit drie kerncomponenten:

A. Dataset Constructie

Schaal en Diversiteit: De dataset bestaat uit 700 gecureerde instanties afgeleid van 4.549 open-source projecten en tool-datasets. Deze instanties dekken 677 verschillende cryptografische schema's (variërend van klassieke authenticatie tot moderne MPC, ZK en post-quantum ontwerpen) en 160 beveiligingseigenschappen.
Taaldekking: Het beslaat 7 mainstream formele verifier-talen geassocieerd met tools zoals Scyther (SPDL), Tamarin (SPTHY), AVISPA (HLPSL), ProVerif (PV/HORN), Maude-NPA (MAUDE), CryptoVerif (CV/OCV) en EasyCrypt (EC).
Adversariële Modellen: De dataset bevat diverse aannames over de tegenstander, van passieve/actieve Dolev-Yao modellen tot uitgebreide modellen (CK, eCK) en domeinspecifieke dreigingen (bijv. IoT wachtwoord raden).
Kwaliteitscontrole: Een strikt proces werd gehanteerd waarbij deduplicatie, uitvoerbaarheidstests en handmatische verificatie betrokken waren. Instanties werden gelabeld als "veilig" (geen bekende aanvallen) of "onveilig" (bekende aanvallen), waarbij de outputs van de tools werden afgezet tegen canonieke labels uit de cryptografische literatuur.

B. Taakdefinitie

De benchmark evalueert vijf kerncapaciteiten van LLM's die essentieel zijn voor tool-bruikbare formele specificatie:

Interpretatie: Het genereren van notatie-niveau commentaren en globale schema-samenvattingen vanuit formele code.
Generatie: Het creëren van volledige formele code vanuit natuurlijke taal-logische beschrijvingen.
Aanvulling (Completion): Het invullen van ontbrekende fragmenten van gedeeltelijk gemaskeerde formele specificaties.
Transformatie: Het vertalen van schema-specificaties van de ene formele taal naar een andere, met behoud van semantiek.
Correctie: Het repareren van code die niet compileert (syntactische fouten) of incorrecte verificatieresultaten produceert (semantische fouten).

C. Evaluatie Pipeline

Geautomatiseerde Verificatie: Een end-to-end pipeline integreert meerdere tools, versies en uitvoeringscommando's om de outputs van LLM's te verifiëren. Het handelt variërende call-gedragingen af (bijv. meerdere backends voor AVISPA) en versie-incompatibiliteiten.
Scoring Framework: Prestaties worden gemeten via een gewogen scoringssysteem dat een balans zoekt tussen:
- Uitvoerbaarheid (Analyseerbaarheid): Of de code compileert en draait.
- Functionele Correctheid: Of de geverifieerde beveiligingseigenschappen overeenkomen met de grondwaarheid (SAFE/UNSAFE), gemeten via Accuraatheid ( $ACC_A$ ) en F1 ( $F1_A$ ).
- Gelijkenis: Code-gelijkenis voor completion-taken en semantische gelijkenis (via embeddings) voor interpretatie-taken.
- Efficiëntie: Runtime en bestandsgrootte.

3. Belangrijkste Resultaten

De auteurs evalueerden 9 state-of-the-art LLM's (inclusief GPT-4o, Claude-3.5-Sonnet-Coder, DeepSeek-Coder, en LLaMA4-Instruct).

Algemene Prestaties: De prestaties zijn over het algemeen beperkt. Het best presterende model, Claude-3.5-Sonnet-Coder, behaalde een algemene score van 48,7 van de 100.
Taakspecifieke Inzichten:
- Sterktes: Modellen presteren goed op Interpretatie en Aanvulling, waarbij ze profiteren van hun code-bewustzijn. Bijvoorbeeld: DeepSeek-Coder en GPT-4o tonen een hoge nauwkeurigheid bij het interpreteren van bestaande code.
- Zwaktes: Modellen worstelen aanzienlijk met Generatie, Transformatie en Correctie.
  - Generatie: Zelfs topmodellen behalen lage analyseerbaarheidsratio's (bijv. ~15% voor Claude-3.5) en worstelen met strikte syntaxis/semantiek in complexe talen zoals EasyCrypt en Maude.
  - Transformatie: Dit is de moeilijkste taak. Cross-language interferentie en semantische mismatches leiden tot zeer lage analyseerbaarheid (vaak <10%), waarbij modellen frequent bronfragmenten kopiëren die incompatibel zijn met de idiomen van de doeltaal.
  - Correctie: Hoewel modellen lokale syntactische fouten kunnen herstellen (compiler-gestuurd), hebben ze moeite met semantische reparaties (bijv. het herstellen van foutieve rapportages over beveiligingseigenschappen).
Variabiliteit in Taal: Prestaties variëren sterk per taal. Modellen presteren over het algemeen beter op ProVerif (PV) vanwege de gelijkenis met mainstream programmeersyntaxis, terwijl ze moeite hebben met herschrijvings-gebaseerde tools zoals Maude-NPA.
Optimalisatiestrategieën:
- Few-Shot Prompting: Verbetert de analyseerbaarheid voor generatie aanzienlijk (van 6,6% naar 24,9% met 3-shot) en de correctheid voor correctie.
- Pass@K: Het verhogen van het aantal generatiepogingen ( $K$ ) verhoogt de waarschijnlijkheid van een analyseerbare output, vooral voor moeilijke taken, hoewel het geen garantie biedt voor semantische correctheid.
- Fine-Tuning: Lichtgewicht LoRA fine-tuning op Qwen2.5-Coder-3B verbeterde de completion- en correctiecapaciteiten, maar had minimale impact op generatie of transformatie.

4. Betekenis en Claims

Het artikel claimt de eerste uitgebreide benchmark te bieden die gezamenlijk zowel symbolische als computationele veiligheid dekt voor het evalueren van LLM's in de analyse van cryptografische schema's.

Gegrond Visie: De auteurs stellen dat hoewel LLM's veelbelovende assistenten zijn voor interpretatie en lokale correctie, ze nog niet betrouwbaar zijn voor end-to-end automatisering van formele schema-generatie of cross-language transformatie.
Identificatie van de Bottleneck: De primaire barrière is niet alleen semantisch redeneren, maar uitvoerbaarheid — het vermogen om code te produceren die voldoet aan strikte formele syntaxis en tool-specifieke beperkingen zonder parse-fouten of timeouts te triggeren.
Praktische Richtlijnen: De studie biedt concrete richtingen voor het verbeteren van LLM-ondersteunde analyse, inclus\ief het gebruik van few-shot prompting, Pass@K sampling en lichtgewicht fine-tuning om de uitvoerbaarheids-bottleneck te verzachten.
Reproduceerbaarheid: De benchmark en dataset worden vrijgegeven om systematische, gestandaardiseerde en reproduceerbare evaluatie van toekomstige modellen in dit domein mogelijk te maken.

De auteurs concluderen dat huidige LLM's sterke "concept-tools" (drafting tools) zijn, maar dat ze een mens-in-de-loop validatie of tool-gestuurde reparatiewerkstromen vereisen om praktisch bruikbaar te zijn voor formele cryptografische analyse.