Formal verification of the W3C web authentication protocol
Formal verification of the W3C web authentication protocol
复制标题
W3C Web 身份验证协议的形式化验证
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
H. Halpin
中科院分区：
文献类型：
--
作者：
Iness Ben Guirat;H. Halpin
安全科学可以通过协议的正式验证建立在坚实的基础上。新协议可以以机械化的方式验证其设计是否存在安全缺陷，从而允许以中立的方式对协议设计进行科学比较。鉴于这些技术已经发现了TLS 1.2等协议中的关键缺陷，并且现在正在用于重新设计TLS 1.3等协议，我们将演示如何使用形式验证来分析新协议，如W3C Web身份验证API。我们使用形式化验证语言ProVerif对W3C Web认证进行建模，表明协议本身是安全的。然而，我们也延伸了形式验证的边界，试图验证的隐私属性的W3C Web认证的同源策略。我们使用ProVerif来表明，如果规范中没有进一步的强制性要求，所声称的隐私属性就不成立。接下来的步骤，如何正式验证可以进一步集成到标准和进一步发展的隐私属性的W3C Web认证的概述。
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.