A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif
| Autor: | Vincent Cheval, Véronique Cortier, Mathieu Turuani |
|---|---|
| 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), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), 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), LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy, Cortier, Véronique, Automated Security Proofs of Cryptographic Protocols: Privacy, Untrusted Platforms and Applications to E-voting Protocols - SPOOC - - H2020 ERC2015-09-01 - 2020-09-01 - 645865 - VALID |
| Jazyk: | angličtina |
| Rok vydání: | 2018 |
| Předmět: |
Protocol (science)
Soundness business.industry Computer science Cryptography 0102 computer and information sciences 02 engineering and technology Cryptographic protocol Computer security computer.software_genre 01 natural sciences [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] 010201 computation theory & mathematics Server Encoding (memory) 0202 electrical engineering electronic engineering information engineering Key (cryptography) 020201 artificial intelligence & image processing business computer Abstraction (linguistics) [INFO.INFO-CR] Computer Science [cs]/Cryptography and Security [cs.CR] |
| Zdroj: | CSF'2018-31st IEEE Computer Security Foundations Symposium CSF'2018-31st IEEE Computer Security Foundations Symposium, Jul 2018, Oxford, United Kingdom [Research Report] Inria Nancy-Grand Est; LORIA, UMR 7503, Université de Lorraine, CNRS, Vandoeuvre-lès-Nancy. 2018 2018 IEEE 31st Computer Security Foundations Symposium (CSF) CSF |
| Popis: | International audience; ProVerif is a popular tool for the fully automatic analysis of security protocols, offering very good support to detect flaws or prove security. One exception is the case of protocols with global states such as counters, tables, or more generally, memory cells. ProVerif fails to analyse such protocols, due to its internal abstraction. Our key idea is to devise a generic transformation of the security properties queried to ProVerif. We prove the soundness of our transformation and implement it into a front-end GSVerif. Our experiments show that our front-end (combined with ProVerif) outperforms the few existing tools, both in terms of efficiency and protocol coverage. We successfully apply our tool to a dozen of protocols of the literature, yielding the first fully automatic proof of a security API and a payment protocol of the literature. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|