International audience

We systematically scrutinise all the facets of privacy in the 5G delegated-authentication procedure called AKMA (Authentication and Key Management for Applications based on 3GPP credentials in the 5G Systems). We define, in general terms, a privacy-threat model and privacy requirements for this protocol. Using these definitions, we find numerous privacy failings in the AKMA protocol. We propose a patch, called AKMAp, which imposes minimal changes on AKMA, yet it attains all our privacy requirements. We also formalise and analyse all of this in terms of formal privacy-verification in the Dolev-Yao model; to this end, we use the Tamarin prover to systematically carried out our formal analyses of AKMA and AKMAp.

Open and disaggregated O-RAN architectures foster flexibility and vendor diversity in 5G/6G networks but simultaneously expose novel attack surfaces exploitable by sophisticated adversaries. Traditional rule-based or signature-driven detection mechanisms struggle against multi-stage, polymorphic threats in such dynamic environments. This paper proposes TwinGuard, a proactive defence framework that integrates a real-time Digital Twin of a live 5G O-RAN deployment with reinforcement learning (RL) for intelligent threat anticipation and mitigation. Our system mirrors critical KPIs, including throughput, PRB utilisation, SINR, and latency, into the Digital Twin, where an RL agent trained via Proximal Policy Optimisation (PPO) learns optimal mitigation strategies. In our prototype, the RL agent identifies and blocks malicious handover attacks within 100 ms, maintaining service continuity and outperforming a DQN-based baseline. In a second prototype deployed on a containerised OpenAirInterface (OAI) 5G Core and FlexRIC-controlled RAN testbed, our xApp swiftly mitigates an E2 subscription flooding attack in under 100 ms, reducing abnormal PRB utilisation from 95% to nominal levels. TwinGuard demonstrates the feasibility and effectiveness of closed-loop, AI-driven cybersecurity in O-RAN systems, offering a blueprint for future trustworthy and resilient 6G networks.

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.

We introduce a subclass of concurrent game structures (CGS) with imperfect information in which agents are endowed with private data-sharing capabilities. Importantly, our CGSs are such that it is still decidable to model-check these CGSs against a relevant fragment of ATL. These systems can be thought as a generalization of architectures allowing information forks, that is, cases where strategic abilities lead to certain agents outside a coalition privately sharing information with selected agents inside that coalition. Moreover, in our case, in the initial states of the system, we allow information forks from agents outside a given set \(A\) to agents inside this group \(A\) . For this reason, together with the fact that the communication in our models underpins a specialized form of broadcast, we call our formalism \(A\) -cast systems . To underline, the fragment of ATL for which we show the model-checking problem to be decidable over \(A\) -cast is a large and significant one; it expresses coalitions over agents in any subset of the set \(A\) . Indeed, as we show, our systems and this ATL fragments can encode security problems that are notoriously hard to express faithfully: terrorist-fraud attacks in identity schemes.

