CCS 2017 - Session 4H

Formal Verification

Thursday, 9:00-10:30am

Session chair: Dinghao Wu

A Comprehensive Symbolic Analysis of TLS 1.3

Cas Cremers (University of Oxford), Marko Horvat (The Max Planck Institute For Software Systems), Jonathan Hoyland (Royal Holloway, University of London), Sam Scott (Royal Holloway, University of London), Thyla van der Merwe (Royal Holloway, University of London)

[PDF]
[Paper]
[Artifact]

HACL*: A Verified Modern Cryptographic Library

Jean-Karim Zinzindohoué (Inria Paris), Karthikeyan Bhargavan (Inria Paris), Jonathan Protzenko (Microsoft Research), Benjamin Beurdouche (Inria Paris)

[PDF]
[Paper]
[Artifact]

Jasmin: High-Assurance and High-Speed Cryptography

José Bacelar Almeida (HASLab – INESC TEC / Universidade do Minho), Manuel Barbosa (HASLab – INESC TEC / DCC FC Universidade do Porto), Gilles Barthe (IMDEA Software Institute), Arthur Blot (ENS Lyon), Benjamin Grégoire (Inria), Vincent Laporte (IMDEA Software Institute), Tiago Oliveira (HASLab – INESC TEC / Universidade do Minho), Hugo Pacheco (HASLab – INESC TEC / Universidade do Minho), Benedikt Schmidt (IMDEA Software Institute), Pierre-Yves Strub (Ecole Polytechnique)

[PDF]
[Artifact]