International Association for Cryptologic Research

Real World Crypto: AgileCrypto 2026: An international scientific conference on cryptography and cryptographic information security tools “Cryptography in a multipolar world”ileCrypto 2026 Jaipur, India, 2 November – 6 November 2026 Event date: 2 November to 6 November 2026

Job Posting: Ph.D. position focusing on Applied Cryptography and Privacy Lund University We now offer a new doctoral student position in the field of Applied Cryptography and Privacy. The primary duties of the doctoral student positions are to perform research and teaching within the Applied Cryptography and Privacy area. The research is devoted to the broader area of privacy-preserving communication and computation outsourcing. Communication over the internet is susceptible to surveillance and censorship. Privacy preserving communication techniques (e.g., Tor, Nym, Snowflake) allow users to circumvent such surveillance and censorship. The research scope would include designing, analysing and implementing such systems; additionally, studying different attacks and countermeasures are expected to be part of the research method. Privacy-preserving computation outsourcing allows users to outsource computation tasks to a cloud server without revealing to the server anything about the user data or even what kind of computations the user is performing. There are different techniques for such privacy-preserving computation outsourcing such as Trusted Execution Environment (e.g., Intel SGX) and Fully Homomorphic Encryption (TFHE, BGV). Furthermore, the specific functions/tasks can be subject to attacks, and identifying attacks and countermeasures is expected to be studied. The research method will be a combination of system studies, design, and experimental research. The position is funded by the Wallenberg AI, Autonomous Systems and Software Program (WASP). How to apply: Applications need to be submitted to the application portal at: https://lu.varbi.com/en/what:job/jobID:917016/ Applications shall be written in English and include: – CV and a cover letter stating the reasons why you are interested in the doctoral programme/employment and in what way the research project corresponds to your interests and educational background. – Copies of issued study certificates and/or awarded degree certificates. – Other documents you wish to be considered (grade transcripts, contact information for your references, letters of recommendation, etc.) Closing date for applications: Contact: Debajyoti Das (debajyoti.das@eit.lth.se) More information: https://lu.varbi.com/en/what:job/jobID:917016/

Job Posting: professor University of Latvia The University of Latvia announces an open competition for a vacancy of tenured professor in software security and artificial intelligence applications in computer systems security for the purpose of increasing competence in the field of computer systems security. The tenured professor is expected to perform high-quality intensive scientific work in Latvia and internationally. The position includes both a motivating salary and support for the creation of a research group. A detailed advertisement can be found at: https://www.lu.lv/en/about-us/vacancies/tenured-professorship-in-the-area-of-computer-systems-security-in-computer-science-and-informatics-09122025-31012025/ The appointment can be made at the level of Full Professor or Associate Professor, depending on the candidate. The closing date is June 1, 2026. For informal inquiries, please write to Prof. Andris Ambainis at ambainis@lu.lv. Closing date for applications: Contact: Andris Ambainis, ambainis@lu.lv More information: https://www.lu.lv/en/about-us/vacancies/tenured-professorship-in-the-area-of-computer-systems-security-in-computer-science-and-informatics-09122025-31012025/

Job Posting: Junior Research Fellow and Research Associate Positions in Analysis of NIST Accordion Mode Department of Computer Science and Engineering, Indian Institute of Technology Roorkee Applications are invited for a Junior Research Fellow and Research Associate position for the project “Comprehensive security analysis of NIST Accordion mode proposals and their implications to hash functions over Galois fields”. For JRF position, the candidate should have M.Tech in Computer Science and Engineering/Mathematics & Computing or related disciplines. Prior experience on cryptography along with a solid background in programming is essential and will be preferred. For RA position, a PhD degree in Computer Science and Engineering/Mathematics & Computing or related disciplines with specialization in cryptography is essential. Solid background in programming is also essential and will be preferred. The positions are based at the Department of Computer Science and Engineering, Indian Institute of Technology Roorkee, and the successful candidates will join Prof. Raghvendra Rohit’s research group. Interested candidates can email to Dr. Raghvendra Rohit at raghvendra.rohit@cs.iitr.ac.in with their resume. Application deadline: May 31, 2026 for full consideration. After this deadline, applications will be processed as they arrive. Closing date for applications: Contact: Dr. Raghvendra Rohit (raghvendra.rohit@cs.iitr.ac.in)

