Professor Ioana Boureanu (Carlson)

— In this paper, we formally analyse the security of Uptane 2.0 – the latest version 1 of a framework for over-the-air (online) delivery of software to cars. We are doing so by using the threat model and security requirements found in standard document that accompanies Uptane 2.0, as well as a modulation of this threat model and requirements added by ourselves, for a deeper analysis. To undertake this verification, we use the well-known formal protocol-verifier and theorem prover called Tamarin. We discuss our responsible disclosure to and work with the Uptane Alliance.

The Transport Layer Security (TLS) protocol is designed to allow two parties, a client and a server, to communicate securely over an insecure network. However, when TLS connections are proxied through an intermediate middlebox, like a Content Delivery Network (CDN), the standard endto- end security guarantees of the protocol no longer apply. In this paper, we investigate the security guarantees provided by Keyless SSL, a CDN architecture currently deployed by CloudFlare that composes two TLS 1.2 handshakes to obtain a proxied TLS connection. We demonstrate new attacks that show that Keyless SSL does not meet its intended security goals. These attacks have been reported to CloudFlare and we are in the process of discussing fixes. We argue that proxied TLS handshakes require a new, stronger, 3-party security definition. We present 3(S)ACCEsecurity, a generalization of the 2-party ACCE security definition that has been used in several previous proofs for TLS. We modify Keyless SSL and prove that our modifications guarantee 3(S)ACCE-security, assuming ACCE-security for the individual TLS 1.2 connections. We also propose a new design for Keyless TLS 1.3 and prove that it achieves 3(S)ACCEsecurity, assuming that the TLS 1.3 handshake implements an authenticated 2-party key exchange. Notably, we show that secure proxying in Keyless TLS 1.3 is computationally lighter and requires simpler assumptions on the certificate infrastructure than our proposed fix for Keyless SSL. Our results indicate that proxied TLS architectures, as currently used by a number of CDNs, may be vulnerable to subtle attacks and deserve close attention.

Contactless systems, such as the EMV (Europay, Mastercard and Visa) payment protocol, are vulnerable to relay attacks. The typical countermeasure to this relies ondistance bounding protocols, in which a reader estimates an upper bound on its physical distance from a card by doing round-trip time (RTT) measurements. However, these protocols are trivially broken in the presence of rogue readers. At Financial Crypto 2019, we proposed two novel EMV-based relay-resistant protocols: they integrate distance-bounding with the use of hardware roots of trust (HWRoT) in such a way that correct RTT-measurements can no longer be bypassed. Our contributions are threefold: first, we design a calculus to model this advanced type of distance-bounding protocols integrated with HWRoT; as an additional novelty, our calculus is also the first to allow for mobility of cards and readers during a proximity-checking phase. Second, to make it possible to analyse these protocols via more standard mechanisms and tools, we consider a 2018 characterisation of distance-bounding security that does away with physical aspects and relies only on the causality of events; we cast it in our richer calculus and extend its theoretical guarantees to our more expressive models (with mobility, potentially rogue readers, and HWRoT). Due to this extension, we can carry out the security analysis in the standard protocol verification tool ProVerif. Third, we provide the first implementation of Mastercard's relay-resistant EMV protocol PayPass-RRP as well as one of its 2019 extension with HWRoT called PayBCR. We evaluate their efficiency and their robustness to relay attacks, in presence of both honest and rogue readers. Our experiments are the first to show that Mastercard's PayPass-RRP and its HWRoT-based extension PayBCR are both practical in preventing relay attacks of the magnitude shown thusfar in EMV.

We introduce a framework for the symbolic verification of epistemic properties of programs expressed in a class of general-purpose programming languages. To this end, we reduce the verification problem to that of satisfiability of first-order formulae in appropriate theories. We prove the correctness of our reduction and we validate our proposal by applying it to two examples: the dining cryptographers problem and the ThreeBallot voting protocol. We put forward an implementation using existing solvers, and report experimental results showing that the approach can perform better than state-of-the-art symbolic model checkers for temporal-epistemic logic.

