Automated Verification of Dynamic Root of Trust Protocols

DOI10.1007/978-3-662-54455-6_5zbMATH Open1444.68037arXiv1701.08676OpenAlexW3124484319MaRDI QIDQ3304809FDOQ3304809

Authors: Sergiu Bursuc, Christian Johansen, Shiwei Xu 

Publication date: 3 August 2020

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

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.

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

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

Mathematics Subject Classification ID

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

Cites Work

• Mobile values, new names, and secure communication
• 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
• Title not available (Why is that?)
• Reduction of equational theories for verification of trace equivalence: re-encryption, associativity and commutativity
• Parametric verification of address space separation
• Verification of security protocols with lists: from length one to unbounded length
• Analysing routing protocols: four nodes topologies are sufficient
• Compiling Information-Flow Security to Minimal Trusted Computing Bases

Cited In (3)

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

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)