Job Posting: 1-2 PhD Students in Computing Science with focus on Cryptography and Cybersecurity Umeå University, Umeå, Sweden At our department, which conducts research at the highest international level and offers several high-quality educational programs in Computer Science, we are now seeking 1-2 PhD students with a focus on Cryptography and Cybersecurity. The project focuses on the design and analysis of modes of operation for symmetric-key cryptography, including, but not limited to, message authentication codes, pseudorandom functions, encryption schemes, deck functions, hash functions, and hash-based signatures, for applications such as quantum-secure and post-quantum cryptography, and leakage- and tamper-resilient cryptography. It is supervised by Asst. Prof. Mustafa Khairallah. The research is expected to include a mixture of theory and practice. The selected students will be part of the Department of Computing Science at Umeå University, as well as the WASP graduate school. The exact research topics will be tailored to the selected candidate(s) from a range of possible topics. Examples can be found in the link below. Please see the link for information about the requirements and the application procedure. The starting date is negotiable, no earlier than 01/09/2026. For additional information, please contact Asst. Prof. Mustafa Khairallah. Closing date for applications: Contact: mustafa.khairallah@umu.se More information: https://umu.varbi.com/what:job/jobID:933591/

Job Posting: PhD student position in cryptography KTH Royal Institute of Technology This position requires a Swedish citizenship. Information about the position is therefore only available in Swedish. Centrum för cyberförsvar och informationssäkerhet (CDIS) vid KTH — som är ett samarbete mellan KTH och Försvarsmakten, samt vissa andra myndigheter — söker doktorander. Det rör sig om en bred utlysning inom cybersäkerhetsområdet. Vi vill här särskilt peka ut en möjlig specialisering inom kryptologiområdet. Mer specifikt har KTH i samarbete med avdelningen för krypto och IT-säkerhet vid Must pågående spetsforskning som syftar till att möta de utmaningar som följer av kvantdatorutvecklingen. Vi söker nu inom ramen för CDIS utlysning en doktorand som kan bidra till den forskningen. Doktoranden är tänkt att initialt handledas av Johan Håstad och Martin Ekerå. Tjänsten kommer att omfatta 80% doktorandstudier vid KTH och 20% placering vid Must där möjlighet ges att arbeta med några av Sveriges främsta kryptologer. Resultatet för doktoranden blir en unik kombination av teori och praktik inom kryptologiområdet. Vid intresse, sök en av de av CDIS utlysta tjänsterna. För mer information, kontakta Johan Håstad (johanh@kth.se) eller Martin Ekerå (ekera@kth.se). Sista ansökningsdag är 27 maj 2026. Observera att svenskt medborgarskap är ett krav för tjänsten, och att tjänsten medför krav på säkerhetsprövning. Closing date for applications: Contact: Martin Ekerå (ekera@kth.se) More information: https://www.kth.se/lediga-jobb/926878?l=sv

ePrint Report: An analysis of a weakened version of PRISM Jolijn Cottaar, Steven D. Galbraith, Luciano Maino, Monika Trimoska PRISM (PKC25) is a hash-and-sign signature scheme whose security relies on the hardness of computing large-prime-degree isogenies originating from a curve of unknown endomorphism ring. In PRISM, the degree of such isogenies is obtained by hashing messages onto a set of large odd integers that pass a primality test. In this work, we investigate the impact of the choice of primality test on the security of PRISM. We first show that when a weak primality test is used, the assumption underlying the security proof in the standard model does not hold. We then extend our analysis to the assumption used in the security proof in the (quantum) random oracle model. In this setting, we argue that the Miller-Rabin test suffices and estimate the minimal number of iterations required for PRISM to achieve the desired security level, thus minimising signing costs.

