Compiling Protocol Narrations into Applied Pi Processes
Translated title
Kompilering fra Protokolfortællinger til Applied Pi Processer
Author
Olesen, Sam Sepstrup
Term
4. term
Education
Publication year
2015
Submitted on
2015-06-08
Pages
41
Abstract
This thesis addresses how informal protocol narrations—concise descriptions of message exchanges between principals—can be compiled into formal processes in the applied pi calculus to ease the design and analysis of cryptographic protocols. Building on the work of Briais and Nestmann, it extends their syntax with an equational theory and defines a general term-derivation mechanism for arbitrary equational theories. This enables a projection (compilation) from protocol narrations to applied pi processes, avoiding the limitations of a fixed set of cryptographic primitives as in the spi calculus. We also study computational complexity and show that the term derivation problem is NP-complete. The translation is implemented in OCaml in the compiler narcapi. The report covers background, the formal compilation, the complexity result, design choices, and examples, aiming to make implicit reception checks explicit and to reduce error-prone manual modeling while supporting diverse cryptographic primitives.
Dette speciale undersøger, hvordan uformelle protokolnarrationer – korte beskrivelser af, hvilke beskeder parter udveksler – kan oversættes til formelle processer i applied pi-kalkylen for at lette design og analyse af kryptografiske protokoller. Med udgangspunkt i Briais og Nestmanns arbejde udvides syntaksen med en lighedsteori (equational theory), og der defineres en generel term-derivationsmekanisme for vilkårlige lighedsteorier. Dette muliggør en projektion (kompilering) fra protokolnarrationer til applied pi-processer, så protokoller ikke er begrænset til en fast mængde kryptografiske primitive som i spi-kalkylen. Vi analyserer også beregningskompleksiteten og viser, at term-derivationsproblemet er NP-komplet. Oversættelsen er implementeret i OCaml i kompileren narcapi. Rapporten dækker baggrund, formel oversættelse, kompleksitetsanalyse, designbeslutninger og eksempler, med målet at gøre eksplicitte sikkerhedstjek og modellering mindre fejlbehæftet og mere fleksibel på tværs af kryptografiske primitive.
[This apstract has been generated with the help of AI directly from the project full text]
Keywords