Sjouke Mauw

Clément Aubert, Ross Horne, Christian Johansen et al.

An ever-increasing number of critical infrastructures rely heavily on the assumption that security protocols satisfy a wealth of requirements. Hence, the importance of certifying e.g., privacy properties using methods that are better at detecting attacks can hardly be overstated. This paper scrutinises the "unlinkability" privacy property using relations equating behaviours that cannot be distinguished by attackers. Starting from the observation that some reasonable design choice can lead to formalisms missing attacks, we draw attention to a classical concurrent semantics accounting for relationship between past events, and show that there are concurrency-aware semantics that can discover attacks on all protocols we consider.More precisely, we focus on protocols where trace equivalence is known to miss attacks that are observable using branching-time equivalences. We consider the impact of three dimensions: design decisions made by the programmer specifying an unlinkability problem (style), semantics respecting choices during execution (branching-time), and semantics sensitive to concurrency (non-interleaving), and discover that reasonable styles miss attacks unless we give attackers enough power to observe choices and concurrency. Our main contribution is to draw attention to how a popular concurrent semantics -- history-preserving bisimilarity -- when defined for the non-interleaving applied \(π\)-calculus, can discover attacks on all protocols we consider, regardless of the choice of style. Furthermore, we can describe all such attacks using a novel modal logic that is hence suitable to formally certify attacks on privacy properties.

Chenxiang Zhang, Tongxi Qu, Zhong Li et al.

Deep neural networks are widely deployed with quantization techniques to reduce memory and computational costs by lowering the numerical precision of their parameters. While quantization alters model parameters and their outputs, existing privacy analyses primarily focus on full-precision models, leaving a gap in understanding how bit-width reduction can affect privacy leakage. We present the first systematic study of the privacy-utility relationship in post-training quantization (PTQ), a versatile family of methods that can be applied to pretrained models without further training. Using membership inference attacks as our evaluation framework, we analyze three popular PTQ algorithms-AdaRound, BRECQ, and OBC-across multiple precision levels (4-bit, 2-bit, and 1.58-bit) on CIFAR-10, CIFAR-100, and TinyImageNet datasets. Our findings consistently show that low-precision PTQs can reduce privacy leakage. In particular, lower-precision models demonstrate up to an order of magnitude reduction in membership inference vulnerability compared to their full-precision counterparts, albeit at the cost of decreased utility. Additional ablation studies on the 1.58-bit quantization level show that quantizing only the last layer at higher precision enables fine-grained control over the privacy-utility trade-off. These results offer actionable insights for practitioners to balance efficiency, utility, and privacy protection in real-world deployments.

Barbara Kordy, Piotr Kordy, Sjouke Mauw et al.

The ADTool is free, open source software assisting graphical modeling and quantitative analysis of security, using attack-defense trees. The main features of the ADTool are easy creation, efficient editing, and automated bottom-up evaluation of security-relevant measures. The tool also supports the usage of attack trees, protection trees and defense trees, which are all particular instances of attack-defense trees.

Chenxiang Zhang, Alexander Theus, Damien Teney et al.

Model merging methods combine models with different capabilities into a single one while maintaining the same inference cost. Two popular approaches are linear interpolation, which linearly interpolates between model weights, and task arithmetic, which combines task vectors obtained by the difference between finetuned and base models. While useful in practice, what properties make merging effective are poorly understood. This paper explores how the optimization process affects the loss landscape geometry and its impact on merging success. We show that a single quantity -- the effective noise scale -- unifies the impact of optimizer and data choices on model merging. Across architectures and datasets, the effectiveness of merging success is a non-monotonic function of effective noise, with a distinct optimum. Decomposing this quantity, we find that larger learning rates, stronger weight decay, smaller batch sizes, and data augmentation all independently modulate the effective noise scale, exhibiting the same qualitative trend. Unlike prior work that connects optimizer noise to the flatness or generalization of individual minima, we show that it also affects the global loss landscape, predicting when independently trained solutions can be merged. Our findings broaden the understanding of how optimization shapes the loss landscape geometry and its downstream consequences for model merging, suggesting the possibility of further manipulating the training dynamics to improve merging effectiveness.

Zach Smith, Hugo Jonker, Sjouke Mauw et al.

Message forwarding protocols are protocols in which a chain of agents handles transmission of a message. Each agent forwards the received message to the next agent in the chain. For example, TLS middleboxes act as intermediary agents in TLS, adding functionality such as filtering or compressing data. In such protocols, an attacker may attempt to bypass one or more intermediary agents. Such an agent-skipping attack can the violate security requirements of the protocol. Using the multiset rewriting model in the symbolic setting, we construct a comprehensive framework of such path protocols. In particular, we introduce a set of security goals related to path integrity: the notion that a message faithfully travels through participants in the order intended by the initiating agent. We perform a security analysis of several such protocols, highlighting key attacks on modern protocols.