ePrint Report: Zero-Knowledge Proofs for Gradient Boosted Decision Trees Jiacheng Gao, Wenjie Qu, Yuan Zhang, Sheng Zhong, Jiaheng Zhang Gradient boosted decision trees (GBDTs) are among the most effective models for tabular data and are widely used in domains such as finance, healthcare, and risk assessment. As these models are increasingly trained and served by external providers, clients need a way to check that a prediction or a model update was produced by the claimed training pipeline. At the same time, the provider may need to keep the training data and model parameters private. This makes zero-knowledge proofs for GBDT training and inference a natural tool for accountable machine learning. Existing constructions for proving GBDT training typically rely on generic ZKP compilers. They build a certification circuit that checks the forest against the training data, and then prove the circuit execution. This leads to high prover cost. On the other hand, a more direct approach to decompose proof of training into algebraic constraints inevitably introduces many auxiliary witnesses to assist proving. Proving these constraints separately could result in a huge amount of independent auxiliary commitments, whose committing and opening could dominate both proof size and prover time. Batching these constraints is also difficult because they come from different stages of training and have potentially different witness shapes and sizes, which are committed over different domains. We present \textsc{Terrae}, a zero-knowledge proof system for quantized GBDT training and inference based on KZG polynomial commitments. \textsc{Terrae} avoids both dependency on proving circuit computation and proving each constraint separately by leveraging the structure of GBDT training and novelly batching the constraints. We introduce two batching techniques: domain-lifting batching for linear constraints and interleaving batching for non-linear constraints. Both techniques work over differently-sized domains and reduce many constraints to a single claim without introducing extra polynomial commitments. We also design a histogram proof that proves the correctness of converting sample-wise data into its frequency representation, which may be of independent interest. Our evaluation shows that, compared with prior approaches, \textsc{Terrae} significantly reduces proof-generation time while adding only a small proof-size overhead.

ePrint Report: Titan: Efficient Polynomial Commitments from IOPs over Groups Chethan Kamath, Ravi Prakash, Samipa Samanta, Sruthi Sekar, Nitin Singh In this paper, we propose Titan, an efficient polynomial commitment scheme (PCS) with transparent setup. It achieves commitment time of $O(n)$, evaluation time of $O(\sqrt{n})$ while the proof size and verification scales as $O(\sqrt[4]{n})$. Titan features an order of magnitude smaller proof sizes than hash based PCS, while featuring a significantly more efficient prover and verifier compared to state of the art group based schemes like Dory and Hyrax. To achieve this balance, Titan borrows two-tiered commitments from Dory, and realizes outer commitment using interactive protocols of proximity (IOPP) over groups, specifically WHIR, instead of expensive bilinear pairings. This allows Titan to be instantiated over general curves with discrete-log hardness such as Pasta Curves, instead of requiring pairing friendly curves. We compile a variant of Spartan protocol for R1CS with Titan PCS to realize a new SNARK, which we call TitanSnark. Our construction TitanSnark preserves the prover efficiency of the existing Spartan protocol, while improving proof size and verification quadratically from $O(\sqrt{n})$ to $O(\sqrt[4]{n})$. Concretely, for circuits of size $\geq 2^{22}$ this results in around $3\times$ more efficient proof size and verification. Our blueprint of combining IOPPs over groups with Pedersen style inner commitments is of independent interest, as are several optimizations towards efficiently realizing WHIR IOPP over prime-order groups.

