'Logics for The Applied Pi Calculus'
Author
Pedersen, Michael David
Term
4. term
Education
Publication year
2006
Abstract
I denne afhandling udvikler vi en modal logik for Applied Pi‑kalkulen, et matematisk sprog til at beskrive samtidige processer og kryptografiske protokoller. Logikken beskriver, hvornår to processer ser ens ud for en observatør (observationsækvivalens), og er generel, så den kan tilpasses forskellige anvendelser ved at vælge regler for, hvordan termer er lig eller kan forenkles. Som første skridt definerer vi en stærk form for statisk ækvivalens for frames (repræsentationer af den tilgængelige information), hvor man kan observere både ligheder mellem termer og deres reduktioner. Vi argumenterer for, at den stærke version er meningsfuld i praksis og giver to raffinerede definitioner inspireret af idéen om cores fra Spi‑kalkulen, som undgår at kvantificere over vilkårlige termer og derfor egner sig til logisk karakterisering. Vi viser, at disse raffineringer falder sammen med den oprindelige stærke statiske ækvivalens under generelle betingelser. På den baggrund giver vi en førsteordenslogik for frames, der karakteriserer stærk statisk ækvivalens og giver karakteristiske formler. Det gør det muligt at ræsonnere direkte om termer i en frame og indirekte om den viden, der kan udledes af en frame. Ved at tilføje Hennessy–Milner‑lignende modaliteter får vi en logik for Applied Pi, som understøtter ræsonnement om både statiske egenskaber og processers mulige handlinger. Til sidst illustrerer vi logikken ved at analysere Needham–Schroeder‑protokollen med offentlige nøgler.
In this thesis, we develop a modal logic for the Applied Pi calculus, a mathematical language for describing concurrent processes and cryptographic protocols. The logic captures when two processes appear the same to any observer (observational equivalence) and is designed to be generic: it can be tailored to different applications by choosing rules that define how terms are equal or can be simplified. As a first step, we define a strong form of static equivalence for frames (representations of available information), where both equalities between terms and their reductions are observable. We argue that this strong version is meaningful in practice and provide two refined definitions, inspired by the idea of cores from the Spi calculus, that avoid quantifying over arbitrary terms and are therefore suitable for logical characterization. We prove that, under general conditions, these refined definitions coincide with the original notion of strong static equivalence. Based on them, we present a first-order logic for frames that characterizes strong static equivalence and yields characteristic formulae. This enables direct reasoning about the terms in a frame and indirect reasoning about what knowledge can be deduced from it. By adding Hennessy–Milner style modalities, we obtain a logic for Applied Pi that supports reasoning about both static properties and the possible actions of processes. Finally, we illustrate the logic by analyzing the Needham–Schroeder public-key protocol.
[This abstract was generated with the help of AI]
Documents