Security Made Easy
Author
Jørgensen, Morten
Term
2. term
Education
Publication year
2008
Abstract
This thesis presents a type inference algorithm for an effect-based, dependent type system for a variant of the pi calculus used to model security protocols. The type system guarantees that well-typed processes satisfy an authenticity property expressed as correspondences. Given a process and a type context, the algorithm generates constraints that are satisfiable if and only if the process can be made well-typed under the context. Type constraints are solved by unification, while effect constraints—capturing correspondence obligations—are handled by a non-deterministic procedure that essentially performs correspondence matching. The resulting solution can be turned into an efficient proof of safety in the form of a derivation tree, enabling automated proof generation. A Caml implementation has been used for experiments, and the results indicate good practical performance. The thesis also provides background on type systems and security protocols and presents the underlying typed calculus along with a nameless formulation of the type system.
Dette speciale præsenterer en typeinferens-algoritme for et effektbaseret, afhængigt typesystem til en variant af pi-kalkylen, som bruges til at modellere sikkerhedsprotokoller. Typesystemet garanterer, at velformede processer opfylder en autenticitetsegenskab udtrykt som korrespondencer. Givet en proces og en typekontekst genererer algoritmen begrænsninger, der er opfyldelige, hvis og kun hvis processen kan gøres velformet under konteksten. Typebegrænsninger løses ved unifikation, mens effektbegrænsninger – der indfanger korrespondencekrav – håndteres af en ikke-deterministisk metode, der i praksis matcher korrespondencer. Løsningen kan omsættes til et effektivt sikkerhedsbevis i form af et udledningstræ og muliggør automatiseret bevisgenerering. En Caml-implementering er brugt til eksperimenter, som indikerer god ydeevne i praksis. Specialet giver desuden en introduktion til typesystemer og sikkerhedsprotokoller samt præsenterer den underliggende typede kalkyle og en navneløs formulering af typesystemet.
[This apstract has been generated with the help of AI directly from the project full text]