Probabilistic Polynomial-time Semantics for a Protocol Security Logic

Anupam Datta 1 Ante Derek 1 John C. Mitchell 1 Vitaly Shmatikov 2 Mathieu Turuani 3
3 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We describe a cryptographically sound formal logic for proving protocol security properties without explicitly reasoning about probability, asymptotic complexity, or the actions of a malicious attacker. The approach rests on a new probabilistic, polynomial-time semantics for an existing protocol security logic, replacing an earlier semantics that uses nondeterministic symbolic evaluation. While the basic form of the protocol logic remains unchanged from previous work, there are some interesting technical problems involving the difference between efficiently recognizing and efficiently producing a value, and involving a reinterpretation of standard logical connectives that seems necessary to support certain forms of reasoning.
Type de document :
Communication dans un congrès
Luis Caires et al. 32nd International Colloquium on Automata, Languages and Programming - ICALP 2005, Jul 2005, Lisbon/Portugal, Springer, 3580, pp.16--29, 2005, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00103654
Contributeur : Mathieu Turuani <>
Soumis le : mercredi 4 octobre 2006 - 18:27:47
Dernière modification le : vendredi 6 juillet 2018 - 15:06:09

Identifiants

  • HAL Id : inria-00103654, version 1

Citation

Anupam Datta, Ante Derek, John C. Mitchell, Vitaly Shmatikov, Mathieu Turuani. Probabilistic Polynomial-time Semantics for a Protocol Security Logic. Luis Caires et al. 32nd International Colloquium on Automata, Languages and Programming - ICALP 2005, Jul 2005, Lisbon/Portugal, Springer, 3580, pp.16--29, 2005, Lecture Notes in Computer Science. 〈inria-00103654〉

Partager

Métriques

Consultations de la notice

165