inria-00448703, version 1
Cap Unification: Application to Protocol Security modulo Homomorphic Encryption
5th ACM Symposium on Information, Computer and Communications Security - ASIACCS 2010 (2010)
Résumé : We address the insecurity problem for cryptographic protocols, for an active intruder and a bounded number of sessions. The protocol steps are modeled as rigid Horn clauses, and the intruder abilities as an equational theory. The problem of active intrusion -- such as whether a secret term can be derived, possibly via interaction with the honest participants of the protocol -- is then formulated as a Cap Unification problem. Cap Unification is an extension of Equational Unification: look for a cap to be placed on a given set of terms, so as to unify it with a given term modulo the equational theory. We give a decision procedure for Cap Unification, when the intruder capabilities are modeled as homomorphic encryption theory. Our procedure can be employed in a simple manner to detect attacks exploiting some properties of block ciphers.
- a – Université d'Orléans
- b – Clarkson University, Potsdam, NY (USA)
- c – University at Albany-SUNY, NY (USA)
- 1 :
- Université d'Orléans : EA4022 – Ecole Nationale Supérieure d'Ingénieurs de Bourges
- 2 :
- INRIA – CNRS : FRE2661 – Université de Franche-Comté – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
- Domaine : Informatique/Informatique et langage
- Mots-clés : Rewriting – Unification – Protocol – Secrecy Analysis
- inria-00448703, version 1
- http://hal.inria.fr/inria-00448703
- oai:hal.inria.fr:inria-00448703
- Contributeur :
- Soumis le : Mardi 19 Janvier 2010, 17:51:17
- Dernière modification le : Mercredi 27 Janvier 2010, 09:53:05
Exporter