This book constitutes the refereed post-conference proceedings of the Interdisciplinary Workshop on Trust, Identity, Privacy, and Security in the Digital Economy, DETIPS 2020; the First International Workshop on Dependability and Safety of Emerging Cloud and Fog Systems, DeSECSys 2020; Third International Workshop on Multimedia Privacy and Security, MPS 2020; and the Second Workshop on Security, Privacy, Organizations, and Systems Engineering, SPOSE 2020; held in Guildford, UK, in September 2020, in conjunction with the 25th European Symposium on Research in Computer Security, ESORICS 2020.A total of 42 papers was submitted. For the DETIPS Workshop 8 regular papers were selected for presentation. Topics of interest address various aspect of the core areas in relation to digital economy.For the DeSECSys Workshop 4 regular papers are included. The workshop had the objective of fostering collaboration and discussion among cyber-security researchers and practitioners to discuss the various facets and trade-o s of cyber security. In particular, applications, opportunities and possible shortcomings of novel security technologies and their integration in emerging application domains.For the MPS Workshop 4 regular papers are presented which cover topics related to the security and privacy of multimedia systems of Internet-based video conferencing systems (e.g., Zoom, Microsoft Teams, Google Meet), online chatrooms (e.g., Slack), as well as other services to support telework capabilities.For the SPOSE Workshop 3 full papers were accepted for publication. They reflect the discussion, exchange, and development of ideas and questions regarding the design and engineering of technical security and privacy mechanisms with particular reference to organizational contexts.

Whilst proximity-checking mechanisms are on the rise, proximity-based attacks other than relaying have not been studied from a practical viewpoint, not even in academia. Are the simplest proximity-based attacks, namely distance frauds, a practical danger? Can an attacker make it look like they are here and there at the same time? In this paper, we first distinguish “credible” vs. impractical distance frauds, in a quantifiable, formal manner. Second, we implement two “credible” distance frauds on off-the-shelf NFC-enabled Android phones. We present an initial evaluation focused on their feasibility.

Distance-bounding protocols were introduced in 1993 as a countermeasure to relay attacks, in which an adversary fraudulently forwards the communication between a verifier and a distant prover. In the more than 40 different protocols that followed, assumptions were taken on the structure of distance-bounding protocols and their threat models. In this paper, we survey works disrupting these assumptions, and discuss the remaining challenges.

We define and formalise a generic cryptographic construction that underpins coupling of companion devices, e.g., biometrics-enabled devices, with main devices(e.g., PCs), in a user-aware manner, mainly for on-demand authentication and secure storage for applications running on the main device. We define the security requirements of such constructions, provide a full instantiation in a protocol-suite and prove its computational as well as Dolev-Yao security. Finally, we implement our protocol suite and one password-manager use-case

LoRaWAN (Low-power Wide-Area Networks) is the main specification for application-level IoT (Internet of Things). The current version, published in October 2017, is LoRaWAN 1.1, with its 1.0 precursor still being the main specification supported by commercial devices such as PyCom LoRa transceivers. Prior (semi)-formal investigations into the security of the LoRaWAN protocols are scarce, especially for Lo-RaWAN 1.1. Moreover, amongst these few, the current encodings [4], [9] of LoRaWAN into verification tools unfortunately rely on much-simplified versions of the LoRaWAN protocols, undermining the relevance of the results in practice. In this paper, we fill in some of these gaps. Whilst we briefly discuss the most recent cryptographic-orientated works [5] that looked at LoRaWAN 1.1, our true focus is on producing formal analyses of the security and correctness of LoRaWAN, mechanised inside automated tools. To this end, we use the state-of-the-art prover, Tamarin. Importantly, our Tamarin models are a faithful and precise rendering of the LoRaWAN specifications. For example, we model the bespoke nonce-generation mechanisms newly introduced in LoRaWAN 1.1, as well as the "classical" but shortdomain nonces in LoRaWAN 1.0 and make recommendations regarding these. Whilst we include small parts on device-commissioning and application-level traffic, we primarily scrutinise the Join Procedure of LoRaWAN, and focus on version 1.1 of the specification, but also include an analysis of Lo-RaWAN 1.0. To this end, we consider three increasingly strong threat models, resting on a Dolev-Yao attacker acting modulo different requirements made on various channels (e.g., secure/insecure) and the level of trust placed on entities (e.g., honest/corruptible network servers). Importantly, one of these threat models is exactly in line with the LoRaWAN specification, yet it unfortunately still leads to attacks. In response to the exhibited attacks, we propose a minimal patch of the LoRaWAN 1.1 Join Procedure, which is as backwards-compatible as possible with the current version. We analyse and prove this patch secure in the strongest threat model mentioned above. This work has been responsibly disclosed to the LoRa Alliance, and we are liaising with the Security Working Group of the LoRa Alliance, in order to improve the clarity of the LoRaWAN 1.1 specifications in light of our findings, but also by using formal analysis as part of a feedback-loop of future and current specification writing.

