Lightnews — Scholar-powered news

Reposted by Sabine Oechsner 🟥

KIT Graduate School Cyber Security @kitcybersec.bsky.social · 5d

You are an Early Career Researcher in #cybersec? Here is an opportunity: The AEC chairs of @USENIXSecurity '26 are looking for (self)nominations for the Artifact Evaluation Committee. Deadline: October 17th, 2025, so sign up soon!
@chwress.bsky.social, @kumarde.bsky.social, @aurore-fass.bsky.social

9 5

Reposted by Sabine Oechsner 🟥

ePrint Updates @eprint.ing.bot · 7d

Who Verifies the Verifiers? Lessons Learned From Formally Verified Line-Point Zero-Knowledge (Sabine Oechsner, Vitor Pereira, Peter Scholl) ia.cr/2025/1835

Abstract. Computer-aided cryptography, with particular emphasis on formal verification, promises an interesting avenue to establish strong guarantees about cryptographic primitives. The appeal of formal verification is to replace the error-prone pen-and-paper proofs with a proof that was checked by a computer and, therefore, does not need to be checked by a human. In this paper, we ask the question of how reliable are these machine-checked proofs by analyzing a formally verified implementation of the Line-Point Zero-Knowledge (LPZK) protocol (Dittmer, Eldefrawy, Graham-Lengrand, Lu, Ostrovsky and Pereira, CCS 2023). The implementation was developed in EasyCrypt and compiled into OCaml code that was claimed to be high-assurance, i.e., that offers the formal guarantees of guarantees of completeness, soundness, and zero knowledge. We show that despite these formal claims, the EasyCrypt model was flawed, and the implementation (supposed to be high-assurance) had critical security vulnerabilities. Concretely, we demonstrate that: 1) the EasyCrypt soundness proof was incorrectly done, allowing an attack on the scheme that leads honest verifiers into accepting false statements; and 2) the EasyCrypt formalization inherited a deficient model of zero knowledge for a class of non-interactive zero knowledge protocols that also allows the verifier to recover the witness. In addition, we demonstrate 3) a gap in the proof of the perfect zero knowledge property of the LPZK variant of Dittmer, Ishai, Lu and Ostrovsky (CCS 2022) that the EasyCrypt proof is based, which, depending on the interpretation of the protocol and security claim, could allow a malicious verifier to learn the witness. Our findings highlight the importance of scrutinizing machine-checked proofs, including their models and assumptions. We offer lessons learned for both users and reviewers of tools like EasyCrypt, aimed at improving the transparency, rigor, and accessibility of machine-checked proofs. By sharing our methodology and challenges, we hope to foster a culture of deeper engagement with formal verification in the cryptographic community.

3 3

Reposted by Sabine Oechsner 🟥

Nigel Smart @smartcryptology.bsky.social · 8d

Volume 2 Issue 3 of Communications in Cryptology is now available....

cic.iacr.org/i/2/3

Volume 2, Issue 3

cic.iacr.org

2 3

Sabine Oechsner 🟥 @proofnerd.bsky.social · 8d

What you don't need to check anymore is the proof itself. That's what computers are for 😎 (Once someone has told them how to check your proofs...)

Deirdre Connolly¹ ² @durumcrustulum.com · May 6

🤞

1

Sabine Oechsner 🟥 @proofnerd.bsky.social · 8d

Checking definitions is way easier than proving stuff! I promise!

1

Sabine Oechsner 🟥 @proofnerd.bsky.social · 8d

TL;DR: Yes, formal verification is cool and everything, but cryptographers should still check each other's definitions 🤷 (And not only the ones in the paper. Also the ones in the actual code!)

1

Sabine Oechsner 🟥 @proofnerd.bsky.social · 8d

New paper with Vitor Pereira and Peter Scholl (@schollster.bsky.social)!

We found flaws in a supposedly formally verified security proof of LPZK, leading to attacks on soundness and zk.
The culprit: a mismatch between definitions in their code and the original LPZK papers.

cic.iacr.org/p/2/3/24

Screenshot from CiC website:

Who Verifies the Verifiers? Lessons Learned from Formally Verified Line-Point Zero-Knowledge

Authors Sabine Oechsner, Vitor Pereira, Peter Scholl

1 1 4

Reposted by Sabine Oechsner 🟥

depths of wikipedia @depthsofwikipedia.bsky.social · 10d

this is the photo in the "absurdity" article on Danish Wikipedia ("A rabbit with a waffle. On the head")

20 560 1.9K

Sabine Oechsner 🟥 @proofnerd.bsky.social · 21d

What do you mean by garbage? Hasn't the policy always been to accept anything that remotely resembles a paper about crypto?

2 2

Sabine Oechsner 🟥 @proofnerd.bsky.social · 28d

It dings you for having coauthors.

1

Reposted by Sabine Oechsner 🟥

Sophie Schmieg @sophieschmieg.infosec.exchange.ap.brid.gy · Sep 13

When you think about it, we really should call "Tesla autopilot" vibe driving

3 68 3

Sabine Oechsner 🟥 @proofnerd.bsky.social · Sep 12

Asiacrypt camera-ready?

Reposted by Sabine Oechsner 🟥

str👻d @str4d.xyz · Sep 12

Apparently the threshold for the auto-moderator to tag an entire account as spam is currently 15 image posts within 2 minutes.

