The paper entitled “Root-of-Trust Abstractions for Symbolic Analysis: Application to Attestation Protocols” has been accepted for presentation at the 17th International Workshop on Security and Trust Management, co-located with the 26th European Symposium on Research in Computer Security (ESORICS) 2021, held virtually from October 4 – 8, 2021. Dr Thanassis Giannetsos, Head of UBITECH’s Digital Security and Trusted Computing Research Group, and his co-authors propose a methodology for proving security in scenarios based on services that make use of Roots-of-Trust (RoTs), by idealizing the internal functionalities of the security device, except those that provide explicit cryptographic functionalities for the service being offered.
In order to illustrate their methodology, they concentrate on a class of remote attestation services based on the TPM. Even though they focus on a particular case of attestation, they build an abstract model for a subset of TPM primitives sufficient to implement the core functionalities of generic attestation services. From the perspective of formally verifying RoT-based applications, this model represents a means of reasoning about security and privacy (of offered services) without being bogged down by the intricacies of various crypto primitives considered in the different platforms. They conduct their analysis in the symbolic model of cryptography (Dolev-Yao adversary) through the Tamarin prover and its front-end SAPiC. They define a number of security properties relevant for the considered scenario, and successfully verify them with this framework
For more technical details, you may have a look (open access) at our paper.