@inproceedings{14758,
  abstract     = {We present a flexible and efficient toolchain to symbolically solve (standard) Rabin games, fair-adversarial Rabin games, and 2 1/2 license type-player Rabin games. To our best knowledge, our tools are the first ones to be able to solve these problems. Furthermore, using these flexible game solvers as a back-end, we implemented a tool for computing correct-by-construction controllers for stochastic dynamical systems under LTL specifications. Our implementations use the recent theoretical result that all of these games can be solved using the same symbolic fixpoint algorithm but utilizing different, domain specific calculations of the involved predecessor operators. The main feature of our toolchain is the utilization of two programming abstractions: one to separate the symbolic fixpoint computations from the predecessor calculations, and another one to allow the integration of different BDD libraries as back-ends. In particular, we employ a multi-threaded execution of the fixpoint algorithm by using the multi-threaded BDD library Sylvan, which leads to enormous computational savings.},
  author       = {Majumdar, Rupak and Mallik, Kaushik and Rychlicki, Mateusz and Schmuck, Anne-Kathrin and Soudjani, Sadegh},
  booktitle    = {35th International Conference on Computer Aided Verification},
  isbn         = {9783031377082},
  issn         = {1611-3349},
  location     = {Paris, France},
  pages        = {3--15},
  publisher    = {Springer Nature},
  title        = {{A flexible toolchain for symbolic rabin games under fair and stochastic uncertainties}},
  doi          = {10.1007/978-3-031-37709-9_1},
  volume       = {13966},
  year         = {2023},
}

@inproceedings{14829,
  abstract     = {This paper explores a modular design architecture aimed at helping blockchains (and other SMR implementation) to scale to a very large number of processes. This comes in contrast to existing monolithic architectures that interleave transaction dissemination, ordering, and execution in a single functionality. To achieve this we first split the monolith to multiple layers which can use existing distributed computing primitives. The exact specifications of the data dissemination part are formally defined by the Proof of Availability & Retrieval (PoA &R) abstraction. Solutions to the PoA &R problem contain two related sub-protocols: one that “pushes” information into the network and another that “pulls” this information. Regarding the latter, there is a dearth of research literature which is rectified in this paper. We present a family of pulling sub-protocols and rigorously analyze them. Extensive simulations support the theoretical claims of efficiency and robustness in case of a very large number of players. Finally, actual implementation and deployment on a small number of machines (roughly the size of several industrial systems) demonstrates the viability of the architecture’s paradigm.},
  author       = {Cohen, Shir and Goren, Guy and Kokoris Kogias, Eleftherios and Sonnino, Alberto and Spiegelman, Alexander},
  booktitle    = {27th International Conference on Financial Cryptography and Data Security},
  isbn         = {9783031477508},
  issn         = {1611-3349},
  location     = {Bol, Brac, Croatia},
  pages        = {36--53},
  publisher    = {Springer Nature},
  title        = {{Proof of availability and retrieval in a modular blockchain architecture}},
  doi          = {10.1007/978-3-031-47751-5_3},
  volume       = {13951},
  year         = {2023},
}

@inproceedings{13143,
  abstract     = {GIMPS and PrimeGrid are large-scale distributed projects dedicated to searching giant prime numbers, usually of special forms like Mersenne and Proth primes. The numbers in the current search-space are millions of digits large and the participating volunteers need to run resource-consuming primality tests. Once a candidate prime N has been found, the only way for another party to independently verify the primality of N used to be by repeating the expensive primality test. To avoid the need for second recomputation of each primality test, these projects have recently adopted certifying mechanisms that enable efficient verification of performed tests. However, the mechanisms presently in place only detect benign errors and there is no guarantee against adversarial behavior: a malicious volunteer can mislead the project to reject a giant prime as being non-prime.
In this paper, we propose a practical, cryptographically-sound mechanism for certifying the non-primality of Proth numbers. That is, a volunteer can – parallel to running the primality test for N – generate an efficiently verifiable proof at a little extra cost certifying that N is not prime. The interactive protocol has statistical soundness and can be made non-interactive using the Fiat-Shamir heuristic.
Our approach is based on a cryptographic primitive called Proof of Exponentiation (PoE) which, for a group G, certifies that a tuple (x,y,T)∈G2×N satisfies x2T=y (Pietrzak, ITCS 2019 and Wesolowski, J. Cryptol. 2020). In particular, we show how to adapt Pietrzak’s PoE at a moderate additional cost to make it a cryptographically-sound certificate of non-primality.},
  author       = {Hoffmann, Charlotte and Hubáček, Pavel and Kamath, Chethan and Pietrzak, Krzysztof Z},
  booktitle    = {Public-Key Cryptography - PKC 2023},
  isbn         = {9783031313677},
  issn         = {1611-3349},
  location     = {Atlanta, GA, United States},
  pages        = {530--553},
  publisher    = {Springer Nature},
  title        = {{Certifying giant nonprimes}},
  doi          = {10.1007/978-3-031-31368-4_19},
  volume       = {13940},
  year         = {2023},
}

