Tessera

Folgen

François Dupressoir

@francois.dupressoir.eu

Proof nerd, dad, computer scientist.

69 Posts109 Follower 65 Folgt

post malone ergo propter malone @proptermalone.bsky.social · last mo.

just to be excruciatingly clear it is also not okay to shoot the target of your warrant as an arresting LEO. the warrant is not a warrant to shoot someone. it is a warrant for arrest.

Doreen Riepel @doreenriepel.bsky.social · 3mo ago

Join us tomorrow for ProTeCS, one of Eurocrypt’s affiliated events! We are thankful to have two amazing invited speakers, Bart Mennink and Mike Rosulek! We are also happy to have seven contributed talks from the community. Check out our full program here: protecs-workshop.gitlab.io/program

Program

Workshop on Proofs and Proof Techniques for Cryptographic Security. Affiliated with Eurocrypt 2026.

protecs-workshop.gitlab.io

Sabine Oechsner @proofnerd.bsky.social · 4mo ago

I'm looking for a PhD student to work with me on formal verification for cryptographic protocols. This is a 4-year position at VU Amsterdam, co-supervised with Kristina Sojakova. Send me an email if you want to know more!

ePrint Updates @eprint.ing.bot · 4mo ago

Optimizing and Implementing Threshold MAYO (Diego Aranha, Giacomo Borin, Sofia Celi, Guilhem Niot) ia.cr/2026/710

Abstract. Threshold signatures distribute trust across multiple parties, eliminating single points of failure and reducing insider and key-exfiltration risks—properties that are increasingly important for high-assurance deployments and recently emphasized by NIST’s Multi-Party Threshold Cryptography (MPTC) initiative. We present a practical t-out-of-n threshold variant and emulation of MAYO, a post-quantum signature candidate to NIST’s call for additional signatures. Our proposal builds upon the threshold MAYO design of Celi, Escudero and Niot (PQCrypto2025), which we significantly refine to achieve practical performance. To this end, we introduce two algorithmic modifications to MAYO tailored for the distributed setting: (1) Explicit-Salt MAYO, which allows for pre-determined salts to enable a single-round online phase; and (2) Depth-Reduced MAYO, which restructures the signing algorithm to minimize the depth of secret-dependent operations. We then propose a unified protocol framework that integrate these techniques, plus other MPC specific optimizations, with the goal of minimizing online latency. Finally, we provide a concrete instantiation and local emulation in the dishonest majority setting, secure against active adversaries. Our emulation shows that threshold signing is practical at typical threshold sizes and amenable to deployment. By releasing an open-source implementation and reporting end-to-end performance, this work offers a concrete reference for the thresholdization of post-quantum signatures. Clearly the aforementioned framework is not limited to MAYO, and can be applied to the UOV family of signatures more generally.

School of Computer Science University of Bristol @compscibristol.bsky.social · 6mo ago

We’re hiring in Artificial Intelligence We are recruiting two Lecturers / Senior Lecturers in AI to join our growing, world-leading community. 📅 Closing date: 24 March 🔗 Full details & apply: www.bristol.ac.uk/jobs/find/de... Please share with anyone who might be interested.

François Dupressoir @francois.dupressoir.eu · 7mo ago

This was a fun piece of work, if your idea of fun is trying to prove false for a month before realising that the RFC and its reference implementation are equivalent for the parameters defined in the RFC (and elsewhere) but not for all values of the parameters. Fortunately for me, it's mine.

ePrint Updates@eprint.ing.bot · 7mo ago

Completing the Chain: Verified Implementations of Hash-Based Signatures and Their Security (Manuel Barbosa, François Dupressoir, Rui Fernandes, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub) ia.cr/2026/134

