Cette thèse se situe dans le cadre de l'analyse symbolique des protocoles Les contributions sont représentées par l'obtention de résultats de décidabilité et de transfert dans les directions suivantes qui sont des thèmes majeurs en vérification des protocoles :<ul><li>traitement des primitives cryptographiques : chiffrement CBC, signatures en aveugle;</li><li>propriétés de sécurité : secret fort, existence de cycles de clefs;</li><li>approches pour la sécurité : construction de protocoles sûrs.</li></ul>Ainsi, nous avons montré la décidabilité (d'une part) de l'existence de cycles de clefs et (d'autre part) du secret pour des protocoles utilisant le mode de chiffrement CBC ou des signatures en aveugle. Nous avons aussi transféré la sécurité des protocoles d'un cadre faible vers un cadre plus fort dans les sens suivants. D'une part, nous avons montré qu'une propriété de secret faible implique sous certaines hypothèses une propriété de secret plus forte. D'une autre part, nous avons construit des protocoles sûrs à partir de protocoles ayant des propriétés plus faibles.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00338362 |
| Date | 17 December 2007 |
| Creators | Zalinescu, Eugen |
| Publisher | Université Henri Poincaré - Nancy I |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0023 seconds