@inproceedings{11707,
  abstract     = {In this work we introduce the graph-theoretic notion of mendability: for each locally checkable graph problem we can define its mending radius, which captures the idea of how far one needs to modify a partial solution in order to “patch a hole.” We explore how mendability is connected to the existence of efficient algorithms, especially in distributed, parallel, and fault-tolerant settings. It is easy to see that O(1)-mendable problems are also solvable in O(log∗n) rounds in the LOCAL model of distributed computing. One of the surprises is that in paths and cycles, a converse also holds in the following sense: if a problem Π can be solved in O(log∗n), there is always a restriction Π′⊆Π that is still efficiently solvable but that is also O(1)-mendable. We also explore the structure of the landscape of mendability. For example, we show that in trees, the mending radius of any locally checkable problem is O(1), Θ(logn), or Θ(n), while in general graphs the structure is much more diverse.},
  author       = {Balliu, Alkida and Hirvonen, Juho and Melnyk, Darya and Olivetti, Dennis and Rybicki, Joel and Suomela, Jukka},
  booktitle    = {International Colloquium on Structural Information and Communication Complexity},
  editor       = {Parter, Merav},
  isbn         = {9783031099922},
  issn         = {1611-3349},
  location     = {Paderborn, Germany},
  pages        = {1--20},
  publisher    = {Springer Nature},
  title        = {{Local mending}},
  doi          = {10.1007/978-3-031-09993-9_1},
  volume       = {13298},
  year         = {2022},
}

@inproceedings{12167,
  abstract     = {Payment channels effectively move the transaction load off-chain thereby successfully addressing the inherent scalability problem most cryptocurrencies face. A major drawback of payment channels is the need to “top up” funds on-chain when a channel is depleted. Rebalancing was proposed to alleviate this issue, where parties with depleting channels move their funds along a cycle to replenish their channels off-chain. Protocols for rebalancing so far either introduce local solutions or compromise privacy.
In this work, we present an opt-in rebalancing protocol that is both private and globally optimal, meaning our protocol maximizes the total amount of rebalanced funds. We study rebalancing from the framework of linear programming. To obtain full privacy guarantees, we leverage multi-party computation in solving the linear program, which is executed by selected participants to maintain efficiency. Finally, we efficiently decompose the rebalancing solution into incentive-compatible cycles which conserve user balances when executed atomically.},
  author       = {Avarikioti, Georgia and Pietrzak, Krzysztof Z and Salem, Iosif and Schmid, Stefan and Tiwari, Samarth and Yeo, Michelle X},
  booktitle    = {Financial Cryptography and Data Security},
  isbn         = {9783031182822},
  issn         = {1611-3349},
  location     = {Grenada},
  pages        = {358--373},
  publisher    = {Springer Nature},
  title        = {{Hide & Seek: Privacy-preserving rebalancing on payment channel networks}},
  doi          = {10.1007/978-3-031-18283-9_17},
  volume       = {13411},
  year         = {2022},
}

