Dr Christopher J P Newton


Research Fellow

Academic and research departments

Surrey Centre for Cyber Security.

Publications

Andreea-Ina Radu, Tom Chothia, Christopher J.P. Newton, Ioana Boureanu, Liqun Chen (2022)Practical EMV Relay Protection, In: Proceedings of the 2022 IEEE Symposium on Security and Privacy (SP 2022)pp. 1737-1756 Institute of Electrical and Electronics Engineers (IEEE)

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.

Liqun Chen, Changyu Dong, Nada El Kassem, Christopher J. P. Newton, Yalan Wang (2023)Hash-Based Direct Anonymous Attestation, In: Post-Quantum Cryptographypp. 565-600 Springer Nature Switzerland

Direct Anonymous Attestation (DAA) was designed for the Trusted Platform Module (TPM) and versions using RSA and elliptic curve cryptography have been included in the TPM specifications and in ISO/IEC standards. These standardised DAA schemes have their security based on the factoring or discrete logarithm problems and are therefore insecure against quantum attackers. Research into quantum-resistant DAA has resulted in several lattice-based schemes. Now in this paper, we propose the first post-quantum DAA scheme from symmetric primitives. We make use of a hash-based signature scheme, which is a slight modification of SPHINCS+, as a DAA credential. A DAA signature, proving the possession of such a credential, is a multiparty computation-based non-interactive zero-knowledge proof. The security of our scheme is proved under the Universal Composability (UC) model. While maintaining all the security properties required for a DAA scheme, we try to make the TPM’s workload as low as possible. Our DAA scheme can handle a large group size (up to \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$2^{60}$$\end{document} group members), which meets the requirements of rapidly developing TPM applications.

Liqun Chen, Nada El Kassem, Christopher J. P. Newton (2023)How To Bind A TPM's Attestation Keys With Its Endorsement Key, In: Computer journal Oxford Univ Press

A trusted platform module is identified by its endorsement key, while it uses an attestation key to provide attestation services, for example, signing a set of platform configuration registers, providing a timestamp or certifying another of its keys. This paper addresses the problem of how a certificate authority binds the endorsement and attestation keys together. This is necessary for the authority to be able to reliably certify the attestation key. This key binding also enables the authority to revoke the attestation key should the endorsement key be compromised. We study all of the existing solutions and show that they either do not solve the problem or cannot be implemented with a real trusted platform module (or both). We propose a new solution which addresses this problem. We develop a security model for our solution and provide a rigorous security proof under this model. We have also implemented the solution using a real trusted platform module, and our implementation results show that this solution is feasible and efficient.

Loganathan Parthipan, Liqun Chen, David Gerault, Yunpeng Li, Fei Liu, Christopher J P Newton, Donghui Wang (2021)A Survey of Technologies for Building Trusted Networks, In: 2021 IEEE Globecom Workshops (GC Wkshps)pp. 1-6 IEEE

In the current generation of networks, there has been a strong focus on security and integrity. In sixth-generation (6G) networks trust will also be an important requirement, but how do we build trust in a network? Many researchers have started to pay attention to this, but research in this field is still at an early stage. Taking our lead from the development of trusted computing for single devices we require a root of trust and a mechanism for reliably measuring and reporting on the state of the network. In this paper, we survey existing technologies that we feel can be used to achieve this. We explore trusted computing technologies that enable a single device to be trusted and suggest how they can be adapted to help build a trusted network. For reporting, we need a mechanism to immutably store measurements on the system. We consider that distributed ledger technologies could fulfil this role as they offer immutability, decentralised consensus, and transparency.

N. J. Mottram, C. J. P. Newton (2016)Liquid Crystal Theory and Modeling, In: Handbook of Visual Display Technologypp. 2021-2051 Springer International Publishing

In this chapter, we explain the rationale behind the theoretical modeling of liquid crystals and explain the important steps to construct a realistic and accurate model for a particular physical system. We then summarize two commonly used theories of nematics: one based on using the director as a dependent variable and one based on using the tensor order parameter. Using an example problem, the π-cell, we show the advantages and disadvantages of these two theoretical approaches, demonstrating the importance of carefully considering the choice of model before embarking on simulations.

Matthew Casey, Mark Manulis, Christopher J. P Newton, Robin Savage, Helen Treharne (2020)An Interoperable Architecture for Usable Password-Less Authentication, In: Emerging Technologies for Authorization and Authenticationpp. 16-32 Springer International Publishing

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.

