Abstract

Cryptanalysis—the task of finding attacks against cryptographic schemes—sits at the intersection of mathematical reasoning and programming, two areas where LLMs have made rapid progress. Just like math and programming, cryptanalytic attacks are formally defined and can be unambiguously verified. This raises the question if cryptanalysis might experience a similar acceleration in progress through LLMs. In this paper we introduce CryptanalysisBench, a benchmark of 114 tasks spanning six families of cryptographic primitives (block ciphers, hash functions, etc) drawn primarily from four NIST standardization competitions. Each task asks an agent to break an implementation of a cryptographic primitive by winning a formal security game. The benchmark has three tiers: (1) primitives with known practical breaks; (2) scaled-down variants of primitives without one; (3) a challenge set of unbroken production primitives. We evaluate Claude Opus 4.7, GPT-5.5 and Claude Mythos: all three solve a majority of Tier 1 (72.4%, 79.3%, and 75.9% respectively), while Tier 2 remains largely out of reach. One notable exception in Tier 2 is the SPoC AEAD, for which Mythos proposed a novel full key recovery attack. For Tier 1 successes, we provide a fine-grained analysis distinguishing paper recall from source-level rediscovery. We release CryptanalysisBench both as a forecasting tool to track when AI cryptanalytic capability becomes a serious factor, and as scaffolding for subjecting candidate schemes to more attacks before they are deployed.

Bio

Prof. Orr Dunkelman is a full professor at the Computer Science Dept. in the University of Haifa and a Guest Professor at the Technical University of Berlin. His research interests cover cryptography, with emphasis on cryptanalysis, privacy, with emphasis on biometric data, and computer security. He has served as the head of the Sub-center for Biometrics and its Applications here at the Center for Cyber, Law and Policy, and is a co-founder of the center (and was the center’s vice-director). He served on the board of the International Association for Cryptologic Research (IACR), as a delegate to the ISO/IEC SC27 WG2 and WG3 (as an expert in cryptography and computer security), and he is a co-founder of the “Privacy Israel” NGO. Currently he serves as the chair of the Fast Software Encryption steering committee.

During his academic career, Prof. Dunkelman published more than 130 papers in international venues, including the introduction of new cryptanalytic techniques and best known cryptanalysis results against specific ciphers (such as the AES). As part of his analysis work, he is also a co-designer of multiple cryptographic schemes such as the HAIFA framework for hash functions, the KATAN and KTANTAN block ciphers, and the SHAvite-3 hash function. He served on almost 100 program committees (including EUROCRYPT, CRYPTO, ASIACRYPT, and Usenix), and as a program chair of 6 conferences (including EUROCRYPT 2022 and FSE 2009). He won numerous awards such as the Krill prize (2014) and Best Paper Awards (e.g., Crypto 2012 and FSE 2012).

Photo provided by speaker

We’ll give an overview of the Major in Information Security and all you need to know about it (including our Master@ISEC network and its benefits), and provide an opportunity to meet fellow students and lecturers while enjoying some snacks.

No matter if you just started or are heading to the end of your studies, anyone interested is welcome! 

📷 Please be aware that we will be taking photos & videos at this event. Find the privacy policy here.
If you do not want to be photographed, please approach one of the organizers at the event.

>> Pentesting Lab course <<

Abstract

Generative AI, and especially LLMs, are being touted as the be-all-end-all for the future of any programming related task. Of course, the people making these claims usually have a financial interest in everyone replacing workers and experts with artificial “intelligence”.

Based on experience in machine learning (ML) research, as well as by now multiple years of penetration testing experience, Alex will talk about the actual everyday impact that LLMs have on our security work.
What we see is not the replacement of knowledgable security workers, but merely another tool in our toolbox. Let’s talk about how LLMs are utilized in our day-to-day work to help us speed up testing, which tasks can be handled by LLMs, and where human expertise, oversight, and communication skills will likely never be replaced.


Bio
Alex has studied Computer Science at the University of Innsbruck in the Bachelor’s and Master’s focussing on security related topics and machine learning (ML) topics and courses where available.
After finishing the undergraduate studies, he worked as a graduate researcher for four years, publishing a number of papers in the realm of adversarial ML and ML security.
For the past years he has been working as a penetration tester, and in this time has successfully pwned various web servers, mobile applications, and even certificate authorities.

Photo provided by speaker

We’re hosting FMCAD 2026 (Formal Methods in Computer-Aided Design), an annual conference on the theory and applications of formal methods in hardware and system verification. 

FMCAD provides a leading forum to researchers in academia and industry for presenting and discussing groundbreaking methods, technologies, theoretical results, and tools for reasoning formally about computing systems. FMCAD covers formal aspects of computer-aided system design including verification, specification, synthesis, and testing. 

Continuing the tradition of the previous years, FMCAD 2026 is hosting a Student Forum that provides a platform for students at any career stage (undergraduate or graduate) to introduce their research to the wider Formal Methods community and solicit feedback.

Student forum abstract submission: June 16, 2026

Abstract

Neural networks are increasingly deployed in safety-critical domains, where failures can have severe consequences. However, standard evaluation based on testing and validation datasets cannot provide formal guarantees about model behavior under all possible inputs. This talk introduces neural network verification, focusing on methods that provide provable guarantees of safety and robustness. We present the problem as checking whether a model satisfies a given property over a set of inputs, such as robustness to bounded perturbations or compliance with safety constraints. We then survey key approaches, including exact methods based on mixed-integer linear programming (MILP) and SMT solving, as well as more scalable but approximate techniques based on over-approximation and bound propagation. Simple examples illustrate how these methods work and highlight the trade-off between precision and scalability. The talk concludes with a brief overview of current limitations and emerging research directions, including certified robustness and integration with training procedures.

Bio

Laura Nenzi is an Associate Professor in Computer Science at the University of Trieste. Her research lies in formal methods for complex systems, with a focus on runtime verification,spatio-temporal logics, and the formal analysis of cyber-physical systems. She is also interested in verified and explainable artificial intelligence, aiming to provide rigorous guarantees for modern data-driven models.

Photo provided by speaker