@inproceedings{12168,
  abstract     = {Advances in blockchains have influenced the State-Machine-Replication (SMR) world and many state-of-the-art blockchain-SMR solutions are based on two pillars: Chaining and Leader-rotation. A predetermined round-robin mechanism used for Leader-rotation, however, has an undesirable behavior: crashed parties become designated leaders infinitely often, slowing down overall system performance. In this paper, we provide a new Leader-Aware SMR framework that, among other desirable properties, formalizes a Leader-utilization requirement that bounds the number of rounds whose leaders are faulty in crash-only executions.
We introduce Carousel, a novel, reputation-based Leader-rotation solution to achieve Leader-Aware SMR. The challenge in adaptive Leader-rotation is that it cannot rely on consensus to determine a leader, since consensus itself needs a leader. Carousel uses the available on-chain information to determine a leader locally and achieves Liveness despite this difficulty. A HotStuff implementation fitted with Carousel demonstrates drastic performance improvements: it increases throughput over 2x in faultless settings and provided a 20x throughput increase and 5x latency reduction in the presence of faults.},
  author       = {Cohen, Shir and Gelashvili, Rati and Kokoris Kogias, Eleftherios and Li, Zekun and Malkhi, Dahlia and Sonnino, Alberto and Spiegelman, Alexander},
  booktitle    = {International Conference on Financial Cryptography and Data Security},
  isbn         = {9783031182822},
  issn         = {1611-3349},
  location     = {Grenada},
  pages        = {279--295},
  publisher    = {Springer Nature},
  title        = {{Be aware of your leaders}},
  doi          = {10.1007/978-3-031-18283-9_13},
  volume       = {13411},
  year         = {2022},
}

@inproceedings{12170,
  abstract     = {We present PET, a specialized and highly optimized framework for partial exploration on probabilistic systems. Over the last decade, several significant advances in the analysis of Markov decision processes employed partial exploration. In a nutshell, this idea allows to focus computation on specific parts of the system, guided by heuristics, while maintaining correctness. In particular, only relevant parts of the system are constructed on demand, which in turn potentially allows to omit constructing large parts of the system. Depending on the model, this leads to dramatic speed-ups, in extreme cases even up to an arbitrary factor. PET unifies several previous implementations and provides a flexible framework to easily implement partial exploration for many further problems. Our experimental evaluation shows significant improvements compared to the previous implementations while vastly reducing the overhead required to add support for additional properties.},
  author       = {Meggendorfer, Tobias},
  booktitle    = {20th International Symposium on Automated Technology for Verification and Analysis},
  isbn         = {9783031199912},
  issn         = {1611-3349},
  location     = {Virtual},
  pages        = {320--326},
  publisher    = {Springer Nature},
  title        = {{PET – A partial exploration tool for probabilistic verification}},
  doi          = {10.1007/978-3-031-19992-9_20},
  volume       = {13505},
  year         = {2022},
}

@inproceedings{12171,
  abstract     = {We propose an algorithmic approach for synthesizing linear hybrid automata from time-series data. Unlike existing approaches, our approach provides a whole family of models with the same discrete structure but different dynamics. Each model in the family is guaranteed to capture the input data up to a precision error ε, in the following sense: For each time series, the model contains an execution that is ε-close to the data points. Our construction allows to effectively choose a model from this family with minimal precision error ε. We demonstrate the algorithm’s efficiency and its ability to find precise models in two case studies.},
  author       = {Garcia Soto, Miriam and Henzinger, Thomas A and Schilling, Christian},
  booktitle    = {20th International Symposium on Automated Technology for Verification and Analysis},
  isbn         = {9783031199912},
  issn         = {1611-3349},
  location     = {Virtual},
  pages        = {337--353},
  publisher    = {Springer Nature},
  title        = {{Synthesis of parametric hybrid automata from time series}},
  doi          = {10.1007/978-3-031-19992-9_22},
  volume       = {13505},
  year         = {2022},
}

@inproceedings{12175,
  abstract     = {An automaton is history-deterministic (HD) if one can safely resolve its non-deterministic choices on the fly. In a recent paper, Henzinger, Lehtinen and Totzke studied this in the context of Timed Automata [9], where it was conjectured that the class of timed ω-languages recognised by HD-timed automata strictly extends that of deterministic ones. We provide a proof for this fact.},
  author       = {Bose, Sougata and Henzinger, Thomas A and Lehtinen, Karoliina and Schewe, Sven and Totzke, Patrick},
  booktitle    = {16th International Conference on Reachability Problems},
  isbn         = {9783031191343},
  issn         = {1611-3349},
  location     = {Kaiserslautern, Germany},
  pages        = {67--76},
  publisher    = {Springer Nature},
  title        = {{History-deterministic timed automata are not determinizable}},
  doi          = {10.1007/978-3-031-19135-0_5},
  volume       = {13608},
  year         = {2022},
}

