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

A payment channel protocol does not only have to provide the payment functionality, it also has to fulfill security guarantees such as ensuring that an honest party receives their correct balance. For complexity reasons, it is typically difficult to assess the security of such a protocol or to find counterexamples in insecure protocols. In this poster, we present an approach to specify functional as well as security properties for a payment channel protocol in TLA+and show that a Lightning Network-style protocol fulfills the required properties. In case a counterexample is found, we provide protocol developers with a graphical and intuitive output. We present the challenges we faced and our approach to meeting these challenges.

In many public transport networks, multiple providers cooperate to offer integrated services and, conse-quently, provide integrated fare collection. Thus, ticket revenues need to be redistributed so that each provider receives its respective share. Typically, the customers' travel behavior is surveyed and the fares paid are aggregated over certain periods of time, and the revenue is periodically allocated based on this information. To avoid a centralized trusted third party or the exchange of sensitive information between providers, we present an approach that integrates revenue allocation directly into the payment process: The proposed approach is based on payment channel networks and utilizes multi-hop payments to perform revenue allocation. We thereby show how to make use of payment channel networks in this setting as well as the corresponding benefits.

Ethereum is a platform for deploying smart contracts, which due to their public nature and the financial value of the assets they manage are attractive targets for attacks. With asset management as a main task of smart contracts, access control aspects are naturally part of the application itself, but also of the functions implemented in a smart contract. Therefore, it is desirable to establish the correctness of smart contracts and their access control on application and single-function level through formal methods. However, there is no established methodology of formalising and verifying correctness properties of smart contracts. In this work, we make an attempt in this direction on the basis of a case study. We choose an existing smart contract application which aims to ascertain the integrity of binary files distributed over the Internet by means of decentralised identity management and access control. We formally specify and verify correctness at the level of single functions as well as temporal properties of the overall application. We demonstrate how to use verified low-level correctness properties for showing correctness at the higher level. In addition, we report on our experience with existing verification tools.