[isabelle] New AFP entry: Inductive Study of Confidentiality

Inductive Study of Confidentiality
Giampaolo Bella

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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.