We give a general-purpose programming language in which programs can reason about their own knowledge. To specify what these intelligent programs know, we define a " program epistemic " logic, akin to a dynamic epistemic logic for programs. Our logic properties are complex , including programs introspecting into future state of affairs, i.e., reasoning now about facts that hold only after they and other threads will execute. To model aspects anchored in privacy, our logic is interpreted over partial observability of variables, thus capturing that each thread can " see " only a part of the global space of variables. We verify program-epistemic properties on such AI-centred programs. To this end, we give a sound translation of the validity of our program-epistemic logic into first-order validity, using a new weakest-precondition semantics and a book-keeping of variable assignment. We implement our translation and fully automate our verification method for well-established examples using SMT solvers.

Relay attackers can forward messages between a contactless EMV bank card and a shop reader, making it possible to wirelessly pickpocket money. To protect against this, Apple Pay requires a user's fingerprint or Face ID to authorise payments, while Mastercard and Visa have proposed protocols to stop such relay attacks. We investigate transport payment modes and find that we can build on relaying to bypass the Apple Pay lock screen, and illicitly pay from a locked iPhone to any EMV reader, for any amount, without user authorisation. We show that Visa's proposed relay-countermeasure can be bypassed using rooted smart phones. We analyse Mastercard's relay protection, and show that its timing bounds could be more reliably imposed at the ISO 14443 protocol level, rather than at the EMV protocol level. With these insights, we propose a new relay-resistance protocol (L1RP) for EMV. We use the Tamarin prover to model mobile-phone payments with and without user authentication, and in different payment modes. We formally verify solutions to our attack suggested by Apple and Visa, and used by Samsung, and we verify that our proposed protocol provides protection from relay attacks.

We introduce a new framework, TrackDev, for encoding and analysing what we call the “tracking” of an entity via its executions of a protocol or its usages of a system. TrackDev considers multiple dimensions combined: whether the attacker is active or passive, whether an entity is trackable in its every single appearance on the network or just in a compound set thereof, and whether the entity can be explicitly or implicitly identified. TrackDev can be applied to most identification-based systems, and, interestingly, in practice, i.e., over actual executions of systems. To this end, we test TrackDev on real-life traffic for two well-known protocols, the LoRaWAN Join and 5G handovers, showing new trackability/privacy attacks on these and proposing countermeasures. We study the strength of TrackDev’s various trackability properties and show that many of our notions are incomparable amongst each other, thus justifying the fine-grained nature of TrackDev. Finally, we detail how the main thrust of TrackDev can be mechanised in formal-verification tools. We exemplify this fully on the LoRaWAN Join, in the Tamarin prover. We also uncover and discuss within two important aspects: (a) TrackDev’s separation between “explicit” and “implicit” trackability offers new formal-verification insights; (b) our analyses of the LoRaWAN Join protocol in Tamarin against TrackDev’s privacy notions, as well as against existing approximations of unlinkability by Baelde et al., concretely show that the latter approximations can be coarser than our notions.

