arXiv subjects

Hannes Hartenstein

Publications and source records attributed to Hannes Hartenstein.

At least 19 recordsLinked to original sources

arXiv2026

Accountable Transaction Inclusion Lists: Enhancing Ethereum's Censorship Resistance

In Ethereum, transaction inclusion is rarely in question; what matters is the delay until inclusion. Currently, block builders could exercise censorship across consecutive blocks, threatening time-critical applications, such as on-chain auctions. To mitigate this risk, existing proposals such as FOCIL, scheduled for deployment in late 2026, assign a committee to list transactions for mandatory inclusion. However, no committee member is held accountable for the actual inclusion of the transactions: an adversary can bribe the entire committee to omit any transaction for less than 2 Euro per block under current conditions. We argue that accountability, i.e., requiring all exclusion decisions to be publicly disclosed and verifiably complete, with violations attributable to a specific party, substantially raises censorship costs. To this end, we propose Fair Forward Inclusion Lists (FairFIL) as an accountable censorship resistance mechanism for Ethereum. In FairFIL, every builder must publish all transactions the builder chooses to censor, subject to a protocol-anchored policy; a committee verifies the completeness and validity of this disclosure. The subsequent builder must include these transactions, forfeiting the full block reward upon any omission. Therefore, under FairFIL, extending censorship beyond a single slot requires an assembler to forfeit a full block reward. We show that compliance is rational for all participants within our behavior model. Our empirical evaluation on Ethereum mainnet indicates that multi-block censorship costs one order of magnitude more than under existing proposals, while leaving the builder's MEV extraction freedom largely intact. Initial measurements further suggest that the mempool consistency FairFIL requires is met in practice.

cs.DC↗

arXiv2026

Towards System-Oriented Formal Verification of Local-First Access Control

Conflict-free replicated data types (CRDTs) and the local-first concept are increasingly employed not only in small-scale collaboration systems among few users who trust each other, but also in large-scale systems, like Matrix for instant messaging and Keyhive for collaborative documents. Since mutual trust is no longer warranted, these systems require Byzantine fault tolerance and fine-grained access control. As of today, Matrix and Keyhive pair an informal specification with an unverified reference implementation. In this work, we follow a bottom-up approach towards constructing formally verified authorization algorithms for Byzantine fault-tolerant local-first systems. As intermediate target for formal verification, we contribute semantics and invariants of a replicated data type for managing simplified collaboration groups, based on capabilities for access control and hash chronicles for replication. To enable future integration into local-first systems like Matrix and Keyhive, we strive for accessibility to system engineers by using the Rust programming language for formal specification, verification, and implementation, enabled by the Verus framework using the Z3 theorem prover at zero runtime cost. We report on our experience and preliminary results following this approach, and discuss next steps towards scaling up access control expressiveness. Whether this approach can be scaled up to the complexity of real-world local-first access control systems like Matrix or Keyhive remains future work, but our findings demonstrate the potential of system-oriented formal verification with Verus.

cs.DC↗

arXiv2026

Why Ethereum Needs Fairness Mechanisms that Do Not Depend on Participants' Altruism

Ethereum's ideal of censorship resistance, together with related fairness properties, is undermined in practice, motivating fairness mechanisms that aim to restore these properties. Several of these mechanisms hand control over block contents to a committee of proposers under a 1-of-n honest assumption: at least one committee member complies with the mechanism even when deviating would increase personal revenue. We refer to such proposers as altruistic. Yet prior work shows that roughly 91 percent of blocks are constructed by centralized block-building services that demonstrably take user-adverse actions for financial gain; the responsible proposers sign these blocks blindly, without any means of intervention. A common reading of this figure is that 9 percent of proposers forgo these gains and act altruistically. Our empirical analysis of the full year 2025 shows that this share is far smaller: at most 1.55 percent of proposers can plausibly be regarded as altruistic, whereas the remaining 98.45 percent of proposers exhibit observable non-altruistic behavior. We interpret 1.55 percent as an upper bound on the prevalence of altruistic proposers. These results imply that committee-based fairness mechanisms that rely on altruistic members would require substantially larger committees than currently proposed. This raises concerns about their practical viability and motivates mechanisms in which fair behavior is the rational choice.

cs.DC↗

arXiv2025

Not eXactly Byzantine: Efficient and Resilient TEE-Based State Machine Replication

