A master thesis from Aalborg University
Secrecy and Authenticity in Mobile Ad-Hoc Networks
Author(s)
Term
2. term
Education
Publication year
2008
Submitted on
2008-06-10
Pages
125 pages
Abstract
This thesis documents a framework for verifying secrecy and authenticity properties of Mobile Ad-hoc Networks. We present the Distributed Applied Pi Calculus with Broadcast, which is a simple, yet generic, expressive, and lightweight extension to the well-established Applied Pi calculus consisting of connectivity graphs, broadcast primitives, and explicit locations. The calculus can be instantiated by an arbitrary Term Rewrite System, and the semantics of the calculus is largely like that of Applied Pi. We inherit key definitions of secrecy and authenticity from Applied Pi to our calculus, as well as those of frames and static equivalence. We prove a powerful teorem expressing a syntactic relationship between Horn clauses generated from a process in the calculus of Abadi and Blanchet, and the source process. Several interesting corollaries follow from this theorem, including that Horn clause deduction overapproximates active syntactic secrecy, and that claims of message-passing deduced from the Horn clauses are sound with regards to the messages passed in the source process. During the process of this proof, we observe a frequently overlooked assumption in the Dolev-Yao threat model which causes frames to become inconsistent if particular internal reductions are performed. To address this, we give a (easily generalised) revelation semantics which ensures frames are consistent in the presense of such reductions. At last, specifying how to extend the Horn clause generator to take into account connectivity graphs, We inherit a proof of soundness of deduction from Horn clauses for our calculus, thus clearing the way for the application of automated Horn clause constraint solvers.
Keywords
Colophon: This page is part of the AAU Student Projects portal, which is run by Aalborg University. Here, you can find and download publicly available bachelor's theses and master's projects from across the university dating from 2008 onwards. Student projects from before 2008 are available in printed form at Aalborg University Library.
If you have any questions about AAU Student Projects or the research registration, dissemination and analysis at Aalborg University, please feel free to contact the VBN team. You can also find more information in the AAU Student Projects FAQs.