Exploiting Symmetries When Proving Equivalence Properties for Security Protocols
| Autor: | Vincent Cheval, Steve Kremer, Itsaka Rakotonirina |
|---|---|
| Přispěvatelé: | 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), ANR-17-CE39-0004,TECAP,Analyse de protocoles - unir les outils existants(2017), 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) |
| Jazyk: | angličtina |
| Rok vydání: | 2019 |
| Předmět: |
Cryptographic primitive
Theoretical computer science Computational complexity theory Computer science 0102 computer and information sciences 02 engineering and technology Cryptographic protocol 01 natural sciences Undecidable problem Partial-Order Reductions Symmetry [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] 010201 computation theory & mathematics Bounded function Homogeneous space 0202 electrical engineering electronic engineering information engineering Security Protocols 020201 artificial intelligence & image processing Equivalence (formal languages) |
| Zdroj: | CCS'19-26th ACM Conference on Computer and Communications Security CCS'19-26th ACM Conference on Computer and Communications Security, Nov 2019, London, United Kingdom Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security CCS |
| Popis: | International audience; Verification of privacy-type properties for cryptographic protocols in an active adversarial environment, modelled as a behavioural equivalence in concurrent-process calculi, exhibits a high computational complexity. While undecidable in general, for some classes of common cryptographic primitives the problem is coNEXP-complete when the number of honest participants is bounded.In this paper we develop optimisation techniques for verifying equivalences, exploiting symmetries between the two processes under study. We demonstrate that they provide a significant (several orders of magnitude) speed-up in practice, thus increasing the size of the protocols that can be analysed fully automatically. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|