fyi: Formal verification of the W3C web authentication protocol

Formal verification of the W3C web authentication protocol
Iness Ben Guirat, Harry Halpin
https://dl.acm.org/citation.cfm?id=3190640

ProVerif code: https://github.com/hhalpin/weauthn-model

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.

Received on Friday, 26 October 2018 17:51:42 UTC