Abstract. We present the first formally verified implementation of a hash-based signature scheme that is linked to a machine-checked proof of security. Specifically, we provide reference implementations of XMSS and XMSS^(MT) written in Jasmin, targeting the AMD64 architecture. Beyond the implementations, we provide formal EasyCrypt specifications of XMSS and XMSS^(MT), transcribed from RFC~8391, and prove that our implementations adhere to these specifications. Furthermore, for XMSS, we give a machine-checked proof that our specification of RFC~8391 refines the abstract specification proven secure in EasyCrypt by Barbosa, Dupressoir, Grégoire, Hülsing, Meijers and Strub [CRYPTO’23]. In particular, we prove the security of our specification via a reduction, demonstrating that breaking our specification contradicts the [CRYPTO’23] result for our instantiation. Consequently, our implementation is not only functionally correct, but also adheres to a specification that is proven secure. The core technical challenge in our work resides in bridging low-level implementations of TreeHash algorithms with high-level functional specifications used in the pre-existing formalization.

Doreen Riepel @doreenriepel.bsky.social · 7mo ago

Planning your trip to Eurocrypt or looking for an excuse to still go? The reviewers did not appreciate your too involved or too elegant proofs? Consider submitting a talk to ProTeCS (protecs-workshop.gitlab.io), an affiliated event of EC, where we celebrate proofs as independent objects of study!

Call for Presentations

Workshop on Proofs and Proof Techniques for Cryptographic Security. Affiliated with Eurocrypt 2026.

protecs-workshop.gitlab.io

ePrint Updates @eprint.ing.bot · 7mo ago

Extending RISC-V to Support Flexible-Radix Multiply-Accumulate Operations (Isaar Ahmad, Hao Cheng, Johann Großschädl, Daniel Page) ia.cr/2026/108

Abstract. Specified as part of the (standard, optional) M extension, the mul and mulhu instructions reflect support for unsigned integer multiplication in RISC-V base Instruction Set Architectures (ISAs) such as RV32I and RV64I: given w-bit integers x and y for a word size w, they respectively produce the less- and more-significant w bits of the (2 · w)-bit product r = x × y. This typically minimal, and hence RISC-like form contrasts sharply with many alternative ISAs. For example, ARMv7-M includes a rich set of multiply and multiply-accumulate instructions; these cater for a wide variety of important use-cases in cryptography, where multi-precision integer arithmetic is often a central requirement. In this paper, we explore the extension of RV32I and RV64I, i.e., an Instruction Set Extension (ISE), with richer support for unsigned integer multiplication. Our design has three central features: 1) it includes dedicated carry propagation and multiply-accumulate instructions, 2) those instructions allow flexible selection of the radix (thus catering for reduced- and full-radix representations), and 3) the design can be considered for any w, and so uniformly across both RV32I and RV64I. A headline outcome of our evaluation is that, for X25519-based scalar multiplication, use of the ISE affords 1.5× and 1.6× improvement for full- and reduced-radix cases, respectively, on RV32I, and 1.3× and 1.7× improvement for full- and reduced-radix cases, respectively, on RV64I.

ePrint Updates @eprint.ing.bot · 7mo ago

Veriﬁed non-recursive calculation of Beneš networks applied to Classic McEliece (Wrenna Robson, Samuel Kelly) ia.cr/2026/107

Abstract. The Beneš network can be utilised to apply a single permutation to different inputs repeatedly. We present novel generalisations of Bernstein’s formulae for the control bits of a Beneš network and from them derive an iterative control bit setting algorithm. We provide verified proofs of our formulae and prototype a a provably correct implementation in the Lean language and theorem prover. We develop and evaluate portable and vectorised implementations of our algorithm in the C programming language. Our implementation utilising Intel’s Advanced Vector eXtensions 2 feature reduces execution latency by 25% compared to the equivalent implementation in the libmceliece software library.

François Dupressoir @francois.dupressoir.eu · 11mo ago

SUBMIT

Marcus Brinkmann@lambdafu.bsky.social · 11mo ago

This is a friendly reminder that the call for contributed talks to Real World Crypto in Taipei 2026 is open until October 10. We are looking for interesting talks bridging cryptography and its real-world use! Also it’s a great way to meet new people! rwc.iacr.org/2026/contrib...

ePrint Updates @eprint.ing.bot · 11mo ago

Faster Verification of Faster Implementations: Combining Deductive and Circuit-Based Reasoning in EasyCrypt (José Bacelar Almeida et al.) ia.cr/2025/1607

