Publications (37)
It Takes a Village: Bridging the Gaps between Current and Formal Specifications for Protocols
David Basin, Nate Foster, Kenneth L. McMillan +5
Formal specifications have numerous benefits for both designers and users of network protocols. They provide clear, unambiguous representations, which are useful as documentation a…
One For All: Formally Verifying Protocols which use Aggregate Signatures (extended version)
Xenia Hofmeier, Andrea Raguso, Ralf Sasse +2
Aggregate signatures are digital signatures that compress multiple signatures from different parties into a single signature, thereby reducing storage and bandwidth requirements. B…
Oblivious Digital Tokens
Mihael Liskij, Xuhua Ding, Gene Tsudik +1
A computing device typically identifies itself by exhibiting unique measurable behavior or by proving its knowledge of a secret. In both cases, the identifying device must reveal i…
Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification
Christoph Sprenger, Tobias Klenze, Marco Eilers +4
Lighthouse projects such as CompCert, seL4, IronFleet, and DeepSpec have demonstrated that full verification of entire systems is feasible by establishing a refinement relation bet…
Efficient Evaluation of Arbitrary Relational Calculus Queries
Martin Raszyk, David Basin, SrÄan KrstiÄ +1
The relational calculus (RC) is a concise, declarative query language. However, existing RC query evaluation approaches are inefficient and often deviate from established algorithm…
Efficient Black-box Checking of Snapshot Isolation in Databases
Kaile Huang, Si Liu, Zhenge Chen +4
Snapshot isolation (SI) is a prevalent weak isolation level that avoids the performance penalty imposed by serializability and simultaneously prevents various undesired data anomal…
Differential privacy with partial knowledge
Damien Desfontaines, Esfandiar Mohammadi, Elisabeth Krahmer +1
Differential privacy offers formal quantitative guarantees for algorithms over datasets, but it assumes attackers that know and can influence all but one record in the database. Th…
A Theory of Black-Box Tests
Mohammad Torabi Dashti, David Basin
The purpose of testing a system with respect to a requirement is to refute the hypothesis that the system satisfies the requirement. We build a theory of tests and refutation based…
Runtime Verification of Temporal Properties over Out-of-order Data Streams
David Basin, Felix Klaedtke, Eugen ZÄlinescu
We present a monitoring approach for verifying systems at runtime. Our approach targets systems whose components communicate with the monitors over unreliable channels, where messa…
Role Mining with Probabilistic Models
Mario Frank, Joachim M. Buhmann, David Basin
Role mining tackles the problem of finding a role-based access control (RBAC) configuration, given an access-control matrix assigning users to access permissions as input. Most rol…
A Formal Analysis of 5G Authentication
David Basin, Jannik Dreier, Lucca Hirschi +3
Mobile communication networks connect much of the world's population. The security of users' calls, SMSs, and mobile data depends on the guarantees provided by the Authenticated Ke…
SealClub: Computer-aided Paper Document Authentication
MartÃn Ochoa, Jorge Toro-Pozo, David Basin
Digital authentication is a mature field, offering a range of solutions with rigorous mathematical guarantees. Nevertheless, paper documents, where cryptographic techniques are not…
Exploring Website Location as a Security Indicator
Der-Yeuan Yu, Elizabeth Stobert, David Basin +1
Authenticating websites is an ongoing problem for users. Recent proposals have suggested strengthening current server authentication methods by incorporating website location as a…
Protocols to Code: Formal Verification of a Next-Generation Internet Router
João C. Pereira, Tobias Klenze, Sofia Giampietro +8
We present the first formally-verified Internet router, which is part of the SCION Internet architecture. SCION routers run a cryptographic protocol for secure packet forwarding in…
SoK: Attacks on Modern Card Payments
Xenia Hofmeier, David Basin, Ralf Sasse +1
EMV is the global standard for smart card payments and its NFC-based version, EMV contactless, is widely used, also for mobile payments. In this systematization of knowledge, we ex…
Locality-Sensitive Hashing Does Not Guarantee Privacy! Attacks on Google's FLoC and the MinHash Hierarchy System
Florian Turati, Carlos Cotrini, Karel Kubicek +1
Recently proposed systems aim at achieving privacy using locality-sensitive hashing. We show how these approaches fail by presenting attacks against two such systems: Google's FLoC…
The EMV Standard: Break, Fix, Verify
David Basin, Ralf Sasse, Jorge Toro-Pozo
EMV is the international protocol standard for smartcard payment and is used in over 9 billion cards worldwide. Despite the standard's advertised security, various issues have been…
The Next 700 Policy Miners: A Universal Method for Building Policy Miners
Carlos Cotrini, Luca Corinzia, Thilo Weghorn +1
A myriad of access control policy languages have been and continue to be proposed. The design of policy miners for each such language is a challenging task that has required specia…
Strong and Provably Secure Database Access Control
Marco Guarnieri, Srdjan Marinovic, David Basin
Existing SQL access control mechanisms are extremely limited. Attackers can leak information and escalate their privileges using advanced database features such as views, triggers,…
Cardinality Estimators do not Preserve Privacy
Damien Desfontaines, Andreas Lochbihler, David Basin
Cardinality estimators like HyperLogLog are sketching algorithms that estimate the number of distinct elements in a large multiset. Their use in privacy-sensitive contexts raises t…
Dispute Resolution in Voting
David Basin, Sasa Radomirovic, Lara Schmid
In voting, disputes arise when a voter claims that the voting authority is dishonest and did not correctly process his ballot while the authority claims to have followed the protoc…
IFCIL: An Information Flow Configuration Language for SELinux (Extended Version)
Lorenzo Ceragioli, Letterio Galletta, Pierpaolo Degano +1
Security Enhanced Linux (SELinux) is a security architecture for Linux implementing mandatory access control. It has been used in numerous security-critical contexts ranging from s…
SoK: Delegation and Revocation, the Missing Links in the Web's Chain of Trust
Laurent Chuat, AbdelRahman Abdou, Ralf Sasse +3
The ability to quickly revoke a compromised key is critical to the security of any public-key infrastructure. Regrettably, most traditional certificate revocation schemes suffer fr…
Access Control Synthesis for Physical Spaces
Petar Tsankov, Mohammad Torabi Dashti, David Basin
Access-control requirements for physical spaces, like office buildings and airports, are best formulated from a global viewpoint in terms of system-wide requirements. For example,…
Reduce Once, Verify Many: Verifying Isolation Guarantees via Hierarchical Abstractions
Shabnam Ghasemirad, Christoph Sprenger, Si Liu +1
We present a mathematically rigorous, systematic approach for the verification of database isolation guarantees, which (i) supports a spectrum of seven isolation levels, (ii) uncov…
Sound Verification of Security Protocols: From Design to Interoperable Implementations (extended version)
Linard Arquint, Felix A. Wolf, Joseph Lallemand +5
We provide a framework consisting of tools and metatheorems for the end-to-end verification of security protocols, which bridges the gap between automated protocol verification and…
Reachability Analysis of the Domain Name System
Dhruv Nevatia, Si Liu, David Basin
The high complexity of DNS poses unique challenges for ensuring its security and reliability. Despite continuous advances in DNS testing, monitoring, and verification, protocol-lev…
SOAP: A Social Authentication Protocol
Felix Linker, David Basin
Social authentication has been suggested as a usable authentication ceremony to replace manual key authentication in messaging applications. Using social authentication, chat partn…
Runtime Verification over Out-of-order Streams
David Basin, Felix Klaedtke, Eugen Zalinescu
We present an approach for verifying systems at runtime. Our approach targets distributed systems whose components communicate with monitors over unreliable channels, where message…
FABRID: Flexible Attestation-Based Routing for Inter-Domain Networks
Cyrill Krähenbühl, Marc Wyss, David Basin +3
In its current state, the Internet does not provide end users with transparency and control regarding on-path forwarding devices. In particular, the lack of network device informat…
Secure Deletion on Log-structured File Systems
Joel Reardon, Claudio Marforio, Srdjan Capkun +1
We address the problem of secure data deletion on log-structured file systems. We focus on the YAFFS file system, widely used on Android smartphones. We show that these systems pro…
Securing Databases from Probabilistic Inference
Marco Guarnieri, Srdjan Marinovic, David Basin
Databases can leak confidential information when users combine query results with probabilistic data dependencies and prior knowledge. Current research offers mechanisms that eithe…
Beyond the Finite Variant Property: Extending Symbolic Diffie-Hellman Group Models (Extended Version)
Sofia Giampietro, Ralf Sasse, David Basin
Diffie-Hellman groups are commonly used in cryptographic protocols. While most state-of-the-art, symbolic protocol verifiers support them to some degree, they do not support all ma…
VerIso: Verifiable Isolation Guarantees for Database Transactions
Shabnam Ghasemirad, Si Liu, Christoph Sprenger +2
Isolation bugs, stemming especially from design-level defects, have been repeatedly found in carefully designed and extensively tested production databases over decades. In paralle…
Pushing the Limit: Verified Performance-Optimal Causally-Consistent Database Transactions
Shabnam Ghasemirad, Christoph Sprenger, Si Liu +2
Modern web services crucially rely on high-performance distributed databases, where concurrent transactions are isolated from each other using concurrency control protocols. Relaxe…
Abstract Data Types in Event-B - An Application of Generic Instantiation
David Basin, Andreas Fürst, Thai Son Hoang +2
Integrating formal methods into industrial practice is a challenging task. Often, different kinds of expertise are required within the same development. On the one hand, there are…
Decentralized Privacy-Preserving Proximity Tracing
Carmela Troncoso, Mathias Payer, Jean-Pierre Hubaux +31
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 foundat…