pi_RA: A pi-calculus for verifying protocols that use remote attestation
Remote attestation (RA) is a primitive that allows authentication of software components on untrusted systems by relying on a root of trust. Network protocols can use the primitive to establish trust in remote software components they communicate with. As such, RA can be regarded as a first-class security primitive like (a)symmetric encryption, message authentication, etc. However, current formal models of RA do not allow analysing protocols that use the primitive without tying them to specific platforms, low-level languages, memory protection models or implementation details.
In this paper, we propose and demonstrate a new model, called pi_RA, that supports RA at a high level of abstraction by treating it as a cryptographic primitive in a variant of the applied pi-calculus. To demonstrate the use of pi_RA, we use it to formalise and analyse the security of MAGE, an SGX-based framework that allows mutual attestation of multiple enclaves. The protocol is formalised in the form of a compiler that implements actor-based communication primitives in a source language (pi_Actor) in terms of remote attestation primitives in pi_RA. Subsequently, to prove the security of MAGE, we prove that the compiler representing MAGE is secure. Our security analysis also uncovers a caveat in the security of MAGE that was left unmentioned in the original paper.
|Extended abstract Pi_RA (extendedAbstractPiRA.pdf)||461KiB|
Sat 21 JanDisplayed time zone: Eastern Time (US & Canada) change
11:00 - 12:30
Session 2PriSC at Park
Chair(s): Cătălin Hriţcu MPI-SP
|Automated Learning and Verification of Embedded Security Architectures|
Matteo Busi University Ca' Foscari, Venice, Riccardo Focardi University Ca' Foscari, Venice, Flaminia L. Luccio University Ca' Foscari, VeniceFile Attached
|pi_RA: A pi-calculus for verifying protocols that use remote attestation|
Emiel Lanckriet KU Leuven, Matteo Busi University Ca' Foscari, Venice, Dominique Devriese KU LeuvenFile Attached
|Robust Constant-Time Cryptography|
Matthew Kolosick University of California at San Diego, Basavesh Ammanaghatta Shivakumar Max Planck Institute for Security and Privacy (MPI-SP), Sunjay Cauligi University of California at San Diego, USA, Marco Patrignani University of Trento, Marco Vassena Utrecht University, Ranjit Jhala University of California at San Diego, Deian Stefan University of California at San DiegoPre-print
|Short Talk: Generalising secure compilation criteria|
Emiel Lanckriet KU Leuven