Ross Horne, Sjouke Mauw, Semen Yurkov

To address known privacy problems with the EMV standard, EMVCo have proposed a Blinded Diffie-Hellman key establishment protocol, which is intended to be part of a future 2nd Gen EMV protocol. We point out that active attackers were not previously accounted for in the privacy requirements of this proposal protocol, and demonstrate that an active attacker can compromise unlinkability within a distance of 100cm. Here, we adopt a strong definition of unlinkability that does account for active attackers and propose an enhancement of the protocol proposed by EMVCo. We prove that our protocol does satisfy strong unlinkability, while preserving authentication.

Christof Ferreira Torres, Mathis Baden, Robert Norvill et al.

In recent years, smart contracts have suffered major exploits, costing millions of dollars. Unlike traditional programs, smart contracts are deployed on a blockchain. As such, they cannot be modified once deployed. Though various tools have been proposed to detect vulnerable smart contracts, the majority fails to protect vulnerable contracts that have already been deployed on the blockchain. Only very few solutions have been proposed so far to tackle the issue of post-deployment. However, these solutions suffer from low precision and are not generic enough to prevent any type of attack. In this work, we introduce ÆGIS, a dynamic analysis tool that protects smart contracts from being exploited during runtime. Its capability of detecting new vulnerabilities can easily be extended through so-called attack patterns. These patterns are written in a domain-specific language that is tailored to the execution model of Ethereum smart contracts. The language enables the description of malicious control and data flows. In addition, we propose a novel mechanism to streamline and speed up the process of managing attack patterns. Patterns are voted upon and stored via a smart contract, thus leveraging the benefits of tamper-resistance and transparency provided by the blockchain. We compare ÆGIS to current state-of-the-art tools and demonstrate that our solution achieves higher precision in detecting attacks. Finally, we perform a large-scale analysis on the first 4.5 million blocks of the Ethereum blockchain, thereby confirming the occurrences of well reported and yet unreported attacks in the wild.

Ross Horne, Sjouke Mauw

We uncover privacy vulnerabilities in the ICAO 9303 standard implemented by ePassports worldwide. These vulnerabilities, confirmed by ICAO, enable an ePassport holder who recently passed through a checkpoint to be reidentified without opening their ePassport. This paper explains how bisimilarity was used to discover these vulnerabilities, which exploit the BAC protocol - the original ICAO 9303 standard ePassport authentication protocol - and remains valid for the PACE protocol, which improves on the security of BAC in the latest ICAO 9303 standards. In order to tackle such bisimilarity problems, we develop here a chain of methods for the applied $π$-calculus including a symbolic under-approximation of bisimilarity, called open bisimilarity, and a modal logic, called classical FM, for describing and certifying attacks. Evidence is provided to argue for a new scheme for specifying such unlinkability problems that more accurately reflects the capabilities of an attacker.

Xihui Chen, Sjouke Mauw, Yunior Ramírez-Cruz

We present a novel method for publishing differentially private synthetic attributed graphs. Unlike preceding approaches, our method is able to preserve the community structure of the original graph without sacrificing the ability to capture global structural properties. Our proposal relies on C-AGM, a new community-preserving generative model for attributed graphs. We equip C-AGM with efficient methods for attributed graph sampling and parameter estimation. For the latter, we introduce differentially private computation methods, which allow us to release community-preserving synthetic attributed social graphs with a strong formal privacy guarantee. Through comprehensive experiments, we show that our new model outperforms its most relevant counterparts in synthesising differentially private attributed social graphs that preserve the community structure of the original graph, as well as degree sequences and clustering coefficients.

Ahto Buldas, Olga Gadyatskaya, Aleksandr Lenin et al.

Attack trees are considered a useful tool for security modelling because they support qualitative as well as quantitative analysis. The quantitative approach is based on values associated to each node in the tree, expressing, for instance, the minimal cost or probability of an attack. Current quantitative methods for attack trees allow the analyst to, based on an initial assignment of values to the leaf nodes, derive the values of the higher nodes in the tree. In practice, however, it shows to be very difficult to obtain reliable values for all leaf nodes. The main reasons are that data is only available for some of the nodes, that data is available for intermediate nodes rather than for the leaf nodes, or even that the available data is inconsistent. We address these problems by developing a generalisation of the standard bottom-up calculation method in three ways. First, we allow initial attributions of non-leaf nodes. Second, we admit additional relations between attack steps beyond those provided by the underlying attack tree semantics. Third, we support the calculation of an approximative solution in case of inconsistencies. We illustrate our method, which is based on constraint programming, by a comprehensive case study.

