Benoit Viguier
– PhD in Cryptography & Formal methods
Benoit Viguier
[--cv] ... [--phd] [--gh] [--mail] [-l]
Benoit Viguier
is a Cryptographer at ABN AMRO in Amsterdam, The Netherlands.
Before that he was a PhD student at the Digital Security group and the Department of Software Science of the Radboud University in Nijmegen, working on tools for formally verifying cryptographic software under the supervision of Peter Schwabe, Freek Wiedijk, Joan Daemen and Herman Geuvers.
In 2014-2015, he was an engineering student at the INSA Rennes (National Institute of Applied Science, France) and master student in Research in Computer Science (MRI).
--cv
--phd
--gh
GitHub repository.
--mail
λ x y.
x @ y .nl
benoit viguier
-l
| --location
Zwanenveld 9150
6538 SJ Nijmegen
The Netherlands
TLK-2024-0506 -
Real World Cryptography in Practive
Benoît Viguier
Guest speaker - Applied Cryptography Lecture - Radboud Universiteit
We provide an overview of how cryptography is used in enterprises and its challenges. We then describe the solutions developed at ABN AMRO BANK to tackle those.
[slides]
TLK-2021-1213 -
A Panorama on Classical Cryptography
Benoît Viguier
PhD Defense
In this thesis we cover a large part of the classical cryptography world: we examine the design of new symmetric primitive; we explore implementation strategies of lightweight schemes; we analyze a new high performance algorithm; we use formal verification to prove the correctness of Elliptic Curve Cryptography implementations; and finally we describe one of the way algorithms are standardized.
[slides]
[www]
TLK-2021-0624 -
A Coq proof of the correctness of X25519 in TweetNaCl
Peter Schwabe and Benoît Viguier and Timmy Weerwag and Freek Wiedijk
34th IEEE Computer Security Foundations Symposium - CSF 2021
Presentation of the complete proof of the correctness of X25519 in TweetNaCl at CSF 2021.
[YT]
TLK-2020-1216 -
Assembly or Optimized C for Lightweight Cryptography on RISC-V?
Fabio Campos and Lars Jellema and Mauk Lemmen and Lars Müller and Daan Sprenkels and Benoit Viguier
CONFERENCE ON CRYPTOLOGY AND NETWORK SECURITY - CANS 2020
Presentation of the complete proof of the correctness of X25519 in TweetNaCl at CANS 2020.
[YT]
PUB-2020-1209 -
A Coq proof of the correctness of X25519 in TweetNaCl
Peter Schwabe and Benoit Viguier and Timmy Weerwag and Freek Wiedijk
34th IEEE Computer Security Foundations Symposium - CSF 2021
We formally prove that the C implementation of the X25519 key-exchange protocol in the TweetNaCl library is correct. We prove both that it correctly implements the protocol from Bernstein’s 2006 paper, as standardized in RFC 7748, as well as the absence of undefined behavior like arithmetic overflows and array out of bounds errors. We also formally prove, based on the work of Bartzia and Strub, that X25519 is mathematically correct, i.e., that it correctly computes scalar multiplication on the elliptic curve Curve25519.
The proofs are all computer-verified using the Coq theorem prover. To establish the link between C and Coq we use the Verified Software Toolchain (VST).
[pdf]
PUB-2020-0707 -
Assembly or Optimized C for Lightweight Cryptography on RISC-V?
Fabio Campos and Lars Jellema and Mauk Lemmen and Lars Müller and Daan Sprenkels and Benoit Viguier
CONFERENCE ON CRYPTOLOGY AND NETWORK SECURITY - CANS 2020
we analyzed different strategies for the optimization of several candidates of NIST's lightweight cryptography standardization project on a RISC-V architecture. In particular, we studied the general impact of optimizing symmetric-key algorithms in assembly and in plain C.
[pdf]
TLK-2019-1129 -
A Coq proof of the correctness of X25519 in TweetNaClPresentation of the complete proof of the correctness of X25519 in TweetNaCl at the Crypto Working Group in Utrecht.
TLK-2019-1025 -
Advance Use of GitBrief presentation of branches and other functionalities of Git at ICIS DS Lunch Talk in Nijmegen.
TLK-2019-0318 -
Verification of TweetNaCl’s Curve25519Presentation of the verification of TweetNaCl's Curve25519 implementation at Journée GT Méthodes Formelles pour la Sécurité.
TLK-2018-1204 -
Cryptanalysis of MORUSPresentation of the Linear Cryptanalysis part of Cryptanalysis of Morus at ASIACRYPT 2018.
TLK-2018-1010 -
Gimli: A Cross-Platform PermutationPresentation of Gimli at Advances in permutation-based cryptography in Milan.
TLK-2018-0717 -
KangarooTwelve draft-viguier-kangarootwelve-02Presentation of a RFC draft about KangarooTwelve at the IRTF Crypto Forum Research Group (CFRG) meeting in Montreal.
TLK-2018-0622 -
Linear Cryptanalysis of MorusPresentation of the Linear Cryptanalysis part of our paper Cryptanalysis of Morus.
PUB-2016-770 -
KangarooTwelve: fast hashing based on Keccak-p
Guido Bertoni and Joan Daemen and Michaël Peeters and Gilles Van Assche and Ronny Van Keer and Benoît Viguier
Applied Cryptography and Network Security – ACNS 2018, Lecture Notes in Computer Science, Springer-Verlag
KangarooTwelve, a fast and secure arbitrary output-length hash function aiming at a higher speed than the FIPS 202's SHA-3 and SHAKE functions.
[pdf] [www]
PUB-2018-464 -
Cryptanalysis of MORUS
Tomer Ashur and Maria Eichlseder and Martin M. Lauridsen and Gaëtan Leurent and Brice Minaud and Yann Rotella and Yu Sasaki and Benoît Viguier
Advances in Cryptology – ASIACRYPT 2018, Lecture Notes in Computer Science, Springer-Verlag
As our main result, we present a linear correlation in the keystream of full MORUS, which can be used to distinguish its output from random and to recover some plaintext bits in the broadcast setting.
[pdf]
TLK-2018-0319 -
KangarooTwelve draft-viguier-kangarootwelve-01Presentation of a RFC draft about KangarooTwelve at the IRTF Crypto Forum Research Group (CFRG) meeting in London.
TLK-2017-0926 -
Bookmarks for CryptographersPresentation of Tikz for Cryptographer and the Crypto Stack Exchange Community at CHES Rump Session in Taipei - 2017
TLK-2017-0908/0915/0927 -
Gimli: A Cross-Platform Permutation
[slides 0908] Presentation of Gimli at the Crypto Working Group in Utrecht.
[slides 0915] Presentation of Gimli at the Digital Security Lunch talk in Nijmegen.
[slides 0927] Presentation of Gimli at CHES in Taipei.
PUB-2017-630 -
Gimli: A Cross-Platform Permutation
Daniel J. Bernstein, Stefan Kölbl, Stefan Lucks, Pedro Maat Costa Massolino, Florian Mendel, Kashif Nawaz, Tobias Schneider, Peter Schwabe, François-Xavier Standaert, Yosuke Todo, and Benoît Viguier
Cryptographic Hardware and Embedded Systems – CHES 2017, Lecture Notes in Computer Science, Springer-Verlag
Gimli, a 384-bit permutation designed to achieve high security with high performance across a broad range of platforms.
[pdf] [bib] [www]
TLK-2017-0720 -
Toward the correctness of TweetNaCl’s Ed25519 with VSTPresentation of the correctness of the Big Num arithmetic of TweetNaCl at the Student presentation of the Deep Spec Summer School - 2017
TLK-2017-0718 -
KangarooTwelve draft-viguier-kangarootwelve-00Presentation of a RFC draft about KangarooTwelve at the IRTF Crypto Forum Research Group (CFRG) meeting in Prague. Presentation kindly done by Dang, Quynh (NIST).
TLK-2017-0605 -
Bookmarks for CryptographersPresentation of Tikz for Cryptographer and the Crypto Stack Exchange Community at the Summer School on real-world crypto and privacy in Croatia - 2017
TLK-2016-1209 -
Curve25519: Proving datatypes with a roosterFormalization of the Big Num arithmetic of TweetNaCl at ICIS DS Lunch
Lychee is a free and open-source photo-management tool.
2021 - Dec. - PhD defense
Officially a Doctor in Computer Science
2021 - Apr. - ABN AMRO Bank
Started working at CISO.
2019 - Jun. - Summer School on real-world crypto and privacy - Šibenik
Summer School organised by Radboud University, ETH Zurich & FER Zagreb about recent advances in symmetric and assymetric cryptography, privacy and software and hardware security.
2018 - Dec. – 2019 - Jan. - Internship at INRIA - Sophia-Antipolis
factorizing x86 and adding A64 in Jasmin-lang.
2018 - Mar. - Flexible Symmetric Cryptography - Leiden
Workshop organised by Christina Boura, Joan Daemen, Stefan Lucks, Bart Mennink, François-Xavier Standaert
2018 - Jan. - High Assurance Cryptographic Software Workshop - Zurich
Workshop following Real World Crypto 2018.
How formal specifications can improve the trust in cryptographic softare.
2017 - Sep. - Visit of INRIA - Sophia-Antipolis
An introduction to Jasmin-lang.
2017 - Oct. - School on Computer-Aided Security Proofs - Aarhus
Fall School organised by Bas Spitters about Computer-aided security proofs using Fstar and EasyCrypt.
2017 - Jul. - Deep Spec Summer School - Philadelphia
Summer School organised by UPenn, Princeton, Yale & MIT about Formal Methods and their applications to Compilers and Code verification.
2017 - Jun. - Summer School on real-world crypto and privacy - Šibenik
Summer School organised by Radboud University, KU Leuven, ETH Zurich & FER Zagreb about recent advances in symmetric and assymetric cryptography, privacy and software and hardware security.
2017 - Jan. - Visit of Princeton University- Princeton
A detailed introduction to VST usage.
2017 - Jan. - High Assurance Cryptographic Software Workshop - New-York
Workshop following Real World Crypto 2017.
How formal Methods and Fuzzing can improve the trust in cryptographic softare.
2016 - Internship at STMicroelectronics
Formal methods in differential and linear trail search : [report] [slides]
With respect to the original version, typos have been corrected and some parts from the Apendix have been placed after the Preface.
Presentation: A brief introduction to Logic [slides]
Copyright (C) 2024 Benoit Viguier.