Contingent payments on a public ledger: models and reductions for automated verification
| Autor: | Sergiu Bursuc, Steve Kremer |
|---|---|
| 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), 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), European Project: 645865,H2020 ERC,ERC-2014-CoG,SPOOC(2015), 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) |
| Jazyk: | angličtina |
| Rok vydání: | 2019 |
| Předmět: |
Security properties
050101 languages & linguistics Cryptographic primitive Computer science Semantics (computer science) media_common.quotation_subject 05 social sciences 02 engineering and technology Payment Computer security computer.software_genre [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] Ledger 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing 0501 psychology and cognitive sciences computer media_common |
| Zdroj: | ESORICS 2019-The 24th European Symposium on Research in Computer Security ESORICS 2019-The 24th European Symposium on Research in Computer Security, Sep 2019, Luxembourg, Luxembourg Lecture Notes in Computer Science ISBN: 9783030299583 ESORICS (1) Computer Security – ESORICS 2019-24th European Symposium on Research in Computer Security, Luxembourg, September 23–27, 2019, Proceedings, Part I Lecture Notes in Computer Science Lecture Notes in Computer Science-Computer Security – ESORICS 2019 |
| ISSN: | 0302-9743 1611-3349 |
| Popis: | International audience; We study protocols that rely on a public ledger infrastructure, concentrating on protocols for zero-knowledge contingent payment, whose security properties combine diverse notions of fairness and privacy. We argue that rigorous models are required for capturing the ledger semantics, the protocol-ledger interaction, the cryptographic primitives and, ultimately, the security properties one would like to achieve.Our focus is on a particular level of abstraction, where network messages are represented by a term algebra, protocol execution by state transition systems (e.g. multiset rewrite rules) and where the properties of interest can be analyzed with automated verification tools. We propose models for: (1) the rules guiding the ledger execution, taking the coin functionality of public ledgers such as Bitcoin as an example; (2) the security properties expected from ledger-based zero-knowledge contingent payment protocols; (3) two different security protocols that aim at achieving these properties relying on different ledger infrastructures; (4) reductions that allow simpler term algebras for homomorphic cryptographic schemes.Altogether, these models allow us to derive a first automated verification for ledger-based zero-knowledge contingent payment using the Tamarin prover. Furthermore , our models help in clarifying certain underlying assumptions, security and efficiency tradeoffs that should be taken into account when deploying protocols on the blockchain. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|