ePrint Report: On Succinct Non-Interactive Secure Computation with Malicious Security Maya Farber Brodsky, Arka Rai Choudhuri, Abhishek Jain, Omer Paneth A non-interactive secure computation (NISC) protocol allows a client with input $x$ and a server with input $y$ to compute $f(x,y)$ using a single message from the client and a single response from the server. The protocol is called succinct if the size of the server’s message depends only on the output length and is independent of the size of $y$ and the complexity of $f$. In the semi-honest setting, succinct NISC is known from fully homomorphic encryption (FHE). In contrast, malicious security is currently known only from non-standard assumptions, such as SNARKs for NP. In this work, we construct maliciously secure succinct NISC protocols for natural and widely studied functionalities from standard assumptions, namely, FHE and batch arguments (BARGs). Our first result is a protocol for private set membership (PSM): the client holds an element $x$, the server holds a large set $S$, and the function outputs $1$ if and only if $x \in S$. We then give several generalizations: – Dictionary lookup: The server holds a dictionary $D$ of key–value pairs, the client’s input is a key $k$, and the output is $D[k]$. – Verifiable dictionary lookup: The server’s dictionary must additionally satisfy a predicate $P$, computable by a read-once machine with small state. – UP search: The client input is an instance $x$, and the output is $D[w]$, where $w$ is the unique witness for $x$ under some UP relation. Our protocols achieve split-simulation security against a malicious server and standard security against a malicious client. Split-simulation is a relaxation of the standard real-ideal paradigm, where correctness of the client’s output and indistinguishability of the server’s view are guaranteed separately. At the heart of our results lies a new simulation technique in which the server’s large input is extracted piece by piece and reconstructed into a coherent input. This reconstruction is enabled by a new monotone coupling argument based on Strassen’s theorem.

ePrint Report: UnifOMR: Oblivious Message Retrieval with Near-optimal Concrete Efficiency Ben Fisch, Zeyu Liu, Eran Tromer, Yunhao Wang End-to-end encryption guarantees message confidentiality but does not hide metadata such as communication patterns among senders and recipients, or their identities. Oblivious Message Retrieval (OMR) is a cryptographic protocol that enables servers to assist recipients in retrieving their messages from a database without learning the mapping between messages and recipients, thereby protecting such metadata. This paper investigates two central questions of OMR: (1) What is the precise relationship between OMR and the better-studied primitive of Private Information Retrieval (PIR)? (2) Can OMR schemes achieve concrete efficiency comparable to state-of-the-art PIR protocols? We show that OMR with a property we call strong detection-key-unlinkability is at least as hard as PIR, and that existing OMR constructions already satisfy this property. This PIR-to-OMR reduction has low overhead, suggesting that OMR cannot be made substantially more efficient than PIR. We then present $\mathsf{UnifOMR}$, which achieves $20\times$ to $1080\times$ faster server runtime over the state-of-the-art $\mathsf{SophOMR}$ under practical parameter settings. For $2^{19}$ messages of 612 bytes each, $\mathsf{UnifOMR}$ completes in only ${\sim}25$ seconds with 4 MB of communication, compared to $>1250$ seconds and 260 KB for $\mathsf{SophOMR}$. These gains come with two trade-offs: an asymptotically linear digest size (albeit with small constants), and two rounds of interaction between the detector and the client. Furthermore, crucially, $\mathsf{UnifOMR}$ uses batch PIR as a black-box component, which in our experiments accounts for $50$–$92\%$ of the server runtime. Thus, $\mathsf{UnifOMR}$ nearly matches the aforementioned lower bound concretely (for databases of $2^{16}$ to $2^{23}$ messages, each with $612$ to $3060$ bytes), given the status quo of batch PIR.

ePrint Report: UC4Free! Existing Threshold Signatures are UC Secure Jan Bobolz, Elizabeth Crites, Markulf Kohlweiss, Akira Takahashi Threshold signatures have received considerable attention in recent years due to ongoing standardization efforts and deployment in real-world systems. In this work, we prove the universal composability of a wide range of threshold signature schemes, including state-of-the-art protocols compatible with standard signatures used in practice, such as BLS and Schnorr signatures, as well as emerging post-quantum solutions. Importantly, we show UC security without any modifications to the existing protocols. To this end, we design natural game-based definitions to capture different combinations of main threshold signature scheme properties, such as different levels of unforgeability, adaptive corruption, robustness, and different degrees of preprocessing. These definitions generalize prior definitional work, such as Bellare et al. (CRYPTO’22), and cover a wide range of existing schemes. Moreover, we identify and resolve gaps in prior work. We then express these properties in terms of a UC ideal functionality $\mathcal{F}\text{-}\mathtt{TS3}$. We prove that a threshold signature scheme UC-realizes $\mathcal{F}\text{-}\mathtt{TS3}$ if and only if it satisfies our game-based definitions. This opens up the usage of (existing) threshold signature schemes in a UC setting, enabling scheme designers to formulate their protocols relative to an ideal threshold signature functionality and use the UC composition theorem to argue security given any concrete instantiation. To further support UC scheme designers and to give further guidance on UC modeling for threshold signatures, we provide additional ideal threshold signature functionalities $\mathcal{F}\text{-}\mathtt{TS2}$, $\mathcal{F}\text{-}\mathtt{TS1}$, $\mathcal{F}\text{-}\mathtt{TSSync2}$, and $\mathcal{F}\text{-}\mathtt{TSSync1}$, which capture fewer properties than $\mathcal{F}\text{-}\mathtt{TS3}$ but are more convenient to use. $\mathcal{F}\text{-}\mathtt{TS2}$, $\mathcal{F}\text{-}\mathtt{TS1}$, $\mathcal{F}\text{-}\mathtt{TSSync2}$, $\mathcal{F}\text{-}\mathtt{TSSync1}$ can also be UC-realized by schemes proven secure according to our game-based definitions. Through this work, we show that composable security does not require sacrificing performance, but it does require rigor when setting up game-based definitions and ideal functionalities.

