ProSe

There is nowadays a huge quantity of information that flows through untrusted channels. And this will still increase dramatically in the future. Mobile sensor networks are deployed everywhere and control more and more social activites: car driving, health care, traffic control, ... Mobile and ad hoc networks, iphone and more generally mobile terminals are increasingly used in everyday life. Chips are used to store sensitive data and are supposed to secure critical transactions: they are embedded in electronic passports, cash cards, ... Securing the communications is therefore an important challenge. The research community in computer and information sciences has deployed a lot of efforts in trying to secure the communications. There is also a lot of efforts, in trying to increase our confidence by providing with ``security proofs''. Such proofs require a formal model for the protocols, for the security properties and for the attacker capabilities. Until 2001, different research communities worked independently, using different formal models. This includes for instance a logical (or symbolic) model and analysis, whose successes can be illustrated by the numerous man-in-the-middle attacks that have been found on security protocols. A second approach is computational, inheriting from complexity theory; it assumes for instance that the attacker is any randomized polynomial time Turing machine. This is the favorite model of cryptographers. A third approach is more pragmatic and tries to prove/find attacks on actual implementations of the protocols (this has been more successful in finding attacks than in proving protocols secure). The main goal of the ProSe project is to provide with security proofs at several levels: symbolic, computational, and implementation. In a nutshell, the aim of the project is to develop automatic protocol verification tools in the symbolic model, in the computational model, and in an implementation model. We will rely on the partner's experience in the areas of symbolic security proofs and their relationships with computational proofs.