Rhys Miller, Ioana Boureanu, Stephan Wesemeyer, Christopher J. P. Newton (2022)The 5G Key-Establishment Stack: In-Depth Formal Verification and Experimentation, In: ASIA CCS'22: PROCEEDINGS OF THE 2022 ACM ASIA CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITYpp. 237-251 Assoc Computing Machinery

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

Kang Yang, Liqun Chen, Zhenfeng Zhang, Christopher J. P. Newton, Bo Yang, Li Xi (2021)Direct Anonymous Attestation With Optimal TPM Signing Efficiency, In: IEEE Transactions on Information Forensics and Security16pp. 2260-2275 Institute of Electrical and Electronics Engineers (IEEE)

Direct Anonymous Attestation (DAA) is an anonymous signature scheme, which allows the Trusted Platform Module (TPM), a small chip embedded in a host computer, to attest to the state of the host system, while preserving the privacy of the user. DAA provides two signature modes: fully anonymous signatures and pseudonymous signatures. One main goal of designing DAA schemes is to reduce the TPM signing workload as much as possible, as the TPM has only limited resources. In an optimal DAA scheme, the signing workload on the TPM will be no more than that required for a normal signature like ECSchnorr. To date, no scheme has achieved the optimal signing efficiency for both signature modes. In this paper, we propose the first DAA scheme which achieves the optimal TPM signing efficiency for both signature modes. In this scheme, the TPM takes only a single exponentiation to generate a signature, and this single exponentiation can be pre-computed. Our scheme can be implemented using the existing TPM 2.0 commands, and thus is compatible with the TPM 2.0 specification. We benchmarked the TPM 2.0 commands needed for three DAA use cases on an Infineon TPM 2.0 chip, and also implemented the host signing and verification algorithm for our DAA scheme on a laptop with 1.80GHz Intel Core i7-8550U CPU. Our experimental results show that our DAA scheme obtains a total signing time of about 144 ms for either signature mode, while with pre-computation we can obtain a signing time of about 65 ms. Based on our benchmark results for the pseudonymous signature mode, our scheme is roughly 2\times (resp., 5\times ) faster than the existing DAA schemes supported by TPM 2.0 in terms of total (resp., online) signing efficiency.

N. J. Mottram, C. J. P. Newton (2012)Liquid Crystal Theory and Modelling, In: J Chen, W Cranton, M Fihn (eds.), Handbook of Visual Display Technologypp. 1403-1429 Springer Nature

In this chapter we explain the rationale behind the theoretical modeling of liquid crystals and explain the important steps to construct a realistic and accurate model for a particular physical system. We then summarize two commonly used theories of nematics: one based on using the director as a dependent variable and one based on using the tensor order parameter. Using an example problem, the pi-cell, we show the advantages and disadvantages of these two theoretical approaches, demonstrating the importance of carefully considering the choice of model before embarking on simulations.

W. R. B. Lionheart, C. J. P. Newton (2007)Analysis of the inverse problem for determining nematic liquid crystal director profiles from optical measurements using singular value decomposition, In: New journal of physics9(3)pp. 63-63 Iop Publishing Ltd

We use the problem of determining nematic liquid crystal director profiles from optical measurements as an example to illustrate that what is often treated purely as a data fitting problem is really an inverse problem and that useful insights can be obtained by treating it in this way. Specifically we illustrate the analysis of the sufficiency of data and the sensitivity of a solution to measurement errors. We assume a stratified medium where the Berreman method can be used for the optical forward problem and we consider the inverse problem to be the determination of an anisotropic dielectric permittivity tensor from optical data. A numerical singular value decomposition (SVD) analysis reveals that although this inverse problem is severely ill-conditioned it is possible to determine depth-dependent information provided the medium is sufficiently birefringent and that, as one might expect, a larger range of incident angles gives greater information. Analytical solutions of the Berreman equations for general perturbations of an orthorhombic crystal confirm the uniqueness of solution for the linearized problem and give further insights into the severely ill-posed nature of the inverse problem.

Mikhail Yakutovich, Chris Care, Cjp Newton, Doug Cleaver, Christopher James Percival Newton (2010)Mesh-free modelling of liquid crystals using modified smoothed particle hydrodynamics, In: Physical review. E, Statistical, nonlinear, and soft matter physics82(4)pp. 041703-041703 American Physical Society

