The goal of the lecture is to present some aspects of formal security proofs of protocols. This is a wide area, and there is another lecture (by B. Banchet) on related topics. The idea is therefore to explain in depth one particular technique, that relies on deducibility constraints. We rely mainly on two introductory documents [8,14]. Actually, the current notes are the beginning of .
Here is a roadmap:
1. We introduce the problem with examples and touch a little the question of the validity of the security models (section 1).
We describe then a small process algebra, that will serve as a model for the protocols, as well as a few security properties (section 2).
2. The core of the lecture is here: we introduce the attacker model, as a deduction system, and show how to represent any execution in the hostile environment as deducibility constraints. In short, a deducibility constraint is a sequence of proofs, in which some parts are unknown (and formalized with variables) and possibly re-used in other constraints. An instance of such a constraints yields an attacker's strategy.
We explain how to solve such constraints in a particular setting of a few cryptographic primitives. This is more or less what is described in the first part of  and is detailed in the section 3.
Though the lecture aims at being self-contained, it assumes some familiarity with inference rules/ formal proofs (or SOS for programming languages) and terms/ substitutions/ unification. Similarly, a knowledge on concurrency is not required, but will make easier the understanding of the model.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 firstname.lastname@example.org
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 email@example.com