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.