We present a generalisation of the Modified Smooth Particle Hydrodynamics simulation technique capable of simulating static and dynamic liquid crystalline behaviour. This generalisation is then implemented in the context of the Qian-Sheng description of nematodynamics. To test the method, we first use it to simulate switching in both a Freedericksz setup and a chiral hybrid aligned nematic\ud cell. In both cases, the results obtained give excellent agreement with previously published results. We then apply the technique in a 3-dimensional simulation of the switching dynamics of the post aligned bistable nematic device.

Giuseppe Lombardo, Christopher J. Newton, John C. Rudin (2003)An Auto-Aligning Photopolarimeter, In: Molecular crystals and liquid crystals (Philadelphia, Pa. : 2003)398(1)pp. 117-126 Taylor & Francis Group

A new auto-aligning photopolarimeter, that will be used to probe a liquid crystal (LC) cell, is described. As the LC cell is rotated, it steers the probing laser beam and the photopolarimeter head must be re-aligned to allow for this. To efficiently collect data this re-alignment must be done automatically. We show that using a quadrant photodetector (QD) and a two dimensional duo-lateral position sensing detector (PSD) it is possible to dynamically re-align the head. Also we introduce a new method to calibrate this auto-aligning system. We can collect data from points distributed over the Poincairé sphere and then use all of these to find the instrument matrix M c that minimizes the error (in the least squares sense).

E. G. Edwards, C. V. Brown, E. E. Kriezis, S. J. Elston, S. C. Kitson, C. J. P. Newton (2004)Diffraction From the Two Stable States in a Nematic Liquid Crystal cell containing a mono-grating with homeotropic director alignment, In: Molecular crystals and liquid crystals (Philadelphia, Pa. : 2003)410(1)pp. 401-408 Taylor & Francis Group

In this work we use the Q-tensor order parameter to express the elastic free energy of a nematic liquid crystal. This correctly preserves the +n/−n symmetry and thus allows the modelling of defects. Using this, we calculate director profiles for cells containing surface relief gratings. Director profiles are presented which demonstrate that the cell supports two stable director configurations, in agreement with previous investigations [1-3]. The director profiles calculated are used in conjunction with Finite-Difference Time-Domain optical modelling to simulate the diffraction from the two stable states. The results of these simulations are then compared with experimental results for a cell fabricated with a relief grating on one internal surface. Diffraction strength is measured as a function of incident angle and as a function of incident polarisation.

Apala Majumdar, Christopher Newton, Jonathan Robbins, Maxim Zyskin, Christopher James Percival Newton (2004)Quasi-stable configurations of liquid crystals in polyhedral geometries, In: Proceedings of SPIE5565(1)pp. 185-190

Bistable director configurations are of great interest in liquid crystal display technologies, offering the possibility of higher resolution combined with reduced power consumption. One way to achieve such bistability is to use the cell geometry. As part of an ongoing programme to analyze quasi-stable configurations of liquid crystals in polyhedral geometries, we construct a topological classification scheme of unit-vector fields in convex polyhedra subject to tangential boundary conditions and obtain a general lower bound on the energy of these configurations. We also study the specific case of a unit cube, where we obtain lower and upper bounds for the energies of a family of topological types.

M. V. Yakutovich, C. J. P. Newton, D. J. Cleaver (2009)Mesh-Free Simulation of Complex LCD Geometries, In: Molecular crystals and liquid crystals (Philadelphia, Pa. : 2003)502(1)pp. 245-257 Taylor & Francis

We use a novel mesh-free simulation approach to study the post aligned bistable nematic (PABN) cell. By employing the Qian-Sheng formalism for liquid crystals along with a smooth representation of the surface posts, we have been able to identify two distinct stable configurations. The three-dimensional order field configurations of these states and their elastic free energies are consistent with both experimental results and previous simulation attempts. However, alternative states suggested in previous studies do not appear to remain stable when finite post curvature is considered.

Y. G. J. Lau, S. Klein, C. J. P. Newton, R. M. Richardson (2007)Surface ordering at the air-nematic interface. Part 2. A spectroscopic ellipsometry study of orientational order, In: Liquid crystals34(4)pp. 421-429 Taylor & Francis

Spectroscopic ellipsometry has been used to measure enhanced orientational ordering at the nematic-air interface of 8CB as the smectic A phase was approached by cooling from the isotropic phase. The depth profile of the orientational order has been estimated by calculating the ellipsometric parameters for a homeotropic uniaxial surface film on a uniaxial sub-phase using the Abelès matrix method. This showed that the depth of the enhanced orientationally ordered region was ∼10 nm at 0.5°C above the nematic-smectic A transition. This is substantially less than the thickness of the region with surface enhanced smectic order as determined by neutron reflection and a model of the surface structure consistent with both sets of results is proposed.

