【网络安全研究进展系列】FIDO UAF协议的形式化分析

安全协议是以密码学为基础的消息交换协议，它被广泛地应用在信息系统之间的加密传输、消息和实体认证、密钥分配等方面，对保障网络中各种通信、交易的安全运行起着十分关键的作用。

然而，正是这样一个以保障安全为目的的安全协议，其自身却不一定安全。常见的安全协议，如TLS协议、蓝牙协议和WiFi协议等都被发现存在漏洞。安全协议的漏洞将导致隐私信息泄露，甚至造成财产损失。

依靠人工制定和分析协议只能在一定程度上加强协议的安全性，无法保证协议是安全的。形式化分析技术借助数学和计算机技术，解决了人工分析面临的难题。计算机的参与让协议分析变得便捷、高效和自动化。借助数学原理，还能实现安全性的证明。

现有的协议形式化分析技术主要有3种。逻辑推理技术基于知识和信念推理，通过逻辑学的基本原则，从系统初始状态、接收和发送的消息出发，构建用户的信念或知识，并通过一系列的推理公式推导出新的信念和知识，最终判断协议是否满足安全目标，如BAN逻辑、GNY逻辑等。模型检测技术主要利用有限状态机理论，通过状态空间搜索方法来检测协议安全性。定理证明技术将需要证明的安全目标以定理的形式进行描述，通过定理推导来证明协议是否满足安全属性。

结合这3种技术，目前出现了很多形式化分析工具，如ProVerif、Tamarin、Scyther、AVISPA等。通过将自然语言的协议文档，翻译为形式化分析工具可以接受的形式化模型和代码，并将其导入形式化分析工具，工具就可以自动证明安全目标，或构建攻击路径。在本文的分析过程中，我们选择了ProVerif形式化分析工具。

形式化分析技术在提出的30多年来，已经被应用在大量的协议分析中，除了常见的TLS协议、5G协议等，还包括文件系统的协议验证和医疗领域的协议验证。

FIDO UAF协议作为当下流行的生物因子身份认证协议，已经被大量应用。目前对UAF协议的分析仅限于人工分析，还没有相关的形式化分析，所以本文将使用形式化分析技术对UAF协议进行分析验证。

身份认证在保障互联网信息安全中起到了至关重要的作用。当下，基于文本的密码仍旧是最普通的身份验证方式，但是这种验证方式存在严重的安全缺陷，并且成为了黑客主要的攻击对象之一。每年都有数以亿计的密码被攻破，导致许多用户账户陷入危险。

为了提高身份认证的安全性，近20年出现了很多有效的方法，其中，于2012年成立的快速线上身份认证（FIDO）联盟获得了广泛的关注。截至2021年2月，超过250家公司已经成为FIDO联盟的成员，市场上已有超过700种经过FIDO认证的产品。

FIDO包括两种基本的认证协议，一个是双因子认证协议U2F协议，在认证时，它要求用户在输入密码的同时提供第二个验证因子，如U盾。另一个是通用认证框架UAF协议，它借助生物因子验证技术，彻底取代传统的文本密码登录。

UAF协议分为注册和认证两个阶段，如图1所示（原图来源于FIDO官网）。在注册阶段，用户首先使用传统的密码方式登录到依赖方，如银行网站。用户的设备中内置一个可信的认证器，它能够记录用户的指纹，并生成专属于用户账户的认证签名密钥对，认证器会使用预先内置的鉴证密钥的私钥签名生成的认证密钥的公钥部分，并发送给依赖方，依赖方会将该公钥与用户的账户进行关联，并与认证器建立信任关系。在随后的认证阶段，认证器和依赖方会运行一个挑战-响应协议，用户只需要在认证器本地验证自己的身份，随后认证器会解锁注册阶段生成的认证签名密钥私钥，并对依赖方发送的响应等信息进行签名，来完成身份验证。

 图1

对UAF协议进行形式化分析有如下几个难点。

（1） UAF协议的描述，以及安全目标、安全假设需要从19个文档共500多页中提取。很多安全假设和安全目标的表述并不清晰，需要花很多时间去整理并将它们提取出来。

（2） 虽然UAF协议只包含两个阶段（注册和认证），但是UAF协议支持使用不同类型的认证器，它们会影响协议的具体流程，例如绑定认证器可以内置在手机中，漫游认证器可以便携使用，使用这两种类型的认证器时，协议流程不同。

（3）在不同的认证场景下，协议的交互也不同。例如，在用户首次登录时，依赖方不提供用于定位密钥的KeyID，而在已经登录过，需要再一次进行身份验证时，依赖方提供KeyID。

（4）和很多常见的安全协议不同，为了部署UAF协议，用户设备中需要增加额外的UAF实体，如认证器、ASM和UAF客户端等。这增加了协议交互的复杂度，使分析变得更加困难。

（5）传统协议一般运行在公开网络下，在进行协议分析时，通常假设攻击者符合Dolev-Yao模型，即攻击者可以窃听、拦截消息，存储、转发消息，主动构造并发送消息，以及假冒合法主体参与协议。但是，由于UAF协议中，大多数实体和他们之间的通信都在设备内部，用户代理和依赖方服务器之间的通信又受到TLS的保护，因此实体之间的交互在一定程度上受到保护。为此，不能单纯地使用Dolev-Yao模型，需要特意为UAF协议的运行环境构建合适的攻击者模型。

版权声明：本书由网络安全研究国际学术论坛（InForSec）汇编，人民邮电出版社出版，版权属于双方共有，并受法律保护。转载、摘编或利用其它方式使用本研究报告文字或者观点的，应注明来源。