We propose, implement, and evaluate NxBFT, a resilient and efficient State Machine Replication protocol using Trusted Execution Environments (TEEs). NxBFT focuses on a "Not eXactly Byzantine" (NxB) operating model as a middle ground between crash and Byzantine fault tolerance. NxBFT's consensus layer is asynchronous, graph-based, leaderless, and optimized for the NxB operating model, enabling load-balancing of requests between replicas and, in fault-free cases, two network round trips between decisions. We identify fundamental issues with crash recovery due the use of TEEs in asynchrony that only can be circumvented by relying on synchrony for liveness. We provide a throughput-latency trade-off analysis of NxBFT, Chained-Damysus (rotating leader), and MinBFT (static leader) for up to 40 replicas and network round trip latencies up to 150 ms. NxBFT achieves the highest throughput in all scenarios. When small latencies are required, MinBFT and Damysus are at an advantage with Damysus benefiting from the NxB model in terms of throughput for small deployments. In contrast to leader-based approaches, NxBFT's performance is almost not impacted when actual crash faults occur.

cs.DC↗

arXiv2025

Model Checking the Security of the Lightning Network

Payment channel networks are an approach to improve the scalability of blockchain-based cryptocurrencies. The Lightning Network is a payment channel network built for Bitcoin that is already used in practice. Because the Lightning Network is used for transfer of financial value, its security in the presence of adversarial participants should be verified. The Lightning protocol's complexity makes it hard to assess whether the protocol is secure. To enable computer-aided security verification of Lightning, we formalize the protocol in TLA+ and formally specify the security property that honest users are guaranteed to retrieve their correct balance. While model checking provides a fully automated verification of the security property, the state space of the protocol's specification is so large that model checking becomes unfeasible. We make model checking the Lightning Network possible using two refinement steps that we verify using proofs. In a first step, we prove that the model of time used in the protocol can be abstracted using ideas from the research of timed automata. In a second step, we prove that it suffices to model check the protocol for single payment channels and the protocol for multi-hop payments separately. These refinements reduce the state space sufficiently to allow for model checking Lightning with models with payments over up to four hops and two concurrent payments. These results indicate that the current specification of Lightning is secure.

cs.CR↗

arXiv2023

How to Raise a Robot -- A Case for Neuro-Symbolic AI in Constrained Task Planning for Humanoid Assistive Robots

Humanoid robots will be able to assist humans in their daily life, in particular due to their versatile action capabilities. However, while these robots need a certain degree of autonomy to learn and explore, they also should respect various constraints, for access control and beyond. We explore the novel field of incorporating privacy, security, and access control constraints with robot task planning approaches. We report preliminary results on the classical symbolic approach, deep-learned neural networks, and modern ideas using large language models as knowledge base. From analyzing their trade-offs, we conclude that a hybrid approach is necessary, and thereby present a new use case for the emerging field of neuro-symbolic artificial intelligence.

cs.RO↗

arXiv2023

Let It TEE: Asynchronous Byzantine Atomic Broadcast with $n \geq 2f+1$

Asynchronous Byzantine Atomic Broadcast (ABAB) promises simplicity in implementation as well as increased performance and robustness in comparison to partially synchronous approaches. We adapt the recently proposed DAG-Rider approach to achieve ABAB with $n\geq 2f+1$ processes, of which $f$ are faulty, with only a constant increase in message size. We leverage a small Trusted Execution Environment (TEE) that provides a unique sequential identifier generator (USIG) to implement Reliable Broadcast with $n>f$ processes and show that the quorum-critical proofs still hold when adapting the quorum size to $\lfloor \frac{n}{2} \rfloor + 1$. This first USIG-based ABAB preserves the simplicity of DAG-Rider and serves as starting point for further research on TEE-based ABAB.

cs.DC↗

arXiv2023

Towards a Formal Verification of the Lightning Network with TLA+

Payment channel networks are an approach to improve the scalability of blockchain-based cryptocurrencies. Because payment channel networks are used for transfer of financial value, their security in the presence of adversarial participants should be verified formally. We formalize the protocol of the Lightning Network, a payment channel network built for Bitcoin, and show that the protocol fulfills the expected security properties. As the state space of a specification consisting of multiple participants is too large for model checking, we formalize intermediate specifications and use a chain of refinements to validate the security properties where each refinement is justified either by model checking or by a pen-and-paper proof.

cs.LO↗

arXiv2023

On Extend-Only Directed Posets and Derived Byzantine-Tolerant Replicated Data Types (Extended Version)

We uncover the extend-only directed posets (EDP) structure as a unification of recently discussed DAG-based Byzantine-tolerant conflict-free replicated data types (CRDT). We also show how a key-value map model can be derived from the EDP formulation, and give an outlook on an EDP-based systemic access control CRDT as a formalization of the CRDT used in the Matrix messaging system.

cs.DC↗

