BLUE
Login
Profile banner
FD
François Dupressoir
@francois.dupressoir.eu
Proof nerd, dad, computer scientist.
22 followers24 following15 posts
OverviewPostsReplies
Reposted by François Dupressoir
MRmalb.bsky.social

My department is recruiting two lecturers (~ assistant professors) www.kcl.ac.uk/jobs/096025-... Cryptography is not high on the list of priorities for these ones, though.

Lecturer in Computer Science x2
Lecturer in Computer Science x2

0
FDfrancois.dupressoir.eu

The Rumineers

Oonlymemes.bsky.social

Name this band

In a foggy pasture with leaf-less trees in the background stand from left to right, a white llama, a tan and black sheep, a brown bull cow with a shaggy mane, a white and brown goat, and then a black and white speckled rooster in front of the cow. They are all staring moodily at you.
0
Reposted by François Dupressoir
Ccryspen.bsky.social

We are happy to announce the release of OpenMLS v0.6, a significant update to our open-source MLS implementation. This version includes several new features and improvements. Read all details on the blog: https://buff.ly/47aL5dz#MLS#opensource#cryptography

0
Reposted by François Dupressoir
CLclist.bsky.social

We are hiring a postdoc at LMU's Munich Center for Mathematical Philosophy. Areas: decision theory, social choice theory, philosophy of action, the study of agency & free will, and/or related themes in the philosophy of mind. Deadline 8 Sept. Please spread the word. job-portal.lmu.de/jobposting/4...

0
Reposted by François Dupressoir
MRmalb.bsky.social

At @SandboxAQ we're hiring for an engineering consulting position in the areas of (post-quantum) cryptography or privacy: www.iacr.org/jobs/item/3716 part-time or full-time.

0
Reposted by François Dupressoir
MRmalb.bsky.social

Postdoc Position in Cryptography: Social Foundations of Cryptography: martinralbrecht.wordpress.com/2024/06/11/c...social-foundations-of-cryptography.gitlab.io

Cryptography Postdoc Position in Social Foundations of Cryptography
Cryptography Postdoc Position in Social Foundations of Cryptography

We are looking for a postdoc to work with us on the social foundations of cryptography. This is a two-year full-time position based in London at a salary of £47,978 per annum. We. This postdoc positio...

1
Reposted by François Dupressoir
EUeprint.bsky.social

A Tight Security Proof for SPHINCS⁺, Formally Verified (Manuel Barbosa, François Dupressoiria.cr/2024/910

Abstract. SPHINCS⁺ is a post-quantum signature scheme that, at the time of writing, is being standardized as SLH-DSA. It is the most conservative option for post-quantum signatures, but the original tight proofs of security were flawed—as reported by Kudinov, Kiktenko and Fedorov in 2020. In this work, we formally prove a tight security bound for SPHINCS⁺ using the EasyCrypt proof assistant, establishing greater confidence in the general security of the scheme and that of the parameter sets considered for standardization. To this end, we reconstruct the tight security proof presented by Hülsing and Kudinov (in 2022) in a modular way. A small but important part of this effort involves a complex argument relating four different games at once, of a form not yet formalized in EasyCrypt (to the best of our knowledge). We describe our approach to overcoming this major challenge, and develop a general formal verification technique aimed at this type of reasoning. Enhancing the set of reusable EasyCrypt artifacts previously produced in the formal verification of stateful hash-based cryptographic constructions, we (1) improve and extend the existing libraries for hash functions and (2) develop new libraries for fundamental concepts related to hash-based cryptographic constructions, including Merkle trees. These enhancements, along with the formal verification technique we develop, further ease future formal verification endeavors in EasyCrypt, especially those concerning hash-based cryptographic constructions.
Image showing part 2 of abstract.
0
FDfrancois.dupressoir.eu

The University of Bristol is looking to grow its verification activities. A lectureship in verification is open in an adjacent group. The group itself is very project-driven, with the environment around it giving a nice mix of curiosity- and mission-driven groups. www.bristol.ac.uk/jobs/find/de...

0
Reposted by François Dupressoir
MRmalb.bsky.social

We are looking for a postdoc to work with us on lattice-based cryptography: www.kcl.ac.uk/jobs/090126-...malb.io/sis-with-hin...martinralbrecht.wordpress.com/2023/01/31/e...

Research Fellow/Research Associate in Cryptography
Research Fellow/Research Associate in Cryptography

0
Reposted by François Dupressoir
EUeprint.bsky.social

Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt (José Bacelar Almeida et al.ia.cr/2024/843

Abstract. We present a formally verified proof of the correctness and IND-CCA security of ML-KEM, the Kyber-based Key Encapsulation Mechanism (KEM) undergoing standardization by NIST. The proof is machine-checked in EasyCrypt and it includes: 1) A formalization of the correctness (decryption failure probability) and IND-CPA security of the Kyber base public-key encryption scheme, following Bos et al. at Euro S&P 2018; 2) A formalization of the relevant variant of the Fujisaki-Okamoto transform in the Random Oracle Model (ROM), which follows closely (but not exactly) Hofheinz, Hovelmanns and Kiltz at TCC 2017; 3) A proof that the IND-CCA security of the ML-KEM specification and its correctness as a KEM follows from the previous results; 4) Two formally verified implementations of ML-KEM written in Jasmin that are provably constant-time, functionally equivalent to the ML-KEM specification and, for this reason, inherit the provable security guarantees established in the previous points. The top-level theorems give self-contained concrete bounds for the correctness and security of MLKEM down to (a variant of) Module-LWE. We discuss how they are built modularly by leveraging various EasyCrypt features.
Image showing part 2 of abstract.
0
Profile banner
FD
François Dupressoir
@francois.dupressoir.eu
Proof nerd, dad, computer scientist.
22 followers24 following15 posts
HomePopularExplore