Dr Christopher J P Newton

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.

We formally analyse the security of each 5G authenticated key-establisment (AKE) procedures: the 5G registration, the 5G authen-tication 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 ". CCS CONCEPTS • Security and privacy → Formal security models.

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.

Passwords are the de facto standard for authentication despite their significant weaknesses. While businesses are currently focused on implementing multi-factor authentication to provide greater security, user adoption is still low. An alternative, WebAuthn, uses cryptographic key pairs to provide password-less authentication. WebAuthn has been standardised and is resilient to phishing attacks. However, its adoption is also very low; the barriers to adoption include usability and resilience of keys. We propose a novel architecture for password-less authentication designed to improve usability and deployability. Our architecture is based on the WebAuthn standards and supports registration and login to web-services. We support a WebAuthn authenticator that generates and uses the key pairs on the client device by providing resilience for these key pairs by using a backup key store in the cloud. We also propose a WebAuthn authenticator using a key store in the cloud so that password-less authentication can be used interoperably between devices. We also assess the properties of these architectures against identified threats and how they can form the basis for improving usability and lowering the technical barriers to adoption of password-less authentication.