T B Grimley, CJP Newton, Christopher James Percival Newton (1975)OVERCOMPLETENESS IN THEORY OF CHEMISORPTION, In: Physics letters. AA 51(5)pp. 267-268 Elsevier
Craig S. MacDonald, John A. Mackenzie, Alison Ramage, Christopher J. P. Newton (2015)EFFICIENT MOVING MESH METHODS FOR Q-TENSOR MODELS OF NEMATIC LIQUID CRYSTALS, In: SIAM journal on scientific computing37(2)pp. B215-B238 Siam Publications

This paper describes a robust and efficient numerical scheme for solving the system of six coupled partial differential equations which arises when using Q-tensor theory to model the behavior of a nematic liquid crystal cell under the influence of an applied electric field. The key novel feature is the use of a full moving mesh partial differential equation approach to generate an adaptive mesh which accurately resolves important solution features. This includes the use of a new monitor function based on a local measure of biaxiality. In addition, adaptive time-step control is used to ensure the accurate predicting of the switching time, which is often critical in the design of liquid crystal cells. We illustrate the behavior of the method on a one-dimensional time-dependent problem in a Pi-cell geometry which admits two topologically different equilibrium states, modeling the order reconstruction which occurs on the application of an electric field. Our numerical results show that, in addition to achieving optimal rates of convergence in space and time, we obtain higher levels of solution accuracy and a considerable improvement in computational efficiency compared to other moving mesh methods used previously for liquid crystal problems.

Alison Ramage, Christopher J. P. Newton (2007)Adaptive solution of a one-dimensional order reconstruction problem in Q-tensor theory of liquid crystals, In: Liquid crystals34(4)pp. 479-487 Taylor & Francis

In this paper we illustrate the suitability of an adaptive moving mesh method for modelling a one-dimensional liquid crystal cell using Q-tensor theory. Specifically, we consider a time-dependent problem in a Pi-cell geometry which admits two topologically different equilibrium states and model the order reconstruction which occurs on the application of an electric field. An adaptive finite element grid is used where the grid points are moved according to equidistribution of a monitor function based on a specific property of the Q-tensor. We show that such moving meshes provide the same level of accuracy as uniform grids but using far fewer points, and that inaccurate results can be obtained if uniform grids are not sufficiently refined.

Ariosto Matranga, Sarwat Baig, Jessica Boland, Christopher Newton, Timothy Taphouse, Gary Wells, Stephen Kitson (2013)Biomimetic Reflectors Fabricated Using Self-Organising, Self-Aligning Liquid Crystal Polymers, In: Advanced materials (Weinheim)25(4)pp. 520-523 Wiley

The photograph shows a polymer reflector that mimics the colour and underlying molecular structure of a golden beetle. It is formed from self-organizing layers of photopolymerised liquid crystal. These require an aligning layer, but we show that a layer of the material can be used as to self-align subsequent coatings, enabling the construction of complex structures by sequential coating of engineered materials.

Emmanouil E Kriezis, Christopher J P Newton, Timothy P Spiller, Steve J Elston (2002)Three-dimensional simulations of light propagation in periodic liquid-crystal microstructures, In: Applied optics (2004)41(25)pp. 5346-5356

A composite scheme based on the finite-difference time-domain method and a plane-wave expansion method is developed and applied to the optics of periodic liquid-crystal microstructures. This is used to investigate three-dimensional light-wave propagation in grating-induced bistable nematic devices with double periodicity. Detailed models of realistic devices are analyzed with emphasis on two different underlying surface-relief grating structures: a smooth bisinusoidal grating and a square-post array. The influence of the grating feature size is quantified. Device performance is examined in conjunction with an appropriate compensation layer, and the optimum layer thickness is determined for the different grating geometries.

Craig S. MacDonald, John A. Mackenzie, Alison Ramage, Christopher J. P. Newton (2012)Robust adaptive computation of a one-dimensional Q-tensor model of nematic liquid crystals, In: Computers & mathematics with applications (1987)64(11)pp. 3627-3640 Elsevier

