Résolution de contraintes de déductibilité : application à la composition de services Web sécurisés / Tigran Avanesov ; sous la direction de Michaël Rusinowitch

Date :

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : anglais / English

Services Web

Cryptographie

Protocoles de réseaux d'ordinateurs -- Modèles mathématiques

Méthodes formelles (informatique)

Logiciels -- Vérification

Rusinowitch, Michaël (1956-....) (Directeur de thèse / thesis advisor)

Université de Nancy I (1970-2012) (Organisme de soutenance / degree-grantor)

École doctorale IAEM Lorraine - Informatique, Automatique, Électronique - Électrotechnique, Mathématiques de Lorraine (Ecole doctorale associée à la thèse / doctoral school)

Laboratoire lorrain de recherche en informatique et ses applications (Laboratoire associé à la thèse / thesis associated laboratory)

Résumé / Abstract : Les contraintes de déductibilité ont été introduites pour vérifier les protocoles cryptographiques. Cette thèse présente une procédure de décision pour le problème de satisfaisabilité des systèmes généraux de contraintes de déductibilité. Deux cas sont envisagés: la théorie de Dolev-Yao standard et son extension par un opérateur associatif, commutatif, idempotent. Le résultat est utilisé pour résoudre le problème de l'orchestration automatique et distribué de services Web sécurisés. Comme seconde application nous proposons une procédure pour décider la sécurité d'un nombre fini de sessions de protocole en présence de plusieurs intrus qui ne communiquent pas. Nous montrons également comment il est possible de détecter certaines attaques par réécriture qui exploitent le format des messages en XML

Résumé / Abstract : Deducibility constraints have been introduced to verify cryptographic protocols. This thesis gives a decision procedure for the satisfiability problem of general deducibility constraints. Two cases are considered: the standard Dolev-Yao theory and its extension with an associative, commutative idempotent operator. The result is applied to solve the automated distributed orchestration problem for secured Web services. As a second application we give a procedure to decide the security of a cryptographic protocol in presence of several non-communicating intruders. We also show how it is possible to detect some XML rewriting attacks on Web services