Search

Your search keyword '"Proof techniques for security protocols (PESTO)"' showing total 2 results
Start Over Author "Proof techniques for security protocols (PESTO)" Journal proceedings of the 2021 acm sigsac conference on computer and communications security
2 results on '"Proof techniques for security protocols (PESTO)"'

1. Structured Leakage and Applications to Cryptographic Constant-Time and Cost

Author

Swarn Priya, Benjamin Grégoire, Gilles Barthe, Vincent Laporte, Institute IMDEA Software [Madrid], Max Planck Institute for Security and Privacy [Bochum] (MPI Security and Privacy), Sûreté du logiciel et Preuves Mathématiques Formalisées (STAMP), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), 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), and 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)

Subjects
Semantics (computer science), Computer science, Cryptography, 02 engineering and technology, computer.software_genre, Operational semantics, Security and privacy, law.invention, Formal methods and theory of security, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], 03 medical and health sciences, Constant (computer programming), law, 0202 electrical engineering, electronic engineering, information engineering, Transformer, ComputingMilieux_MISCELLANEOUS, 030304 developmental biology, Leakage (electronics), 0303 health sciences, Sequence, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], business.industry, 020207 software engineering, Computer engineering, Logic and verification, Compiler, business, computer
Abstract

International audience; Many security properties of interest are captured by instrumented semantics that model the functional behavior and the leakage of programs. For several important properties, including cryptographic constant-time (CCT), leakage models are sufficiently abstract that one can define instrumented semantics for high-level and low-level programs. One important goal is then to relate leakage of source programs and leakage of their compilation---this can be used, e.g., to prove preservation of CCT. To simplify this task, we put forward the idea of structured leakage. In contrast to the usual modeling of leakage as a sequence of observations, structured leakage is tightly coupled with the operational semantics of programs. This coupling greatly simplifies the definition of leakage transformers that map the leakage of source programs to leakage of their compilation and yields more precise statements about the preservation of security properties. We illustrate our methods on the Jasmin compiler and prove preservation results for two policies of interest: CCT and cost.

Published
2021
Full Text
View/download PDF

2. Verifying Table-Based Elections

Author

Jannik Dreier, Saša Radomirović, Sofia Giampietro, David Basin, Institute of Information Security [ETH Zürich], Department of Computer Science [ETH Zürich] (D-INFK), Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology [Zürich] (ETH Zürich)- Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology [Zürich] (ETH Zürich), 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), and Heriot-Watt University [Edinburgh] (HWU)

Subjects
Protocol (science), Correctness, Electronic voting, Computer science, business.industry, media_common.quotation_subject, Cryptography, 02 engineering and technology, Elections, 16. Peace & justice, Computer security, computer.software_genre, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Protocol verification, 020204 information systems, Secrecy, 0202 electrical engineering, electronic engineering, information engineering, Key (cryptography), Table (database), Verifiability, 020201 artificial intelligence & image processing, Simplicity, business, computer, media_common
Abstract

International audience; Verifiability is a key requirement for electronic voting. However, the use of cryptographic techniques to achieve it usually requires specialist knowledge to understand; hence voters cannot easily assess the validity of such arguments themselves. To address this, solutions have been proposed using simple tables and checks, which require only simple verification steps with almost no cryptography. This simplicity comes at a cost: numerous verification checks must be made on the tables to ensure their correctness, raising the question whether the success of all the small verification steps entails the overall goal of end-to-end verifiability while preserving vote secrecy. Do the final results reflect the voters' will? Moreover, do the verification steps leak information about the voters' choices? In this paper, we provide mathematical foundations and an associated methodology for defining and proving verifiability and voter privacy for table-based election protocols. We apply them to three case studies: the Eperio protocol, Scantegrity, and Chaum's Random-Sample Election protocol. Our methodology helps us, in all three cases, identify previously unknown problems that allow an election authority to cheat and modify the election outcome. Furthermore, it helps us formulate and verify the corrected versions.

Published
2021
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results