Inductive Study of Confidentiality

Title:	Inductive Study of Confidentiality
Author:	Giampaolo Bella
Submission date:	2012-05-02
Abstract:	This document contains the full theory files accompanying article Inductive Study of Confidentiality --- for Everyone in Formal Aspects of Computing. They aim at an illustrative and didactic presentation of the Inductive Method of protocol analysis, focusing on the treatment of one of the main goals of security protocols: confidentiality against a threat model. The treatment of confidentiality, which in fact forms a key aspect of all protocol analysis tools, has been found cryptic by many learners of the Inductive Method, hence the motivation for this work. The theory files in this document guide the reader step by step towards design and proof of significant confidentiality theorems. These are developed against two threat models, the standard Dolev-Yao and a more audacious one, the General Attacker, which turns out to be particularly useful also for teaching purposes.
BibTeX:	@article{Inductive_Confidentiality-AFP, author = {Giampaolo Bella}, title = {Inductive Study of Confidentiality}, journal = {Archive of Formal Proofs}, month = may, year = 2012, note = {\url{http://isa-afp.org/entries/Inductive_Confidentiality.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.