Paper 2022/1724

Formal Analysis of SPDM: Security Protocol and Data Model version 1.2

Cas Cremers, CISPA Helmholtz Center for Information Security
Alexander Dax, CISPA Helmholtz Center for Information Security, Saarland University
Aurora Naska, CISPA Helmholtz Center for Information Security, Saarland University

DMTF is a standards organization by major industry players in IT infrastructure including AMD, Alibaba, Broadcom, Cisco, Dell, Google, Huawei, IBM, Intel, Lenovo, and NVIDIA, which aims to enable interoperability, e.g., including cloud, virtualization, network, servers and storage. It is currently standardizing a security protocol called SPDM, which aims to secure communication over the wire and to enable device attestation, notably also explicitly catering for communicating hardware components. The SPDM protocol inherits requirements and design ideas from IETF’s TLS 1.3. However, its state machines and transcript handling are substantially different and more complex. While architecture, specification, and open-source libraries of the current versions of SPDM are publicly available, these include no significant security analysis of any kind. In this work we develop the first formal models of the three modes of the SPDM protocol version 1.2.1, and formally analyze their main security properties.

Available format(s)
Cryptographic protocols
Publication info
Tamarin ProverSPDMFormal AnalysisSecurity Protocols
Contact author(s)
cremers @ cispa de
alexander dax @ cispa de
aurora naska @ cispa de
2023-03-20: last of 2 revisions
2022-12-14: received
See all versions
Short URL
Creative Commons Attribution


      author = {Cas Cremers and Alexander Dax and Aurora Naska},
      title = {Formal Analysis of {SPDM}: Security Protocol and Data Model version 1.2},
      howpublished = {Cryptology ePrint Archive, Paper 2022/1724},
      year = {2022},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.