Email Gateway (Aug 18 2022 at 20:01): Email Gateway (Aug 18 2022 at 20:01):From: Tobias Nipkow <nipkow@in.tum.de>
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.
http://afp.sourceforge.net/entries/Inductive_Confidentiality.shtml
Last updated: Apr 25 2024 at 16:19 UTC