References of "Mauw, Sjouke 50002343"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailUnlinkability of an Improved Key Agreement Protocol for EMV 2nd Gen Payments
Horne, Ross James UL; Mauw, Sjouke UL; Yurkov, Semen UL

Scientific Conference (2022, August 10)

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 ... [more ▼]

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. [less ▲]

Detailed reference viewed: 42 (1 UL)
Peer Reviewed
See detailUnderstanding Content Bias: Qualitative research supports computational methods
Hoehn, Sviatlana UL; Lewandowska-Tomaszczyk, Barbara; Mauw, Sjouke UL et al

Scientific Conference (2022, July 01)

Full Text
Peer Reviewed
See detailPreventing active re-identification attacks on social graphs via sybil subgraph obfuscation
Mauw, Sjouke UL; Ramirez Cruz, Yunior UL; Trujillo Rasua, Rolando UL

in Knowledge and Information Systems (2022), 64

Active re-identification attacks constitute a serious threat to privacy-preserving social graph publication, because of the ability of active adversaries to leverage fake accounts, a.k.a. sybil nodes, to ... [more ▼]

Active re-identification attacks constitute a serious threat to privacy-preserving social graph publication, because of the ability of active adversaries to leverage fake accounts, a.k.a. sybil nodes, to enforce structural patterns that can be used to re-identify their victims on anonymised graphs. Several formal privacy properties have been enunciated with the purpose of characterising the resistance of a graph against active attacks. However, anonymisation methods devised on the basis of these properties have so far been able to address only restricted special cases, where the adversaries are assumed to leverage a very small number of sybil nodes. In this paper, we present a new probabilistic interpretation of active re-identification attacks on social graphs. Unlike the aforementioned privacy properties, which model the protection from active adversaries as the task of making victim nodes indistinguishable in terms of their fingerprints with respect to all potential attackers, our new formulation introduces a more complete view, where the attack is countered by jointly preventing the attacker from retrieving the set of sybil nodes, and from using these sybil nodes for re-identifying the victims. Under the new formulation, we show that k-symmetry, a privacy property introduced in the context of passive attacks, provides a sufficient condition for the protection against active re-identification attacks leveraging an arbitrary number of sybil nodes. Moreover, we show that the algorithm K-Match, originally devised for efficiently enforcing the related notion of k-automorphism, also guarantees k-symmetry. Empirical results on real-life and synthetic graphs demonstrate that our formulation allows, for the first time, to publish anonymised social graphs (with formal privacy guarantees) that effectively resist the strongest active re-identification attack reported in the literature, even when it leverages a large number of sybil nodes. [less ▲]

Full Text
Peer Reviewed
See detailBelElect: A New Dataset for Bias Research from a ”Dark” Platform
Hoehn, Sviatlana UL; Mauw, Sjouke UL; Asher, Nicholas

in Vol. 16 (2022): Proceedings of the Sixteenth International AAAI Conference on Web and Social Media (2022)

Detailed reference viewed: 22 (1 UL)
Full Text
Peer Reviewed
See detailA Graphical Proof Theory of Logical Time
Acclavio, Matteo UL; Horne, Ross James UL; Mauw, Sjouke UL et al

in Felty, Amy P. (Ed.) Proc. 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022) (2022)

Logical time is a partial order over events in distributed systems, constraining which events precede others. Special interest has been given to series-parallel orders since they correspond to formulas ... [more ▼]

Logical time is a partial order over events in distributed systems, constraining which events precede others. Special interest has been given to series-parallel orders since they correspond to formulas constructed via the two operations for "series" and "parallel" composition. For this reason, series-parallel orders have received attention from proof theory, leading to pomset logic, the logic BV, and their extensions. However, logical time does not always form a series-parallel order; indeed, ubiquitous structures in distributed systems are beyond current proof theoretic methods. In this paper, we explore how this restriction can be lifted. We design new logics that work directly on graphs instead of formulas, we develop their proof theory, and we show that our logics are conservative extensions of the logic BV. [less ▲]

Full Text
Peer Reviewed
See detailContingent payments from two-party signing and verification for abelian groups
Bursuc, Sergiu UL; Mauw, Sjouke UL