We propose a new approach to the verification of epis-temic properties of programs. First, we introduce the new " program-epistemic " logic L PK , which is strictly richer and more general than similar formalisms appearing in the literature. To solve the verification problem in an efficient way, we introduce a translation from our language L PK into first-order logic. Then, we show and prove correct a reduction from the model checking problem for program-epistemic formulas to the satisfiability of their first-order translation. Both our logic and our translation can handle richer specification w.r.t. the state of the art, allowing us to express the knowledge of agents about facts pertaining to programs (i.e., agents' knowledge before and after a program is executed). Furthermore, we implement our translation in Haskell in a general way (i.e., independently of the programs in the logical statements), and we use existing SMT-solvers to check satisfaction of L PK formulas on a benchmark example in the AI/agency field.

We introduce a new framework, TrackDev, for encoding and analysing the tracing or "tracking" of an entity (e.g., a device) via its executions of a protocol or its usages of a system. TrackDev considers multiple dimensions combined: whether the attacker is active or passive, whether an entity is trackable in its every single appearances or just in a compound set thereof, and whether the entity can be explicitly or implicitly identified. TrackDev can be applied to most identification-based systems. TrackDev is to be applied in practice, over actual executions of systems; to this end, we test TrackDev on real-life traffic for two well-known protocols, the LoRaWAN Join and the 5G handovers, showing new trackability attacks therein and proposing countermeasures. We study the strength of TrackDev's various trackability properties and show that many of our notions are incomparable amongst each other, thus justifying the fine-grained nature of TrackDev. Finally, we detail how the main thrust of TrackDev can be mechanised in formal-verification tools, without any loss; we exemplify this fully on the LoRaWAN Join, in the Tamarin prover. In this process, we also uncover and discuss within two important aspects: (a) TrackDev’s separation between "explicit" and "implicit" trackability offers new formal-verification insights; (b) our analyses of the LoRaWAN Join protocol in Tamarin against TrackDev as well as against existing approximations of unlinkability by Baelde et al. concretely show that the latter approximations can be coarser than our notions.

Post-Compromise Security (PCS) is a property of secure-channel establishment schemes, which limits the security breach of an adversary that has compromised one of the end-point to a certain number of messages, after which the channel heals. An attractive property, especially in view of Snowden's revelation of mass-surveillance, PCS features in prominent messaging protocols such as Signal. In this paper, we introduce a framework for quantifying and comparing PCS security, with respect to a broad taxonomy of adversaries. The generality and flexibility of our approach allows us to model the healing speed of a broad class of protocols, including Signal, but also an identity-based messaging protocol named SAID, and even a composition of 5G handover protocols. We also apply the results obtained for this latter example in order to provide a quick fix, which massively improves its post-compromise security.

Much of Internet traffic nowadays passes through active proxies, whose role is to inspect, filter, cache, or transform data exchanged between two endpoints. To perform their tasks, such proxies modify channel-securing protocols, like TLS, resulting in serious vulnerabilities. Such problems are exacerbated by the fact that middleboxes are often invisible to one or both endpoints, leading to a lack of accountability. A recent protocol, called mcTLS, pioneered accountability for proxies, which are authorized by the endpoints and given limited read/write permissions to application traffic. Unfortunately, we show that mcTLS is insecure: the protocol modifies the TLS protocol, exposing it to a new class of middlebox-confusion attacks. Such attacks went unnoticed mainly because mcTLS lacked a formal analysis and security proofs. Hence, our second contribution is to formalize the goal of accountable proxying over secure channels. Third, we propose a provably-secure alternative to soon-to-be-standardized mcTLS: a generic and modular protocol-design that care- fully composes generic secure channel-establishment protocols, which we prove secure. Finally, we present a proof-of-concept implementation of our design, instantiated with unmodified TLS 1.3, and evaluate its overheads.

HB+ is a lightweight authentication scheme, which is secure against passive attacks if the Learning Parity with Noise Prob- lem (LPN) is hard. However, HB+ is vulnerable to a key- recovery, man-in-the-middle (MiM) attack dubbed GRS. The HB+DB protocol added a distance-bounding dimension to HB+, and was experimentally proven to resist the GRS attack. We exhibit several security flaws in HB+DB. First, we refine the GRS strategy to induce a different key-recovery MiM attack, not deterred by HB+DB's distance bounding. Second, we prove HB+DB impractical as a secure distance-bounding (DB) protocol, as its DB security-levels scale poorly compared to other DB protocols. Third, we refute that HB+DB's security against passive attackers relies on the hardness of LPN; more-over, (erroneously) requiring such hardness lowers HB+DB's efficiency and security. We also propose a new distance-bounding protocol called BLOG. It retains parts of HB+DB, yet BLOG is provably secure and enjoys better (asymptotical) security.

By design, TLS (Transport Layer Security) is a 2- party, end-to-end protocol. Yet, in practice, TLS delegation is often deployed: that is, middlebox proxies inspect and even modify TLS traffic between the endpoints. Recently, industry-leaders (e.g., Akamai, Cloudflare, Telefonica, Ericcson), standardization bodies (e.g., IETF, ETSI), and academic researchers have pro-posed numerous ways of achieving safer TLS delegation. We present LURK the LURK (Limited Use of Remote Keys) extension for TLS 1.2, a suite of designs for TLS delegation, where the TLS-server is aware of the middlebox. We implement and test LURK. We also cryptographically prove and formally verify, in Proverif, the security of LURK. Finally, we comprehensively analyze how our designs balance (provable) security and competitive performance.

In relay attacks, a man-in-the-middle adversary impersonates a legitimate party and makes it this party appear to be of an authenticator, when in fact they are not. In order to counteract relay attacks, distance-bounding protocols provide a means for a verifier (e.g., an payment terminal) to estimate his relative distance to a prover (e.g., a bankcard). We propose FlexiDB, a new cryptographic model for distance bounding, parameterised by different types of fine-grained corruptions. FlexiDB allows to consider classical cases but also new, generalised corruption settings. In these settings, we exhibit new attack strategies on existing protocols. Finally, we propose a proof-of-concept mechanisation of FlexiDB in the interactive cryptographic prover EasyCrypt. We use this to exhibit a flavour of man-in-the-middle security on a variant of MasterCard's contactless-payment protocol.

It is possible to relay signals between a contactless EMV card and a shop's EMV reader and so make a fraudulent payment without the card-owner's knowledge. Existing countermeasures rely on proximity checking: the reader will measure round trip times in message-exchanges, and will reject replies that take longer than expected (which suggests they have been relayed). However, it is the reader that would receive the illicit payment from any relayed transaction, so a rogue reader has little incentive to enforce the required checks. Furthermore, cases of malware targeting point-of-sales systems are common. We propose three novel proximity-checking protocols that use a trusted platform module (TPM) to ensure that the reader performs the time-measurements correctly. After running one of our proposed protocols, the bank can be sure that the card and reader were in close proximity, even if the reader tries to subvert the protocol. Our first protocol makes changes to the cards and readers, our second modifies the readers and the banking backend, and our third allows the detection of relay attacks, after they have happened, with only changes to the readers.

We study the problem of analysing the security for an unbounded number of concurrent sessions of a cryptographic protocol. Our formal model accounts for an arbitrary number of agents involved in a protocol-exchange which is subverted by a Dolev-Yao attacker. We define the parameterised model checking problem with respect to security requirements expressed in temporal-epistemic logics. We formulate sufficient conditions for solving this problem, by analysing several finite models of the system. We primarily explore authentication and key-establishment as part of a larger class of protocols and security requirements amenable to our methodology. We introduce a tool implementing the technique, and we validate it by verifying the NSPK and ASRPC protocols.

Welcome to the 2023 ACM Conference on Security and Privacy in Wireless and Mobile Networks (ACM WiSec)! Now in its 16th year, WiSec continues to be the premier venue for research on all aspects of security and privacy in wireless and mobile networks, their systems, and their applications. We are hosted by the Surrey Centre for Cyber Security on the beautiful campus of the University of Surrey in Guildford, UK. We begin our exciting three-day main conference program on May 29th with single-track technical paper sessions, a poster and demo session, two excellent keynotes from cellular experts Prof. Yongdae Kim (KAIST) and David Rogers (GSMA Fraud and Security Group), and a panel on "Academic and Industry Views of Cellular Security Research." The WiseML Workshop follows the main program on June 1st. We invite participants to attend the exciting paper presentations and keynotes, interact with the presenters during the Q&A sessions after each talk, network during the coffee breaks and lunches each day, and socialize during the combined reception/poster/demo session and the banquet dinner. We will make talk recordings available to the public after the conference. This year's technical program features 34 outstanding papers: 27 full papers, 5 short papers, and 2 SoK papers. We also have 5 posters and 3 demonstrations of early results and working prototypes. The technical program covers a wide range of security and privacy issues related to IoT security, cellular communication security, wireless technologies (e.g., Wi-Fi), application of cryptographic protocols, authentication, applications using machine learning for identity verification, machine learning for security, and machine learning for privacy.

In mobile networks, the User Equipment (UE) secures some of the communication with its serving Radio Access Network (RAN) node ("base station") via a set of keys known as Access Stratum (AS) keys. Unfortunately, the level of secrecy of these keys varies with the mobile procedures re-establishing them. To improve the secrecy of the AS keys, we propose minimal changes to 5G & 4G handovers, i.e., the main AS-key establishment procedures. We show the minimality of our changes also via an implementation of one of our protocol in the 3GPP-compliant Open5GCore 5G testbed. We also cross-compare standard handovers with our amended handovers, systematically via MobTrustCom: a framework to quantify especially trust but also communication complexity in mobile networks. Moreover, we use Tamarin, a formal security-protocol verification tool, to prove no loss of "classical" security yet an increase in AS-keys' secrecy brought by our improvements to handovers.

We formally analyse the security of each 5G authenticated key-establisment (AKE) procedures: the 5G registration, the 5G authentication and key agreement (AKA) and 5G handovers. We also study the security of their composition, which we call the 5GAKE_stack. Our security analysis focuses on aspects of multi-party AKEs that occur in the 5GAKE_stack. We also look at the consequences this AKE (in)security has over critical mobile-networks' objects such as the Protocol Data Unit (PDU) sessions, which are used to bill subscribers and ensure quality of service as per their contracts/plans. In our assessments, we augment the standard Dolev-Yao model with different levels of trust and threat by considering honest, honest-but-curious, as well as completely rogue radio nodes. We formally prove security in the first case, and insecurity in the latter two as well as making formal recommendations on this. We carry out our formal analysis using the Tamarin-Prover. Lastly, we also present an emulator of the 5GAKE_stack. This can be a useful "5G API"-like tool for the community to experiment with the 5GAKE_stack, since the 5G networks are not yet fully deployed and mobile networks are proprietary and closed "loops".

Distance bounding protocols allow a verifier to both authenticate a prover and evaluate whether the latter is located in his vicinity. These protocols are of particular interest in contactless systems, e.g., electronic payment or access control systems, which are vulnerable to distance-based frauds. This survey analyzes and compares in a unified manner many existing distance bounding protocols with respect to several key security and complexity features.

It is possible to relay signals between a contactless EMV card and a shop’s EMV reader and so make a fraudulent payment without the card-owner’s knowledge. Existing countermeasures rely on proximity checking: the reader will measure round trip times in message-exchanges, and rejects replies that take longer than expected (which suggests they have been relayed). However, it is the reader that would receive the illicit payment from any relayed transaction, so a rogue reader has little incentive to enforce the required checks. Furthermore, cases of malware targeting point-of-sales systems are common.We propose three novel proximity-checking protocols that use a trusted platform module (TPM) to ensure that the reader performs the time measurements correctly. After running one of our proposed protocols, the bank can be sure that the card and reader were in close proximity, even if the reader tries to subvert the protocol. Our first protocol makes changes to the cards and readers, our second protocol modifies the readers and the banking backend, and our third protocol allows the detection of relay attacks, after they have happened, with only changes to the readers.