On Communication Models When Verifying Equivalence Properties
| Autor: | Steve Kremer, Kushal Babel, Vincent Cheval |
|---|---|
| Přispěvatelé: | Indian Institute of Technology Bombay (IIT Bombay), Proof techniques for security protocols (PESTO), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), ANR-14-CE28-0030,Sequoia,Propriété de sécurité, équivalence de processes et vérification automatique(2014), European Project: 645865,H2020 ERC,ERC-2014-CoG,SPOOC(2015), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL) |
| Rok vydání: | 2017 |
| Předmět: |
Theoretical computer science
Computer science Internal communications 0102 computer and information sciences 02 engineering and technology Cryptographic protocol Adversary 01 natural sciences Scheduling (computing) [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] 010201 computation theory & mathematics Reachability Authentication protocol Models of communication 0202 electrical engineering electronic engineering information engineering Equivalence relation 020201 artificial intelligence & image processing |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783662544549 POST 6th International Conference on Principles of Security and Trust (POST) 6th International Conference on Principles of Security and Trust (POST), Apr 2017, Uppsala, Sweden Lecture Notes in Computer Science Lecture Notes in Computer Science-Principles of Security and Trust |
| ISSN: | 0302-9743 1611-3349 |
| Popis: | International audience; Symbolic models for security protocol verification, following the sem-inal ideas of Dolev and Yao, come in many flavors, even though they share the same ideas. A common assumption is that the attacker has complete control over the network: he can therefore intercept any message. Depending on the precise model this may be reflected either by the fact that any protocol output is directly routed to the adversary, or communications may be among any two participants, including the attacker — the scheduling between which exact parties the communication happens is left to the attacker. These two models may seem equivalent at first glance and, depending on the verification tools, either one or the other semantics is implemented. We show that, unsurprisingly, they indeed coincide for reachability properties. However, when we consider indistinguishability properties, we prove that these two semantics are incomparable. We also introduce a new semantics, where internal communications are allowed but messages are always eavesdropped by the attacker. We show that this new semantics yields strictly stronger equivalence relations. We also identify two subclasses of protocols for which the three semantics coincide. Finally, we implemented verification of trace equivalence for each of these semantics in the APTE tool and compare their performances on several classical examples. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|