in Conference Proceedings 2022 IEEE 35th Computer Security Foundations Symposium (CSF) (2022)

The fair exchange problem has faced for a long time the bottleneck of a required trusted third party. The recent development of blockchains introduces a new type of party to this problem, whose ... [more ▼]

The fair exchange problem has faced for a long time the bottleneck of a required trusted third party. The recent development of blockchains introduces a new type of party to this problem, whose trustworthiness relies on a public ledger and distributed computation. The challenge in this setting is to reconcile the minimalistic and public nature of blockchains with elaborate fair exchange requirements, from functionality to privacy. Zero-knowledge contingent payments (ZKCP) are a class of protocols that are promising in this direction, allowing the fair exchange of data for payment. We propose a new ZKCP protocol that, when compared to others, requires less computation from the blockchain and less interaction between parties. The protocol is based on two-party (weak) adaptor signatures, which we show how to instantiate from state of the art multiparty sign- ing protocols. We improve the symbolic definition of ZKCP security and, for automated verification with Tamarin, we propose a general security reduction from the theory of abelian groups to the theory of exclusive or. [less ▲]

Detailed reference viewed: 18 (2 UL)
Full Text
Peer Reviewed
See detailCloud removal from satellite imagery using multispectral edge-filtered conditional generative adversarial networks
Hasan, Cengis; Horne, Ross James UL; Mauw, Sjouke UL et al

in International Journal of Remote Sensing (2022), 43(5), 1881-1893

Detailed reference viewed: 39 (1 UL)
Full Text
Peer Reviewed
See detailIs Eve nearby? Analysing protocols under the distant-attacker assumption
Gil Pons, Reynaldo UL; Horne, Ross James UL; Mauw, Sjouke UL et al

in IEEE Computer Security Foundations Symposium, August 7 - 10, 2022, Haifa, Israel (2022)

Detailed reference viewed: 62 (12 UL)
Full Text
Peer Reviewed
See detailProvably Improving Election Verifiability in Belenios
Baloglu, Sevdenur UL; Bursuc, Sergiu UL; Mauw, Sjouke UL et al

in Electronic Voting 6th International Joint Conference, E-Vote-ID 2021 Virtual Event, October 5–8, 2021, Proceedings (2021, October)

Belenios is an online voting system that provides a strong notion of election verifiability, where no single party has to be trusted, and security holds as soon as either the voting registrar or the ... [more ▼]

Belenios is an online voting system that provides a strong notion of election verifiability, where no single party has to be trusted, and security holds as soon as either the voting registrar or the voting server is honest. It was formally proved to be secure, making the assump- tion that no further ballots are cast on the bulletin board after voters verified their ballots. In practice, however, revoting is allowed and voters can verify their ballots anytime. This gap between formal proofs and use in practice leaves open space for attacks, as has been shown recently. In this paper we make two simple additions to Belenios and we formally prove that the new version satisfies the expected verifiability properties. Our proofs are automatically performed with the Tamarin prover, under the assumption that voters are allowed to vote at most four times. [less ▲]

Detailed reference viewed: 126 (23 UL)
Full Text
Peer Reviewed
See detailElection Verifiability Revisited: Automated Security Proofs and Attacks on Helios and Belenios
Baloglu, Sevdenur UL; Bursuc, Sergiu UL; Mauw, Sjouke UL et al

in IEEE 34th Computer Security Foundations Symposium, Dubrovnik 21-25 June 2021 (2021, June)

Election verifiability aims to ensure that the outcome produced by electronic voting systems correctly reflects the intentions of eligible voters, even in the presence of an adversary that may corrupt ... [more ▼]