ePrint Report: Improved TensorPIR: Single-Server PIR with Lower Communication Cost Yingchu Lv, Yanbin Pan, Huaxiong Wang Private Information Retrieval (PIR) is of growing importance in privacy-preserving data access, as it enables users to retrieve information from databases without revealing their query content, thereby aligning with modern data protection and regulatory standards. State-of-the-art schemes, such as HintlessPIR and TensorPIR proposed by Li et al. at CRYPTO 2024, leverage lattice-based cryptography for efficient and privacy-preserving data retrieval. HintlessPIR achieves a communication complexity of $O(N^{1/2})$, which remains suboptimal for large databases. To further reduce communication overhead, the same work introduces TensorPIR, lowering the asymptotic complexity to $O(N^{1/3})$. However, this improvement requires larger parameters and more CRT moduli, leading to a practical communication cost that is not significantly smaller than that of HintlessPIR. In this work, we propose a new framework that rethinks the encryption strategy for the index, reducing both communication and computation costs through fewer CRT moduli. In experiments on 16 GB, 32 GB, 64 GB, and 128 GB databases, our total communication cost drops to as low as 45.5% of TensorPIR’s. Theoretically, as $N$ grows, our query and answer sizes are reduced to 36.9% and 22.2% of TensorPIR’s, respectively. Compared with HintlessPIR, our scheme achieves lower theoretical communication complexity, leading to substantially smaller practical communication for large $N$. Moreover, our total online time is reduced to 28.9% to 56.1% of HintlessPIR’s.

ePrint Report: Algorithmic Toolkit for Linearization of S-boxes Alex Biryukov, Philip Tureček, Aleksei Udovenko Linearization is a cryptanalysis technique in which a nonlinear function (an S-box) is represented by an affine mapping on a certain subset of inputs. Its variants were applied to analyze Keccak, LowMC, RAIN and AIM. In these primitives, the S-boxes are either very small (up to 5 bits) or are very specific monomial functions over a binary field. Linearization of arbitrary S-boxes was never practically explored due to the lack of theoretic, algorithmic, and cryptanalytic understanding. For the first time, we develop an algorithmic toolkit which allows one to compute strong linearizations of S-boxes, when they exist. For up to $n=8$ bits, our algorithms are able to find provably the best possible approximations, while for larger S-boxes it is feasible to obtain good approximations together with meaningful upper bounds. We apply our algorithms to a variety of S-boxes from existing primitives, to monomial functions, to so-called APN functions, and to 16-bit Super-Sboxes. We obtain interesting results raising many new open questions and open up new research directions, as well as a foundation for developing cryptanalytic attacks. To advance the cryptanalytic utility of linearization, we study and solve the problem of covering an S-box with multiple approximations. As an application, we derive a generic linearization approach for the CICO problem (constrained-input-constrained-output) over SPN-based permutations (Substitution-Permutation Networks) with general linear layers. This is the first such general cryptanalysis based on the existence of a strong linearization of the S-box.

