Dans les deux dernières décennies, l’Internet a apporté une nouvelle dimension aux communications.
Il est maintenant possible de communiquer avec n’importe qui, n’importe
où, n’importe quand et ce, en quelques secondes. Alors que certains systèmes de
communication distribués, comme le courriel, le chat, . . . , sont plutôt informels et
ne nécessitent aucune sécurité, d’autres comme l’échange d’informations militaires ou
encore médicales, le commerce électronique, . . . , sont très formels et nécessitent de très
hauts niveaux de sécurité.
Pour atteindre les objectifs de sécurité voulus, les protocoles cryptographiques sont
souvent utilisés. Cependant, la création et l’analyse de ces protocoles sont très difficiles.
Certains protocoles ont été montrés incorrects plusieurs années après leur conception.
Nous savons maintenant que les méthodes formelles sont le seul espoir pour avoir des
protocoles parfaitement corrects. Ce travail est une contribution dans le domaine de
l’analyse des protocoles cryptographiques de la façon suivante:
• Une classification des méthodes formelles utilisées pour l’analyse des protocoles
cryptographiques.
• L’utilisation des systèmes d’inférence pour la mod´elisation des protocoles cryptographiques.
• La définition d’une classe de systèmes d’inférence qui ont une theorie décidable.
• La proposition d’une procédure de décision pour une grande classe de protocoles
cryptographiques / In the last two decades, Internet brought a new dimension to communications. It
is now possible to communicate with anyone, anywhere at anytime in few seconds.
While some distributed communications, like e-mail, chat, . . . , are rather informal
and require no security at all, others, like military or medical information exchange,
electronic-commerce, . . . , are highly formal and require a quite strong security.
To achieve security goals in distributed communications, it is common to use cryptographic
protocols. However, the informal design and analysis of such protocols are
error-prone. Some protocols were shown to be deficient many years after their conception.
It is now well known that formal methods are the only hope of designing
completely secure cryptographic protocols. This thesis is a contribution in the field of
cryptographic protocols analysis in the following way:
• A classification of the formal methods used in cryptographic protocols analysis.
• The use of inference systems to model cryptographic protocols.
• The definition of a class of theory-decidable inference systems.
• The proposition of a decision procedure for a wide class of cryptographic protocols. / Inscrit au Tableau d'honneur de la Faculté des études supérieures
| Identifer | oai:union.ndltd.org:LACETR/oai:collectionscanada.gc.ca:QQLA.2005/22448 |
| Date | 02 1900 |
| Creators | Gagnon, François |
| Contributors | Mejri, Mohamed |
| Publisher | Université Laval |
| Source Sets | Library and Archives Canada ETDs Repository / Centre d'archives des thèses électroniques de Bibliothèque et Archives Canada |
| Language | English |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation |
| Format | text/html, application/pdf |
| Rights | © François Gagnon, 2005 |
Page generated in 0.0016 seconds