This paper illustrates the use of an adaptive finite element method to solve a nonlinear singularly perturbed boundary value problem which arises from a one-dimensional Q-tensor model of liquid crystals. The adaptive non-uniform mesh is generated by equidistribution of a strictly positive monitor function which is a linear combination of a constant floor and a power of the first derivative of the numerical solution. By an appropriate selection of the monitor function parameters, we show that the computed numerical solution converges at an optimal rate with respect to the mesh density and that the solution accuracy is robust to the size of the singular perturbation parameter. (C) 2012 Elsevier Ltd. All rights reserved.

G. G. Wells, M. A. Matranga, C. J. P. Newton, T. S. Taphouse, S. A. Baig, S. C. Kitson (2013)Electrowetting pixels with improved transmittance using dye doped liquid crystals, In: Applied physics letters103(3) Amer Inst Physics

Electrowetting display pixels have been created using a dye doped liquid crystal as the dielectric liquid in a simple electrowetting architecture. In addition to electrowetting, the dye doped liquid crystal reorients, giving two mechanisms to modulate the light. We show that realignment of the liquid crystal, due to the electric field, occurs both before and during electrowetting. The transmission of the pixel has been compared to the transmission of a pixel containing an isotropic liquid, using a simple mathematical model, and we show that electrical realignment of the LC improves the transmission of the pixel. We show a 6.8% gain in the transmission during electrowetting, and before electrowetting occurs. (C) 2013 AIP Publishing LLC.

S. L. Cornford, T. S. Taphouse, C. J. PNewton, J. R. Sambles, Christopher James Percival Newton (2007)Determination of the director profile in a nematic cell from guided wave data: an inverse problem, In: New journal of physics9(6)pp. 166-166 Iop Publishing Ltd

We consider an inverse problem: the estimation of the nematic director profile from experimental fully leaky guided mode data. This inverse problem is ill-posed in that small changes in the data may lead to large changes in the estimates of the director profile. The continuum equations for a nematic are exploited to stabilize the problem. We use experimental data drawn from a study of the dynamics of a hybrid-aligned nematic cell as an example.

Emmanouil E. Kriezis, Steve J. Elston, Christopher J. Newton, Timothy P. Spiller (2004)3-D OPTICAL SIMULATIONS OF AZIMUTHAL BISTABLE NEMATIC DEVICES, In: Molecular crystals and liquid crystals (Philadelphia, Pa. : 2003)413(1)pp. 321-331 Taylor & Francis Group

A composite scheme based on the Finite-Difference Time-Domain (FDTD) method and a plane wave expansion is developed and applied to the optics of doubly periodic liquid crystal microstructures. This is used to investigate 3-D light wave propagation in grating aligned azimuthal bistable nematic devices.

Alison Ramage, Christopher J. P. Newton (2008)Adaptive grid methods for Q-tensor theory of liquid crystals: A one-dimensional feasibility study, In: Molecular crystals and liquid crystals (Philadelphia, Pa. : 2003)480(1)pp. 160-181 Taylor & Francis

This article illustrates the use of moving mesh methods for solving partial differential equation (PDE) problems in Q-tensor theory of liquid crystals. We present the results of an initial study using a simple one-dimensional test problem which illustrates the feasibility of applying adaptive grid techniques in such situations. We describe how the grids are computed using an equidistribution principle, and investigate the comparative accuracy of adaptive and uniform grid strategies, both theoretically and via numerical examples.

A Majumdar, C J P Newton, J M Robbins, M Zyskin (2007)Topology and bistability in liquid crystal devices, In: Physical review. E, Statistical, nonlinear, and soft matter physics75(5 Pt 1)pp. 051703-051703

We study nematic liquid crystal configurations in a prototype bistable device -- the post aligned bistable nematic (PABN) cell. Working within the Oseen-Frank continuum model, we describe the liquid crystal configuration by a unit-vector field n , in a model version of the PABN cell. First, we identify four distinct topologies in this geometry. We explicitly construct trial configurations with these topologies which are used as initial conditions for a numerical solver, based on the finite-element method. The morphologies and energetics of the corresponding numerical solutions qualitatively agree with experimental observations and suggest a topological mechanism for bistability in the PABN cell geometry.

Steve Wesemeyer, Christopher Newton, Helen Treharne, Liqun Chen, Ralf Sasse, Jordan Whitefield (2020)Formal Analysis and Implementation of a TPM 2.0-based Direct Anonymous Attestation Scheme, In: 15th ACM ASIA Conference on Computer and Communications Security

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.