Secrecy and Authenticity in Mobile Ad-Hoc Networks
Author
Rafnsson, Willard
Term
2. term
Education
Publication year
2008
Pages
125
Abstract
Afhandlingen udvikler et rammeværk til at verificere hemmeligholdelse og autenticitet i mobile ad hoc-netværk (MANETs), hvor enheder danner midlertidige netværk uden central kontrol. Vi introducerer den Distribuerede Applied Pi-kalkyle med broadcast: en enkel, generisk og let udvidelse af den veletablerede Applied Pi-kalkyle, der tilføjer forbindelsesgrafer (netværkets topologi), broadcast-primitiver (udsendelse til flere modtagere) og eksplicitte lokationer (noder). Kalkylen kan instansieres med et vilkårligt term-omskrivningssystem, som beskriver, hvordan termer og kryptografiske operationer transformeres, og dens semantik ligger tæt op ad Applied Pi. Vi overtager centrale definitioner af hemmeligholdelse og autenticitet samt begreberne rammer (den observerbare viden) og statisk ækvivalens (om to rammer ser ens ud for en angriber). Vi beviser en stærk sætning, der etablerer en syntaktisk sammenhæng mellem Horn-klausuler, genereret fra en proces i Abadi og Blanchets kalkyle, og kildeprocessen. Heraf følger flere vigtige konsekvenser, bl.a. at slutning med Horn-klausuler overapproksimerer aktiv syntaktisk hemmelighed, og at påstande om meddelelsesudveksling afledt af Horn-klausuler er lyd med hensyn til de meddelelser, der faktisk sendes i kildeprocessen. Undervejs identificerer vi en ofte overset antagelse i Dolev–Yao-trusselsmodellen, som kan gøre rammer inkonsistente ved bestemte interne reduktioner. For at afhjælpe dette introducerer vi en let generaliserbar afsløringssemantik, der sikrer konsistente rammer i sådanne tilfælde. Endelig beskriver vi, hvordan Horn-klausulgeneratoren udvides til at tage højde for forbindelsesgrafer, og vi arver et bevis for lydhed af deduktion fra Horn-klausuler for vores kalkyle, hvilket baner vejen for at anvende automatiske løsere af Horn-klausulbegrænsninger.
This thesis develops a framework for verifying secrecy and authenticity in Mobile Ad-hoc Networks (MANETs), where devices form temporary networks without central control. We introduce the Distributed Applied Pi Calculus with Broadcast: a simple, generic, and lightweight extension of the well-established Applied Pi calculus that adds connectivity graphs (the network topology), broadcast primitives (sending to many receivers), and explicit locations (nodes). The calculus can be instantiated by any Term Rewrite System, which specifies how terms and cryptographic operations transform, and its semantics largely match those of Applied Pi. We carry over key definitions of secrecy and authenticity, as well as the notions of frames (observable knowledge) and static equivalence (whether two frames look the same to an attacker). We prove a strong theorem that establishes a syntactic relationship between Horn clauses generated from a process in Abadi and Blanchet’s calculus and the source process. Several important corollaries follow, including that Horn-clause deduction overapproximates active syntactic secrecy, and that message-passing claims derived from the Horn clauses are sound with respect to the messages actually passed in the source process. In the course of the proof, we identify a frequently overlooked assumption in the Dolev–Yao threat model that can make frames inconsistent under certain internal reductions. To address this, we introduce an easily generalised revelation semantics that ensures frames remain consistent in such cases. Finally, we specify how to extend the Horn-clause generator to account for connectivity graphs and inherit a proof of soundness of deduction from Horn clauses for our calculus, paving the way for the use of automated Horn-clause constraint solvers.
[This abstract was generated with the help of AI]
Keywords