Election verifiability aims to ensure that the outcome produced by electronic voting systems correctly reflects the intentions of eligible voters, even in the presence of an adversary that may corrupt various parts of the voting infrastructure. Protecting such systems from manipulation is challenging because of their distributed nature involving voters, election authorities, voting servers and voting platforms. An adversary corrupting any of these can make changes that, individually, would go unnoticed, yet in the end will affect the outcome of the election. It is, therefore, important to rigorously evaluate whether the measures prescribed by election verifiability achieve their goals. We propose a formal framework that allows such an evaluation in a systematic and automated way. We demonstrate its application to the verification of various scenarios in Helios and Belenios, two prominent internet voting systems, for which we capture features and corruption models previously outside the scope of formal verification. Relying on the Tamarin protocol prover for automation, we derive new security proofs and attacks on deployed versions of these protocols, illustrating trade-offs between usability and security. [less ▲]

Detailed reference viewed: 191 (15 UL)
Full Text
Peer Reviewed
See detailExamining Linguisic Biases with a Game Teoretic Analysis
Hoehn, Sviatlana UL; Mauw, Sjouke UL; Asher, Nicholas

in Proceedings of the 3rd Multidisciplinary International Symposium on Disinformation in Open Online Media (2021)

Detailed reference viewed: 155 (9 UL)
Full Text
Peer Reviewed
See detailCompositional Analysis of Protocol Equivalence in the Applied pi-Calculus Using Quasi-open Bisimilarity
Horne, Ross James UL; Mauw, Sjouke UL; Yurkov, Semen UL et al

in Theoretical Aspects of Computing -- ICTAC 2021 (2021)

This paper shows that quasi-open bisimilarity is the coarsest bisimilarity congruence for the applied pi-calculus. Furthermore, we show that this equivalence is suited to security and privacy problems ... [more ▼]

This paper shows that quasi-open bisimilarity is the coarsest bisimilarity congruence for the applied pi-calculus. Furthermore, we show that this equivalence is suited to security and privacy problems expressed as an equivalence problem in the following senses: (1) being a bisimilarity is a safe choice since it does not miss attacks based on rich strategies; (2) being a congruence it enables a compositional approach to proving certain equivalence problems such as unlinkability; and (3) being the coarsest such bisimilarity congruence it can establish proofs of some privacy properties where finer equivalences fail to do so. [less ▲]

Detailed reference viewed: 25 (3 UL)
Full Text
Peer Reviewed
See detailDiscovering ePassport Vulnerabilities using Bisimilarity
Horne, Ross James UL; Mauw, Sjouke UL

in Logical Methods in Computer Science (2021), 17(2), 241--2452

Detailed reference viewed: 20 (1 UL)
Full Text
Peer Reviewed
See detailActive Re-identification Attacks on Periodically Released Dynamic Social Graphs
Chen, Xihui UL; Kepuska, Ema UL; Mauw, Sjouke UL et al

in Chen, Liqun; Li, Ninghui; Liang, Kaitai (Eds.) et al Computer Security - ESORICS 2020 (2020, September 13)

Active re-identification attacks pose a serious threat to privacy-preserving social graph publication. Active attackers create fake accounts to enforce structural patterns that can be used to re-identify ... [more ▼]

Active re-identification attacks pose a serious threat to privacy-preserving social graph publication. Active attackers create fake accounts to enforce structural patterns that can be used to re-identify legitimate users on published anonymised graphs, even without additional background knowledge. So far, this type of attacks has only been studied in the scenario where the inherently dynamic social graph is published once. In this paper, we present the first active re-identification attack in the more realistic scenario where a dynamic social graph is periodically published. Our new attack leverages tempo-structural patterns, created by a dynamic set of sybil nodes, for strengthening the adversary. We evaluate our new attack through a comprehensive set of experiments on real-life and synthetic dynamic social graphs. We show that our new attack substantially outperforms the most effective static active attack in the literature by increasing success probability by at least two times and efficiency by at least 11 times. Moreover, we show that, unlike the static attack, our new attack remains at the same level of efficiency as the publication process advances. Additionally, we conduct a study on the factors that may thwart our new attack, which can help design dynamic graph anonymisation methods displaying a better balance between privacy and utility. [less ▲]

Detailed reference viewed: 65 (4 UL)
Full Text
Peer Reviewed
See detailPublishing Community-Preserving Attributed Social Graphs with a Differential Privacy Guarantee
Chen, Xihui UL; Mauw, Sjouke UL; Ramirez Cruz, Yunior UL