@inproceedings{18229,
  abstract     = {We present Self-Classifier – a novel self-supervised end-to-end classification learning approach. Self-Classifier learns labels and representations simultaneously in a single-stage end-to-end manner by optimizing for same-class prediction of two augmented views of the same sample. To guarantee non-degenerate solutions (i.e., solutions where all labels are assigned to the same class) we propose a mathematically motivated variant of the cross-entropy loss that has a uniform prior asserted on the predicted labels. In our theoretical analysis, we prove that degenerate solutions are not in the set of optimal solutions of our approach. Self-Classifier is simple to implement and scalable. Unlike other popular unsupervised classification and contrastive representation learning approaches, it does not require any form of pre-training, expectation-maximization, pseudo-labeling, external clustering, a second network, stop-gradient operation, or negative pairs. Despite its simplicity, our approach sets a new state of the art for unsupervised classification of ImageNet; and even achieves comparable to state-of-the-art results for unsupervised representation learning. Code is available at https://github.com/elad-amrani/self-classifier.},
  author       = {Amrani, Elad and Karlinsky, Leonid and Bronstein, Alexander},
  booktitle    = {17th European Conference on Computer Vision},
  isbn         = {9783031198205},
  issn         = {1611-3349},
  location     = {Tel Aviv, Israel},
  pages        = {116--132},
  publisher    = {Springer Nature},
  title        = {{Self-supervised classification network}},
  doi          = {10.1007/978-3-031-19821-2_7},
  volume       = {13691},
  year         = {2022},
}

@inproceedings{12298,
  abstract     = {Existing committee-based Byzantine state machine replication (SMR) protocols, typically deployed in production blockchains, face a clear trade-off: (1) they either achieve linear communication cost in the steady state, but sacrifice liveness during periods of asynchrony, or (2) they are robust (progress with probability one) but pay quadratic communication cost. We believe this trade-off is unwarranted since existing linear protocols still have asymptotic quadratic cost in the worst case. We design Ditto, a Byzantine SMR protocol that enjoys the best of both worlds: optimal communication on and off the steady state (linear and quadratic, respectively) and progress guarantee under asynchrony and DDoS attacks. We achieve this by replacing the view-synchronization of partially synchronous protocols with an asynchronous fallback mechanism at no extra asymptotic cost. Specifically, we start from HotStuff, a state-of-the-art linear protocol, and gradually build Ditto. As a separate contribution and an intermediate step, we design a 2-chain version of HotStuff, Jolteon, which leverages a quadratic view-change mechanism to reduce the latency of the standard 3-chain HotStuff. We implement and experimentally evaluate all our systems to prove that breaking the robustness-efficiency trade-off is in the realm of practicality.},
  author       = {Gelashvili, Rati and Kokoris Kogias, Eleftherios and Sonnino, Alberto and Spiegelman, Alexander and Xiang, Zhuolun},
  booktitle    = {Financial Cryptography and Data Security},
  isbn         = {9783031182822},
  issn         = {1611-3349},
  location     = {Radisson Grenada Beach Resort, Grenada},
  pages        = {296--315},
  publisher    = {Springer Nature},
  title        = {{Jolteon and ditto: Network-adaptive efficient consensus with asynchronous fallback}},
  doi          = {10.1007/978-3-031-18283-9_14},
  volume       = {13411},
  year         = {2022},
}

@inproceedings{12302,
  abstract     = {We propose a novel algorithm to decide the language inclusion between (nondeterministic) Büchi automata, a PSPACE-complete problem. Our approach, like others before, leverage a notion of quasiorder to prune the search for a counterexample by discarding candidates which are subsumed by others for the quasiorder. Discarded candidates are guaranteed to not compromise the completeness of the algorithm. The novelty of our work lies in the quasiorder used to discard candidates. We introduce FORQs (family of right quasiorders) that we obtain by adapting the notion of family of right congruences put forward by Maler and Staiger in 1993. We define a FORQ-based inclusion algorithm which we prove correct and instantiate it for a specific FORQ, called the structural FORQ, induced by the Büchi automaton to the right of the inclusion sign. The resulting implementation, called FORKLIFT, scales up better than the state-of-the-art on a variety of benchmarks including benchmarks from program verification and theorem proving for word combinatorics. Artifact: https://doi.org/10.5281/zenodo.6552870},
  author       = {Doveri, Kyveli and Ganty, Pierre and Mazzocchi, Nicolas Adrien},
  booktitle    = {Computer Aided Verification},
  isbn         = {9783031131875},
  issn         = {1611-3349},
  location     = {Haifa, Israel},
  pages        = {109--129},
  publisher    = {Springer Nature},
  title        = {{FORQ-based language inclusion formal testing}},
  doi          = {10.1007/978-3-031-13188-2_6},
  volume       = {13372},
  year         = {2022},
}

@inproceedings{12516,
  abstract     = {The homogeneous continuous LWE (hCLWE) problem is to distinguish samples of a specific high-dimensional Gaussian mixture from standard normal samples. It was shown to be at least as hard as Learning with Errors, but no reduction in the other direction is currently known.
We present four new public-key encryption schemes based on the hardness of hCLWE, with varying tradeoffs between decryption and security errors, and different discretization techniques. Our schemes yield a polynomial-time algorithm for solving hCLWE using a Statistical Zero-Knowledge oracle.},
  author       = {Bogdanov, Andrej and Cueto Noval, Miguel and Hoffmann, Charlotte and Rosen, Alon},
  booktitle    = {Theory of Cryptography},
  isbn         = {9783031223648},
  issn         = {1611-3349},
  location     = {Chicago, IL, United States},
  pages        = {565--592},
  publisher    = {Springer Nature},
  title        = {{Public-Key Encryption from Homogeneous CLWE}},
  doi          = {10.1007/978-3-031-22365-5_20},
  volume       = {13748},
  year         = {2022},
}

@inbook{20062,
  abstract     = {This article presents two fine-grained complexity lower bounds with relevance to algorithmic problems in computer aided verification. We have chosen these lower bounds as the proofs are relatively simple, but the techniques can be extended to give lower bounds for many more algorithmic problems. The goal is to present the bounds with minimal notation, making the results accessible to a broad community and stimulating further research in the area.

Specifically, we first describe a lower bound on the symbolic complexity of computing strongly connected components, which can be extended to show lower bounds for fundamental model-checking questions in graphs, published in [CDHL16b]. Second we present a conditional lower bound for disjunctive safety problems on graphs from [CDHL18] in the RAM model of computation. This bound can be modified to give conditional lower bounds for disjunctive objectives for reachability, Büchi, coBüchi and Rabin objectives in MDPs. We also present various open questions.},
  author       = {Henzinger, Monika H},
  booktitle    = {Principles of Systems Design},
  editor       = {Raskin, Jean-François and Chatterjee, Krishnendu and Doyen, Laurent and Majumdar, Rupak},
  isbn         = {9783031223365},
  issn         = {1611-3349},
  pages        = {292--305},
  publisher    = {Springer Nature Switzerland},
  title        = {{Fine-Grained Complexity Lower Bounds for Problems in Computer Aided Verification}},
  doi          = {10.1007/978-3-031-22337-2_14},
  volume       = {13660},
  year         = {2022},
}

@inproceedings{10891,
  abstract     = {We present a formal framework for the online black-box monitoring of software using monitors with quantitative verdict functions. Quantitative verdict functions have several advantages. First, quantitative monitors can be approximate, i.e., the value of the verdict function does not need to correspond exactly to the value of the property under observation. Second, quantitative monitors can be quantified universally, i.e., for every possible observed behavior, the monitor tries to make the best effort to estimate the value of the property under observation. Third, quantitative monitors can watch boolean as well as quantitative properties, such as average response time. Fourth, quantitative monitors can use non-finite-state resources, such as counters. As a consequence, quantitative monitors can be compared according to how many resources they use (e.g., the number of counters) and how precisely they approximate the property under observation. This allows for a rich spectrum of cost-precision trade-offs in monitoring software.},
  author       = {Henzinger, Thomas A},
  booktitle    = {Software Verification},
  isbn         = {9783030955601},
  issn         = {1611-3349},
  location     = {New Haven, CT, United States},
  pages        = {3--6},
  publisher    = {Springer Nature},
  title        = {{Quantitative monitoring of software}},
  doi          = {10.1007/978-3-030-95561-8_1},
  volume       = {13124},
  year         = {2022},
}

@inproceedings{11185,
  abstract     = {Bundling crossings is a strategy which can enhance the readability of graph drawings. In this paper we consider bundlings for families of pseudosegments, i.e., simple curves such that any two have share at most one point at which they cross. Our main result is that there is a polynomial-time algorithm to compute an 8-approximation of the bundled crossing number of such instances (up to adding a term depending on the facial structure). This 8-approximation also holds for bundlings of good drawings of graphs. In the special case of circular drawings the approximation factor is 8 (no extra term), this improves upon the 10-approximation of Fink et al. [6]. We also show how to compute a 92-approximation when the intersection graph of the pseudosegments is bipartite.},
  author       = {Arroyo Guevara, Alan M and Felsner, Stefan},
  booktitle    = {WALCOM 2022: Algorithms and Computation},
  isbn         = {9783030967307},
  issn         = {1611-3349},
  location     = {Jember, Indonesia},
  pages        = {383--395},
  publisher    = {Springer Nature},
  title        = {{Approximating the bundled crossing number}},
  doi          = {10.1007/978-3-030-96731-4_31},
  volume       = {13174},
  year         = {2022},
}

@inproceedings{11355,
  abstract     = {Contract-based design is a promising methodology for taming the complexity of developing sophisticated systems. A formal contract distinguishes between assumptions, which are constraints that the designer of a component puts on the environments in which the component can be used safely, and guarantees, which are promises that the designer asks from the team that implements the component. A theory of formal contracts can be formalized as an interface theory, which supports the composition and refinement of both assumptions and guarantees.
Although there is a rich landscape of contract-based design methods that address functional and extra-functional properties, we present the first interface theory that is designed for ensuring system-wide security properties. Our framework provides a refinement relation and a composition operation that support both incremental design and independent implementability. We develop our theory for both stateless and stateful interfaces. We illustrate the applicability of our framework with an example inspired from the automotive domain.},
  author       = {Bartocci, Ezio and Ferrere, Thomas and Henzinger, Thomas A and Nickovic, Dejan and Da Costa, Ana Oliveira},
  booktitle    = {Fundamental Approaches to Software Engineering},
  isbn         = {9783030994280},
  issn         = {1611-3349},
  location     = {Munich, Germany},
  pages        = {3--22},
  publisher    = {Springer Nature},
  title        = {{Information-flow interfaces}},
  doi          = {10.1007/978-3-030-99429-7_1},
  volume       = {13241},
  year         = {2022},
}

@book{11429,
  abstract     = {This book constitutes the refereed proceedings of the 18th International Symposium on Web and Wireless Geographical Information Systems, W2GIS 2022, held in Konstanz, Germany, in April 2022.
The 7 full papers presented together with 6 short papers in the volume were carefully reviewed and selected from 16 submissions.  The papers cover topics that range from mobile GIS and Location-Based Services to Spatial Information Retrieval and Wireless Sensor Networks.},
  editor       = {Karimipour, Farid and Storandt, Sabine},
  isbn         = {9783031062445},
  issn         = {1611-3349},
  pages        = {153},
  publisher    = {Springer Nature},
  title        = {{Web and Wireless Geographical Information Systems}},
  doi          = {10.1007/978-3-031-06245-2},
  volume       = {13238},
  year         = {2022},
}

@inproceedings{12176,
  abstract     = {A proof of exponentiation (PoE) in a group G of unknown order allows a prover to convince a verifier that a tuple (x,q,T,y)∈G×N×N×G satisfies xqT=y. This primitive has recently found exciting applications in the constructions of verifiable delay functions and succinct arguments of knowledge. The most practical PoEs only achieve soundness either under computational assumptions, i.e., they are arguments (Wesolowski, Journal of Cryptology 2020), or in groups that come with the promise of not having any small subgroups (Pietrzak, ITCS 2019). The only statistically-sound PoE in general groups of unknown order is due to Block et al. (CRYPTO 2021), and can be seen as an elaborate parallel repetition of Pietrzak’s PoE: to achieve λ bits of security, say λ=80, the number of repetitions required (and thus the blow-up in communication) is as large as λ.

In this work, we propose a statistically-sound PoE for the case where the exponent q is the product of all primes up to some bound B. We show that, in this case, it suffices to run only λ/log(B) parallel instances of Pietrzak’s PoE, which reduces the concrete proof-size compared to Block et al. by an order of magnitude. Furthermore, we show that in the known applications where PoEs are used as a building block such structured exponents are viable. Finally, we also discuss batching of our PoE, showing that many proofs (for the same G and q but different x and T) can be batched by adding only a single element to the proof per additional statement.},
  author       = {Hoffmann, Charlotte and Hubáček, Pavel and Kamath, Chethan and Klein, Karen and Pietrzak, Krzysztof Z},
  booktitle    = {Advances in Cryptology – CRYPTO 2022},
  isbn         = {9783031159787},
  issn         = {1611-3349},
  location     = {Santa Barbara, CA, United States},
  pages        = {370--399},
  publisher    = {Springer Nature},
  title        = {{Practical statistically-sound proofs of exponentiation in any group}},
  doi          = {10.1007/978-3-031-15979-4_13},
  volume       = {13508},
  year         = {2022},
}

@inproceedings{11476,
  abstract     = {Messaging platforms like Signal are widely deployed and provide strong security in an asynchronous setting. It is a challenging problem to construct a protocol with similar security guarantees that can efficiently scale to large groups. A major bottleneck are the frequent key rotations users need to perform to achieve post compromise forward security.

In current proposals – most notably in TreeKEM (which is part of the IETF’s Messaging Layer Security (MLS) protocol draft) – for users in a group of size n to rotate their keys, they must each craft a message of size log(n) to be broadcast to the group using an (untrusted) delivery server.

In larger groups, having users sequentially rotate their keys requires too much bandwidth (or takes too long), so variants allowing any T≤n users to simultaneously rotate their keys in just 2 communication rounds have been suggested (e.g. “Propose and Commit” by MLS). Unfortunately, 2-round concurrent updates are either damaging or expensive (or both); i.e. they either result in future operations being more costly (e.g. via “blanking” or “tainting”) or are costly themselves requiring Ω(T) communication for each user [Bienstock et al., TCC’20].

In this paper we propose CoCoA; a new scheme that allows for T concurrent updates that are neither damaging nor costly. That is, they add no cost to future operations yet they only require Ω(log2(n)) communication per user. To circumvent the [Bienstock et al.] lower bound, CoCoA increases the number of rounds needed to complete all updates from 2 up to (at most) log(n); though typically fewer rounds are needed.

The key insight of our protocol is the following: in the (non-concurrent version of) TreeKEM, a delivery server which gets T concurrent update requests will approve one and reject the remaining T−1. In contrast, our server attempts to apply all of them. If more than one user requests to rotate the same key during a round, the server arbitrarily picks a winner. Surprisingly, we prove that regardless of how the server chooses the winners, all previously compromised users will recover after at most log(n) such update rounds.

To keep the communication complexity low, CoCoA is a server-aided CGKA. That is, the delivery server no longer blindly forwards packets, but instead actively computes individualized packets tailored to each user. As the server is untrusted, this change requires us to develop new mechanisms ensuring robustness of the protocol.},
  author       = {Alwen, Joël and Auerbach, Benedikt and Cueto Noval, Miguel and Klein, Karen and Pascual Perez, Guillermo and Pietrzak, Krzysztof Z and Walter, Michael},
  booktitle    = {Advances in Cryptology – EUROCRYPT 2022},
  isbn         = {9783031070846},
  issn         = {1611-3349},
  location     = {Trondheim, Norway},
  pages        = {815–844},
  publisher    = {Springer Nature},
  title        = {{CoCoA: Concurrent continuous group key agreement}},
  doi          = {10.1007/978-3-031-07085-3_28},
  volume       = {13276},
  year         = {2022},
}