Type-check og type-inferens i en modstanders åsyn
Translated title
Type Checking and Type Inference in the Presence of an Adversary
Author
Raabjerg, Palle
Term
2. term
Education
Publication year
2009
Pages
123
Abstract
Kommunikationsprotokoller skal sikre autentifikation. En måde at udtrykke sådanne garantier er gennem korrespondenspåstande i pi- og Spi-kalkylerne: logiske udsagn, der forbinder protokolbegivenheder (fx at en “finish”-begivenhed kun må ske, hvis en tilsvarende “start”-begivenhed er sket). En protokol er sikker, når disse påstande altid holder. Tidligere arbejde viser, at et typesystem kan give en lyd approksimation af denne sikkerhed (Gordon og Jeffrey), og at lyd og komplet typeinferens er mulig ved at kode begrænsninger i ALFP, en delmængde af propositionel logik, som kan løses af Succinct Solver (Hüttel). Fournet, Gordon og Maffeis generaliserede senere korrespondenspåstande ved hjælp af Datalog—et logikprogrammeringssprog, der er en delmængde af ALFP—og foreslog et typesystem til at verificere dem. En implementering blev nævnt, men tilsyneladende aldrig offentliggjort; tilsvarende findes ingen implementering af Hüttels inferensmetode. I denne afhandling implementerer vi en typechecker for det Datalog-baserede typesystem og påbegynder en implementering af Hüttels typeinferens for ikke-injektive korrespondencer (hvor én begivenhed kan matche flere tidligere begivenheder). Begge dele er skrevet i Objective Caml (OCaml). I typecheckeren bruger vi Succinct Solver til at evaluere Datalog-korrespondencer; i inferensalgoritmen fungerer den som sidste løsningsfase. Vi beviser, at algoritmen bag vores typechecker er lyd og komplet, og vi demonstrerer den med nogle korrekt typede eksempler. Implementeringen af typeinferens er endnu ikke færdig, men vi leverer et rammeværk, identificerer praktiske problemer og angiver, hvordan de kan eller muligvis kan løses.
Communication protocols need to ensure authentication. One way to state such guarantees is through correspondence assertions in the pi- and Spi-calculus: logical statements linking protocol events (for example, a “finish” event should only occur if a matching “start” event has happened). A protocol is safe when these assertions always hold. Prior work shows that a type system can soundly approximate this safety (Gordon and Jeffrey), and that sound and complete type inference is possible by encoding constraints in ALFP, a fragment of propositional logic solvable by the Succinct Solver (Hüttel). Fournet, Gordon, and Maffeis later generalized correspondence assertions using Datalog—a logic programming language that is a subset of ALFP—and proposed a type system to verify them. An implementation was mentioned but apparently never published; likewise, Hüttel’s inference method had not been implemented. In this thesis, we implement a type checker for the Datalog-based type system and begin an implementation of Hüttel’s type inference for non-injective correspondences (where one event may match multiple prior events). Both are written in Objective Caml (OCaml). In the type checker, the Succinct Solver evaluates Datalog correspondences; in the inference algorithm, it serves as the final solving stage. We prove that the algorithm underlying our type checker is sound and complete and demonstrate it with a few correctly typed examples. The type inference implementation remains partial, but we provide a framework, identify practical issues, and indicate how they can be, or might be, addressed.
[This abstract was generated with the help of AI]
Keywords
type checking ; type inference ; spi-calculus ; ALFP ; cryptographic ; opponent ; typecheck ; typeinferens ; spi-kalkyle ; ALFP ; kryptografisk ; modstander