in Proceedings on Privacy Enhancing Technologies (2020), 2020(4), 131-152

We present a novel method for publishing differentially private synthetic attributed graphs. Our method allows, for the first time, to publish synthetic graphs simultaneously preserving structural ... [more ▼]

We present a novel method for publishing differentially private synthetic attributed graphs. Our method allows, for the first time, to publish synthetic graphs simultaneously preserving structural properties, user attributes and the community structure of the original graph. Our proposal relies on CAGM, a new community-preserving generative model for attributed graphs. We equip CAGM with efficient methods for attributed graph sampling and parameter estimation. For the latter, we introduce differentially private computation methods, which allow us to release communitypreserving 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. [less ▲]

Detailed reference viewed: 338 (5 UL)
Full Text
Peer Reviewed
See detailFine-grained Code Coverage Measurement in Automated Black-box Android Testing
Pilgun, Aleksandr UL; Gadyatskaya, Olga UL; Zhauniarovich, Yury et al

in ACM Transactions on Software Engineering and Methodology (2020), 29(4), 1-35

Today, there are millions of third-party Android applications. Some of them are buggy or even malicious. To identify such applications, novel frameworks for automated black-box testing and dynamic ... [more ▼]

Today, there are millions of third-party Android applications. Some of them are buggy or even malicious. To identify such applications, novel frameworks for automated black-box testing and dynamic analysis are being developed by the Android community. Code coverage is one of the most common metrics for evaluating effectiveness of these frameworks. Furthermore, code coverage is used as a fitness function for guiding evolutionary and fuzzy testing techniques. However, there are no reliable tools for measuring fine-grained code coverage in black-box Android app testing. We present the Android Code coVerage Tool, ACVTool for short, that instruments Android apps and measures code coverage in the black-box setting at class, method and instruction granularity. ACVTool has successfully instrumented 96.9% of apps in our experiments. It introduces a negligible instrumentation time overhead, and its runtime overhead is acceptable for automated testing tools. We demonstrate practical value of ACVTool in a large-scale experiment with Sapienz, a state-of-art automated testing tool. Using ACVTool on the same cohort of apps, we have compared different coverage granularities applied by Sapienz in terms of the found amount of crashes. Our results show that none of the applied coverage granularities clearly outperforms others in this aspect. [less ▲]

Detailed reference viewed: 92 (10 UL)
Full Text
Peer Reviewed
See detailÆGIS: Shielding Vulnerable Smart Contracts Against Attacks
Ferreira Torres, Christof UL; Steichen, Mathis UL; Norvill, Robert UL et al

in Proceedings of the 15th ACM Asia Conference on Computer and Communications Security (ASIA CCS ’20), October 5–9, 2020, Taipei, Taiwan (2020)

In recent years, smart contracts have suffered major exploits, cost- ing millions of dollars. Unlike traditional programs, smart contracts are deployed on a blockchain. As such, they cannot be modified ... [more ▼]

In recent years, smart contracts have suffered major exploits, cost- ing 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 vulnera- ble 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. [less ▲]

Detailed reference viewed: 244 (11 UL)
Full Text
Peer Reviewed
See detailAttack-Defence Frameworks: Argumentation-Based Semantics for Attack-Defence Trees.
Gabbay, Dov M. UL; Horne, Ross James UL; Mauw, Sjouke UL et al

in Graphical Models for Security - 7th International Workshop (2020)

Detailed reference viewed: 52 (11 UL)
Full Text
Peer Reviewed
See detailAttack-Tree Series: A Case for Dynamic Attack Tree Analysis
Gadyatskaya, Olga UL; Mauw, Sjouke UL

in Proc.\ 6th International Workshop on Graphical Models for Security (GraMSec'19) (2020)

Detailed reference viewed: 91 (4 UL)
Full Text
Peer Reviewed
See detailAttribute evaluation on attack trees with incomplete information
Buldas, Ahto; Gadyatskaya, Olga UL; Lenin, Aleksandr et al

in Computers and Security (2020), 88(101630),

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 ... [more ▼]

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. [less ▲]

Detailed reference viewed: 98 (5 UL)