pi_RA: A pi-calculus for verifying protocols that use remote attestation
summary
pi_RA is an applied pi-calculus variant that treats remote attestation as a first‑class cryptographic primitive and compiles an actor-style source language into it. The authors build a pre-compiler + compiler that maps pi_Actor communication into RA operations, formalize MAGE (an SGX-based mutual attestation system), and mechanically prove compiler security under two criteria (restricted full abstraction and a robust relational hyperproperty with universal quantification over an identity table). The proof succeeds but exposes a concrete caveat: indistinguishable, replayable copies of components can’t be told apart without extra public-key or lookup machinery.
AI-written summary · about
chapters (16)
- 0:00pi_RA and remote attestation
- 1:07Motivation for remote attestation
- 2:31Remote attestation in practice
- 3:38pi calculus overview
- 4:18get_attest in pi_RA
- 5:23Authenticated communication in pi_RA
- 7:05Mutual authentication problem
- 9:35Limitations in process copies
- 10:17Security goals and compilation
- 12:26Appl with actors source
- 14:13Compiler design and pre-compilation
- 17:05Proving compiler security
- 19:36Q&A: Applicability
- 21:20Q&A: Comparison with languages
- 22:05Q&A: Full abstraction vs assertions
- 23:09Closing remarks
related talks
30mTaming Attestation for the Cloud Native World with Parsec
25mDemystifying remote attestation
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation
16mCerisier: A Program Logic for Attestation in a Capability Machine
25mRuntimeGuard-AI: Cryptographic Compliance
29mA Simple Protocol for Remote Attestation of System Integrity
05mπMPC: Automatic Security Proofs for MPC Protocols
27mProofs of proofs: incremental verifiability from recursion and accumulation