Formal Verification of the W3C Web Authentication Protocol

Properties

Submitted by Katie Dey on Tue, 03/27/2018 - 4:12pm. Contributors:

BIO

Iness Ben Guirat received her Engineering degree in 2017 at INSAT, National Institute of Applied Science and Technology, within the Mathematics-Informatics Department. She did her end-of-year project with IRI in which she collaborated with INRIA Paris as part of the NEXTLEAP Project. She is a Thomas Jefferson alumna; the Thomas Jefferson Program is sponsored by the U.S. Department of State’s Bureau of Educational and Cultural Affairs (ECA). Her background spans a diverse range of disciplines: programming, web design, cryptography, and project management.

ABSTRACT

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