Tessera

@cascremers.bsky.social

My latest project, in collaboration with @cascremers.bsky.social, is out! It is Bob DyLean, a framework to analyze cryptographic protocols in the symbolic model, in Lean.

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

Bob DyLean: A Framework for the Symbolic Analysis of Cryptographic Protocols in Lean (Théophile Wallez, Cas Cremers) ia.cr/2026/1493

Abstract. Over the last decades, symbolic (Dolev-Yao) methods for the analysis of security protocols have proven to be effective to analyze and establish strong guarantees for widely deployed protocols and systems, such as TLS 1.3, E-voting protocols, EMV, and MLS. On the one hand, analysis methods like Tamarin and ProVerif provide automation and support for user-defined equational theories. On the other hand, methods like DY* offer more flexible and modular reasoning, but hardcode threat models and do not support custom equational theories.

We present DyLean, a framework for the symbolic analysis of cryptographic protocols in the Lean theorem prover. Our framework comprises both a flexible general-purpose symbolic semantics, as well as a concrete proof methodology.

DyLean allows defining protocols and expected security properties; its semantics and equational theories can be customized by the user. Furthermore, the semantics are agnostic of the specific proof methodology: our goal is to provide a generic framework that can be used by the community as a foundation to develop various proof methodologies.

Moreover, we provide a concrete proof methodology inspired by DY, based on trace invariants. Thus, DyLean inherits from the qualities of DY: it is able to analyze protocols involving unbounded loops or datastructures, and is able to compose security proofs in a variety of scenarios. Our proof methodology improves on DY* by allowing for user-defined equational theories and threat models. We exercise DyLean on several focused case studies, which include protocols using merkle trees, ratcheting protocols, post-quantum protocols, and protocols analyzed under different equational theories, which demonstrates that DyLean can effectively analyze protocols with each of these features.

@cascremers.bsky.social · 5mo ago

Still buzzing from winning the 2026 Levchin prize, together with David Basin, Jannik Dreier, and Ralf Sasse for our work on the Tamarin prover, at IACR's Real-World Crypto conference in Taipei. More details and videos here: tamarin-prover.com/2026/03/09/L...

Levchin Prize for Real-World Cryptography

khaleesi @khaleesicodes.bsky.social · 10mo ago

Die Abstimmung der #Chatkontrolle im EU-Rat ist verschoben. Das ist ein kleiner Sieg und vor allem euch zu verdanken! Die nächste Abstimmung ist für Dezember geplant - jetzt ist es wichtig den Druck bis dahin hoch zu halten. Mehr Informationen folgen.

Tjerand Silde @tjesi.bsky.social · 11mo ago

The EU Parliament has published a new proposal for Chat Control to mass-surveil all digital communication in Europe. The proposal is ineffective, weakens secure communication, and violates basic human privacy. This must be stopped immediately. #ChatControl csa-scientist-open-letter.org/Sep2025

csa-scientist-open-letter.org

@cascremers.bsky.social · 12mo ago

I'm very happy that physical copies of our Tamarin book are now available from Springer Nature: link.springer.com/book/9783031... or read the PDF and the accompanying files for free: tamarin-prover.com/book/index.h... big thanks to my co-authors David Basin, Jannik Dreier, and Ralf Sasse!

@cascremers.bsky.social · last yr.

My research group has open positions for PhD students and Postdoctoral Researchers, starting fall 2025 or early 2026. Interested in advancing the state-of-the-art in automated verification or modern secure communications? See: people.cispa.io/cas.cremers/...

Home | Cas Cremers

Cas Cremers' publications

people.cispa.io

CISPA Helmholtz Center for Information Security @cispa.de · last yr.

We’re thrilled to share: Three teams from CISPA have been honored at the SpringerOpen Cybersecurity Awards 2025! Track A – Best Theoretical Research Paper Track C – Best Machine Learning and Security Paper Track D – Best Hardware and Physics Paper cybersecurity.springeropen.com/best-paper-a...

@cascremers.bsky.social · last yr.

On August 26 and 27 I'll be speaking at the FOSAD 2025 summer school on "Formal Analysis of Security Protocols: State-of-the-art and Future Challenges", including some of our recent work on Tamarin and its applications. Apply by July 21st here: sites.google.com/uniurb.it/fo...

"Formal Analysis of Security Protocols: State-of-the-art and Future Challenges"

@cascremers.bsky.social · last yr.

Nearly finished! "Modeling and Analyzing Security Protocols with Tamarin: A Comprehensive Guide" (Basin, Cremers, Dreier, and Sasse) will be published by Springer in the near future. I'm very happy to announce that a full draft of our book is now available for download at tamarin-prover.com/book/