ePrint Report: Sponsored Fair Exchange (Extended Abstract) Serge Vaudenay We propose a costless platform for fair exchange based on smart contracts to favor economic inclusion. Our smart contract is minimal, as most of communication is done offchain. The smart contract costs are covered by incentivized sponsors. Our protocol is a knowledge-coin exchange: it allows to exchange a digital item, characterized by an automatically verifiable description, against a payment in cryptocurrency. The exchange is fair in the sense that either both parties receive what they expect (the exchange completes) or both parties lose nothing (the exchange is canceled). We ensure a costless transaction in cancelation cases, and a transaction with pre-determined fee if it completes. We also ensure privacy of the transaction. Our protocol offers an improvement compared to OptiSwap: we can work with any description function. The complexity is never higher and sometimes significantly smaller. Namely, the worst case complexity is logarithmic instead of being linear. Furthermore, we introduce sponsoring as an enabler for economic inclusion.

ePrint Report: Magic Pot: Cryptanalysis of full AIM2 in the standard and related-/reused-key settings using new elimination framework Alex Biryukov, Pablo García Fernández, Aleksei Udovenko In this work, we cryptanalyse the post-quantum signature scheme AIMer v2.1, which is one of the winners of the Korean Post-Quantum Cryptography competition (KpqC), and whose earlier version was a candidate in the US NIST’s additional post-quantum digital signatures call. We show that AIM2, the underlying symmetric-key primitive, is not secure up to the claimed level by developing and applying a new algebraic attack framework based on extended linearization over a univariate polynomial ring and a novel algorithm for finding a null vector of a polynomial matrix. In particular misuse scenarios, such as reused-key or related-key settings, our attacks become practically feasible, allowing experimental verification and benchmarking. We also evaluate the approach on the RAIN block cipher used in the Rainier post-quantum signature scheme and obtain improved attacks, although not threatening its claimed security.

ePrint Report: Maintaining Sublinear Locality Over Time: Adaptively Secure MPC on a Reusable Hidden Graph Elette Boyle, Ran Cohen, Pierre Meyer Communication locality of an $n$-party protocol measures the maximum degree of the communication graph induced by the protocol execution. While secure multi-party computation (MPC) with small, sublinear locality exists in the static-corruption setting, this goal seems nearly paradoxical in the adaptive-corruption setting: Even against fail-stop adversaries, small neighbour sets of honest parties lie vulnerable to identification and corruption. Surprisingly, Chandran et al. [ITCS ’15] showed that for a single MPC execution, sublinear locality and adaptive security can be simultaneously achieved, assuming honest-to-honest channels are hidden from the adversary. Their solution works in the “hidden-graph model,” where a fresh, initially hidden, low-degree graph is being used in each round. In turn, the combined degree grows with every round—inherently limiting the approach to a single-shot MPC execution, and sublinear total rounds. This raises the following question, which is the focus of our work: Is it possible to maintain sublinear locality over an unbounded number of executions facing adaptive adversaries? In this work, we provide an affirmative answer in two settings: First, we consider semi-honest adversaries and information-theoretic security, and construct reusable MPC with polylog($n$) locality. Second, we consider fail-stop adversaries and computational security, and construct reusable MPC with $\tilde O(n^{2/3})$ locality. Our results are obtained by devising low-locality protocols while hiding important information about the graph topology, enabling the parties to reuse a single hidden graph. As an independent contribution, this serves as new results for adaptively secure topology-hiding computation (Moran, Orlov, Richelson [TCC ’15]).

