Interactive tutorial: Towards formal verification of attested TLS

Tentative outline (subject to change based on attendees interest)

  • Overview of attestation 

    • RATS architecture 

  • Overview of TLS 

  • Overview of attested TLS 

  • Intro to formal verification

  • Formal verification of attested TLS

    • RA-TLS in RATS background-check model

  • Intention is: 

    • To share our “attested TLS” journey to help “attestation over EDHOC” ID make progress by learning the design concepts (without going into mathematical jargon)

Slides

Attendees

  • Muhammad Usama Sardar

  • Göran Selander

  • Mališa Vučinić

  • Yuxuan Song

  • Carsten Bormann

  • Göran Selander

  • John Mattsson

  • Abhishek Kumar

  • Benjamin Lion