David Basin

Last Name

Basin

First Name

David

ORCID

0000-0003-2952-939X

Organisational unit

03634 - Basin, David / Basin, David

Show all metadata

Search Results

Publications 1 - 10 of 126

AKMA+: Security and Privacy-Enhanced and Standard-Compatible AKMA for 5G Communication
Yang, Yang; Yang, Guomin; Li, Yingjiu; et al. (2025)
Proceedings of the 34th USENIX Conference on Security Symposium
The Authentication and Key Management for Applications (AKMA) protocol is a fundamental building block for security and privacy of 5G cellular networks. Therefore, it is critical that the protocol is free of vulnerabilities that can be exploited by attackers. Unfortunately, based on a detailed analysis of AKMA, we show that AKMA has several vulnerabilities that may lead to security and privacy breaches. We define AKMA+, an enhanced protocol for 5G communication that protects against security and privacy breaches while maintaining compatibility with existing standards. AKMA+ includes countermeasures for protecting communication between the user equipment (UE) and application functions (AFs) from attackers, including those within the home public land mobile network. These countermeasures ensure mutual authentication between the UE and the AKMA anchor function without altering the protocol flow. We also address vulnerabilities related to subscriber and AKMA key identifiers that could be exploited in linkability attacks. By obfuscating this data, AKMA+ prevents attackers from associating a target UE with its past application access. We employ formal verification to demonstrate that AKMA+ achieves key security and privacy objectives. We conduct extensive experiments demonstrating that AKMA+ incurs acceptable computational overhead, bandwidth costs, and UE battery consumption.
A Formal Framework for End-to-End DNS Resolution
Liu, Si; Duan, Huayi; Heimes, Lukas; et al. (2023)
ACM SIGCOMM '23: Proceedings of the ACM SIGCOMM 2023 Conference
Despite the central importance of DNS, numerous attacks and vulnerabilities are regularly discovered. The root of the problem is the ambiguity and tremendous complexity of DNS protocol specifications, amid a rapidly evolving Internet infrastructure. To counteract the vicious break-and-fix cycle for improving DNS infrastructure, we instigate a foundational approach: we construct the first formal semantics of end-to-end name resolution, a collection of components for the formal analyses of both qualitative and quantitative properties, and an automated tool for discovering DoS attacks. Our formal framework represents an important step towards a substantially more secure and reliable DNS infrastructure.
Inducing Authentication Failures to Bypass Credit Card PINs
Basin, David; Schaller, Patrick; Toro Pozo, Jorge Luis (2023)
Proceedings of the 32nd USENIX Security Symposium
For credit card transactions using the EMV standard, the integrity of transaction information is protected cryptographically by the credit card. Integrity checks by the payment terminal use RSA signatures and are part of EMV’s offline data authentication mechanism. Online integrity checks by the card issuer use a keyed MAC. One would expect that failures in either mechanism would always result in transaction failure, but this is not the case as offline authentication failures do not always result in declined transactions. Consequently, the integrity of transaction data that is not protected by the keyed MAC (online) cannot be guaranteed. We show how this missing integrity protection can be exploited to bypass PIN verification for high-value Mastercard transactions. As a proof-of-concept, we have built an Android app that modifies unprotected card-sourced data, including the data relevant for cardholder verification. Using our app, we have tricked real-world terminals into downgrading from PIN verification to either no cardholder verification or (paper) signature verification, for transactions of up to 500 Swiss Francs. Our findings have been disclosed to the vendor with the recommendation to decline any transaction where offline data authentication fails.
A Formally Verified Monitor for Metric First-Order Temporal Logic
Schneider, Joshua; Basin, David; Krstić, Srđan; et al. (2019)
Lecture Notes in Computer Science ~ Runtime Verification
Formalizing and Analyzing Sender Invariance
Hankes Drielsma, Paul; Mödersheim, Sebastian; Viganò, Luca; et al. (2007)
Lecture Notes in Computer Science ~ Formal Aspects in Security and Trust
In many network applications and services, agents that share no secure channel in advance may still wish to communicate securely with each other. In such settings, one often settles for achieving security goals weaker than authentication, such as sender invariance. Informally, sender invariance means that all messages that seem to come from the same source actually do, where the source can perhaps only be identified by a pseudonym. This implies, in particular, that the relevant parts of messages cannot be modified by an intruder. In this paper, we provide the first formal definition of sender invariance as well as a stronger security goal that we call strong sender invariance. We show that both kinds of sender invariance are closely related to, and entailed by, weak authentication, the primary difference being that sender invariance is designed for the context where agents can only be identified pseudonymously. In addition to clarifying how sender invariance and authentication are related, this result shows how a broad class of automated tools can be used for the analysis of sender invariance protocols. As a case study, we describe the analysis of two sender invariance protocols using the OFMC back-end of the AVISPA Tool.
Real-Time Policy Enforcement with Metric First-Order Temporal Logic
Hublet, François; Basin, David; Krstić, Srđan (2022)
Lecture Notes in Computer Science ~ Computer Security – ESORICS 2022
Correctness and regulatory compliance of today’s software systems are crucial for our safety and security. This can be achieved with policy enforcement: the process of monitoring and possibly modifying system behavior to satisfy a given policy. The enforcer’s capabilities determine which policies are enforceable. We study the enforceability of policies specified in metric first-order temporal logic (MFOTL) with enforcers that can cause and suppress different system actions in real time. We consider an expressive safety fragment of MFOTL and show that a policy from that fragment is enforceable if and only if it is equivalent to a policy in a simpler, syntactically defined MFOTL fragment. We then propose an enforcement algorithm for all monitorable policies from the latter fragment, and show that our EnfPoly enforcer outperforms state-of-the-art tools.
Semantic Vacuity
Petric Maretić, Grgur; Torabi Dashti, Mohammad; Basin, David (2015)
2015 22nd International Symposium on Temporal Representation and Reasoning (TIME)
The vacuous satisfaction of a temporal formula with respect to a model has been extensively studied in the literature. Although a universally accepted definition of vacuity does not yet exist, all existing proposals generalize, in one way or another, the antecedent failure of an implication to the syntax of a temporal logic. They are therefore syntactic: whether a model vacuously satisfies a formula is affected by semantics-preserving changes to the formula. This leads to inconsistent and counter-intuitive results. We propose an alternative: a semantic definition of vacuity for LTL where either two semantically equivalent LTL formulas are both satisfied vacuously in a model, or neither of them are. Our definition is based on a syntactic-invariant separation of LTL formulas, which gives rise to an algorithm for detecting semantic vacuity using trap properties. We also propose an alternative algorithm for Buchi automata, which can be used to detect the vacuous satisfaction of omega-regular properties as well as LTL formulas. We analyze this algorithm's worst-case complexity and, using real-world examples, demonstrate that semantic vacuity can be efficiently decided in practice.
Sound Verification of Security Protocols: From Design to Interoperable Implementations
Arquint, Linard; Wolf, Felix; Lallemand, Joseph; et al. (2023)
2023 IEEE Symposium on Security and Privacy (SP)
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 code-level proofs. We automatically translate a Tamarin protocol model into a set of I/O specifications expressed in separation logic. Each such specification describes a protocol role's intended I/O behavior against which the role's implementation is then verified. Our soundness result guarantees that the verified implementation inherits all security (trace) properties proved for the Tamarin model. Our framework thus enables us to leverage the substantial body of prior verification work in Tamarin to verify new and existing implementations. The possibility to use any separation logic code verifier provides flexibility regarding the target language. To validate our approach and show that it scales to realworld protocols, we verify a substantial part of the official Go implementation of the WireGuard VPN key exchange protocol.
Mechanizing Privacy by Design
Basin, David; Hublet, François; Krstić, Srđan; et al. (2025)
CCS '25: Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security
Privacy by design requires integrating data protection into systems from the outset, during their design, rather than building it in later. Related legislation does not specify how to achieve this and mainstream languages and frameworks lack support for privacy by design. To address this long-standing problem, we have developed diferent, effective technical solutions. First, we have developed powerful logic-based tools that enforce formal data protection policies at runtime by controlling relevant system actions. Second, we have proposed methods and tools for integrating privacy models into system design models, enabling model-driven privacy enforcement. We report on our methods, tools, and practical experiences using them
Looping for Good: Cyclic Proofs for Security Protocols
Linker, Felix Emanuel; Sprenger, Christoph; Cremers, Cas; et al. (2025)
CCS '25: Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security
Security protocols often involve loops, such as for ratcheting or for manipulating inductively-defined data structures. However, the automated analysis of security protocols has struggled to keep up with these features. The state-of-the-art often necessitates working with abstractions of such data structures or relies heavily on auxiliary, user-defined lemmas. In this work, we advance the state-of-the-art in symbolic protocol verification by adapting cyclic induction proof systems to the security protocol domain. We introduce reasoning rules for the Tamarin prover for cyclic proofs, enabling new, compact proofs, and we prove their soundness. Moreover, we implement new, simple, and effective proof search strategies that leverage these rules. With these additions, Tamarin can prove many lemmas that previously required, often complex, auxiliary lemmas. We showcase our approach on fourteen case studies, ranging from toy examples to a detailed model of the Signal protocol. Our work opens an exciting new research area where automatic induction helps scale security protocol verification, as we provide a fundamentally new and general induction mechanism

Publications 1 - 10 of 126

David Basin

Last Name

First Name

ORCID

Organisational unit

Filters

Search Results