2021
Autores
Barbosa, M; Barthe, G; Fan, X; Gregoire, B; Hung, SH; Katz, J; Strub, PY; Wu, XD; Zhou, L;
Publicação
CCS '21: PROCEEDINGS OF THE 2021 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY
Abstract
EasyCrypt is a formal verification tool used extensively for formalizing concrete security proofs of cryptographic constructions. However, the EasyCrypt formal logics consider only classical attackers, which means that post-quantum security proofs cannot be formalized and machine-checked with this tool. In this paper we prove that a natural extension of the EasyCrypt core logics permits capturing a wide class of post-quantum cryptography proofs, settling a question raised by (Unruh, POPL 2019). Leveraging our positive result, we implement EasyPQC, an extension of EasyCrypt for post-quantum security proofs, and use EasyPQC to verify post-quantum security of three classic constructions: PRF-based MAC, Full Domain Hash and GPV08 identity-based encryption.
2021
Autores
Barbosa, M; Barthe, G; Grégoire, B; Koutsos, A; Strub, PY;
Publicação
IACR Cryptol. ePrint Arch.
Abstract
2021
Autores
Barbosa, M; Barthe, G; Fan, X; Grégoire, B; Hung, SH; Katz, J; Strub, PY; Wu, X; Zhou, L;
Publicação
IACR Cryptol. ePrint Arch.
Abstract
2021
Autores
Abdalla, M; Barbosa, M; Rønne, PB; Ryan, PYA; Sala, P;
Publicação
IACR Cryptol. ePrint Arch.
Abstract
2020
Autores
Silva, F; Alonso, AN; Pereira, J; Oliveira, R;
Publicação
Distributed Applications and Interoperable Systems - 20th IFIP WG 6.1 International Conference, DAIS 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15-19, 2020, Proceedings
Abstract
The performance and scalability of byzantine fault-tolerant (BFT) protocols for state machine replication (SMR) have recently come under scrutiny due to their application in the consensus mechanism of blockchain implementations. This led to a proliferation of proposals that provide different trade-offs that are not easily compared as, even if these are all based on message passing, multiple design and implementation factors besides the message exchange pattern differ between each of them. In this paper we focus on the impact of different combinations of cryptographic primitives and the message exchange pattern used to collect and disseminate votes, a key aspect for performance and scalability. By measuring this aspect in isolation and in a common framework, we characterise the design space and point out research directions for adaptive protocols that provide the best trade-off for each environment and workload combination. © IFIP International Federation for Information Processing 2020.
2020
Autores
Troncoso, C; Payer, M; Hubaux, JP; Salathé, M; Larus, JR; Bugnion, E; Lueks, W; Stadler, T; Pyrgelis, A; Antonioli, D; Barman, L; Chatel, S; Paterson, KG; Capkun, S; Basin, DA; Beutel, J; Jackson, D; Roeschlin, M; Leu, P; Preneel, B; Smart, NP; Abidin, A; Gürses, SF; Veale, M; Cremers, C; Backes, M; Tippenhauer, NO; Binns, R; Cattuto, C; Barrat, A; Fiore, D; Barbosa, M; Oliveira, R; Pereira, J;
Publicação
IEEE Data Eng. Bull.
Abstract
The access to the final selection minute is only available to applicants.
Please check the confirmation e-mail of your application to obtain the access code.