@INPROCEEDINGS{Sardar2020EPID,
  author={M. U. {Sardar} and D. L. {Quoc} and C. {Fetzer}},
  booktitle={Euromicro Conference on Digital System Design (DSD)}, 
  title={Towards Formalization of Enhanced Privacy ID (EPID)-based Remote Attestation in Intel SGX}, 
  year={2020},
  volume={},
  number={},
  pages={604-607},
  abstract={Vulnerabilities in privileged software layers have been exploited with severe consequences. Recently, Trusted Execution Environments (TEEs) based technologies have emerged as a promising approach since they claim strong confidentiality and integrity guarantees regardless of the trustworthiness of the underlying system software. In this paper, we consider one of the most prominent TEE technologies, referred to as Intel Software Guard Extensions (SGX). Despite many formal approaches, there is still a lack of formal proof of some critical processes of Intel SGX, such as remote attestation. To fill this gap, we propose a fully automated, rigorous, and sound formal approach to specify and verify the Enhanced Privacy ID (EPID)-based remote attestation in Intel SGX under the assumption that there are no side-channel attacks and no vulnerabilities inside the enclave. The evaluation indicates that the confidentiality of attestation keys is preserved against a Dolev-Yao adversary in this technology. We also present a few of the many inconsistencies found in the existing literature on Intel SGX attestation during formal specification.},
  keywords={data privacy;formal specification;program verification;trusted computing;EPID;system software;Intel software guard extensions;formal proof;Intel SGX attestation;formal specification;TEE technologies;trusted execution environments;enhanced privacy ID-based remote attestation;attestation keys;formal verification;Software;Cryptography;Computational modeling;Protocols;Privacy;Testing;remote attestation;formal verification;Trusted Execution Environment;Intel SGX;Enhanced Privacy ID (EPID)},
  doi={10.1109/DSD51259.2020.00099},
  ISSN={},
  month={Aug},}