Abstract. We propose a hybrid formal verification approach that combines high-level deductive reasoning and circuit-based reasoning and apply it to highly optimized cryptographic assembly code. Our approach permits scaling up formal verifi- cation in two complementary directions: 1) it reduces the proof effort required for low-level functions where the computation logics are obfuscated by the intricate use of architecture-specific instructions and 2) it permits amortizing the effort of proving one implementation by using equivalence checking to propagate the guarantees to other implementations of the same computation using different optimizations or targeting different architectures. We demonstrate our approach via an extension to the EasyCrypt proof assistant and by revisiting formally verified implementations of ML-KEM in Jasmin. As a result, we obtain the first formally verified implementation of ML-KEM that offers performance comparable to the fastest non-verified implementation in x86-64 architectures.

ePrint Updates @eprint.ing.bot · last yr.

Threshold Signatures Reloaded: ML-DSA and Enhanced Raccoon with Identifiable Aborts (Giacomo Borin, Sofía Celi, Rafael del Pino, Thomas Espitau, Guilhem Niot, Thomas Prest) ia.cr/2025/1166

Abstract. Threshold signatures enable multiple participants to collaboratively produce a digital signature, ensuring both fault tolerance and decentralization. As we transition to the post-quantum era, lattice-based threshold constructions have emerged as promising candidates. However, existing approaches often struggle to scale efficiently, lack robustness guarantees, or are incompatible with standard schemes — most notably, the NIST-standard ML-DSA. In this work, we explore the design space of Fiat-Shamir-based lattice threshold signatures and introduce the two most practical schemes to date. First, we present an enhanced TRaccoon-based [DKM+24] construction that supports up to 64 participants with identifiable aborts, leveraging novel short secret-sharing techniques to achieve greater scalability than previous state-of-the-art methods. Second — and most importantly — we propose the first practical ML-DSA-compatible threshold signature scheme, supporting up to 6 users. We provide full implementations and benchmarks of our schemes, demonstrating their practicality and efficiency for real-world deployment as protocol messages are computed in at most a few milliseconds, and communication cost ranges from 10.5 kB to 525 kB depending on the threshold.

Martin R. Albrecht @malb.bsky.social · 2y ago

Come work with the rather excellent @bedow.bsky.social (and also me)

Benjamin Dowling@bedow.bsky.social · 2y ago

Excited to announce a funded PhD position analysing the Social Foundations of Cryptography here at King's College London with me and @malb.bsky.social . Applications open now, feel free to reach out for a chat. social-foundations-of-cryptography.gitlab.io Link in next post!

ePrint Updates @eprint.ing.bot · 2y ago

Parametrizing Maximal Orders Along Supersingular ℓ-Isogeny Paths (Laia Amorós, James Clements, Chloe Martindale) ia.cr/2025/033

Abstract. Suppose you have a supersingular ℓ-isogeny graph with vertices given by j-invariants defined over 𝔽_(p²), where p = 4 ⋅ f ⋅ ℓ^(e) − 1 and ℓ ≡ 3 (mod 4). We give an explicit parametrization of the maximal orders in B_(p, ∞) appearing as endomorphism rings of the elliptic curves in this graph that are ≤ e steps away from a root vertex with j-invariant 1728. This is the first explicit parametrization of this kind and we believe it will be an aid in better understanding the structure of supersingular ℓ-isogeny graphs that are widely used in cryptography. Our method makes use of the inherent directions in the supersingular isogeny graph induced via Bruhat-Tits trees, as studied in [1]. We also discuss how in future work other interesting use cases, such as ℓ = 2, could benefit from the same methodology.

Martin R. Albrecht @malb.bsky.social · 2y ago

Khanh and Eamonn are organising UK Crypto Day on 20 February at King's College London. Registration is free (and open) but required: uk-crypto-day.github.io/2025/02/20/u... Help us spread the word and see you there.

UK Crypto Day: 20 February 2025

Schedule

uk-crypto-day.github.io

François Dupressoir @francois.dupressoir.eu · 2y ago

The ProTeCS 2025 call for presentations is out. (Short) Submissions by February 20, 2025. Then off to Madrid just before EuroCrypt to present your nerdy results. (May 3.) Proof nerds: shape the community, and submit the kind of work you want to hear about! protecs-workshop.gitlab.io/call

Call for Presentations

