白泽带你读论文 | A Formal Analysis of the FIDO UAF Protocol

    本文发表于NDSS 2021,第一作者是来自北京邮电大学的Haonan Feng。

    传统验证安全协议是否存在漏洞的方法，主要依赖于设计者的经验和人工分析。这种方式难以全面高效地找出安全协议设计存在的漏洞，而形式化分析通过数学和计算机相结合的方式，可以弥补人工分析的不足。

    作者借助形式化分析工具ProVerif，开发了工具UAFVerif对当前应用广泛的FIDO UAF协议安全进行形式化验证。文章指出了UAF协议在设计中存在的问题，分析出了4种攻击方式，并完成了部分攻击的验证且获得了相应的CNNVD编号。最后作者还对UAF协议提出了改进建议。

    UAF协议允许在线服务器提供无口令和多因子的安全验证方式。用户通过选择本地鉴别机制，例如指纹认证和输入 PIN 码等，将设备注册到在线服务。近年来，UAF协议被广泛应用，但是其安全隐患未被全面地进行形式化分析。

    整体来说，UAF协议包括两个阶段：认证器注册(authenticator registration)和认证(authentication)阶段。在用户通过了文本密码校验后，会进入下图所示的认证器注册阶段：

    在后续的认证过程中，用户可以不输入密码，直接通过指纹认证器解答服务端的挑战值的方式进行认证：

    具体来说，上述两个阶段的流程图和涉及到的字段如下图所示：

    现有工作没有对FIDO的安全假设和目标进行形式化描述，且相关工作对FIDO的研究主要集中在U2F上，攻击模型更简单，建模方式较简单。

    对FIDO UAF协议进行形式化分析有如下挑战：

（1）UAF协议中存在不同类型的认证器；

（2）UAF有不同的应用场景，包括首次登录（不存在用户会话）和递进式鉴别场景（已经存在用户会话）；

（3）UAF协议中存在多实体交互，各个实体都可能是恶意的。

    这些挑战需要作者详细建模各种类型场景以及改进现有的形式化分析工具以支持恶意实体的模拟。

    作者的整体分析思路如下图所示。在形式化翻译出UAF标准文档后，作者制定安全目标和安全假设，并进行形式化建模（基于ProVerif工具实现）和安全目标可满足性分析，最终得出最小的安全假设。

    作者Threat Model的假设有：

（1）加密算法是安全的；

（2）攻击者不能窃听、拦截或操纵合法实体之间建立的通道上的通信，但攻击者可以安装恶意实体来发起和接受通信请求；

（3）攻击者已知协议中的身份标识和公钥，可能已知私钥或其它机密字段，例如skAU和CNTR。攻击者已知不同的机密字段将构成不同的安全假设以进行后续的安全目标验证；

（4）因为大量的认证器可能共享相同的AAID和skAT，假设攻击者可能有一个与用户的AAID和skAT相同的认证器，攻击者可以用它来计算签名并通过RP的认证。

    作者指定的安全目标有三个方面：

（1）机密性目标，即UAF协议中涉及到的私钥的机密性，交易文本的机密性和计数器等数据的机密性；

（2）认证性目标，作者参考Lowe提出的认证性分类标准，分析是否满足单射协议和非单射协议等；

（3）隐私性目标，分析互相勾结的服务方是否能将同一用户的不同会话都关联到该用户。

    ProVerif工具可以证明可达性(reachability property)，一致性断言(correspondence assertion)和可观察的等价性(observational equivalence)，分别对应UAF安全目标中的机密性目标(Confidentiality)，认证性目标(Authentication)和隐私性目标(Unlinkability)。

    作者基于ProVerif实现的UAFVerif工具识别最小安全假设的思路是：先确定一个可变的安全假设集A（初始为空集），然后UAFVerif将安全假设ai加入集合A并触发ProVerif来分析该协议是否满足这些安全假设下的安全属性。UAFVerif首先验证一个单一的安全假设，然后是2个假设的所有组合，以此类推。当安全属性的状态由不满足变为满足时，最小的安全假设要求被记录下来。

    作者根据认证器是否嵌入用户设备（B/R），是否为多因素（1/2），将认证器的种类划分为了4种（1B,2B,1R,2R）。这4种认证器的区别以及作者形式化分析出的最小安全假设如下图所示：

    作者通过分析发现：

（1）KHAccesstoken机制是无效的，攻击者可以容易地计算出token值或者通过拦截得到token值并伪造ASM与认证器通信；

（2）注册阶段比认证阶段更容易受到攻击，主要体现在超过100,000个认证器可以共享相同的鉴证密钥和认证器ID，且依赖方信任任何合法的认证器；

（3）UAF协议满足不可链接性且能够抵御钓鱼攻击。

    作者基于上述安全分析，总结出了4种攻击方式：

（1）认证器重绑定攻击，在注册阶段将用户的账户绑定在攻击者的认证器上，并仿冒用户；

（2）平行会话攻击，在认证阶段使用用户的认证器为攻击者的认证挑战进行签名，并仿冒用户；

（3）隐私揭露攻击，通过破坏CNTR和Tr字段的机密性，泄露用户的认证和交易次数；

（4）DoS攻击，通过恶意伪造的实体阻止用户登录。

    作者成功在京东金融和中国移动支付两个应用上复现攻击。获得一个CNNVD编号，CNNVD-202005-1219。

1. 在规范中以更明确和积极的方式提出安全要求和目标；

2. 修改KHAccessToken机制，以保证ASM和认证器运行环境的安全；

3. 在规范中为CallerID制定一个标准的ASM访问控制机制；

4. 在UAF协议涉及到的实体之间引入额外的验证机制，例如要求UA对UC进行认证。

    本文形式化地分析了UAF协议，建模了该协议的安全假设和目标，提供了该协议的形式化模型。基于ProVerif实现了工具UAFVerif来分析了不同场景下的协议并确定了UAF协议的每个安全目标所需的最小安全假设。最后，作者通过分析最小安全假设的结果，提出了该协议的缺陷并归纳出了4种攻击方式，同时还提供了一些建议以解决所发现的问题。

原文始发于微信公众号（复旦白泽战队）：白泽带你读论文 | A Formal Analysis of the FIDO UAF Protocol