Computationally Sound Compositional Logic for Security Protocols

Anupam Datta 1 Ante Derek 1 John C. Mitchell 1 Arnab Roy 1 Vitaly Shmatikov 2 Mathieu Turuani 3 Bogdan Warinschi 3
1 Computer Science Department [Stanford]
2 ECE - Department of Electrical and Computer Engineering - University of Texas
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, INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We have been developing 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 probabilistic, polynomial-time semantics for a protocol security logic that was originally developed using nondeterministic symbolic semantics. This workshop presentation will discuss ways in which the computational semantics lead to different reasoning methods and report our progress to date in several directions. One significant difference between the symbolic and computational settings results from the computational difference between efficiently recognizing and efficiently producing a value. Among the more recent developments are a compositional method for proving cryptographically sound properties of key exchange protocols, and some work on secrecy properties that illustrates the computational interpretation of inductive properties of protocol roles.
Type de document :
Communication dans un congrès
Véronique Cortier et Steve Kremer. Workshop on Formal and Computational Cryptography - FCC 2006, Jul 2006, Venice/Italy, 2006
Liste complète des métadonnées
https://hal.inria.fr/inria-00080593
Contributeur : Véronique Cortier <>
Soumis le : lundi 19 juin 2006 - 16:05:27
Dernière modification le : jeudi 15 février 2018 - 08:48:09
Document(s) archivé(s) le : lundi 5 avril 2010 - 23:04:21

Fichier

paper2.pdf

Identifiants

  • HAL Id : inria-00080593, version 1

Collections

INRIA | FCC2006 | UNIV-FCOMTE | UNIV-BM | FEMTO-ST | UNIV-BM-THESE | LORIA | UNIV-LORRAINE

Citation

Anupam Datta, Ante Derek, John C. Mitchell, Arnab Roy, Vitaly Shmatikov, et al.. Computationally Sound Compositional Logic for Security Protocols. Véronique Cortier et Steve Kremer. Workshop on Formal and Computational Cryptography - FCC 2006, Jul 2006, Venice/Italy, 2006. 〈inria-00080593〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

377

Téléchargements de fichiers

147

Contact


archive-ouverte@inria.fr