arXiv2022

ETHTID: Deployable Threshold Information Disclosure on Ethereum

We address the Threshold Information Disclosure (TID) problem on Ethereum: An arbitrary number of users commit to the scheduled disclosure of their individual messages recorded on the Ethereum blockchain if and only if all such messages are disclosed. Before a disclosure, only the original sender of each message should know its contents. To accomplish this, we task a small council with executing a distributed generation and threshold sharing of an asymmetric key pair. The public key can be used to encrypt messages which only become readable once the threshold-shared decryption key is reconstructed at a predefined point in time and recorded on-chain. With blockchains like Ethereum, it is possible to coordinate such procedures and attach economic stakes to the actions of participating individuals. In this paper, we present ETHTID, an Ethereum smart contract application to coordinate Threshold Information Disclosure. We base our implementation on ETHDKG [1], a smart contract application for distributed key generation and threshold sharing, and adapt it to fit our differing use case as well as add functionality to oversee a scheduled reconstruction of the decryption key. For our main cost saving optimisation, we show that the security of the underlying cryptographic scheme is maintained. We evaluate how the execution costs depend on the size of the council and the threshold and show that the presented protocol is deployable on Ethereum with a council of more than 200 members with gas savings of 20-40% compared to ETHDKG.

cs.CR↗

arXiv2021

Estimating the Peer Degree of Reachable Peers in the Bitcoin P2P Network

A recent spam wave of IP addresses in the Bitcoin P2P network allowed us to estimate the degree distribution of reachable peers in the network. The resulting distribution shows that about every second reachable peer runs with Bitcoin Core's default setting of a maximum of 125 concurrent connections and nearly all connection slots are taken. We validate this result and, in addition, use our observations of the spam wave to group addresses that belong to the same peer. By doing this grouping, we improve on previous measurements and show that simply counting addresses overestimates the number of reachable peers by 13 %.

cs.NI↗

arXiv2021

On Conflict-Free Replicated Data Types and Equivocation in Byzantine Setups

We explore the property of equivocation tolerance for Conflict-Free Replicated Data Types (CRDTs). We show that a subclass of CRDTs is equivocation-tolerant and can thereby cope with any number of Byzantine faults: Without equivocation detection, prevention or remediation, they still fulfill strong eventual consistency (SEC). We also conjecture that there is only one operation-based CRDT design supporting non-commutative operations that fulfills SEC in Byzantine environments with any number of faults.

cs.DC↗

arXiv2021

Advancing Protocol Diversity in Network Security Monitoring

With information technology entering new fields and levels of deployment, e.g., in areas of energy, mobility, and production, network security monitoring needs to be able to cope with those environments and their evolution. However, state-of-the-art Network Security Monitors (NSMs) typically lack the necessary flexibility to handle the diversity of the packet-oriented layers below the abstraction of TCP/IP connections. In this work, we advance the software architecture of a network security monitor to facilitate the flexible integration of lower-layer protocol dissectors while maintaining required performance levels. We proceed in three steps: First, we identify the challenges for modular packet-level analysis, present a refined NSM architecture to address them and specify requirements for its implementation. Second, we evaluate the performance of data structures to be used for protocol dispatching, implement the proposed design into the popular open-source NSM Zeek and assess its impact on the monitor performance. Our experiments show that hash-based data structures for dispatching introduce a significant overhead while array-based approaches qualify for practical application. Finally, we demonstrate the benefits of the proposed architecture and implementation by migrating Zeek's previously hard-coded stack of link and internet layer protocols to the new interface. Furthermore, we implement dissectors for non-IP based industrial communication protocols and leverage them to realize attack detection strategies from recent applied research. We integrate the proposed architecture into the Zeek open-source project and publish the implementation to support the scientific community as well as practitioners, promoting the transfer of research into practice.

cs.NI↗

arXiv2021

On the Estimation of the Number of Unreachable Peers in the Bitcoin P2P Network by Observation of Peer Announcements

