PhD Thesis

Title: Security of cryptographic protocols: decidability and transfer results
Advisors: Véronique Cortier and Michaël Rusinowitch
Defense:
Monday 17 December 2007 at 14:30
Loria, room A008 (how to reach)
Manuscript (in English): [pdf file (1.2MB) | ps file (3.0MB)] (current version 12/11/2008)
Jury:
Abstract

This thesis is developed in the framework of the symbolic analysis of security protocols. The contributions are represented by decidability and transfer results in the following directions which are major topics in protocol verification:
  • treatment of the cryptographic primitives: CBC encryption, blind signatures;
  • security properties: strong secrecy, existence of key cycles;
  • approaches for protocol security: construction of the secure protocols.
Thus, we showed the decidability (on the one hand) of the existence of key cycles for a bounded number of sessions using a generalised constraint system approach, and (on the other hand) of secrecy for protocols using the CBC encryption or blind signatures for an unbounded number of sessions by using a refined resolution strategy on a new fragment of Horn clauses.

We also transferred protocol security from a weak framework towards a stronger framework in the following directions. On the one hand, we showed that a weak property of secrecy (i.e. reachability-based secrecy) implies under certain well-motivated assumptions a stronger secrecy property (i.e. equivalence-based secrecy). On the other hand, we built protocols secure against active adversaries considering an unbounded number of sessions, by transforming protocols which are secure in a non-adversarial setting.


Back