Computationally Complete Symbolic Attacker and Key Exchange

Abstract : Recently, Bana and Comon-Lundh introduced the notion of computationally complete symbolic attacker to deliver unconditional computational soundness to symbolic protocol verification. First we explain the relationship between their technique and Fitting's embedding of classical logic into S4. Then, based on predicates for "key usability", we provide an axiomatic system in their framework to handle secure encryption when keys are allowed to be sent. We examine both IND-CCA2 and KDM-CCA2 encryptions, both symmetric and asymmetric situations. For unforgeability, we consider INT-CTXT encryptions. This technique does not require the usual limitations of computational soundness such as the absence of dynamic corruption, the absence of key-cycles or unambiguous parsing of bit strings. In particular, if a key-cycle possibly corrupts CCA2 encryption, our technique delivers an attack. If it does not endanger security, the security proof goes through. We illustrate how our notions can be applied in protocol proofs.
Type de document :
Communication dans un congrès
ACM Conference on Computer and Communications Security (CCS'13), 2013, Berlin, Germany. ACM, pp.1231--1246, 2013
Liste complète des métadonnées

https://hal.inria.fr/hal-00918848
Contributeur : Ben Smyth <>
Soumis le : dimanche 15 décembre 2013 - 17:05:40
Dernière modification le : jeudi 30 novembre 2017 - 01:15:25

Identifiants

  • HAL Id : hal-00918848, version 1

Collections

Citation

Gergei Bana, Koji Hasebe, Mitsuhiro Okada. Computationally Complete Symbolic Attacker and Key Exchange. ACM Conference on Computer and Communications Security (CCS'13), 2013, Berlin, Germany. ACM, pp.1231--1246, 2013. 〈hal-00918848〉

Partager

Métriques

Consultations de la notice

108