Bitcoin is based on a P2P network that is used to propagate transactions and blocks. While the P2P network design intends to hide the topology of the P2P network, information about the topology is required to understand the network from a scientific point of view. Thus, there is a natural tension between the 'desire' for unobservability on the one hand, and for observability on the other hand. On a middle ground, one would at least be interested on some statistical features of the Bitcoin network like the number of peers that participate in the propagation of transactions and blocks. This number is composed of the number of reachable peers that accept incoming connections and unreachable peers that do not accept incoming connections. While the number of reachable peers can be measured, it is inherently difficult to determine the number of unreachable peers. Thus, the number of unreachable peers can only be estimated based on some indicators. In this paper, we first define our understanding of unreachable peers and then propose the PAL (Passive Announcement Listening) method which gives an estimate of the number of unreachable peers by observing ADDR messages that announce active IP addresses in the network. The PAL method allows for detecting unreachable peers that indicate that they provide services useful to the P2P network. In conjunction with previous methods, the PAL method can help to get a better estimate of the number of unreachable peers. We use the PAL method to analyze data from a long-term measurement of the Bitcoin P2P network that gives insights into the development of the number of unreachable peers over five years from 2015 to 2020. Results show that about 31,000 unreachable peers providing useful services were active per day at the end of the year 2020. An empirical validation indicates that the approach finds about 50 % of unreachable peers that provide useful services.

cs.CR↗

arXiv2020

Analysis of the Matrix Event Graph Replicated Data Type

Matrix is a new kind of decentralized, topic-based publish-subscribe middleware for communication and data storage that is getting popular particularly as a basis for secure instant messaging. In comparison to traditional decentralized communication systems, Matrix replaces pure message passing with a replicated data structure. This data structure, which we extract and call the Matrix Event Graph (MEG), depicts the causal history of messages. We show that this MEG represents an interesting and important replicated data type for general decentralized applications that are based on causal histories of publish-subscribe events: we show that a MEG possesses strong properties with respect to consistency, byzantine attackers, and scalability. First, we show that the MEG provides Strong Eventual Consistency (SEC), and that it is available under partition, by proving that the MEG is a Conflict-Free Replicated Data Type for causal histories. While strong consistency is impossible here as shown by the famous CAP theorem, SEC is among the best known achievable trade-offs. Second, we discuss the implications of byzantine attackers on the data type's properties. We note that the MEG, as it does not strive for consensus, can cope with $n > f$ environments with $n$ total participants of which $f$ show byzantine faults. Furthermore, we analyze scalability: Using Markov chains we study the width of the MEG, defined as the number of forward extremities, over time and observe an almost optimal evolution. We conjecture that this property is inherent to the underlying spatially inhomogeneous random walk.

cs.DC↗

arXiv2020

Fundamental Properties of the Layer Below a Payment Channel Network (Extended Version)

Payment channel networks are a highly discussed approach for improving scalability of cryptocurrencies such as Bitcoin. As they allow processing transactions off-chain, payment channel networks are referred to as second layer technology, while the blockchain is the first layer. We uncouple payment channel networks from blockchains and look at them as first-class citizens. This brings up the question what model payment channel networks require as first layer. In response, we formalize a model (called RFL Model) for a first layer below a payment channel network. While transactions are globally made available by a blockchain, the RFL Model only provides the reduced property that a transaction is delivered to the users being affected by a transaction. We show that the reduced model's properties still suffice to implement payment channels. By showing that the RFL Model can not only be instantiated by the Bitcoin blockchain but also by trusted third parties like banks, we show that the reduction widens the design space for the first layer. Further, we show that the stronger property provided by blockchains allows for optimizations that can be used to reduce the time for locking collateral during payments over multiple hops in a payment channel network.

cs.CR↗

arXiv2019

Attacks on Dynamic Protocol Detection of Open Source Network Security Monitoring Tools

Protocol detection is the process of determining the application layer protocol in the context of network security monitoring, which requires a timely and precise decision to enable protocol-specific deep packet inspection. This task has proven to be complex, as isolated characteristics like port numbers are not sufficient to reliably determine the application layer protocol. Hence, more dynamic detection approaches have been developed. In this paper, we analyze the Dynamic Protocol Detection mechanisms employed by popular and widespread open-source network monitoring tools. We show on the example of HTTP that all analyzed detection mechanisms are vulnerable to evasion attacks, which pose a serious threat to real-world monitoring operations. We find that the underlying fundamental problem of protocol disambiguation is not adequately addressed in two of three monitoring systems that we analyzed. To enable adequate operational decisions, this paper highlights the inherent trade-offs within Dynamic Protocol Detection.

cs.NI↗

arXiv2019

A Glimpse of the Matrix (Extended Version): Scalability Issues of a New Message-Oriented Data Synchronization Middleware

Matrix is a new message-oriented data synchronization middleware, used as a federated platform for near real-time decentralized applications. It features a novel approach for inter-server communication based on synchronizing message history by using a replicated data structure. We measured the structure of public parts in the Matrix federation as a basis to analyze the middleware's scalability. We confirm that users are currently cumulated on a single large server, but find more small servers than expected. We then analyze network load distribution in the measured structure and identify scalability issues of Matrix' group communication mechanism in structurally diverse federations.

cs.NI↗