@inproceedings{22006, abstract = {Runtime monitoring checks, during execution, whether a partial signal produced by a hybrid system satisfies its specification. Signal First-Order Logic (SFO) offers expressive real-time specifications over such signals, but currently comes only with Boolean semantics and has no tool support. We provide the first robustness-based quantitative semantics for SFO, enabling the expression and evaluation of rich real-time properties beyond the scope of existing formalisms such as Signal Temporal Logic. To enable online monitoring, we identify a past-time fragment of SFO and give a pastification procedure that transforms bounded-response SFO formulas into equisatisfiable formulas in this fragment. We then develop an efficient runtime monitoring algorithm for this past-time fragment and evaluate its performance on a set of benchmarks, demonstrating the practicality and effectiveness of our approach. To the best of our knowledge, this is the first publicly available prototype for online quantitative monitoring of full SFO.}, author = {Chalupa, Marek and Henzinger, Thomas A and Sarac, Naci E and Yu, Zhengqi}, booktitle = {27th International Symposium on Formal Methods}, isbn = {9783032262196}, issn = {1611-3349}, keywords = {Signal first-order logic, Robustness-based quantitative semantics, Online runtime monitoring}, location = {Tokyo, Japan}, pages = {214--233}, publisher = {Springer Nature}, title = {{Quantitative monitoring of Signal First-Order logic}}, doi = {10.1007/978-3-032-26220-2_11}, volume = {16557}, year = {2026}, } @inproceedings{21042, abstract = {Many blockchains such as Ethereum execute all incoming transactions sequentially significantly limiting the potential throughput. A common approach to scale execution is parallel execution engines that fully utilize modern multi-core architectures. Parallel execution is then either done optimistically, by executing transactions in parallel and detecting conflicts on the fly, or guided, by requiring exhaustive client transaction hints and scheduling transactions accordingly. However, recent studies have shown that the performance of parallel execution engines depends on the nature of the underlying workload. In fact, in some cases, only a 60% speed-up compared to sequential execution could be obtained. This is the case, as transactions that access the same resources must be executed sequentially. For example, if 10% of the transactions in a block access the same resource, the execution cannot meaningfully scale beyond 10 cores. Therefore, a single popular application can bottleneck the execution and limit the potential throughput. In this paper, we introduce Anthemius, a block construction algorithm that optimizes parallel transaction execution throughput. We evaluate Anthemius exhaustively under a range of workloads, and show that Anthemius enables the underlying parallel execution engine to process over twice as many transactions.}, author = {Neiheiser, Ray and Kokoris Kogias, Eleftherios}, booktitle = {29th International Conference on Financial Cryptography and Data Security}, isbn = {9783032070234}, issn = {1611-3349}, location = {Miyakojima, Japan}, pages = {307--323}, publisher = {Springer Nature}, title = {{Anthemius: Efficient and modular block assembly for concurrent execution}}, doi = {10.1007/978-3-032-07024-1_18}, volume = {15751}, year = {2026}, } @inproceedings{21044, abstract = {Scalability is a crucial requirement for modern large-scale systems, enabling elasticity and ensuring responsiveness under varying load. While cloud systems have achieved scalable architectures, blockchain systems remain constrained by the need to over-provision validator machines to handle peak load. This leads to resource inefficiency, poor cost scaling, and limits on performance. To address these challenges, we introduce Pilotfish, the first scale-out transaction execution engine for blockchains. Pilotfish enables validators to scale horizontally by distributing transaction execution across multiple worker machines, allowing elasticity without compromising consistency or determinism. It integrates seamlessly with the lazy blockchain architecture, completing the missing piece of execution elasticity. To achieve this, Pilotfish tackles several key challenges: ensuring scalable and strongly consistent distributed transactions, handling partial crash recovery with lightweight replication, and maintaining concurrency with a novel versioned-queue scheduling algorithm. Our evaluation shows that Pilotfish scales linearly up to at least eight workers per validator for compute-bound workloads, while maintaining low latency. By solving scalable execution, Pilotfish brings blockchains closer to achieving end-to-end elasticity, unlocking new possibilities for efficient and adaptable blockchain systems.}, author = {Kniep, Quentin and Kokoris Kogias, Eleftherios and Sonnino, Alberto and Zablotchi, Igor and Zhang, Nuda}, booktitle = {29th International Conference on Financial Cryptography and Data Security}, isbn = {9783032070234}, issn = {1611-3349}, location = {Miyakojima, Japan}, pages = {287--306}, publisher = {Springer Nature}, title = {{Pilotfish: Distributed execution for scalable blockchains}}, doi = {10.1007/978-3-032-07024-1_17}, volume = {15751}, year = {2026}, } @inproceedings{21134, abstract = {The Nakamoto consensus protocol underlying the Bitcoin blockchain uses proof of work as a voting mechanism. Honest miners who contribute hashing power towards securing the chain try to extend the longest chain they are aware of. Despite its simplicity, Nakamoto consensus achieves meaningful security guarantees assuming that at any point in time, a majority of the hashing power is controlled by honest parties. This also holds under “resource variability”, i.e., if the total hashing power varies greatly over time. Proofs of space (PoSpace) have been suggested as a more sustainable replacement for proofs of work. Unfortunately, no construction of a “longest-chain” blockchain based on PoSpace, that is secure under dynamic availability, is known. In this work, we prove that without additional assumptions no such protocol exists. We exactly quantify this impossibility result by proving a bound on the length of the fork required for double spending as a function of the adversarial capabilities. This bound holds for any chain selection rule, and we also show a chain selection rule (albeit a very strange one) that almost matches this bound. The Nakamoto consensus protocol underlying the Bitcoin blockchain uses proof of work as a voting mechanism. Honest miners who contribute hashing power towards securing the chain try to extend the longest chain they are aware of. Despite its simplicity, Nakamoto consensus achieves meaningful security guarantees assuming that at any point in time, a majority of the hashing power is controlled by honest parties. This also holds under “resource variability”, i.e., if the total hashing power varies greatly over time. Proofs of space (PoSpace) have been suggested as a more sustainable replacement for proofs of work. Unfortunately, no construction of a “longest-chain” blockchain based on PoSpace, that is secure under dynamic availability, is known. In this work, we prove that without additional assumptions no such protocol exists. We exactly quantify this impossibility result by proving a bound on the length of the fork required for double spending as a function of the adversarial capabilities. This bound holds for any chain selection rule, and we also show a chain selection rule (albeit a very strange one) that almost matches this bound. Concretely, we consider a security game in which the honest parties at any point control 0 > 1 times more space than the adversary. The adversary can change the honest space by a factor 1+- E with every block (dynamic availability), and “replotting” the space (which allows answering two challenges using the same space) takes as much time as p blocks. We prove that no matter what chain selection rule is used, in this game the adversary can create a fork of length o^2 . p/E that will be picked as the winner by the chain selection rule. We also provide an upper bound that matches the lower bound up to a factor o. There exists a chain selection rule (albeit a very strange one) which in the above game requires forks of length at least o . p/E Our results show the necessity of additional assumptions to create a secure PoSpace based longest-chain blockchain. The Chia network in addition to PoSpace uses a verifiable delay function. Our bounds show that an additional primitive like that is necessary.}, author = {Baig, Mirza Ahad and Pietrzak, Krzysztof Z}, booktitle = {29th International Conference on Financial Cryptography and Data Security}, isbn = {9783032070340}, issn = {1611-3349}, location = {Miyakojima, Japan}, pages = {127--142}, publisher = {Springer Nature}, title = {{On the (in)security of Proofs-of-space based longest-chain blockchains}}, doi = {10.1007/978-3-032-07035-7_8}, volume = {15752}, year = {2026}, } @inproceedings{21135, abstract = {Three-dimensional (3D) microscopy data is often anisotropic with significantly lower resolution (up to 8x) along the z axis than along the xy axes. Computationally generating plausible isotropic resolution from anisotropic imaging data would benefit the visual analysis of large-scale volumes. This paper proposes niiv, a self-supervised method for isotropic reconstruction of 3D microscopy data that can quickly produce images at arbitrary output resolutions. The representation embeds a learned latent code within a neural field that describes the implicit higher-resolution isotropic image region. We use an attention-guided latent interpolation approach, which allows flexible information exchange over a local latent neighborhood. Under isotropic volume assumptions, we self-supervise this representation on low-/high-resolution lateral image pairs to reconstruct an isotropic volume from low-resolution axial images. We evaluate our method on simulated and real anisotropic electron (EM) and light microscopy (LM) data. Compared to diffusion-based baselines, niiv shows improved reconstruction quality (+1 dB PSNR) and is over three orders of magnitude faster (1,000x) to infer. Specifically, niiv reconstructs a 128^3 voxel volume in 2/10th of a second, renderable at varying (continuous) high resolutions for display. Our code is available at https://github.com/jakobtroidl/niiv-miccai.}, author = {Troidl, Jakob and Liang, Yiqing and Beyer, Johanna and Tavakoli, Mojtaba and Danzl, Johann G and Hadwiger, Markus and Pfister, Hanspeter and Tompkin, James}, booktitle = {1st International Workshop on Efficient Medical Artificial Intelligence}, isbn = {9783032139603}, issn = {1611-3349}, location = {Daejeon, South Korea}, pages = {257--267}, publisher = {Springer Nature}, title = {{niiv: Interactive Self-supervised Neural Implicit Isotropic Volume Reconstruction}}, doi = {10.1007/978-3-032-13961-0_26}, volume = {16318}, year = {2026}, } @inproceedings{21374, abstract = {Let . S be a set of distinct points in general position in the Euclidean plane. A plane Hamiltonian path on . S is a crossing-free geometric path such that every point of .S is a vertex of the path. It is known that, if. S is sufficiently large, there exist three edge-disjoint plane Hamiltonian paths on . S. In this paper we study an edge-constrained version of the problem of finding Hamiltonian paths on a point set. We first consider the problem of finding a single plane Hamiltonian path . π with endpoints .s, t ∈ S and constraints given by a segment . ab, where .a, b ∈ S. We consider the following scenarios: (i) .ab ∈ π; (ii) .ab π. We characterize those quintuples . S, a, b, s, t for which . π exists. Secondly, we consider the problem of finding two plane Hamiltonian paths . π1, π2 on a set . S with constraints given by a segment . ab, where .a, b ∈ S. We consider the following scenarios: (i) .π1 and .π2 share no edges and .ab is an edge of . π1; (ii) .π1 and .π2 share no edges and none of them includes .ab as an edge; (iii) both .π1 and .π2 include .ab as an edge and share no other edges. In all cases, we characterize those triples . S, a, b for which .π1 and .π2 exist.}, author = {Antić, Todor and Džuklevski, Aleksa and Fiala, Jiří and Kratochvíl, Jan and Liotta, Giuseppe and Saghafian, Morteza and Saumell, Maria and Zink, Johannes}, booktitle = {51st International Conference on Current Trends in Theory and Practice of Computer Science}, isbn = {9783032178008}, issn = {1611-3349}, location = {Krakow, Poland}, pages = {532--546}, publisher = {Springer Nature}, title = {{Edge-constrained Hamiltonian paths on a point set}}, doi = {10.1007/978-3-032-17801-5_39}, volume = {16448}, year = {2026}, } @inproceedings{21410, abstract = {Given a finite set of red and blue points in R^d, the MST-ratio is defined as the total length of the Euclidean minimum spanning trees of the red points and the blue points, divided by the length of the Euclidean minimum spanning tree of their union. The MST-ratio has recently gained attention due to its direct interpretation in topological models for studying point sets with applications in spatial biology. The maximum MST-ratio of a point set is the maximum MST-ratio over all proper colorings of its points by red and blue. We prove that finding the maximum MST-ratio of a given point set is NP-hard when the dimension is part of the input. Moreover, we present a quadratic-time 3-approximation algorithm for this problem. As part of the proof, we show that in any metric space, the maximum MST-ratio is smaller than 3. Furthermore, we study the average MST-ratio over all colorings of a set of n points. We show that this average is always at least n-2/n-1, and for n random points uniformly distributed in a d-dimensional unit cube, the average tends to (math formular) in expectation as n approaches infinity.}, author = {Jabal Ameli, Afrouz and Motiei, Faezeh and Saghafian, Morteza}, booktitle = {20th International Conference and Workshops on Algorithms and Computation}, isbn = {9789819571260}, issn = {1611-3349}, location = {Perugia, Italy}, pages = {386--401}, publisher = {Springer Nature}, title = {{On the MST-ratio: Theoretical bounds and complexity of finding the maximum}}, doi = {10.1007/978-981-95-7127-7_26}, volume = {16444}, year = {2026}, } @inproceedings{20844, abstract = {We introduce and construct a new proof system called Non-interactive Arguments of Knowledge or Space (NArKoS), where a space-bounded prover can convince a verifier they know a secret, while having access to sufficient space allows one to forge indistinguishable proofs without the secret. An application of NArKoS are space-deniable proofs, which are proofs of knowledge (say for authentication in access control) that are sound when executed by a lightweight device like a smart-card or an RFID chip that cannot have much storage, but are deniable (in the strong sense of online deniability) as the verifier, like a card reader, can efficiently forge such proofs. We construct NArKoS in the random oracle model using an OR-proof combining a sigma protocol (for the proof of knowledge of the secret) with a new proof system called simulatable Proof of Transient Space (simPoTS). We give two different constructions of simPoTS, one based on labelling graphs with high pebbling complexity, a technique used in the construction of memory-hard functions and proofs of space, and a more practical construction based on the verifiable space-hard functions from TCC’24 where a prover must compute a root of a sparse polynomial. In both cases, the main challenge is making the proofs efficiently simulatable.}, author = {Dujmovic, Jesko and Günther, Christoph Ullrich and Pietrzak, Krzysztof Z}, booktitle = {23rd International Conference on Theory of Cryptography}, isbn = {9783032122896}, issn = {1611-3349}, location = {Aarhus, Denmark}, pages = {171--202}, publisher = {Springer Nature}, title = {{Space-deniable proofs}}, doi = {10.1007/978-3-032-12290-2_6}, volume = {16271}, year = {2025}, } @inproceedings{20845, abstract = {We develop new attacks against the Evasive LWE family of assumptions, in both the public and private-coin regime. To the best of our knowledge, ours are the first attacks against Evasive LWE in the public-coin regime, for any instantiation from the family. Our attacks are summarized below. Public-Coin Attacks. 1.The recent work by Hseih, Lin and Luo [17] constructed the first Attribute Based Encryption (ABE) for unbounded depth circuits by relying on the “circular” evasive LWE assumption. This assumption has been popularly considered as a safe, public-coin instance of Evasive LWE in contrast to its “private-coin” cousins (for instance, see [10, 11]). We provide the first attack against this assumption, challenging the widely held belief that this is a public-coin assumption. 2. We demonstrate a counter-example against vanilla public-coin evasive LWE by Wee [26] in an unnatural parameter regime. Our attack crucially relies on the error in the pre-condition being larger than the error in the post-condition, necessitating a refinement of the assumption. Private-Coin Attacks. 1. The recent work by Agrawal, Kumari and Yamada [2] constructed the first functional encryption scheme for pseudorandom functionalities (PRFE) and extended this to obfuscation for pseudorandom functionalities (PRIO) [4] by relying on private-coin evasive LWE. We provide a new attack against the assumption stated in the first posting of their work (subsequently refined to avoid these attacks). 2. The recent work by Branco et al. [8] (concurrently to [4]) provides a construction of obfuscation for pseudorandom functionalities by relying on private-coin evasive LWE. We provide a new attack against their stated assumption. 3. Branco et al. [8] showed that there exist contrived, “self-referential” classes of pseudorandom functionalities for which pseudorandom obfuscation cannot exist. We extend their techniques to develop an analogous result for pseudorandom functional encryption. While Evasive LWE was developed to specifically avoid “zeroizing attacks”, our work shows that in certain settings, such attacks can still apply.}, author = {Agrawal, Shweta and Modi, Anuja and Yadav, Anshu and Yamada, Shota}, booktitle = {23rd International Conference on Theory of Cryptography}, isbn = {9783032122926}, issn = {1611-3349}, location = {Aarhus, Denmark}, pages = {259--290}, publisher = {Springer Nature}, title = {{Zeroizing attacks against evasive and circular evasive LWE}}, doi = {10.1007/978-3-032-12293-3_9}, volume = {16269}, year = {2025}, } @inproceedings{20846, abstract = {CVRFs are PRFs that unify the properties of verifiable and constrained PRFs. Since they were introduced concurrently by Fuchsbauer and Chandran-Raghuraman-Vinayagamurthy in 2014, it has been an open problem to construct CVRFs without using heavy machinery such as multilinear maps, obfuscation or functional encryption. We solve this problem by constructing a prefix-constrained verifiable PRF that does not rely on the aforementioned assumptions. Essentially, our construction is a verifiable version of the Goldreich-Goldwasser-Micali PRF. To achieve verifiability we leverage degree-2 algebraic PRGs and bilinear groups. In short, proofs consist of intermediate values of the Goldreich-Goldwasser-Micali PRF raised to the exponents of group elements. These outputs can be verified using pairings since the underlying PRG is of degree 2. We prove the selective security of our construction under the Decisional Square Diffie-Hellman (DSDH) assumption and a new assumption, which we dub recursive Decisional Diffie-Hellman (recursive DDH). We prove the soundness of recursive DDH in the generic group model assuming the hardness of the Multivariate Quadratic (MQ) problem and a new variant thereof, which we call MQ+. Last, in terms of applications, we observe that our CVRF is also an exponent (C)VRF in the plain model. Exponent VRFs were recently introduced by Boneh et al. (Eurocrypt’25) with various applications to threshold cryptography in mind. In addition to that, we give further applications for prefix-CVRFs in the blockchain setting, namely, stake-pooling and compressible randomness beacons.}, author = {Brandt, Nicholas and Cueto Noval, Miguel and Günther, Christoph Ullrich and Ünal, Akin and Wohnig, Stella}, booktitle = {23rd International Conference on Theory of Cryptography}, isbn = {9783032122896}, issn = {1611-3349}, location = {Aarhus, Denmark}, pages = {478--511}, publisher = {Springer Nature}, title = {{Constrained verifiable random functions without obfuscation and friends}}, doi = {10.1007/978-3-032-12290-2_16}, volume = {16271}, year = {2025}, } @inproceedings{21090, abstract = {Fairness in AI is traditionally studied as a static property evaluated once, over a fixed dataset. However, real-world AI systems operate sequentially, with outcomes and environments evolving over time. This paper proposes a framework for analysing fairness as a runtime property. Using a minimal yet expressive model based on sequences of coin tosses with possibly evolving biases, we study the problems of monitoring and enforcing fairness expressed in either toss outcomes or coin biases. Since there is no one-size-fits-all solution for either problem, we provide a summary of monitoring and enforcement strategies, parametrised by environment dynamics, prediction horizon, and confidence thresholds. For both problems, we present general results under simple or minimal assumptions. We survey existing solutions for the monitoring problem for Markovian and additive dynamics, and existing solutions for the enforcement problem in static settings with known dynamics.}, author = {Cano Cordoba, Filip and Henzinger, Thomas A and Kueffner, Konstantin}, booktitle = {25th International Conference on Runtime Verification}, issn = {1611-3349}, location = {Graz, Austria}, pages = {1--21}, publisher = {Springer Nature}, title = {{Algorithmic fairness: A runtime perspective}}, doi = {10.1007/978-3-032-05435-7_1}, volume = {16087}, year = {2025}, } @inproceedings{21091, abstract = {Neural certificates have emerged as a powerful tool in cyber-physical systems control, providing witnesses of correctness. These certificates, such as barrier functions, often learned alongside control policies, once verified, serve as mathematical proofs of system safety. However, traditional formal verification of their defining conditions typically faces scalability challenges due to exhaustive state-space exploration. To address this challenge, we propose a lightweight runtime monitoring framework that integrates real-time verification and does not require access to the underlying control policy. Our monitor observes the system during deployment and performs on-the-fly verification of the certificate over a lookahead region to ensure safety within a finite prediction horizon. We instantiate this framework for ReLU-based control barrier functions and demonstrate its practical effectiveness in a case study. Our approach enables timely detection of safety violations and incorrect certificates with minimal overhead, providing an effective but lightweight alternative to the static verification of the certificates.}, author = {Henzinger, Thomas A and Kueffner, Konstantin and Yu, Zhengqi}, booktitle = {25th International Conference on Runtime Verification}, issn = {1611-3349}, location = {Graz, Austria}, pages = {54--72}, publisher = {Springer Nature}, title = {{Formal verification of neural certificates done dynamically}}, doi = {10.1007/978-3-032-05435-7_4}, volume = {16087}, year = {2025}, } @inproceedings{21092, abstract = {Formal verification provides assurances that a probabilistic system satisfies its specification—conditioned on the system model being aligned with reality. We propose alignment monitoring to watch that this assumption is justified. We consider a probabilistic model well aligned if it accurately predicts the behaviour of an uncertain system in advance. An alignment score measures this by quantifying the similarity between the model’s predicted and the system’s (unknown) actual distributions. An alignment monitor observes the system at runtime; at each point in time it uses the current state and the model to predict the next state. After the next state is observed, the monitor updates the verdict, which is a high-probability interval estimate for the true alignment score. We utilize tools from sequential forecasting to construct our alignment monitors. Besides a monitor for measuring the expected alignment score, we introduce a differential alignment monitor, designed for comparing two models, and a weighted alignment monitor, which permits task-specific alignment monitoring. We evaluate our monitors experimentally on the PRISM benchmark suite. They are fast, memory-efficient, and detect misalignment early.}, author = {Henzinger, Thomas A and Kueffner, Konstantin and Singh, Vasu and Sun, I}, booktitle = {25th International Conference on Runtime Verification}, issn = {1611-3349}, location = {Graz, Austria}, pages = {140--159}, publisher = {Springer Nature}, title = {{Alignment monitoring}}, doi = {10.1007/978-3-032-05435-7_9}, volume = {16087}, year = {2025}, } @inproceedings{21093, abstract = {We propose a monitoring approach for hyperproperties where the system’s observations range over infinite domains. The specifications are given as formulas of symbolic hypernode logic, an extension of earlier versions of hypernode logic that supports events with data. We demonstrate how to translate terms of symbolic hypernode logic into multi-tape symbolic transducers and we present a monitoring algorithm for universally quantified formulas that is based on this translation. We evaluate our approach against the previous approach for monitoring hypernode logic, and we also compare it to other monitors for hyperproperties.}, author = {Chalupa, Marek and Henzinger, Thomas A and Oliveira da Costa, Ana A}, booktitle = {25th International Conference on Runtime Verification}, issn = {1611-3349}, location = {Graz, Austria}, pages = {417--437}, publisher = {Springer Nature}, title = {{Monitoring hypernode logic over infinite domains}}, doi = {10.1007/978-3-032-05435-7_23}, volume = {16087}, year = {2025}, } @inproceedings{21262, abstract = {Continuous Group Key Agreement (CGKA) is the primitive underlying secure group messaging. It allows a large group of N users to maintain a shared secret key that is frequently rotated by the group members in order to achieve forward secrecy and post compromise security. The group messaging scheme Messaging Layer Security (MLS) standardized by the IETF makes use of a CGKA called TreeKEM which arranges the N group members in a binary tree. Here, each node is associated with a public-key, each user is assigned one of the leaves, and a user knows the corresponding secret keys from their leaf to the root. To update the key material known to them, a user must just replace keys at log(N) nodes, which requires them to create and upload log(N) ciphertexts. Such updates must be processed sequentially by all users, which for large groups is impractical. To allow for concurrent updates, TreeKEM uses the “propose and commit” paradigm, where multiple users can concurrently propose to update (by just sampling a fresh leaf key), and a single user can then commit to all proposals at once. Unfortunately, this process destroys the binary tree structure as the tree gets pruned and some nodes must be “blanked” at the cost of increasing the in-degree of others, which makes the commit operation, as well as, future commits more costly. In the worst case, the update cost (in terms of uploaded ciphertexts) per user can grow from log(N) to Ω(N). In this work we provide two main contributions. First, we show that MLS’ communication complexity is bad not only in the worst case but also if the proposers and committers are chosen at random: even if there’s just one update proposal for every commit the expected cost is already over √N, and it approaches N as this ratio changes towards more proposals. Our second contribution is a new variant of propose and commit for TreeKEM which for moderate amounts of update proposals per commit provably achieves an update cost of Θ(log(N)) assuming the proposers and committers are chosen at random.}, author = {Auerbach, Benedikt and Cueto Noval, Miguel and Erol, Boran and Pietrzak, Krzysztof Z}, booktitle = {45th Annual International Cryptology Conference}, isbn = {9783032019127}, issn = {1611-3349}, location = {Santa Barbara, CA, United States}, pages = {141--172}, publisher = {Springer Nature}, title = {{Continuous group-key agreement: Concurrent updates without pruning}}, doi = {10.1007/978-3-032-01913-4_5}, volume = {16007}, year = {2025}, } @inproceedings{21323, abstract = {We present a unifying framework for proving the knowledge-soundness of KZG-like polynomial commitment schemes, encompassing both univariate and multivariate variants. By conceptualizing the proof technique of Lipmaa, Parisella, and Siim for the univariate KZG scheme (EUROCRYPT 2024), we present tools and falsifiable hardness assumptions that permit black-box extraction of the multivariate KZG scheme. Central to our approach is the notion of a canonical Proof-of-Knowledge of a Polynomial (PoKoP) of a polynomial commitment scheme, which we use to capture the extractability notion required in constructions of practical zk-SNARKs. We further present an explicit polynomial decomposition lemma for multivariate polynomials, enabling a more direct analysis of interpolating extractors and bridging the gap between univariate and multivariate commitments. Our results provide the first standard-model proofs of extractability for the multivariate KZG scheme and many of its variants under falsifiable assumptions.}, author = {Belohorec, Juraj and Dvořák, Pavel and Hoffmann, Charlotte and Hubáček, Pavel and Mašková, Kristýna and Pastyřík, Martin}, booktitle = {45th Annual International Cryptology Conference}, isbn = {9783032018861}, issn = {1611-3349}, location = {Santa Barbara, CA, United States}, pages = {584--616}, publisher = {Springer Nature}, title = {{On extractability of the KZG family of polynomial commitment schemes}}, doi = {10.1007/978-3-032-01887-8_19}, volume = {16005}, year = {2025}, } @inproceedings{19375, abstract = {Despite the advances in probabilistic model checking, the scalability of the verification methods remains limited. In particular, the state space often becomes extremely large when instantiating parameterized Markov decision processes (MDPs) even with moderate values. Synthesizing policies for such huge MDPs is beyond the reach of available tools. We propose a learning-based approach to obtain a reasonable policy for such huge MDPs. The idea is to generalize optimal policies obtained by model-checking small instances to larger ones using decision-tree learning. Consequently, our method bypasses the need for explicit state-space exploration of large models, providing a practical solution to the state-space explosion problem. We demonstrate the efficacy of our approach by performing extensive experimentation on the relevant models from the quantitative verification benchmark set. The experimental results indicate that our policies perform well, even when the size of the model is orders of magnitude beyond the reach of state-of-the-art analysis tools.}, author = {Azeem, Muqsit and Chakraborty, Debraj and Kanav, Sudeep and Kretinsky, Jan and Mohagheghi, Mohammadsadegh and Mohr, Stefanie and Weininger, Maximilian}, booktitle = {26th International Conference on Verification, Model Checking, and Abstract Interpretation}, isbn = {9783031827020}, issn = {1611-3349}, location = {Denver, CO, United States}, pages = {97--120}, publisher = {Springer Nature}, title = {{1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization}}, doi = {10.1007/978-3-031-82703-7_5}, volume = {15530}, year = {2025}, } @inproceedings{19445, abstract = {In reconfiguration, we are given two solutions to a graph problem, such as Vertex Cover or Dominating Set, with each solution represented by a placement of tokens on vertices of the graph. Our task is to reconfigure one into the other using small steps while ensuring the intermediate configurations of tokens are also valid solutions. The two commonly studied settings are Token Jumping and Token Sliding, which allows moving a single token to an arbitrary or an adjacent vertex, respectively. We introduce new rules that generalize Token Jumping, parameterized by the number of tokens allowed to move at once and by the maximum distance of each move. Our main contribution is identifying minimal rules that allow reconfiguring any possible given solution into any other for Independent Set, Vertex Cover, and Dominating Set. For each minimal rule, we also provide an efficient algorithm that finds a corresponding reconfiguration sequence. We further focus on the rule that allows each token to move to an adjacent vertex in a single step. This natural variant turns out to be the minimal rule that guarantees reconfigurability for Vertex Cover. We determine the computational complexity of deciding whether a (shortest) reconfiguration sequence exists under this rule for the three studied problems. While reachability for Vertex Cover is shown to be in P, finding a shortest sequence is shown to be NP-complete. For Independent Set and Dominating Set, even reachability is shown to be PSPACE-complete.}, author = {Křišťan, Jan Matyáš and Svoboda, Jakub}, booktitle = {19th International Conference and Workshops on Algorithms and Computation}, isbn = {9789819628445}, issn = {1611-3349}, location = {Chengdu, China}, pages = {244--265}, publisher = {Springer Nature}, title = {{Reconfiguration using generalized token jumping}}, doi = {10.1007/978-981-96-2845-2_16}, volume = {15411}, year = {2025}, } @inproceedings{19600, abstract = {In this work, we explore route discovery in private payment channel networks. We first determine what “ideal" privacy for a routing protocol means in this setting. We observe that protocols achieving this strong privacy definition exist by leveraging Multi-Party Computation but they are inherently inefficient as they must involve the entire network. We then present protocols with weaker privacy guarantees but much better efficiency (involving only a small fraction of the nodes). The core idea is that both sender and receiver gossip a message which propagates through the network, and the moment any node in the network receives both messages, a path is found. In our first protocol the message is always sent to all neighbouring nodes with a delay proportional to the fees of that edge. In our second protocol the message is only sent to one neighbour chosen randomly with a probability proportional to its degree. We additionally propose a more realistic notion of privacy in order to measure the privacy leakage of our protocols in practice. Our realistic notion of privacy challenges an adversary that join the network with a fixed budget to create channels to guess the sender and receiver of a transaction upon receiving messages from our protocols. Simulations of our protocols on the Lightning network topology (for random transactions and uniform fees) show that 1) forming edges with high degree nodes is a more effective attack strategy for the adversary, 2) there is a tradeoff between the number of nodes involved in our protocols (privacy) and the optimality of the discovered path, and 3) our protocols involve a very small fraction of the network on average.}, author = {Avarikioti, Zeta and Bastankhah, Mahsa and Maddah-Ali, Mohammad Ali and Pietrzak, Krzysztof Z and Svoboda, Jakub and Yeo, Michelle X}, booktitle = {Computer Security. ESORICS 2024 International Workshops}, isbn = {9783031823480}, issn = {1611-3349}, location = {Bydgoszcz, Poland}, pages = {207--223}, publisher = {Springer Nature}, title = {{Route discovery in private payment channel networks}}, doi = {10.1007/978-3-031-82349-7_15}, volume = {15263}, year = {2025}, } @inproceedings{19712, abstract = {We study recent algebraic attacks (Briaud-Øygarden EC’23) on the Regular Syndrome Decoding (RSD) problem and the assumptions underlying the correctness of their attacks’ complexity estimates. By relating these assumptions to interesting algebraic-combinatorial problems, we prove that they do not hold in full generality. However, we show that they are (asymptotically) true for most parameter sets, supporting the soundness of algebraic attacks on RSD. Further, we prove—without any heuristics or assumptions—that RSD can be broken in polynomial time whenever the number of error blocks times the square of the size of error blocks is larger than 2 times the square of the dimension of the code. Additionally, we use our methodology to attack a variant of the Learning With Errors problem where each error term lies in a fixed set of constant size. We prove that this problem can be broken in polynomial time, given a sufficient number of samples. This result improves on the seminal work by Arora and Ge (ICALP’11), as the attack’s time complexity is independent of the LWE modulus.}, author = {Cueto Noval, Miguel and Merz, Simon-Philipp and Stählin, Patrick and Ünal, Akin}, booktitle = {44th Annual International Conference on the Theory and Applications of Cryptographic Techniques}, isbn = {9783031910944}, issn = {1611-3349}, location = {Madrid, Spain}, pages = {385--415}, publisher = {Springer Nature}, title = {{On the soundness of algebraic attacks against code-based assumptions}}, doi = {10.1007/978-3-031-91095-1_14}, volume = {15606}, year = {2025}, }