Presentation at CSF 2026
The Computer Security Foundations Symposium (CSF) is an annual forum for research on security theories, formal models, and verification techniques. Its scope includes access control, information flow, cryptographic protocols, database and language-based security, authorization, trust, integrity, availability, and the application of formal methods to security research. The 39th edition took place in Lisbon, Portugal, from July 26 to 29, 2026.
At CSF 2026, Pim Keer presented A Composable Game-Theoretic Framework for Blockchains, co-authored with Fabian Regen, Georg Fuchsbauer, Matteo Maffei, and Zeta Avarikioti.
Blockchains depend on economic incentives to encourage miners, validators, users, and other participants to behave in ways that keep the system secure. In practice, however, blockchain applications do not operate independently. Smart contracts, Layer-2 systems, consensus mechanisms, and network services interact through shared infrastructure, while several protocols may run simultaneously on the same blockchain and compete for the same resources. These interactions can change participants’ incentives and create security risks that are difficult to detect when each protocol is analysed separately.
The researchers developed a new compositional game-theoretic framework for studying these interactions across different parts of a blockchain system. It shows how decisions made at one layer, such as the application, network, or consensus layer, can influence behaviour elsewhere in the system. The framework also models cross-application composition, enabling researchers to analyse how several applications interact when they rely on the same underlying blockchain infrastructure.
This approach supports a more modular form of security analysis. Researchers can first examine the security and incentive properties of individual components and then determine whether those properties continue to hold when the components are combined. This reduces the need to reconstruct the behaviour of an entire blockchain ecosystem whenever a new application or protocol is introduced. It also makes it easier to trace how incentives propagate through the system and to identify the conditions under which an apparently secure design may become vulnerable.
The framework was evaluated through case studies involving Hashed Timelock Contracts, Layer-2 protocols, and Maximal Extractable Value. These examples demonstrate how interactions between different parts of a blockchain ecosystem can create incentive problems that remain hidden when protocols are analysed separately. The case studies highlight risks associated with censorship and bribery attacks, showing how mechanisms that appear secure under standard assumptions may become vulnerable when other actors or protocols influence their operation. The researchers also introduced a new model of rational miner behaviour, providing a more detailed account of how miners may respond to economic incentives. Using this model, they derived new conditions under which timelocks can remain robust against bribery.
The work is particularly relevant as modern blockchain systems become increasingly layered, interconnected, and difficult to analyse. Security guarantees are often established for individual protocols under simplified assumptions, but those guarantees may weaken or fail when a protocol interacts with applications, network components, consensus mechanisms, or other protocols operating on shared infrastructure. Such interactions can alter the incentives of miners, validators, users, and application developers, leading to unexpected strategic behaviour and new dependencies. The proposed framework enables researchers and developers to study these combined effects systematically rather than treating each component as an isolated system. It therefore supports the design of blockchain infrastructures whose security guarantees remain meaningful under realistic deployment conditions.
The proposed approach also opens several directions for further research. Future extensions could incorporate more complex network conditions, including delayed or asynchronous communication, selective message delivery, targeted censorship, and variations in network latency. Another important objective is to automate the translation of blockchain protocol specifications into formal game-theoretic models, making the approach easier to apply to a broader range of systems. Researchers may also use the framework to identify classes of protocols that preserve their security and incentive properties when deployed together. Further work could examine different blockchain environments, including variations in hash-rate distribution, network structure, and assumptions about participant behaviour.