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.

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 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.

Swarm attestation protocols extend remote attestation by allowing a verifier to efficiently measure the integrity of software code running on a collection of heterogeneous devices across a network. Many swarm attestation protocols have been proposed for a variety of system configurations. However, these protocols are currently missing explicit specifications of the properties guaranteed by the protocol and formal proofs of correctness. In this paper, we address this gap in the context of list swarm attestation protocols, a category of swarm attestation protocols that allow a verifier to identify the set of healthy provers in a swarm. We describe the security requirements of swarm attestation protocols. We focus our work on the SIMPLE+ protocol, which we model and verify using the Tamarin prover. Our proofs enable us to identify two variations of SIMPLE+: (1) we remove one of the keys used by SIMPLE+ without compromising security, and (2) we develop a more robust design that increases the resilience of the swarm to device compromise. Using Tamarin, we demonstrate that both modifications preserve the desired security properties.

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.

Users accessing services are often required to provide personal information, for example, age, profession and location, in order to satisfy access polices. This personal information is evident in the application of e-ticketing where discounted access is granted to visitor attractions or transport services if users satisfy policies related to their age or disability or other defined over attributes. We propose a privacy-preserving electronic ticket scheme using attribute-based credentials to protect users' privacy. The benefit of our scheme is that the attributes of a user are certified by a trusted third party so that the scheme can provide assurances to a seller that a user's attributes are valid. The scheme makes the following contributions: (1) users can buy different tickets from ticket sellers without releasing their exact attributes; (2) two tickets of the same user cannot be linked; (3) a ticket cannot be transferred to another user; (4) a ticket cannot be double spent. The novelty of our scheme is to enable users to convince ticket sellers that their attributes satisfy the ticket policies and buy discounted tickets anonymously. This is a step towards identifying an e-ticketing scheme that captures user privacy requirements in transport services. The security of our scheme is proved and reduced to a well-known complexity assumption. The scheme is also implemented and its performance is empirically evaluated.

Direct Anonymous Attestation (Daa) is a set of cryptographic schemes used to create anonymous digital signatures. To provide additional assurance, Daa schemes can utilise a Trusted Platform Module (Tpm) that is a tamper-resistant hardware device embedded in a computing platform and which provides cryptographic primitives and secure storage. We extend Chen and Li's Daa scheme to support: 1) signing a message anonymously, 2) self-certifying Tpm keys, and 3) ascertaining a platform's state as recorded by the Tpm's platform configuration registers (PCR) for remote attestation, with explicit reference to Tpm2.0 API calls. We perform a formal analysis of the scheme and are the first symbolic models to explicitly include the low-level Tpm call details. Our analysis reveals that a fix pro-posed by Whitefield et al. to address an authentication attack on an Ecc-Daa scheme is also required by our scheme. Developing a fine-grained, formal model of a Daa scheme contributes to the growing body of work demonstrating the use of formal tools in supporting security analyses of cryptographic protocols. We additionally provide and benchmark an open-source C++implementation of this Daa scheme supporting both a hardware and a software Tpm and measure its performance.

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.

An anonymous single sign-on (ASSO) scheme allows users to access multiple services anonymously using one credential. We propose a new ASSO scheme, where users can access services anonymously through the use of anonymous credentials and unlinkably through the provision of designated verifiers. Notably, verifiers cannot link a user's service requests even if they collude. The novelty is that when a designated verifier is unavailable, a central authority can authorize new verifiers to authenticate the user on behalf of the original verifier. Furthermore, a central verifier can also be authorized to de-anonymize users and trace their service requests. We formalize the scheme along with a security proof and provide an empirical evaluation of its performance. This scheme can be applied to smart ticketing where minimizing the collection of personal information of users is increasingly important to transport organizations due to privacy regulations such as general data protection regulations (GDPRs).

Direct Anonymous Attestation (DAA) is a cryptographic scheme that provides Trusted Platform Module TPM-backed anonymous credentials. We develop Tamarin modelling of the ECC-based version of the protocol as it is standardised and provide the first mechanised analysis of this standard. Our analysis confirms that the scheme is secure when all TPMs are assumed honest, but reveals a break in the protocol's expected authentication and secrecy properties for all TPMs even if only one is compromised. We propose and formally verify a minimal fix to the standard. In addition to developing the first formal analysis of ECC-DAA, the paper contributes to the growing body of work demonstrating the use of formal tools in supporting standardisation processes for cryptographic protocols.

The Deletion-Insertion Correcting Code construction proposed by Davey and MacKay consists of an inner code that recovers synchronization and an outer code that provides substitution error protection. The inner code uses low-weight codewords which are added (modulo two) to a pilot sequence. The receiver is able to synchronise on the pilot sequence in spite of the changes introduced by the added codeword. The original bit-level formulation of the inner decoder assumes that all bits in the sparse codebook are identically and independently distributed. Not only is this assumption inaccurate, but it also prevents the use of soft a- priori input to the decoder. We propose an alternative symbol-level inner decoding algorithm that takes the actual codebook into account. Simulation results show that the proposed algorithm has an improved performance with only a small penalty in complexity, and it allows other improvements using inner codes with larger minimum distance.

We determine the automorphism group of various Goppa codes /spl Cscr//sub L/(D,G) associated with certain function fields F/F/sub q/ of genus g>0. It is well known that, for deg D=n>2g+2, the automorphism group {Aut/sub D,G/(F/F/sub q/) can be embedded into Aut(/spl Cscr//sub L/(D,G)) as a subgroup. We show that, under certain conditions on the divisors D and G Aut/sub D,G/(F/F/sub q/) is actually isomorphic to Aut(/spl Cscr//sub L/(D,G)).