Faculdade de Ciências e Tecnologia (FCT) >
FCT Departamentos >
FCT: Departamento de Informática >
FCT: DI - Dissertações de Mestrado >
Please use this identifier to cite or link to this item:
|Título: ||A Logic and tool for local reasoning about security protocols|
|Autor: ||Toninho, Bernardo Parente Coutinho Fernandes|
|Orientador: ||Caires, Luís|
|Palavras-chave: ||Protocol analysis|
Mathematical logic and formal languages
|Issue Date: ||2009|
|Editora: ||FCT - UNL|
|Resumo: ||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.|
|Descrição: ||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|
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.