-
A full software stack for epidemic disease management: Unlocking the joint potential of software technology and supercomputing
Authors:
Jonas Gilg,
Johann Fredrik Jadebeck,
Mariama Jaiteh,
David Kerkmann,
Niklas Medinger,
Shahbaz Memon,
Anna Wendler,
Moritz Zeumer,
Henrik Zunker,
Maximilian Betz,
Ralf Hannemann-Tamas,
Jonas Immanuel Heinicke,
Julian Litz,
Achim Basermann,
Cas Cremers,
Manuel Dahmen,
Andreas Gerndt,
Jens Henrik Göbbert,
Björn Hagemeier,
Carolina J. Klett-Tammen,
Berit Lange,
Katharina Nöh,
Sarah Straßburger,
Michael Meyer-Hermann,
Martin J. Kühn
Abstract:
Infectious diseases remain a major threat to human societies. During the recent COVID-19 pandemic, mathematical modeling and extensive computer simulations proved highly effective in supporting public health experts and decision makers.
Despite these advances, the full potential of modern modeling approaches and digital technologies has not yet been realized. Many critical tasks -- including exp…
▽ More
Infectious diseases remain a major threat to human societies. During the recent COVID-19 pandemic, mathematical modeling and extensive computer simulations proved highly effective in supporting public health experts and decision makers.
Despite these advances, the full potential of modern modeling approaches and digital technologies has not yet been realized. Many critical tasks -- including expert consultations, model execution, scenario analyses, report preparation, and result communication -- still relied heavily on manual, human-driven processes with each manual interaction introducing avoidable delays and limiting responsiveness during rapidly evolving outbreaks.
Pandemic preparedness should opt for automated workflows and seamlessly integrated software modules that can improve pandemic mitigation capabilities by substantially reducing response times. For this step, we require robust and flexible computational infrastructure capable of supporting heterogeneous hardware and continuously evolving infectious-disease models. In addition, data sources need to be dynamically integrated. Managing such demands needs infrastructure that supports automated high-performance computing (HPC) workflows. Beyond computational performance, software infrastructure must ensure secure user and data management to comply with data-protection regulations and provide clear, transparent presentation of results to both decision makers and the public.
Meeting the aforementioned challenges requires tight integration of state-of-the-art scientific software with modern, scalable infrastructure that can leverage supercomputing resources when necessary. For rapid deployment in future epidemic or pandemic scenarios, adherence to the FAIR principles for research software is critical to ensure reusability and sustainability.
△ Less
Submitted 27 March, 2026;
originally announced August 2026.
-
Less Effort, Shorter Proofs: Reinforcement Learning for Security Protocol Analysis in Tamarin
Authors:
Matthias Cosler,
Cas Cremers,
Bernd Finkbeiner,
Mohamed Ghanem,
Niklas Medinger
Abstract:
Tools like Tamarin and ProVerif have achieved notable success in analyzing and verifying complex real-world protocols such as EMV, 5G, and WPA2, even detecting zero-day exploits. Despite these successes, verifying such protocols remains a time-consuming, challenging task, often requiring significant human effort and expertise. In this paper, we present a reinforcement learning (RL) framework inspi…
▽ More
Tools like Tamarin and ProVerif have achieved notable success in analyzing and verifying complex real-world protocols such as EMV, 5G, and WPA2, even detecting zero-day exploits. Despite these successes, verifying such protocols remains a time-consuming, challenging task, often requiring significant human effort and expertise. In this paper, we present a reinforcement learning (RL) framework inspired by AlphaZero and AlphaProof that implements a new style of proof search for Tamarin. We have developed a stateless API for Tamarin that acts as a classical RL environment. We guide a Monte Carlo Tree Search (MCTS) by a neural heuristic that learns from completed subproofs. We evaluate our framework on 16 case studies, ranging from classical protocol models to challenging state-of-the-art protocol models from recent publications. Our method finds more proofs automatically than Tamarin's standard search and produces shorter proofs than both the standard and human-engineered heuristics. Our pipeline is applicable out of the box to assist Tamarin users in active research, reducing the human effort required. Moreover, our standardized interface provides a programmatic way for users to interact with Tamarin. Finally, our work demonstrates the promising potential of adapting RL-based methods to the Tamarin domain.
△ Less
Submitted 22 May, 2026;
originally announced May 2026.
-
A Knowledge-Based Language Model: Deducing Grammatical Knowledge in a Multi-Agent Language Acquisition Simulation
Authors:
David Ph. Shakouri,
Crit Cremers,
Niels O. Schiller
Abstract:
This paper presents an initial study performed by the MODOMA system. The MODOMA is a computational multi-agent laboratory environment for unsupervised language acquisition experiments such that acquisition is based on the interaction between two language models, an adult and a child agent. Although this framework employs statistical as well as rule-based procedures, the result of language acquisit…
▽ More
This paper presents an initial study performed by the MODOMA system. The MODOMA is a computational multi-agent laboratory environment for unsupervised language acquisition experiments such that acquisition is based on the interaction between two language models, an adult and a child agent. Although this framework employs statistical as well as rule-based procedures, the result of language acquisition is a knowledge-based language model, which can be used to generate and parse new utterances of the target language. This system is fully parametrized and researchers can control all aspects of the experiments while the results of language acquisition, that is, the acquired grammatical knowledge, are explicitly represented and can be consulted. Thus, this system introduces novel possibilities for conducting computational language acquisition experiments. The experiments presented by this paper demonstrate that functional and content categories can be acquired and represented by the daughter agent based on training and test data containing different amounts of exemplars generated by the adult agent. Interestingly, similar patterns, which are well-established for human-generated data, are also found for these machine-generated data. As the procedures resulted in the successful acquisition of discrete grammatical categories by the child agent, these experiments substantiate the validity of the MODOMA approach to modelling language acquisition.
△ Less
Submitted 1 December, 2025;
originally announced December 2025.
-
Unsupervised Acquisition of Discrete Grammatical Categories
Authors:
David Ph. Shakouri,
Crit Cremers,
Niels O. Schiller
Abstract:
This article presents experiments performed using a computational laboratory environment for language acquisition experiments. It implements a multi-agent system consisting of two agents: an adult language model and a daughter language model that aims to learn the mother language. Crucially, the daughter agent does not have access to the internal knowledge of the mother language model but only to…
▽ More
This article presents experiments performed using a computational laboratory environment for language acquisition experiments. It implements a multi-agent system consisting of two agents: an adult language model and a daughter language model that aims to learn the mother language. Crucially, the daughter agent does not have access to the internal knowledge of the mother language model but only to the language exemplars the mother agent generates. These experiments illustrate how this system can be used to acquire abstract grammatical knowledge. We demonstrate how statistical analyses of patterns in the input data corresponding to grammatical categories yield discrete grammatical rules. These rules are subsequently added to the grammatical knowledge of the daughter language model. To this end, hierarchical agglomerative cluster analysis was applied to the utterances consecutively generated by the mother language model. It is argued that this procedure can be used to acquire structures resembling grammatical categories proposed by linguists for natural languages. Thus, it is established that non-trivial grammatical knowledge has been acquired. Moreover, the parameter configuration of this computational laboratory environment determined using training data generated by the mother language model is validated in a second experiment with a test set similarly resulting in the acquisition of non-trivial categories.
△ Less
Submitted 14 December, 2025; v1 submitted 24 March, 2025;
originally announced March 2025.
-
Decentralized Privacy-Preserving Proximity Tracing
Authors:
Carmela Troncoso,
Mathias Payer,
Jean-Pierre Hubaux,
Marcel Salathé,
James Larus,
Edouard Bugnion,
Wouter Lueks,
Theresa Stadler,
Apostolos Pyrgelis,
Daniele Antonioli,
Ludovic Barman,
Sylvain Chatel,
Kenneth Paterson,
Srdjan Čapkun,
David Basin,
Jan Beutel,
Dennis Jackson,
Marc Roeschlin,
Patrick Leu,
Bart Preneel,
Nigel Smart,
Aysajan Abidin,
Seda Gürses,
Michael Veale,
Cas Cremers
, et al. (9 additional authors not shown)
Abstract:
This document describes and analyzes a system for secure and privacy-preserving proximity tracing at large scale. This system, referred to as DP3T, provides a technological foundation to help slow the spread of SARS-CoV-2 by simplifying and accelerating the process of notifying people who might have been exposed to the virus so that they can take appropriate measures to break its transmission chai…
▽ More
This document describes and analyzes a system for secure and privacy-preserving proximity tracing at large scale. This system, referred to as DP3T, provides a technological foundation to help slow the spread of SARS-CoV-2 by simplifying and accelerating the process of notifying people who might have been exposed to the virus so that they can take appropriate measures to break its transmission chain. The system aims to minimise privacy and security risks for individuals and communities and guarantee the highest level of data protection. The goal of our proximity tracing system is to determine who has been in close physical proximity to a COVID-19 positive person and thus exposed to the virus, without revealing the contact's identity or where the contact occurred. To achieve this goal, users run a smartphone app that continually broadcasts an ephemeral, pseudo-random ID representing the user's phone and also records the pseudo-random IDs observed from smartphones in close proximity. When a patient is diagnosed with COVID-19, she can upload pseudo-random IDs previously broadcast from her phone to a central server. Prior to the upload, all data remains exclusively on the user's phone. Other users' apps can use data from the server to locally estimate whether the device's owner was exposed to the virus through close-range physical proximity to a COVID-19 positive person who has uploaded their data. In case the app detects a high risk, it will inform the user.
△ Less
Submitted 25 May, 2020;
originally announced May 2020.
-
Improving Automated Symbolic Analysis for E-voting Protocols: A Method Based on Sufficient Conditions for Ballot Secrecy
Authors:
Cas Cremers,
Lucca Hirschi
Abstract:
We advance the state-of-the-art in automated symbolic analysis for e-voting protocols by introducing three conditions that together are sufficient to guarantee ballot secrecy. There are two main advantages to using our conditions, compared to existing automated approaches. The first is a substantial expansion of the class of protocols and threat models that can be automatically analysed: we can sy…
▽ More
We advance the state-of-the-art in automated symbolic analysis for e-voting protocols by introducing three conditions that together are sufficient to guarantee ballot secrecy. There are two main advantages to using our conditions, compared to existing automated approaches. The first is a substantial expansion of the class of protocols and threat models that can be automatically analysed: we can systematically deal with (a) honest authorities present in different phases, (b) threat models in which no dishonest voters occur, and (c) protocols whose ballot secrecy depends on fresh data coming from other phases. The second advantage is that it can significantly improve verification efficiency, as the individual conditions are often simpler to verify. E.g., for the LEE protocol, we obtain a speedup of over two orders of magnitude. We show the scope and effectiveness of our approach using ProVerif in several case studies, including FOO, LEE, JCJ, and Belenios. In these case studies, our approach does not yield any false attacks, suggesting that our conditions are tight.
△ Less
Submitted 15 March, 2019; v1 submitted 1 September, 2017;
originally announced September 2017.
-
An Object-Oriented and Fast Lexicon for Semantic Generation
Authors:
Maarten Hijzelendoorn,
Crit Cremers
Abstract:
This paper is about the technical design of a large computational lexicon, its storage, and its access from a Prolog environment. Traditionally, efficient access and storage of data structures is implemented by a relational database management system. In Delilah, a lexicon-based NLP system, efficient access to the lexicon by the semantic generator is vital. We show that our highly detailed HPSG-…
▽ More
This paper is about the technical design of a large computational lexicon, its storage, and its access from a Prolog environment. Traditionally, efficient access and storage of data structures is implemented by a relational database management system. In Delilah, a lexicon-based NLP system, efficient access to the lexicon by the semantic generator is vital. We show that our highly detailed HPSG-style lexical specifications do not fit well in the Relational Model, and that they cannot be efficiently retrieved. We argue that they fit more naturally in the Object-Oriented Model. Although storage of objects is redundant, we claim that efficient access is still possible by applying indexing, and compression techniques from the Relational Model to the Object-Oriented Model. We demonstrate that it is possible to implement object-oriented storage and fast access in ISO Prolog.
△ Less
Submitted 20 May, 2009;
originally announced May 2009.
-
On the Protocol Composition Logic PCL
Authors:
Cas Cremers
Abstract:
A recent development in formal security protocol analysis is the Protocol Composition Logic (PCL). We identify a number of problems with this logic as well as with extensions of the logic, as defined in [DDMP05,HSD+05,He05,Dat05,Der06,DDMR07]. The identified problems imply strong restrictions on the scope of PCL, and imply that some currently claimed PCL proofs cannot be proven within the logic,…
▽ More
A recent development in formal security protocol analysis is the Protocol Composition Logic (PCL). We identify a number of problems with this logic as well as with extensions of the logic, as defined in [DDMP05,HSD+05,He05,Dat05,Der06,DDMR07]. The identified problems imply strong restrictions on the scope of PCL, and imply that some currently claimed PCL proofs cannot be proven within the logic, or make use of unsound axioms. Where possible, we propose solutions for these problems.
△ Less
Submitted 22 February, 2008; v1 submitted 7 September, 2007;
originally announced September 2007.
-
A framework for compositional verification of security protocols
Authors:
Suzana Andova,
Cas Cremers,
Kristian Gjosteen,
Sjouke Mauw,
Stig F. Mjolsnes,
Sasa Radomirovic
Abstract:
Automatic security protocol analysis is currently feasible only for small protocols. Since larger protocols quite often are composed of many small protocols, compositional analysis is an attractive, but non-trivial approach.
We have developed a framework for compositional analysis of a large class of security protocols. The framework is intended to facilitate automatic as well as manual verifi…
▽ More
Automatic security protocol analysis is currently feasible only for small protocols. Since larger protocols quite often are composed of many small protocols, compositional analysis is an attractive, but non-trivial approach.
We have developed a framework for compositional analysis of a large class of security protocols. The framework is intended to facilitate automatic as well as manual verification of large structured security protocols. Our approach is to verify properties of component protocols in a multi-protocol environment, then deduce properties about the composed protocol. To reduce the complexity of multi-protocol verification, we introduce a notion of protocol independence and prove a number of theorems that enable analysis of independent component protocols in isolation.
To illustrate the applicability of our framework to real-world protocols, we study a key establishment sequence in WiMax consisting of three subprotocols. Except for a small amount of trivial reasoning, the analysis is done using automatic tools.
△ Less
Submitted 1 May, 2007; v1 submitted 14 November, 2006;
originally announced November 2006.
-
Counting Coordination Categorially
Authors:
Crit Cremers,
Maarten Hijzelendoorn
Abstract:
This paper presents a way of reducing the complexity of parsing free coordination. It lives on the Coordinative Count Invariant, a property of derivable sequences in occurrence-sensitive categorial grammar. This invariant can be exploited to cut down deterministically the search space for coordinated sentences to minimal fractions. The invariant is based on inequalities, which is shown to be the…
▽ More
This paper presents a way of reducing the complexity of parsing free coordination. It lives on the Coordinative Count Invariant, a property of derivable sequences in occurrence-sensitive categorial grammar. This invariant can be exploited to cut down deterministically the search space for coordinated sentences to minimal fractions. The invariant is based on inequalities, which is shown to be the best one can get in the presence of coordination without proper parsing. It is implemented in a categorial parser for Dutch. Some results of applying the invariant to the parsing of coordination in this parser are presented.
△ Less
Submitted 7 May, 1996; v1 submitted 6 May, 1996;
originally announced May 1996.