Zobrazeno 1 - 10
of 49
pro vyhledávání: '"Pierre-Yves Strub"'
Autor:
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré, Pierre-Yves Strub
Publikováno v:
Transactions on Cryptographic Hardware and Embedded Systems, Vol 2023, Iss 3 (2023)
In this paper we present the first formally verified implementations of Kyber and, to the best of our knowledge, the first such implementations of any post-quantum cryptosystem. We give a (readable) formal specification of Kyber in the EasyCrypt proo
Externí odkaz:
https://doaj.org/article/c082783eb324437292b239d88846e0e8
Publikováno v:
Logical Methods in Computer Science, Vol Volume 18, Issue 2 (2022)
Faces play a central role in the combinatorial and computational aspects of polyhedra. In this paper, we present the first formalization of faces of polyhedra in the proof assistant Coq. This builds on the formalization of a library providing the bas
Externí odkaz:
https://doaj.org/article/9efc2b3e111647cfb13ae78165495090
Publikováno v:
Logical Methods in Computer Science, Vol Volume 15, Issue 4 (2019)
Recent developments in formal verification have identified approximate liftings (also known as approximate couplings) as a clean, compositional abstraction for proving differential privacy. This construction can be defined in two styles. Earlier defi
Externí odkaz:
https://doaj.org/article/4bb4567898494012ad3434e7b842561b
Publikováno v:
CCS 2021-ACM SIGSAC Conference on Computer and Communications Security
CCS 2021-ACM SIGSAC Conference on Computer and Communications Security, Nov 2021, Virtual Event, South Korea. pp.2541-2563, ⟨10.1145/3460120.3484548⟩
CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security
CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security, Nov 2021, Virtual Event, South Korea. pp.2541-2563, ⟨10.1145/3460120.3484548⟩
CCS
CCS 2021-ACM SIGSAC Conference on Computer and Communications Security, Nov 2021, Virtual Event, South Korea. pp.2541-2563, ⟨10.1145/3460120.3484548⟩
CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security
CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security, Nov 2021, Virtual Event, South Korea. pp.2541-2563, ⟨10.1145/3460120.3484548⟩
CCS
International audience; In this paper we enhance the EasyCrypt proof assistant to reason about computational complexity of adversaries. The key technical tool is a Hoare logic for reasoning about computational complexity (execution time and oracle ca
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9b208fe87f394ab3c610c6a3ba5f9e67
https://doi.org/10.1145/3589962
https://doi.org/10.1145/3589962
Publikováno v:
Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c94325789d6ca1c119fe8ad5e063d2af
https://doi.org/10.1145/3573105.3575678
https://doi.org/10.1145/3573105.3575678
CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum programming language, in which classic quantum algorithms are easily expressed, and an expressive program logic fo
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::04a293ebbd0c639969a056631cfb8ba1
http://arxiv.org/abs/2207.11350
http://arxiv.org/abs/2207.11350
Publikováno v:
CPP 2022: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs
CPP 2022: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2022, Philadelphia, United States. pp.197-209, ⟨10.1145/3497775.3503692⟩
CPP 2022: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2022, Philadelphia, United States. pp.197-209, ⟨10.1145/3497775.3503692⟩
International audience; We explore the features of a user interface where formal proofs can be built through gestural actions. In particular, we show how proof construction steps can be associated to drag-and-drop actions. We argue that this can prov
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::63f92b14106ffda287fbb44dd1a9d83d
https://doi.org/10.1145/3497775.3503692
https://doi.org/10.1145/3497775.3503692
Publikováno v:
Advances in Cryptology – CRYPTO 2022 ISBN: 9783031158018
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f9caf738daaf2edde447f23f8e4bdcf6
https://doi.org/10.1007/978-3-031-15802-5_22
https://doi.org/10.1007/978-3-031-15802-5_22
Autor:
Shih-Han Hung, Gilles Barthe, Pierre-Yves Strub, Xiong Fan, Manuel Barbosa, Benjamin Grégoire, Li Zhou, Xiaodi Wu, Jonathan Katz
Publikováno v:
CCS
ACM CCS 2021-ACM SIGSAC Conference on Computer and Communications Security
ACM CCS 2021-ACM SIGSAC Conference on Computer and Communications Security, Nov 2021, Virtual Event, South Korea. pp.2564-2586, ⟨10.1145/3460120.3484567⟩
ACM CCS 2021-ACM SIGSAC Conference on Computer and Communications Security
ACM CCS 2021-ACM SIGSAC Conference on Computer and Communications Security, Nov 2021, Virtual Event, South Korea. pp.2564-2586, ⟨10.1145/3460120.3484567⟩
International audience; 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-qu
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9acee3f1c0ecab2987370fc2508fe242
https://doi.org/10.1145/3460120.3484567
https://doi.org/10.1145/3460120.3484567
Autor:
Tiago Oliveira, Adrien Koutsos, José B. Almeida, Pierre-Yves Strub, Vincent Laporte, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire
Publikováno v:
SP 2020-41st IEEE Symposium on Security and Privacy
SP 2020-41st IEEE Symposium on Security and Privacy, May 2020, San Francisco / Virtual, United States. pp.965-982, ⟨10.1109/SP40000.2020.00028⟩
IEEE Symposium on Security and Privacy
SP 2020-41st IEEE Symposium on Security and Privacy, May 2020, San Francisco / Virtual, United States. pp.965-982, ⟨10.1109/SP40000.2020.00028⟩
IEEE Symposium on Security and Privacy
We develop a new approach for building cryptographic implementations. Our approach goes the last mile and delivers assembly code that is provably functionally correct, protected against side-channels, and as efficient as handwritten assembly. We illu
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b6f1cc4c35cb2796677a765c91ed1177
https://hal.univ-lorraine.fr/hal-02974993
https://hal.univ-lorraine.fr/hal-02974993