Workshop on Proofs and Proof Techniques for Cryptographic Security. Affiliated with Eurocrypt 2025.

protecs-workshop.gitlab.io

Deirdre Connolly¹ ² @durumcrustulum.com · 2y ago

The EasyCrypt proofs for X-Wing are now on GitHub: github.com/formosa-cryp...

GitHub - formosa-crypto/formosa-x-wing

Contribute to formosa-crypto/formosa-x-wing development by creating an account on GitHub.

github.com

Real World Crypto Symposium @rwc.iacr.org · 2y ago

Stipend applications for #RealWorldCrypto2025 are now open! These grants support students, early-career researchers, and individuals from underrepresented groups, enabling them to engage with pivotal developments in cryptographic research and applications. rwc.iacr.org/2025/stipend...

RWC 2025 student stipends

Real World Crypto Symposium

rwc.iacr.org

Martin R. Albrecht @malb.bsky.social · 2y ago

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

kcl.ac.uk

François Dupressoir @francois.dupressoir.eu · 2y ago

The Rumineers

OnlyMemes@onlymemes.bsky.social · 2y ago

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.

Cryspen @cryspen.com · 2y ago

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

OpenMLS 0.6 released

Today, we are releasing version 0.6 of OpenMLS. In this post we’ll go over the most significant changes since our last release. New Storage Provider To make it easier to persist group state, the…

buff.ly

Christian List @clist.bsky.social · 2y ago

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...

Postdoctoral Fellow (m/f/x)

job-portal.lmu.de

Martin R. Albrecht @malb.bsky.social · 2y ago

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.

Engineering Consulting Position

iacr.org

Martin R. Albrecht @malb.bsky.social · 2y ago

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

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...

martinralbrecht.wordpress.com

ePrint Updates @eprint.ing.bot · 2y ago

A Tight Security Proof for SPHINCS⁺, Formally Verified (Manuel Barbosa, François Dupressoir, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub) ia.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.

François Dupressoir @francois.dupressoir.eu · 2y ago

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...

Details | Working at Bristol | University of Bristol

bristol.ac.uk

Martin R. Albrecht @malb.bsky.social · 2y ago

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

Research Fellow/Research Associate in Cryptography

kcl.ac.uk

ePrint Updates @eprint.ing.bot · 2y ago

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.

ePrint Updates @eprint.ing.bot · 2y ago

SQIsign2D-West: The Fast, the Small, and the Safer (Andrea Basso, Luca De Feo, Pierrick Dartois, Antonin Leroux, Luciano Maino, Giacomo Pope, Damien Robert, Benjamin Wesolowski) ia.cr/2024/760

Abstract. We introduce SQIsign2D-West, a variant of SQIsign using two-dimensional isogeny representations. SQIsignHD was the first variant of SQIsign to use higher dimensional isogeny representations. Its eight-dimensional variant is geared towards provable security but is deemed unpractical. Its four-dimensional variant is geared towards efficiency and has significantly faster signing times than SQIsign, but slower verification owing to the complexity of the four-dimensional representation. Its authors commented on the apparent difficulty of getting any improvement over SQIsign by using two-dimensional representations. In this work, we introduce new algorithmic tools that make two-dimensional representations a viable alternative. These lead to a signature scheme with sizes comparable to SQIsignHD, slightly slower signing than SQIsignHD but still much faster than SQIsign, and the fastest verification of any known variant of SQIsign. We achieve this without compromising on the security proof: the assumptions behind SQIsign2D-West are similar to those of the eight-dimensional variant of SQIsignHD. Additionally, like SQIsignHD, SQIsign2D-West favourably scales to high levels of security Concretely, for NIST level I we achieve signing times of 80 ms and verifying times of 4.5 ms, using optimised arithmetic based on intrinsics available to the Ice Lake architecture. For NIST level V, we achieve 470 ms for signing and 31 ms for verifying.

Martin R. Albrecht @malb.bsky.social · 2y ago

UK Crypto Day | 20 June 2024 | Edinburgh uk-crypto-day.github.io/2024/06/20/u...

UK Crypto Day: 20 June 2024 at The University of Edinburgh

Schedule

uk-crypto-day.github.io