VOTEE: Voting on Trusted Execution Environments
Lead Research Organisation:
University of Surrey
Department Name: Computing Science
Abstract
Bring your own device (BYOD) technologies, such as the Trusted Execution Environment (TEE) enabled by ARM's TrustZone, can isolate sensitive corporate software from personal applications on employee owned devices. These technologies are expected to feature widely in future Thales security products and in systems where BYOD may be offered as a user terminal option. This iCASE provides an opportunity to investigate and evaluate in depth the protection provided by TEE/TrustZone technologies using the example of eVoting.
Publications
Bendisposto J
(2016)
Integrated Formal Methods
Whitefield J
(2019)
A Symbolic Analysis of ECC-based Direct Anonymous Attestation
Whitefield J
(2017)
Security and Trust Management
Whitefield J
(2017)
Privacy-Enhanced Capabilities for VANETs using Direct Anonymous Attestation
Studentship Projects
| Project Reference | Relationship | Related To | Start | End | Student Name |
|---|---|---|---|---|---|
| EP/N509383/1 | 01/10/2015 | 31/03/2021 | |||
| 1652008 | Studentship | EP/N509383/1 | 01/10/2015 | 31/03/2019 | Jorden Whitefield |
| Description | Identified limitations in current standards specifications for the deployment of future connect transportation systems, e.g. Vehicle-2-anything (V2X) communication. To partially address the discovered limitations we have utilised trusted computing within vehicles, and enabled a shift of trust from the architecture to inside vehicles. An additional, finding has also been formal analysis on academic security protocols used for vehicle revocation. Revocation is the process of removing a bad/misbehaving vehicle from the network, thus ensures safe and healthy operation of the transportation system. From performing formal analysis on these protocols, we discovered an attack on authentication that would allow a vehicle to remain connected to the network as a legitimate entity. Identified an attack in Direct Anonymous Attestation (DAA) through the use of formal analysis. DAA is a standardised set of operations originally developed for the Trusted Platform Module (TPM), and specified in ISO/IEC 20008 & ISO/IEC 11889. The analysis revealed that if the integrity of one TPM is compromised, then the security of all TPMs cannot be guaranteed. More broadly, this research plays a role in future security of networks in the Internet of Things (IoT), and in particular vehicular networks. Notably our research contributes to the growing body of work in the formal analysis of security protocols, and standardised security schemes. The research goes beyond the formal analysis, it has provided the research necessary to develop a demonstrator of a new security architecture for privacy-preserving V2X communications by employing DAA. |
| Exploitation Route | The research is not limited to vehicular architectures, and the techniques are applicable to any device and secure communications. |
| Sectors | Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software),Transport |
| Description | Our proposal for using Direct Anonymous Attestation in vehicular architectures has been realised in a proof of concept as part of an EPSRC IAA project in collaboration with Thales UK. The impact of Surrey's work in this project was a proof of concept demonstrator that evaluated the challenges of scalability. We demonstrated the applicability of our DAA V2X architecture in a relevant lab environment using actual automotive boxes and communication interfaces and message standards that have been defined by the industry. |
| First Year Of Impact | 2018 |
| Sector | Digital/Communication/Information Technologies (including Software),Transport |
| Description | IAA |
| Amount | £47,961 (GBP) |
| Funding ID | 15220193 |
| Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
| Sector | Public |
| Country | United Kingdom |
| Start | 02/2018 |
| End | 12/2018 |
| Description | IEEE Euro S&P |
| Organisation | ETH Zurich |
| Country | Switzerland |
| Sector | Academic/University |
| PI Contribution | Formal modelling, generation of collaborative research ideas |
| Collaborator Contribution | Domain expertise in formal verification of security protocols |
| Impact | Produced paper "A Symbolic Analysis of ECC-based Direct Anonymous Attestation" IEEE Euro S&P |
| Start Year | 2018 |
| Description | STM17 |
| Organisation | Aalto University |
| Department | Department of Computer Science |
| Country | Finland |
| Sector | Academic/University |
| PI Contribution | Formal modelling, generation of collaborative research ideas |
| Collaborator Contribution | Domain expertise in vehicular technology and Hardware systems |
| Impact | Produced paper Formal Analysis of V2X Revocation Protocols presented at STM 2017 |
| Start Year | 2016 |
| Description | STM17 |
| Organisation | University of Ulm |
| Department | Faculty of Engineering, Computer Science and Psychology |
| Country | Germany |
| Sector | Academic/University |
| PI Contribution | Formal modelling, generation of collaborative research ideas |
| Collaborator Contribution | Domain expertise in vehicular technology and Hardware systems |
| Impact | Produced paper Formal Analysis of V2X Revocation Protocols presented at STM 2017 |
| Start Year | 2016 |
| Description | iFM16 |
| Organisation | Heinrich Heine University Düsseldorf |
| Department | Department of Computer Science |
| Country | Germany |
| Sector | Academic/University |
| PI Contribution | Expertise in CSP||B |
| Collaborator Contribution | Expertise in tooling support |
| Impact | Publication at Symbolic Reachability Analysis of B through ProB and LTSmin at iFM 2016 |
| Start Year | 2015 |
| Description | iFM16 |
| Organisation | University of Twente |
| Department | Faculty of Science and Technology |
| Country | Netherlands |
| Sector | Academic/University |
| PI Contribution | Expertise in CSP||B |
| Collaborator Contribution | Expertise in tooling support |
| Impact | Publication at Symbolic Reachability Analysis of B through ProB and LTSmin at iFM 2016 |
| Start Year | 2015 |
| Title | DAA C++ Implementation code |
| Description | C++ Implementation for DAA Implementation related to Asia CSS 2020 paper |
| Type Of Technology | New/Improved Technique/Technology |
| Year Produced | 2020 |
| Impact | This output has been used further in an IAA project related to V2X. |
| URL | https://dl.acm.org/doi/10.1145/3320269.3372197 |
| Title | DAA Tamarin Implementation Models |
| Description | Tamarin implementation models for ECC-DAA implementations. |
| Type Of Technology | New/Improved Technique/Technology |
| Year Produced | 2020 |
| Impact | publication in Asia CCS 2020 |
| URL | https://dl.acm.org/doi/10.1145/3320269.3372197 |
| Title | Tamarin code EuroSP 2019 |
| Description | This is the Tamarin code associated with the paper "A symbolic analysis of ecc-based direct anonymous attestation" |
| Type Of Technology | Software |
| Year Produced | 2019 |
| Open Source License? | Yes |
| Impact | https://ieeexplore.ieee.org/abstract/document/8806715 |
| URL | https://ieeexplore.ieee.org/abstract/document/8806715 |
| Description | Real World Crypto Presentation |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Professional Practitioners |
| Results and Impact | Real World Crypto is an annual event that promotes the novel applications of cryptography in the real world. The purpose of the talk was to demonstrate the challenge of applying cryptography in intelligent transport systems. |
| Year(s) Of Engagement Activity | 2019 |
| URL | https://rwc.iacr.org/2019/slides/DAA.pdf |