Please use this identifier to cite or link to this item:
Title: A Logic and tool for local reasoning about security protocols
Author: Toninho, Bernardo Parente Coutinho Fernandes
Advisor: Caires, Luís
Keywords: Protocol analysis
Mathematical logic and formal languages
Spatial logics
Defense Date: 2009
Publisher: FCT - UNL
Abstract: This thesis tackles the problem of developing a formal logic and associated model-checking techniques to verify security properties, and its integration in the Spatial Logic Model Checker(SLMC) tool. In the areas of distributed system design and analysis, there exists a substantial amount of work related to the verification of correctness properties of systems, in which the work aimed at the verification of security properties mostly relies on precise yet informal methods of reasoning. This work follows a line of research that applies formal methodologies to the verification of security properties in distributed systems, using formal tools originally developed for the study of concurrent and distributed systems in general. Over the years, several authors have proposed spatial logics for local and compositional reasoning about algebraic models of distributed systems known as process calculi. In this work, we present a simplification of a process calculus known as the Applied - calculus, introduced by Abadi and Fournet, designed for the study of security protocols. We then develop a spatial logic for this calculus, extended with knowledge modalities, aimed at reasoning about security protocols using the concept of local knowledge of processes. Furthermore, we conclude that the extensions are sound and complete regarding their intended semantics and that they preserve decidability, under reasonable assumptions. We also present a model-checking algorithm and the proof of its completeness for a large class of processes. Finally, we present an OCaml implementation of the algorithm, integrated in the Spatial Logic Model Checker tool, developed by Hugo Vieira and Luis Caires, thus producing the first tool for security protocol analysis that employs spatial logics.
Description: Trabalho apresentado no âmbito do Mestrado em Engenharia Informática, como requisito parcial para obtenção do grau de Mestre em Engenharia Informática
Appears in Collections:FCT: DI - Dissertações de Mestrado

Files in This Item:
File Description SizeFormat 
Toninho_2009.pdf511,53 kBAdobe PDFView/Open

FacebookTwitterDeliciousLinkedInDiggGoogle BookmarksMySpace
Formato BibTex MendeleyEndnote Degois 

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.