Computationally Complete Symbolic Attacker and Key Exchange
| Autor: | Mitsuhiro Okada, Gergei Bana, Koji Hasebe |
|---|---|
| Přispěvatelé: | Programming securely with cryptography (PROSECCO), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Department of Computer Science [Tsukuba], Graduate School of Systems and Information Engineering [Tsukuba], Université de Tsukuba = University of Tsukuba -Université de Tsukuba = University of Tsukuba, Department of Philosophy (Keio University) |
| Jazyk: | angličtina |
| Rok vydání: | 2013 |
| Předmět: |
Soundness
Theoretical computer science business.industry Computer science Classical logic Axiomatic system 0102 computer and information sciences 02 engineering and technology Cryptographic protocol Encryption Mathematical proof 01 natural sciences [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] Adaptive chosen-ciphertext attack 010201 computation theory & mathematics 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing business Key exchange |
| Zdroj: | CCS '13 Proceedings of the 2013 ACM SIGSAC conference on Computer & communications security CCS 2013-20th ACM Conference on Computer and Communications Security CCS 2013-20th ACM Conference on Computer and Communications Security, Nov 2013, Berlin, Germany. pp.1231-1246, ⟨10.1145/2508859.2516710⟩ ACM Conference on Computer and Communications Security |
| DOI: | 10.1145/2508859.2516710⟩ |
| Popis: | International audience; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|