Sabine Oechsner 🟥
LightNews LightNews
banner
proofnerd.bsky.social
Sabine Oechsner 🟥
@proofnerd.bsky.social
210 followers 190 following 59 posts
cryptography and pretty proofs | PL-curious | assistant professor @ VU Amsterdam

soechsner.de
Posts Replies Media Videos
proofnerd.bsky.social
I had almost forgotten about Time AI
November 25, 2025 at 8:36 PM
Reposted by Sabine Oechsner 🟥
benadida.com
The International Association for Cryptologic Research has used heliosvoting.org – my online voting system – for a number of years.

This year, a trustee lost their secret key. The election has to be re-run.

Below, a few thoughts that didn't fit in the NYT piece.

www.nytimes.com/2025/11/21/w...
Cryptographers Held an Election. They Can’t Decrypt the Results.
www.nytimes.com
November 22, 2025 at 2:40 AM
proofnerd.bsky.social
Question for the dog people: Is there any way to communicate to otherwise well-behaved dogs that you want them to go away?
November 16, 2025 at 9:46 AM
proofnerd.bsky.social
AV team knows the struggle
A flipped over display. The label on the back says "Flip the display for equipment control"
November 4, 2025 at 10:13 AM
Reposted by Sabine Oechsner 🟥
jade.packet.science
Every time I see physical attacks on TEEs, I wish someone would put out a position paper on @hdevalence.bsky.social 's "guy with a glock" model
x.com/hdevalence/s...
October 29, 2025 at 4:46 PM
Reposted by Sabine Oechsner 🟥
tobycmurray.bsky.social
Program verification methods aim to be scalable (able to reason about large programs), automatic (require little human input), and precise (reason about complex properties). Yet no method does all three. In fact, they form a "trilemma". See this very short post: verse.systems/blog/post/20...
October 22, 2025 at 11:26 AM
Reposted by Sabine Oechsner 🟥
eprint.ing.bot
What is Cryptography Hiding from Itself? (Diego F. Aranha, Nikolas Melissaris) ia.cr/2025/1951
Abstract. The European Commission’s 2022 proposal for a regulation on child sexual abuse material, popularly labelled ChatControl, obliges online services to detect, report, and remove prohibited content, through client-side scanning. This paper examines the proposal as a case of undone science in computer security ethics: a domain where technical feasibility and rights-compatibility questions remain systematically underexplored. Combining legal analysis with philosophy of technology, the paper argues that client-side scanning transforms end-to-end encryption from a right to secrecy into a conditional privilege of use. By integrating Isaiah Berlin’s concept of negative liberty, Langdon Winner’s account of the politics of artifacts, and David Hess’s notion of undone science, the analysis traces how design choices become moral constraints. The discussion situates the European debate within broader concerns about proportionality, epistemic selectivity, and the governance of digital infrastructures. Ultimately, the study shows that the controversy over ChatControl is not only about privacy or child protection but about the epistemic norms that define what counts as legitimate technological knowledge. Image showing part 2 of abstract.
October 20, 2025 at 1:09 AM
Reposted by Sabine Oechsner 🟥
mccurley.bsky.social
How dominant is LaTeX in computer science? Very. It turns out that among the 1895 papers uploaded to eprint.iacr.org this year, it looks like 3 were produced from typst, 10 were produced from Microsoft Word, and three of indeterminate origin. The rest were various flavors of LaTeX.
Cryptology ePrint Archive
eprint.iacr.org
October 19, 2025 at 7:23 AM
Reposted by Sabine Oechsner 🟥
aurore-fass.bsky.social
Last chance to (self-) nominate for USENIX Security'26 Artifact Evaluation Committee!
You should expect a low load of ~1 artifact for functionality/reproducibility assessments per cycle (max 3 for the whole year).

Please support Open Science and fill the form by Oct 17: forms.gle/WoYRX4govNY1... 🚀
(Self-)Nomination for the USENIX Security '26 Artifact Evaluation Committee (AEC)
For the seventh year, USENIX Security allows the evaluation of artifacts that support a paper: software, hardware, evaluation data and documentation, raw measurement data, raw survey results, mechaniz...
forms.gle
October 16, 2025 at 5:48 AM
Reposted by Sabine Oechsner 🟥
kitcybersec.bsky.social
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
October 10, 2025 at 10:16 AM
Reposted by Sabine Oechsner 🟥
eprint.ing.bot
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. Image showing part 2 of abstract.
October 8, 2025 at 3:36 AM
Reposted by Sabine Oechsner 🟥
smartcryptology.bsky.social
Volume 2 Issue 3 of Communications in Cryptology is now available....

cic.iacr.org/i/2/3
Volume 2, Issue 3
cic.iacr.org
October 7, 2025 at 6:57 AM
proofnerd.bsky.social
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
October 7, 2025 at 7:21 AM
Reposted by Sabine Oechsner 🟥
depthsofwikipedia.bsky.social
this is the photo in the "absurdity" article on Danish Wikipedia ("A rabbit with a waffle. On the head")
En kanin med en vaffel. På hovedet.
October 4, 2025 at 10:17 PM
Reposted by Sabine Oechsner 🟥
sophieschmieg.infosec.exchange.ap.brid.gy
When you think about it, we really should call "Tesla autopilot" vibe driving
September 13, 2025 at 1:49 AM
Reposted by Sabine Oechsner 🟥
str4d.xyz
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.
September 12, 2025 at 2:26 PM
proofnerd.bsky.social
Interesting approach from the PL community to deal with reviewing an unexpectedly high number of submissions...
sigplan.bsky.social 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
September 9, 2025 at 7:10 PM
Reposted by Sabine Oechsner 🟥
andreavbasso.bsky.social
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
September 9, 2025 at 10:40 AM
Reposted by Sabine Oechsner 🟥
eprint.ing.bot
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 à 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. Image showing part 2 of abstract.
September 3, 2025 at 11:58 PM
Reposted by Sabine Oechsner 🟥
mccurley.bsky.social
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
August 16, 2025 at 4:58 AM
proofnerd.bsky.social
test test test
An empty beach volleyball court. The banner on the fence says "Volleybalvelddoek test tekst 120 pt. Volleybalvelddoek test tekst 60 pt."
August 15, 2025 at 10:41 AM
Reposted by Sabine Oechsner 🟥
alexanderlhicks.com
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
August 8, 2025 at 12:46 PM
Reposted by Sabine Oechsner 🟥
jannosiim.bsky.social
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:
July 16, 2025 at 11:25 AM
Reposted by Sabine Oechsner 🟥
rwc.iacr.org
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
July 13, 2025 at 3:52 PM
Reposted by Sabine Oechsner 🟥
eprint.ing.bot
Replication of Quantum Factorisation Records with an 8-bit Home Computer, an Abacus, and a Dog (Peter Gutmann, Stephan Neuhaus) ia.cr/2025/1237
Abstract. This paper presents implementations that match and, where possible, exceed current quantum factorisation records using a VIC-20 8-bit home computer from 1981, an abacus, and a dog. We hope that this work will inspire future efforts to match any further quantum factorisation records, should they arise.
July 11, 2025 at 9:42 PM