Towards Unconditional Soundness: Computationally Complete Symbolic Attacker
| Autor: | Gergei Bana, Hubert Comon-Lundh |
|---|---|
| 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), Security of information systems (SECSI), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France |
| Jazyk: | angličtina |
| Rok vydání: | 2012 |
| Předmět: |
Soundness
0303 health sciences Computational model Theoretical computer science Cryptographic primitive Computer science Atomic formula 0102 computer and information sciences Cryptographic protocol 16. Peace & justice 01 natural sciences 03 medical and health sciences [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] 010201 computation theory & mathematics Symbolic trajectory evaluation The Symbolic 030304 developmental biology TRACE (psycholinguistics) Computer Science::Cryptography and Security |
| Zdroj: | 2nd Conference on Principles of Security and Trust (POST 2012) 2nd Conference on Principles of Security and Trust (POST 2012), 2012, Unknown, pp.189-208 Lecture Notes in Computer Science ISBN: 9783642286407 POST |
| Popis: | International audience; We consider the question of the adequacy of symbolic models versus computational models for the verification of security protocols. We neither try to include properties in the symbolic model that reflect the properties of the computational primitives nor add computational requirements that enforce the soundness of the symbolic model. We propose in this paper a different approach: everything is possible in the symbolic model, unless it contradicts a computational assumption. In this way, we obtain unconditional soundness almost by construction. And we do not need to assume the absence of dynamic corruption or the absence of key-cycles, which are examples of hypotheses that are always used in related works. We set the basic framework, for arbitrary cryptographic primitives and arbitrary protocols, however for trace security properties only. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|