Automated Verification of Dynamic Root of Trust Protocols

DOI10.1007/978-3-662-54455-6_5MaRDI QIDQ3304809zbMATH OpenOpenAlexFDO

Authors Sergiu Bursuc, Christian Johansen, Shiwei Xu

Publication date 3 August 2020

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1701.08676

Mathematics Subject Classification ID

Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60) Computer security (68M25)

Abstract: Automated verification of security protocols based on dynamic root of trust, typically relying on protected hardware such as TPM, involves several challenges that we address in this paper. We model the semantics of trusted computing platforms (including CPU, TPM, OS, and other essential components) and of associated protocols in a classical process calculus accepted by ProVerif. As part of the formalization effort, we introduce new equational theories for representing TPM specific platform states and dynamically loaded programs. Formal models for such an extensive set of features cannot be readily handled by ProVerif, due especially to the search space generated by unbounded extensions of TPM registers. In this context we introduce a transformation of the TPM process, that simplifies the structure of the search space for automated verification, while preserving the security properties of interest. This allows to run ProVerif on our proposed models, so we can derive automatically security guarantees for protocols running in a dynamic root of trust context.

Recommendations

• Type-Based Automated Verification of Authenticity in Cryptographic Protocols
• scientific article; zbMATH DE number 1903362
• Automated verification of selected equivalences for security protocols
• Automated verification of equivalence properties of cryptographic protocols
• Automated verification of equivalence properties of cryptographic protocols
• Type-based automated verification of authenticity in asymmetric cryptographic protocols
• Tools and Algorithms for the Construction and Analysis of Systems
• Automatic verification of cryptographic protocols with SETHEO
• Verifying security protocols modelled by networks of automata

Cites work

• scientific article; zbMATH DE number 1418311 (Why is no real title available?)
• Analysing routing protocols: four nodes topologies are sufficient
• Compiling Information-Flow Security to Minimal Trusted Computing Bases
• Mobile values, new names, and secure communication
• Parametric verification of address space separation
• Principles of security and trust. First international conference, POST 2012, held as part of the European joint conferences on theory and practice of software, ETAPS 2012, Tallinn, Estonia, March 24 -- April 1, 2012. Proceedings
• Reduction of equational theories for verification of trace equivalence: re-encryption, associativity and commutativity
• Verification of security protocols with lists: from length one to unbounded length

Cited in

(3)

• Formal verification of establishment of chain of trust in trusted computing
• A Symbolic Model for Systematically Analyzing TEE-Based Protocols
• Dynamic measurement and protected execution: model and analysis

Describes a project that uses

Uses Software

• ProVerif

This page was built for publication: Automated Verification of Dynamic Root of Trust Protocols

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3304809)