Dr Steve Wesemeyer

Research on vehicular networking (V2X) security has produced a range of security mechanisms and protocols tailored for this domain, addressing both security and privacy. Typically, the security analysis of these proposals has largely been informal. However, formal analysis can be used to expose flaws and ultimately provide a higher level of assurance in the protocols. This paper focusses on the formal analysis of a particular element of security mechanisms for V2X found in many proposals, that is the revocation of malicious or misbehaving vehicles from the V2X system by invalidating their credentials. This revocation needs to be performed in an unlinkable way for vehicle privacy even in the context of vehicles regularly changing their pseudonyms. The Rewire scheme by Förster et al. and its subschemes Plain and R-token aim to solve this challenge by means of cryptographic solutions and trusted hardware. Formal analysis using the Tamarin prover identifies two flaws: one previously reported in the literature concerned with functional correctness of the protocol, and one previously unknown flaw concerning an authentication property of the R-token scheme. In response to these flaws we propose Obscure Token (O-token), an extension of Rewire to enable revocation in a privacy preserving manner. Our approach addresses the functional and authentication properties by introducing an additional key-pair, which offers a stronger and verifiable guarantee of successful revocation of vehicles without resolving the long-term identity. Moreover O-token is the first V2X revocation protocol to be co-designed with a formal model.

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.

Anonymous Single-Sign-On authentication schemes have been proposed to allow users to access a service protected by a verifier without revealing their identity. This has become more important with the introduction of strong privacy regulations. In this paper we describe a new approach whereby anonymous authentication to different verifiers is achieved via authorisation tags and pseudonyms. The particular innovation of our scheme is that authentication can occur only between a user and its designated verifier for a service, and the verification cannot be performed by any other verifier. The benefit of this authentication approach is that it prevents information leakage of a user's service access information, even if the verifiers for these services collude. Our scheme also supports a trusted third party who is authorised to de-anonymise the user and reveal her whole service access information if required. Furthermore, our scheme is lightweight because it does not rely on attribute or policy-based signature schemes to enable access to multiple services. The scheme's security model is given together with a security proof, an implementation and a performance evaluation.

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.

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.

Near field communication (NFC) is a standard-based, radio frequency (RF), wireless communication technology that allows data to be exchanged between devices that are less than 20 cm apart. NFC security protocols require formal security analysis before massive adoptions, in order to check whether these protocols meet its requirements and goals. In this paper we formally analyse NFC-based mobile coupon protocols using formal methods (Casper/FDR). We find an attack against the advanced protocol, and then we provide a solution that addresses the vulnerability formally.

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 Tpm 2.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 proposed by Whitefield et al. to address an authentication attack on an Ecc-Daa scheme is also required by our scheme. Developing a finegrained, 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.

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

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.