We define an epistemic logic or logic of knowledge, PL, and a formalism to undertake privacy-centric reasoning in security protocols, over a Dolev-Yao model. We are able to automatically verify all the privacy requirements that are commonplace in security-protocol verification (i.e., strong secrecy, anonymity, various types of unlinkablity including weak unlinkability), as well as privacy notions that are less studied (i.e., privacy regarding lists' membership). Our methodology does not vary with the property: it is uniform no matter the kind of privacy requirement specified and/or verified. We operate in the setting of a bounded number of protocol-sessions. We also implement Phoebe – a proof-of-concept model checker for this methodology. We use Phoebe to check all the aforementioned properties, and we also show-case it on the “benchmark” anonymity and unlinkability requirements of several well-known protocols.

We propose a new approach to the verification of epistemic properties of programmes. 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 a program is executed as well as after is has been 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 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.

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 protocols in the 3GPP-compliant Open5GCore 5G testbed. We also systematically cross-compare standard handovers with our amended handovers using 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.

In this paper, we formally analyse the security of Uptane 2.0 – the latest version11“Latest” is meant at the time of this writing, i.e., in April 2023. 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.

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 sub- scribers and ensure quality of service as per their contracts/plans.

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.

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.

Contactless systems, such as the EMV (Europay, Mastercard and Visa) payment protocol, are vulnerable to relay attacks. The typical countermeasure to this relies on distance 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.

In Mastercard's contactless payment protocol called RRP (Relay Resistant Protocol), the reader is measuring the round-trip times of the message-exchanges between itself and the card, to see if they do not take too long. If they do take longer than expected, a relay attack would be suspected and the transaction should be dropped. A recent paper of Financial Crypto 2019 (FC19) raises some questions w.r.t. this type of relay-protection in contactless payments. Namely, the authors point out that the reader has no incentive to protect against relaying, as it stands to gain from illicit payments. The paper defines the notion of such a rogue reader colluding with a MiM attacker, specifically in the context of contactless payments; the paper dubs this as collusive relaying. Two new protocols, PayBCR and PayCCR, which are closely based on Mastercard's RRP and aim to achieve resistance against collusive relaying, are presented therein. Yet, in the FC19 paper, there is no formal treatment of the collusive-relaying notion or of the security of the protocols. In this paper, we first lift the FC19 notions out of the specifics of RRP-based payments - to the generic case of distance bounding. Thus, we set to answer the wider question of what it would mean to catch if RTT-measuring parties (readers, cards, or others) cheat and collude with proximity-based attackers (i.e., relayers or other types). To this end, we give a new distance-bounding primitive (validated distance-bounding) and two new security notions: strong relaying and strong distance-fraud. We also provide a formal model that, for the first time in distance-bounding, caters for dishonest RTT-measurers. In this model, we prove that the new contactless payments in the FC19 paper, PayBCR and PayCCR attain secuity w.r.t. strong relaying. Finally, we define one other primitive (validated and audited distance-bounding), which, in fact, emulates more closely the PayCCR protocol in the Financial Crypto 2019 paper; this is because, contrary to the line introducing them, we note that PayBCR and PayCCR in fact differ in construction and security guarantees especially in those that go past relaying and into authentication.

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.

The following topics are dealt with: security of data; data privacy; learning (artificial intelligence); telecommunication security; Internet; cryptography; mobile computing; computer network security; authorisation; Internet of Things.

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.

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.

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.

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.

HB+ is a lightweight authentication scheme, which is secure against passive attacks if the Learning Parity with Noise Problem (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.

UC security realized with setup devices imposes that single instances of these setups are used. In most cases, UC-realization relies further on other properties of the setups devices, like tamper-resistance. But what happens in stronger versions of the UC framework, like EUC or JUC, where multiple instances of these setups are allowed? Can we formalise what it is about setups like these which makes them sometimes hinder UC, JUC, EUC realizability?

Abstract From contactless payments to remote car unlocking, many applications are vulnerable to relay attacks. Distance bounding protocols are the main practical countermeasure against these attacks. In this paper, we present a formal analysis of SKI, which recently emerged as the first family of lightweight and provably secure distance bounding protocols. More precisely, we explicate a general formalism for distance-bounding protocols, which lead to this practical and provably secure class of protocols (and it could lead to others). We prove that SKI and its variants are provably secure, even under the real-life setting of noisy communications, against the main types of relay attacks: distance-fraud and generalised versions of mafia- and terrorist-fraud. To attain resistance to terrorist-fraud, we reinforce the idea of using secret sharing, combined with the new notion of a leakage scheme. In view of resistance to generalised mafia-frauds (and terrorist-frauds), we present the notion of circular-keying for pseudorandom functions (PRFs); this notion models the employment of a PRF, with possible linear reuse of the key. We also identify the need of PRF masking to fix common mistakes in existing security proofs/claims. Finally, we enhance our design to guarantee resistance to terrorist-fraud in the presence of noise.

The secrecy problem for security protocols is the problem to decide whether or not a given security protocol has leaky runs. In this paper, the (initial) secrecy problem for bounded protocols with freshness check is shown to be NEXPTIME-complete. Relating the formalism in this paper to the multiset rewriting (MSR) formalism we obtain that the initial secrecy problem for protocols in restricted form, with bounded length messages, bounded existentials, with or without disequality tests, and an intruder with no existentials, is NEXPTIME-complete. If existentials for the intruder are allowed but disequality tests are not allowed, the initial secrecy problem still is NEXPTIME-complete. However, if both existentials for the intruder and disequality tests are allowed and the protocols are not well-founded (and, therefore, not in restricted form), then the problem is undecidable. These results also correct some wrong statements in Durgin et al., JCS 12 (2004), 247–311.