Jun Pang, Yang Liu, Sjouke Mauw

The present volume contains the proceedings of the Fourth International Workshop on Engineering Safety and Security Systems (ESSS'15). The workshop was held in Oslo, Norway, on June 22nd, 2015, as a satellite event of the 20th International Symposium on Formal Methods (FM'15).

Gildas Avoine, Sjouke Mauw, Rolando Trujillo-Rasua

Distance bounding protocols are security countermeasures designed to thwart relay attacks. Such attacks consist in relaying messages exchanged between two parties, making them believe they communicate directly with each other. Although distance bounding protocols have existed since the early nineties, this research topic resurrected with the deployment of contactless systems, against which relay attacks are particularly impactful. Given the impressive number of distance bounding protocols that are designed every year, it becomes urgent to provide researchers and engineers with a methodology to fairly compare the protocols in spite of their various properties. This paper introduces such a methodology based on concepts from the decision making field. The methodology allows for a multi-criteria comparison of distance bounding protocols, thereby identifying the most appropriate protocols once the context is provided. As a side effect, this paper clearly identifies the protocols that should no longer be considered, regardless of the considered scenario.

Ravi Jhawar, Barbara Kordy, Sjouke Mauw et al.

We provide the first formal foundation of SAND attack trees which are a popular extension of the well-known attack trees. The SAND attack tree formalism increases the expressivity of attack trees by introducing the sequential conjunctive operator SAND. This operator enables the modeling of ordered events. We give a semantics to SAND attack trees by interpreting them as sets of series-parallel graphs and propose a complete axiomatization of this semantics. We define normal forms for SAND attack trees and a term rewriting system which allows identification of semantically equivalent trees. Finally, we formalize how to quantitatively analyze SAND attack trees using attributes.

Sjouke Mauw, Sasa Radomirovic

Multi-party contract signing (MPCS) protocols allow a group of signers to exchange signatures on a predefined contract. Previous approaches considered either completely linear protocols or fully parallel broadcasting protocols. We introduce the new class of DAG MPCS protocols which combines parallel and linear execution and allows for parallelism even within a signer role. This generalization is useful in practical applications where the set of signers has a hierarchical structure, such as chaining of service level agreements and subcontracting. Our novel DAG MPCS protocols are represented by directed acyclic graphs and equipped with a labeled transition system semantics. We define the notion of abort-chaining sequences and prove that a DAG MPCS protocol satisfies fairness if and only if it does not have an abort-chaining sequence. We exhibit several examples of optimistic fair DAG MPCS protocols. The fairness of these protocols follows from our theory and has additionally been verified with our automated tool. We define two complexity measures for DAG MPCS protocols, related to execution time and total number of messages exchanged. We prove lower bounds for fair DAG MPCS protocols in terms of these measures.

Barbara Kordy, Sjouke Mauw, Wolter Pieters

The present volume contains the proceedings of the First International Workshop on Graphical Models for Security (GraMSec'14). The workshop was held in Grenoble, France, on April 12, 2014, as one of the satellite events of the European Joint Conferences on Theory and Practice of Software 2014 (ETAPS'14). Graphical security models provide an intuitive but systematic methodology to analyze security weaknesses of systems and to evaluate potential protection measures. Such models have been subject of academic research and they have also been widely accepted by the industrial sector, as a means to support and facilitate threat analysis and risk management processes. The objective of GraMSec is to contribute to the development of well-founded graphical security models, efficient algorithms for their analysis, as well as methodologies for their practical usage. The workshop brings together academic researchers and industry practitioners designing and employing visual models for security in order to provide a platform for discussion, knowledge exchange and collaborations.

Barbara Kordy, Sjouke Mauw, Patrick Schweitzer

Attack-defense trees are a novel methodology for graphical security modeling and assessment. The methodology includes visual, intuitive tree models whose analysis is supported by a rigorous mathematical formalism. Both, the intuitive and the formal components of the approach can be used for quantitative analysis of attack-defense scenarios. In practice, we use intuitive questions to ask about aspects of scenarios we are interested in. Formally, a computational procedure, defined with the help of attribute domains and a bottom-up algorithm, is applied to derive the corresponding numerical values. This paper bridges the gap between the intuitive and the formal way of quantitatively assessing attack-defense scenarios. We discuss how to properly specify a question, so that it can be answered unambiguously. Given a well specified question, we then show how to derive an appropriate attribute domain which constitutes the corresponding formal model. Since any attack tree is in particular an attack-defense tree, our analysis is also an advancement of the attack tree methodology.