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 [8].

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 [12] 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.