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!
Yes. It was linked from the section on requirements, which also cites a whole bunch of ETSI standards.
Check Annex A? It's an OpenID cred, it looks like.
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.
Image showing part 2 of abstract.
Optimizing and Implementing Threshold MAYO (Diego Aranha, Giacomo Borin, Sofia Celi, Guilhem Niot) ia.cr/2026/710
Yeah, that's evolved into Nearby Share, which then became Quick Share.
en.wikipedia.org/wiki/Quick_S...
I think what you're talking about is QuickShare? Google and Samsung both maintain their own, incompatible with each other.
I often lean on LocalSend to share files with not-me over the same network. (And I just use syncthing to share with me.)
Can one make money from that?
Quantum computers break ECC as well.
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.
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.
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!
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.
Image showing part 2 of abstract.
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. 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.
Verified non-recursive calculation of Beneš networks applied to Classic McEliece (Wrenna Robson, Samuel Kelly) ia.cr/2026/107
"Designing and crafting good envelopes is really hard, you know?" he writes, for the person whose career is to design and craft really good envelopes to read.
"I want to send you a message. Would you prefer I send it on a postcard, or on a letter inside an envelope?"
"Obviously on a postcard. Someone could open the envelope and give you a false sense of security."
"Ur. What?"
OK, I've just started skimming through, and the first thing I notice is multi-user security definitions. I'm now sitting up right and wondering if I should go to the office to print it out...
This is very nice.
I saw that. And a nice piece of cryptographic design as well.
It's fine as long as all voters get a chance to double vote.
Perfect time to switch to vi.
A joyful face for a joyful book.
SUBMIT
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.
Faster Verification of Faster Implementations: Combining Deductive and Circuit-Based Reasoning in EasyCrypt (José Bacelar Almeida et al.) ia.cr/2025/1607
This is exactly the setup in this 5-bit experiment: the DL instance is set up in a subgroup of the curve of order 2^5 = 32.
There's a reason we usually pick prime order subgroups.
Uh... Working in a subgroup of order 32 seems... ill advised. Even with a 256-bit key, if I pick 2^256 as the order of the group I set up my discrete logarithm instance in, Pohlig-Hellman gives a classical attack in 512 guesses max. (256 on average.) No need for a quantum computer here.
You have 12 usable knuckles on each hand. (Usable because you can point to them nicely with your conveniently opposable thumb.)
This is now also implemented in Rosenpass. (With a more complex PQ key exchange layer.)
rosenpass.eu
Just in case anyone feels really excited, this closed 10 days ago.
ICYMI... Tough, you missed it.
Other governments are still (for now) linking government procurement and transition, and generally aligned on adoption. (France likes XMSS, Germany also likes Classic McEliece.)
Also strong signs that other countries are picking up the advocacy piece.
I'm not going to say it so I don't jinx it.
![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.](https://cdn.bsky.app/img/feed_thumbnail/plain/did:plc:fwa55bujvdrwlwlwgqmmxmuf/bafkreig6agg6pu6cl7s65czcnwu7eg74avis272jmcgxlsqokddotarkuy)
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.
Image showing part 2 of abstract.
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