ePrint Report: Bluestreak: Scaling DAG BFT by Sparsifying Metadata Nikita Polianskii, Ilya Vorobyev, Sebastian Muller DAG-based Byzantine fault-tolerant (BFT) consensus protocols achieve high throughput by allowing many validators to propose concurrently, but scaling them to large committees remains challenging. In a committee of $n$ validators, up to $f$ of which may be Byzantine ($n = 3f{+}1$), dense round-based DAG designs require each block to reference at least $2f{+}1$ blocks from the previous round. This yields $O(n)$ metadata per block, $O(n^2)$ metadata per round, and $O(n^3)$ metadata bytes transmitted per round under all-to-all dissemination, increasing bandwidth and processing costs and making metadata, rather than payload, the latency bottleneck. We present Bluestreak, a sparse uncertified DAG BFT consensus protocol that keeps non-leader blocks constant-size (in $n$) and concentrates committee-scale ancestry in a single leader block per round, yielding constant \emph{average} metadata per block as committees grow. Bluestreak combines this sparse block format with a new leader commit rule co-designed for the sparse DAG and a new pull-based pacemaker, and we prove safety and liveness under partial synchrony using only collision-resistant hashes and standard digital signatures. We implement and evaluate Bluestreak under wide-area latency spanning ten geo-distributed regions. Bluestreak scales from 10 to 400 validators on commodity 4-vCPU instances with sub-second WAN latency throughout (${\approx}\,470$ ms at $n{=}10$, ${\approx}\,720$ ms at $n{=}400$), keeping average per-block metadata constant at ${\approx}\,320$ bytes. At $n{=}120$, Bluestreak sustains ${\approx}\,220$k tx/s with LSM-tree storage and ${\approx}\,400$k tx/s with WAL-based storage, both at sub-second latency.

ePrint Report: VCVio: Verified Cryptography in Lean via Oracle Effects and Handlers Devon Tuma, Quang Dao, James Waters, Alexander Hicks, Nicholas Hopper Mechanized cryptographic proofs face a long-standing trade-off between assurance and expressiveness. Existing foundational frameworks, which reduce every proof step to the kernel of a general-purpose proof assistant, offer a small, auditable trusted base, but struggle to model the oracle manipulations and rewinding arguments pervasive in modern cryptography. They also tend to lack the tactic infrastructure of specialized, non-foundational tools like EasyCrypt. We present VCVio, a foundational framework in Lean 4 that closes both gaps with established ideas from programming-language theory: algebraic effects and handlers on the oracle side, and a modular relational program logic on the tactic side. Concretely, a computation with oracle access is the free monad over the polynomial functor determined by the oracle specification, exposing its interaction history as an explicit syntax tree. Caching, logging, reprogramming, and seed pre-sampling become handler combinators; rewinding reduces to deterministic transcript replay without any internal adversary state. On top of the oracle core, VCVio provides two reusable layers. We extend the recent Loom framework (POPL 2026) to the relational setting, yielding a single tactic framework that handles both unary and relational probabilistic reasoning. Alongside this, our treatment of state-separating proofs achieves compositional separation by typing, whereas Nominal SSProve recovers it by quotienting locations modulo alpha equivalence. We exercise this stack on three case studies: a random-oracle commitment scheme; the Bellare–Neven forking lemma, mechanized without the rewindability axioms used in the recent EasyCrypt formalization by Firsov and Janků; and the Schnorr signature scheme establishing EUF-CMA security. A significant share of our development used LLM coding agents and external automated proof-search systems; we report on the workflows, successes, and failure modes as a data point in LLM-assisted theorem proving.

ePrint Report: Secure Protocol Composition under Dynamic Corruption: Scaling Up Symbolic Analysis for Real-World Security Properties Cas Cremers, Erik Pallas, Aleksi Peltonen Although automated symbolic protocol verification has proven valuable and effective, current approaches begin to reach their limits: While small protocols can be analyzed automatically, the most complex case studies often require substantial expert time and resources. There have been many attempts to solve this problem by compositional verification, but they rely on unrealistic protocol assumptions and do not support real-world security properties like Forward Secrecy. In this work, we enable compositional symbolic analysis for real-world security protocols with respect to modern security properties. We develop a composition result in the Applied π-Calculus that holds even in the presence of attackers capable of dynamic corruption if the protocols satisfy a disjointness requirement. We demonstrate the applicability and effectiveness of our result on the composition of a data exchange protocol with a Diffie-Hellman key exchange and a compositional analysis of Forward Secrecy in TLS 1.3 within the scope of RFC 8446 and the ECH extension. While monolithic analyses of TLS 1.3 with ECH fail to deliver a result in 10% of cases, all compositional analyses succeed. Additionally, runtime decreases by 71% and memory usage by 86% on average.