| ||||||
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:
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. |