Which cryptography conference submission deadline just passed? 😅

Screenshot of my ePrint bot account. The account has been labeled as spam, due to a large number of ePrints being published at the same time.

1 2 10

Sabine Oechsner 🟥 @proofnerd.bsky.social · Sep 9

Also very interesting to see the different attitudes towards review load per PC member and subreviewing across various communities.

Sabine Oechsner 🟥 @proofnerd.bsky.social · Sep 9

Interesting approach from the PL community to deal with reviewing an unexpectedly high number of submissions...

SIGPLAN @sigplan.bsky.social · Sep 9

The OOPSLA 2025 RC chairs, @shriram.bsky.social and Sukyoung Ryu, required some submitting authors to agree to review. Their new blog post describes the policy and its outcomes this year. blog.sigplan.org/2025/09/09/t...

blog.sigplan.org

1 1

Reposted by Sabine Oechsner 🟥

Andrea Basso @andreavbasso.bsky.social · Sep 9

More than 500 researchers have signed an open letter against the dangerous EU proposal on chat control.

The proposal remains ineffective, undoes decades of results in E2E encryption, and threatens the privacy of half a billion citizens.

csa-scientist-open-letter.org/Sep2025

csa-scientist-open-letter.org

1 12 16

Sabine Oechsner 🟥 @proofnerd.bsky.social · Sep 7

What dark corners of the internet were you exploring when you found that 🤨

2

Reposted by Sabine Oechsner 🟥

ePrint Updates @eprint.ing.bot · Sep 3

How Hard Can It Be to Formalize a Proof? Lessons from Formalizing CryptoBox Three Times in EasyCrypt (François Dupressoir, Andreas Hülsing, Cameron Low, Matthias Meijers, Charlotte Mylog, Sabine Oechsner) ia.cr/2025/1569

Abstract. Provable security is a cornerstone of modern cryptography, aiming to provide formal and precise security guarantees. However, for various reasons, security proofs are not always properly verified, possibly leading to unwarranted security claims and, in the worst case, deployment of insecure constructions. To further enhance trust and assurance, machine-checked cryptography makes these proofs more formal and rigorous. Unfortunately, the complexity of writing machine-verifiable proofs remains prohibitively high in many interesting use-cases. In this paper, we investigate the sources of this complexity, specifically examining how the style of security definitions influences the difficulty of constructing machine-verifiable proofs in the context of game-playing security.

Concretely, we present a new security proof for the generic construction of a PKAE scheme from a NIKE and AE scheme, written in a code-based, game-playing style à la Bellare and Rogaway, and compare it to the same proof written in the style of state-separating proofs, a methodology for developing modular game-playing security proofs. Additionally, we explore a third “blended” style designed to avoid anticipated difficulties with the formalization. Our findings suggest that the choice of definition style impacts proof complexity—including, we argue, in detailed pen-and-paper proofs—with trade-offs depending on the proof writer’s goals.

2 6

Reposted by Sabine Oechsner 🟥

mccurley.bsky.social @mccurley.bsky.social · Aug 16

Turns out that discuss.iacr.org is getting some interesting participation in response to the survey that was put out. If you received an invitation, you should consider joining just to read along.

International Association for Cryptologic Research

A place to discuss matters related to IACR

discuss.iacr.org

2 3

Sabine Oechsner 🟥 @proofnerd.bsky.social · Aug 15

Wait, the thing even says "teskt" 😅

Sabine Oechsner 🟥 @proofnerd.bsky.social · Aug 15

test test test

An empty beach volleyball court. The banner on the fence says "Volleybalvelddoek test tekst 120 pt. Volleybalvelddoek test tekst 60 pt."

1 1

Reposted by Sabine Oechsner 🟥

Alex @alexanderlhicks.com · Aug 8

I'm hiring at the EF: jobs.lever.co/ethereumfoun...

If you're into Ethereum, cryptography, and formal verification, please get in touch! 🙂

Ethereum Foundation - Researcher/Engineer (Formal Verification)

Role summary As a member of the Protocol Snarkification team, you will work towards snarkifying Ethereum by working to specify and verify the core cryptographic components of proof systems and their i...

jobs.lever.co

2 2

Sabine Oechsner 🟥 @proofnerd.bsky.social · Aug 3

If you are near Aarhus and don't mind a little trip, you can pick it up yourself from Proshop? www.proshop.dk/Kaffe-og-Esp...

Bialetti Moka Induction 2.0 - 6 cups | På lager | Billig

303,00 kr. Espressokande, 6 kop, rød & sølv Med denne espressokande kan du lave 6 kopper kaffe. Hurtig levering

www.proshop.dk

1 1

Reposted by Sabine Oechsner 🟥

Janno Siim @jannosiim.bsky.social · Jul 16

Springer just sent an "Urgent" email that many authors from Crypto 2025 (all from ZK community) have broken references provided as "?" in their camera-ready version:

2 2 4

Reposted by Sabine Oechsner 🟥

Real World Crypto Symposium @rwc.iacr.org · Jul 13

The Call for Contributed Talks is now open for RWC 2026! And the deadline for submissions is now Oct. 10, 2025.
rwc.iacr.org/2026/contrib...

RWC 2026 call for papers

Real World Crypto Symposium

rwc.iacr.org

1 9 12