Section: Overall Objectives

Overall Objectives

SECSI is a common project between Inria Saclay and the LSV (Laboratoire Spécification et Vérification), itself a common research unit of CNRS (UMR 8643) and the ENS (École Normale Supérieure) de Cachan.

The SECSI project is a research project on the security of information systems. Originally, SECSI was organized around three main themes, and their mutual relationships:

• Automated verification of cryptographic protocols;

• Intrusion detection;

• Static analysis of programs, in order to detect security holes and vulnerabilities at the protocol level.

This has changed. Starting from 2006, SECSI concentrates on the first theme, while keeping an eye on the other two.

In a nutshell, the aim of the SECSI project is to develop logic-based verification techniques for security properties of computer systems and networks.

The thrust is towards more automation (new automata-based, or theorem-proving based verification techniques), more properties (not just secrecy or authentication, but e.g., coercion-resistance in electronic voting schemes), more realism (e.g., cryptographic soundness theorems for formal models).

The new objectives of the SECSI project are:

1. Tree-automata based methods, automated deduction, and approximate/exact cryptographic protocol verification in the Dolev-Yao model.

2. Enriching the Dolev-Yao model with algebraic theories, and associated decision problems.

3. Computational soundness of formal models (Dolev-Yao, applied pi-calculus), proofs of security in computational models.

4. Indistinguishability proofs allowing us to handle more properties, e.g. anonymity.

5. Application to new security protocols, e.g. electronic voting protocols.

6. Security in the presence of probabilistic and demonic non-deterministic choices.

The SECSI project officially terminates at the end of 2012.

The reason that the members of the project-team were given is that no permanent Inria researcher remains.

This will of course create a gap in the panel of research themes covered at Inria Saclay, and especially in computer security. Independently of Inria, the members of SECSI will remain active in the field of computer security. They will also define their new scientific project for the years to come. In time, this will be presented as an Inria project-team proposal.