Formal verification of the W3C Web Authentication Protocol

Iness Ben Guirat (1) , Harry Halpin (2)

1 INSAT - Institut National des Sciences Appliquées et de Technologie [Tunis]
2 PROSECCO - Programming securely with cryptography

The science of security can be set on rm foundations via the formal verication of protocols. New protocols can have their design validated in a mechanized manner for security aws, allowing protocol designs to be scientically compared in a neutral manner. Given that these techniques have discovered critical aws in protocols such as TLS 1.2 and are now being used to redesign protocols such as TLS 1.3, we demonstrate how formal verication can be used to analyze new protocols such as the W3C Web Authen-tication API. We model W3C Web Authentication with the formal verication language ProVerif, showing that the protocol itself is secure. However, we also stretch the boundaries of formal verica-tion by trying to verify the privacy properties of W3C Web Authen-tication given in terms of the same origin policy. We use ProVerif to show that without further mandatory requirements in the speci-cation, the claimed privacy properties do not hold. Next steps on how formal verication can be further integrated into standards and the further development of the privacy properties of W3C Web Authentication is outlined.

Domaines: Cryptographie et sécurité [cs.CR]

Iness Ben Guirat, Harry Halpin. Formal verification of the W3C Web Authentication Protocol. HoTSoS '18 : 5th Annual Symposium and Bootcamp on Hot Topics in the Science of Security, Apr 2018, Raleigh, United States. pp.1-10, ⟨10.1145/3190619.3190640⟩. ⟨hal-01966563⟩