Design Space and Challenges in Design of Attested TLS Protocols
summary
Formal symbolic analysis using ProVerif shows pre- and intra-handshake designs leave many security properties unmet and even the best intra-handshake variant (solution 5) still has a critical cross; the draft argues binding evidence to the ATSC application traffic secret yields stronger guarantees. Post-handshake attestation prevents diversion, relay, and replication attacks per the proofs, gains IETF SEAT traction, has ACCS-accepted results, and now sees reference implementations in rustls and BoringSSL under active development.
AI-written summary · about
chapters (8)
- 0:00Introduction and agenda
- 1:49Attestation in TLS handshake
- 5:46TLS 1.3 key schedule analysis
- 10:00Evidence binding to secrets
- 13:55Security vs privacy arguments
- 14:36Post-handshake attestation consensus
- 15:42Formal analysis and implementations
- 17:26Q&A on post-handshake attestation
related talks
16mSeparate but Together: Integrating Remote Attestation into TLS
24mHardware backed attestation in TLS
39mFormal specification of attestation mechanisms in Confidential Computing
41mFormally Verifying Everybody's Cryptography
53mHansel and Gretel do TLS
29mA Simple Protocol for Remote Attestation of System Integrity
30mDevice Attestation in Hardware TEE based Confidential Computing
19mBoF: Simple Remote Attestation with Secure & Attested Communication Channels