TLS协议的生物特征认证扩展与形式化安全分析

Biometric Authentication Extension for TLS and Formal Security Analysis

摘要

当前客户端身份认证主要有两种方式：传输层安全协议（TLS）和基于TLS协议的上层应用层身份认证方法。现有的TLS协议广泛应用于服务器端身份认证，但其客户端认证因存在证书管理复杂、易受攻击等问题而较少被强制要求使用；基于上层的身份认证存在易遗忘、单点认证、依赖固件和兼容性差等问题。为了解决这些问题，利用TLS协议支持扩展的特征，设计了Bio-TLS扩展协议，将用户的生物特征作为身份认证因子，选取指纹信息作为样例，与TLS结合，在握手阶段实现跨设备的无感认证。通过Tamarin Prover工具进行全自动形式化建模和安全性分析，验证了扩展协议的安全目标。实验结果表明，Bio-TLS协议有效提升了客户端身份认证的安全性，为用户提供了一种更安全、便捷的认证方式。

Abstract

The current client authentication mainly has two methods: Transport Layer Security (TLS) and application-layer authentication methods based on TLS. The existing TLS protocol is widely used for server authentication, but its client authentication is less commonly enforced due to issues such as complex certificate management and vulnerability to attacks. Application-layer authentication has problems such as forgetfulness, single-point authentication, dependency on firmware, and poor compatibility. To solve these problems, we design an extension to the TLS protocol—Bio-TLS, which uses biometric features as an authentication factor, and selects fingerprint information as an example. It integrates with TLS to achieve seamless cross-device authentication during the handshake phase. Formal modeling and security analysis of the extended protocol are conducted using the Tamarin Prover tool to verify its security objectives. Experimental results show that the Bio-TLS protocol effectively enhances the security of client authentication, providing users with a more secure and convenient authentication method.

Graphical abstract

关键词

客户端身份认证 / 生物特征认证 / 传输层安全协议（TLS） / 扩展 / 形式化分析

Key words

client identity authentication / biometric authentication / Transport Layer Security(TLS) / extension / formal analysis

0　 引 言

随着互联网的飞速发展，全球网民数量已达到惊人规模。据统计^[1]，目前互联网上存在近40亿用户和10亿个网站，已形成了一个庞大的在线社区。客户端身份认证技术用于确认用户的真实身份，防止未经授权的访问，从而保护用户的上网安全。近年来，网络攻击和数据泄露事件频发，严重威胁用户隐私和财产安全。作为网络安全的第一道防线，客户端身份认证的安全性对整个网络环境的保护至关重要。

当前客户端身份认证主要有两种方式：一种是传输层安全协议（Transport Layer Security, TLS）的客户端证书身份认证，客户端使用可信第三方证书颁发机构发放的证书证明自己的身份；另外一种是基于TLS的上层应用层身份认证方法，结合传统身份认证方式和生物特征认证技术，提供更强的客户端认证安全性。

TLS协议历经多代优化，目前最新最安全的版本是1.3，其规范由RFC 8446^[2]定义。该协议使用X.509证书，依赖通信双方所选的公钥系统进行身份认证。目前，部分研究者专注于服务器端证书生态系统^[3-5]，研究了服务器端证书的部署、管理、吊销和存在的漏洞等安全问题。同时，部分研究者关注客户端证书生态系统，研究了客户端证书部署和使用中存在的问题，以及用户信息可追溯性带来的隐私泄露问题^[6-7]。这些研究在增强TLS协议安全性方面发挥了重要作用。

基于TLS的上层应用层身份认证技术可分为传统认证与生物认证两种方式。传统认证依靠用户预先知晓的秘密信息（如用户序列号、静态或动态口令）或者用户持有的实体设备（如智能卡、U盾和令牌等）完成认证；生物认证则基于用户独有的生物特征（如指纹、虹膜或面部特征）实现身份验证。当前，身份认证多采用以用户名和口令认证为主，指纹识别或人脸识别等生物认证为辅的多因子身份认证方案^[8]，常取“用户所知”与“用户所拥有”作为身份认证因子。

尽管两种认证方式在一定程度上保障了客户端认证，但仍都存在一些安全问题。

针对TLS认证：1） 由于证书的部署和管理复杂性，且需兼顾用户体验和便利性，当前的TLS协议主要专注于认证服务器端的身份，对客户端身份认证的强制要求相对较少；2） 恶意用户可能通过伪造客户端证书等手段绕过TLS协议的客户端认证^[9-10]，实施未经授权的访问或中间人攻击。针对基于TLS的上层应用层传统身份认证：1） 传统方法主要依赖用户的知识和持有的物理设备，高频率的认证需求导致口令重复使用、易破解、易丢失、难管理，以及物理设备丢失从而阻碍身份认证等安全问题。例如，Gupta等^[11]和Kim^[12]所提出的将智能卡与生物特征相结合的认证方案，均存在对智能卡的过度依赖，未充分考虑智能卡丢失或生物特征隐私泄露等风险，且未提供有效的应对措施。2） 当前身份认证技术缺乏统一的标准和协议，存在身份认证方案质量参差不齐、各自独立且数据无法互联互通等问题，同时也限制了不同身份认证产品之间的兼容性，增加了安全分析的复杂性。

为了解决客户端身份认证存在的安全问题，本文设计了一种基于生物特征认证的TLS扩展协议方案，以指纹信息作为TLS的可选扩展。方案设计需考虑以下问题：

1) 兼容性：需确保扩展与TLS协议的兼容性和互操作性，且扩展的功能对现有TLS协议不会造成冲突或不稳定性，兼容当前的TLS协议并向后兼容。

2) 生物特征信息管理：方案需支持多设备认证场景，并确保可信生物信息的注册安全和隐私保护，实现跨设备指纹认证。

3) 指纹信息被恶意窃取的风险：KnowBe4《2023年网络钓鱼行业基准报告》显示，约有三分之一的用户易受骗点击可疑链接或响应欺诈行为。当用户因误操作被恶意软件感染时，可能面临指纹信息被盗风险，攻击者可借此冒充合法用户。方案需确保即使指纹信息被盗，攻击者也无法完成认证。

4) 安全性分析：TLS是一个复杂的体系，且指纹引入的更改可能会破坏TLS的安全性。因此需构建完整的形式化模型，验证扩展协议满足TLS安全目标，并定义和证明新安全目标的安全性。

因此，本文进行了如下研究：

1) 设计TLS握手协议的生物特征认证扩展（Biometrics-Authenticated TLS Extension, Bio-TLS)。用户通过安全途径（如线下或短期通道）使用原有的身份认证方式（如唯一用户标识、口令）完成认证后，注册指纹信息，在智能设备上，通过指纹的质询-响应方式实现TLS握手阶段的身份认证，支持跨设备无感认证。

2) 引入了迪菲-赫尔曼密钥交换（Diffie-Hellman, DH）棘轮算法^[13]对合法设备进行绑定。每次身份认证，都需要使用上一轮认证过程中DH密钥交换生成的共享秘密，确保即使攻击者窃取了用户的指纹和设备ID，也无法冒充用户完成身份认证，保证了指纹认证的后妥协安全（Post Compromise Security, PCS）。

3) 使用先进的自动化符号分析工具Tamarin Prover，对Bio-TLS进行形式化建模，提取规范中的安全目标，为扩展协议设定新的安全目标，对扩展后的协议进行了全面的分析，实现了对安全目标的全自动验证。

1　 背景知识

1.1　TLS协议

TLS协议用于在客户端和服务器端之间构建一条安全的通信信道。本文重点关注握手协议，它定义了客户端和服务器端之间首次建立安全通信连接的过程，为后续传输的应用数据提供完整性和保密性。握手协议分为3个阶段：协商参数、认证服务器和交换应用数据，如图1所示，具体过程如下。

1) 协商参数：首先双方协商它们共同支持的参数。客户端发送ClientHello消息，该消息主要包括随机数和支持的密码套件列表，而服务器端选择合适的算法，并发送ServerHello。

2) 认证服务器：服务器端随后发送4个加密的握手消息，用于证明自己的身份：Extensions包含未在ServerHello中发送的其他参数；Certificate包含服务器端的公钥证书；CertVerify包含使用服务器端的私钥对迄今为止的握手记录进行签名；Finished包含使用MAC密钥对迄今为止的握手记录的哈希值。Certificate和CertVerify消息用于对服务器端进行身份认证，而Finished提供了密钥和记录的确认，遵循基于签名和消息认证码的密钥交换协议中经典的SIGn-and-MAc协议^[14]设计模式。在此之后，客户端回应并发送自己的Finished消息。一经客户端发送Finished，握手阶段已经结束。此时，客户端和服务器端已经生成了用于后续加密应用程序数据的会话密钥。

3) 交换应用数据：双方使用会话密钥交换应用程序数据。

1.2　TLS协议的扩展

为增强TLS协议的灵活性、功能扩展性和互操作性，互联网工程任务组(Internet Engineering Task Force, IETF)引入了TLS扩展机制^[15]。扩展允许客户端和服务器端协商选择支持的扩展功能^[16-19]，使得TLS协议能够适应不同的应用场景和安全要求。

1.3　TLS协议的安全属性

本文考虑TLS1.3规范要求的6个安全属性：

1) 建立相同的会话密钥：握手完成后，应建立一组双方同意的会话密钥。

2) 会话密钥的保密性：握手完成后，应建立一组仅双方知道的会话密钥。

3) 对等身份认证：在握手完成时，如果客户端认为它正在与服务器端通信，且的确是该服务器端与其进行了TLS通信，即客户端对其通信对等方身份的认知应与服务器的实际身份一致。

4) 会话密钥的唯一性：每次都应该产生不同的、独立的会话密钥。

5) 完美前向保密：如果任何一方的长期密钥被泄露，已完成的会话应该仍然保持安全。

6) 密钥妥协欺骗抵抗：即使攻击者获取了A方的长期密钥，攻击者也不能冒充A方与诚实的另一方进行通信。

1.4　Tamarin Prover符号模型工具

Tamarin Prover^[20]（简称Tamarin）是一种用于密码协议的符号建模和分析的工具，可以自动地分析协议的安全属性是否得到满足，已广泛应用于多个现实协议的分析，如5G^[21]、蓝牙^[22]和EMV^[23]等协议。它的验证算法基于约束求解和多集重写技术，允许用户在有分支和循环的复杂协议中证明复杂的安全属性，并且包含图形用户界面，可以实现证明的可视化和交互式构造。它将待证明的建模协议和安全属性作为输入，并输出建模协议是否满足安全属性，从而证明安全属性是否得到满足。

1) 建模协议：Tamarin使用多集重写规则将通信过程定义为标记迁移系统。协议的运行状态由若干“事实”组成的多重集合表示，系统初始状态为空。每条规则由一个规则名称和三个组成部分（左侧、动作和右侧）构成。仅当规则左侧的所有事实在当前状态下可用时才能执行该规则。当执行规则时，它将消耗左侧的事实，即将它们从状态中删除，并生成右侧的事实，即将它们添加到状态中。动作事实不会影响转换，用于标记转换。当规则被触发时，动作会被“记录”下来，作为路径上可观测的事实，用于定义限制或表达安全属性。事实一般只能消耗一次，但以“!”符号开头的事实视为持久性事实可以消耗任意次。在Tamarin中内置了三种特定类型的事实，Fr()、Out()和In()事实。其中，Fr事实表示生成一个新的（随机的）值，Out()事实表示将一条消息发送到公共通道，In()事实表示从公共通道接收一条消息。以规则Example为例：

rule Example:

[Fr(~k), Fr(~m)]

--[Send(~m)]->

[Out(senc(~m, ~k))]

该规则的名称为Examlple，左侧包含两个Fr事实，动作是自定义的事实Send，右侧是Out事实。只有当左边部分的所有事实均出现在当前状态时，Tamarin才能使用该规则进行状态转移。该规则定义了参与者使用对称加密函数Senc和密钥k加密消息m，并将密文c发送到公共通道。

2) 安全属性：安全属性由基于动作事实和时间点的一阶逻辑公式定义的一组轨迹来表示，即Tamarin的属性规范是一种带有时间点类型的多类型一阶逻辑的受限片段，这种逻辑支持对消息和时间点进行量化处理。具体来说,这套逻辑允许表达和认证诸如在某个时间点发生了某个动作或某个消息在某个时间点被发送等性质。以引理Secrecy为例,该引理定义了一个简单的保密属性，表明每当Secret(x)动作在时间点i发生时，敌手在任意时间点j都不能获得x。

lemma Secrecy

“All x #i. Secrect(x)@i

=> not (Ex #j. K(x)@j)”

3) 攻击者能力：Tamarin使用Dolev⁃Yao攻击者模型作为内置攻击者模型。攻击者完全控制网络，可以拦截、发送、重放和删除任何消息。攻击者可以组合学到的任何信息构造出新的消息发送至网络。

Tamarin可以通过构造额外的攻击者能力来增强或削弱攻击者的能力，如允许妥协协议参与者的长期密钥,或构造安全通信信道来削弱攻击者的能力。

4) 证明：对于给定的安全属性，Tamarin的目标是找到与该属性相矛盾的模型执行跟踪路径，或者验证所有可能的模型执行满足该属性。若可以找到违背该属性的一条执行路径，则说明存在攻击，引理不成立；否则证明引理成立。

2　 Bio-TLS协议系统模型

2.1　系统架构

如图2所示，系统主要涉及四个实体：用户、服务器端、智能设备上的指纹处理器和客户端。诚实用户在设备上按下自己的指纹，设备上的指纹处理器在可信环境中处理指纹信息，客户端利用指纹信息，在TLS握手阶段协助服务器端对用户身份的认证。

用户：在智能设备上选择使用指纹信息进行TLS握手阶段的身份认证。在第一次进行指纹认证之前，用户需要使用传统的用户名和密码完成认证和指纹的注册，负责输入指纹、用户名和密码。

指纹处理器：负责采集用户的指纹信息，将采集到的指纹数据经过处理后生成一对公私钥(Fp_sk,Fp_pk)和指纹标识符\mathrm{F}\mathrm{i}\mathrm{d}，将他们存储在可信环境中，公钥和标识符可以公开使用，而私钥应保持机密，并采取适当的措施防止未授权访问。同时负责对服务器端发送的挑战进行回应，生成证明身份的指纹签名，将指纹公钥和标识符一同发送给客户端。

设备上的客户端：负责与服务器端建立TLS握手连接，生成TLS握手协商与身份认证的材料。并负责转发设备与服务器端之间的指纹认证的挑战与应答信息。

服务器端：负责与客户端建立TLS握手连接，生成TLS握手协商与身份认证的材料，并负责与用户进行指纹身份认证，生成用于指纹认证的挑战值。

2.2　威胁模型和安全假设

Bio-TLS协议系统的威胁模型如下：

1) Dolev⁃Yao攻击者模型；

2) 恶意攻击者：基于Dolev⁃Yao模型，引入了更强大的攻击者能力，具体如下：

a. 在完成一次握手后，攻击者可以妥协协议参与者的长期密钥；

b. 在完成一次握手后，攻击者可以妥协握手过程产生除棘轮算法生成的轮密钥外的所有密钥。

允许攻击者妥协用户，远程获取用户的指纹信息，并尝试假冒用户进行身份认证。

本文在该威胁模型中做出以下假设：

1) 完美密码学：加密方案是完美的黑匣子，攻击者在不拥有密钥的情况下无法从加密消息中学习任何内容。

2) 证书管理机构(Certificate Authority, CA)：CA为服务器端签发证书的通信通道是安全的。

3) 诚实的实体：用户、指纹处理器、客户端以及服务器端都是诚实实体，不会主动妥协。

4) 物理攻击：攻击者无法物理访问用户的设备和获取用户传统认证口令。

5) 指纹采集与传输：设备在安全环境中完成指纹采集，指纹信息安全地存储在设备上。指纹处理和传输过程是安全的。

2.3　安全目标

除TLS 1.3规范中要求的安全目标外，本文对扩展后的协议定义了新的必要的安全目标，所有目标都是针对诚实且经过身份认证的客户端和服务器端之间的消息交互。

1) 指纹信息的保密性：系统应保护用户的指纹信息。即使攻击者获取了认证身份的信息，也不能够获取用户的原始指纹信息。

2) 指纹信息的认证性：指纹信息与用户之间存在一对一的映射关系，只有持有与其指纹信息相匹配的合法用户才能成功完成身份认证。

3) 会话的后妥协安全：PCS是服务器端对客户端的安全保证，即服务器端与客户端通信的安全性可以在客户端妥协后被恢复。即使攻击者妥协了当前会话中客户端的会话密钥，也无法解密所有未来的通信内容。前提是服务器端需要恢复阶段。

2.4　形式定义

TLS握手协议的生物特征认证扩展方案中主要包括以下10个多项式时间算法：

定义1（指纹签名算法） 输入用户私钥\mathrm{F}{\mathrm{p}}_{\mathrm{s}\mathrm{k}}和随机数\mathrm{b}\mathrm{i}\mathrm{o}\mathrm{r}，输出对随机数的签名\sigma，即：

\mathrm{S}\mathrm{i}\mathrm{g}{\mathrm{n}}_{\mathrm{F}{\mathrm{p}}_{\mathrm{s}\mathrm{k}}}\left(\mathrm{b}\mathrm{i}\mathrm{o}\mathrm{r}\right)=\sigma(1)

定义2（指纹认证算法） 输入签名\sigma、被签名的随机数\mathrm{b}\mathrm{i}\mathrm{o}\mathrm{r}和用户公钥\mathrm{F}{\mathrm{p}}_{\mathrm{p}\mathrm{k}}，当\sigma是一个有效的签名时，输出1；否则，输出0，即：

\mathrm{V}\mathrm{e}\mathrm{r}\mathrm{i}\mathrm{f}\mathrm{y}\left(\mathrm{S}\mathrm{i}\mathrm{g}{\mathrm{n}}_{\mathrm{F}{\mathrm{p}}_{\mathrm{p}\mathrm{k}}}\left(\mathrm{b}\mathrm{i}\mathrm{o}\mathrm{r}\right),\mathrm{F}{\mathrm{p}}_{\mathrm{p}\mathrm{k}}\right)=\mathrm{0}/\mathrm{1}(2)

定义3（证书签名算法） 输入服务器端私钥\mathrm{S}{\mathrm{k}}_{\mathrm{S}}和消息m，输出正确的签名\sigma，即：

\mathrm{S}\mathrm{i}\mathrm{g}{\mathrm{n}}_{\mathrm{S}{\mathrm{k}}_{\mathrm{S}}}\left(m\right)=\sigma(3)

定义4（证书生成算法） 输入服务器端的长期公私钥\mathrm{P}{\mathrm{k}}_{\mathrm{S}},\mathrm{S}{\mathrm{k}}_{\mathrm{S}}，输出证书\mathrm{C}\mathrm{e}\mathrm{r}{\mathrm{t}}_{\mathrm{S}}，即：

\mathrm{C}\mathrm{e}\mathrm{r}\mathrm{t}\mathrm{i}\mathrm{f}\mathrm{i}\mathrm{c}\mathrm{a}\mathrm{t}\mathrm{e}\left(\mathrm{P}{\mathrm{k}}_{\mathrm{S}},\mathrm{S}\mathrm{i}\mathrm{g}{\mathrm{n}}_{\mathrm{S}{\mathrm{k}}_{\mathrm{S}}}\left(\mathrm{P}{\mathrm{k}}_{\mathrm{S}}\right)\right)=\mathrm{C}\mathrm{e}\mathrm{r}{\mathrm{t}}_{\mathrm{S}}(4)

定义5（证书认证算法） 输入签名\sigma,签名消息m和服务器端公钥\mathrm{P}{\mathrm{k}}_{\mathrm{S}},当\sigma是一个关于m的有效签名时，输出1；否则，输出0，即:

\mathrm{V}\mathrm{e}\mathrm{r}\mathrm{i}\mathrm{f}{\mathrm{y}}_{\mathrm{P}{\mathrm{k}}_{\mathrm{S}}}\left(\sigma ,m\right)=\mathrm{0}/\mathrm{1}(5)

定义6（加密算法） 输入对称密钥k和消息m，输出密文c，即：

\mathrm{E}\mathrm{n}{\mathrm{c}}_k\left(m\right)=c(6)

定义7（消息摘要算法） 输入密钥k和消息m，输出消息m的散列值h，即：

\mathrm{m}\mathrm{a}{\mathrm{c}}_k\left(m\right)=h(7)

定义8（握手密钥导出算法） 输入临时DH共享密钥g^{xy}、客户端随机数rc和服务器端随机数rs，输出握手密钥hs，即

\mathrm{k}\mathrm{d}\mathrm{f}\left(g^{xy},\mathrm{r}\mathrm{c},\mathrm{r}\mathrm{s}\right)=\mathrm{h}\mathrm{s}(8)

定义9（多个密钥导出算法） 输入握手密钥\mathrm{h}\mathrm{s}和握手转录日志\mathrm{l}\mathrm{o}{\mathrm{g}}_{\mathrm{1}}，输出主密钥\mathrm{m}\mathrm{s}，客户端握手加密密钥k_{\mathrm{C}}^h，服务器端握手加密密钥k_{\mathrm{S}}^h，客户端MAC密钥k_{\mathrm{C}}^m，服务器端MAC密钥k_{\mathrm{S}}^m，即：

\mathrm{k}\mathrm{d}\mathrm{f}\left(\mathrm{h}\mathrm{s},\mathrm{l}\mathrm{o}{\mathrm{g}}_{\mathrm{1}}\right)=\left(\mathrm{m}\mathrm{s},k_C^h,k_S^h,k_C^m,k_S^m\right)(9)

定义10（应用加密密钥导出算法） 输入主密钥\mathrm{m}\mathrm{s}和握手转录日志\mathrm{l}\mathrm{o}{\mathrm{g}}_{\mathrm{1}}，输出客户端应用加密密钥k_c和服务器端加密密钥k_{\mathrm{S}}，即：

\mathrm{k}\mathrm{d}\mathrm{f}\left(\mathrm{m}\mathrm{s},\mathrm{l}\mathrm{o}{\mathrm{g}}_{\mathrm{4}}\right)=\left(k_C,k_S\right)(10)

3　 Bio-TLS扩展协议设计方案

在指纹扩展设计中，考虑了3种不同情况下的认证阶段：指纹注册阶段、新设备注册阶段和指纹认证阶段。在任何情况下，协议设计默认用户的行为是使用指纹进行TLS握手，根据用户信息和设备ID是否已经注册决定服务器端的行为。服务器端的行为包括：同意使用指纹认证客户端身份、拒绝用户使用指纹认证并提示用户注册指纹和拒绝用户使用指纹认证并提示用户注册新设备。本文专注于扩展设计的研究，不考虑0-RTT、PSK模式下的TLS握手过程。在严格遵守协议规范的前提下，简化了握手过程中算法的协商、证书的部署与管理等步骤。

3.1　DH棘轮算法

本文在扩展中加入了DH棘轮算法，与TLS握手中临时DH协商区别开，使用\mathrm{S}\mathrm{k}\mathrm{r}\mathrm{x},\mathrm{P}\mathrm{k}\mathrm{r}\mathrm{x}符号表示DH棘轮共享密钥的协商，算法定义如下：

1) 初始化：在第1轮TLS认证过程中，双方使用DH算法生成DH棘轮密钥对(Skrc₁,Pkrc₁)和(Skrs₁,Pkrs₁)，利用扩展将自己的棘轮公钥发送给对方，双方利用自己的DH棘轮私钥和对方的DH棘轮公钥生成DH共享密钥\mathrm{D}\mathrm{H}{\mathrm{c}}_{\mathrm{1}}=\mathrm{P}\mathrm{k}\mathrm{r}{\mathrm{s}}_{\mathrm{1}}^{\mathrm{S}\mathrm{k}\mathrm{r}{\mathrm{c}}_{\mathrm{1}}}，\mathrm{D}\mathrm{H}{\mathrm{s}}_{\mathrm{1}}=\mathrm{P}\mathrm{k}\mathrm{r}{\mathrm{c}}_{\mathrm{1}}^{\mathrm{S}\mathrm{k}\mathrm{r}{\mathrm{s}}_{\mathrm{1}}}。客户端使用指纹挑战值\mathrm{b}\mathrm{i}\mathrm{o}\mathrm{r}完成一次承诺\mathrm{E}\mathrm{n}{\mathrm{c}}_{\mathrm{D}\mathrm{H}{\mathrm{c}}_{\mathrm{1}}}\left(\mathrm{b}\mathrm{i}\mathrm{o}\mathrm{r}\right)，服务器端认证承诺，完成第一轮认证。客户端存储此轮的DH密钥对，服务器端存储客户端的DH棘轮公钥，用于下一轮DH共享密钥的协商。

2) 在第n轮TLS握手中的使用：客户端存储上轮DH轮密钥对(Skrc _n-1,Pkrc _n-1)，服务器端存储上轮客户端发送的DH轮公钥\mathrm{P}\mathrm{k}\mathrm{r}{\mathrm{c}}_{n-\mathrm{1}}。在发送ServerHello后，服务器端生成此轮的DH轮密钥对(Skrc _n,Pkrc _n )，并生成此轮DH共享密钥\mathrm{D}\mathrm{H}{\mathrm{s}}_n=\mathrm{P}\mathrm{k}\mathrm{r}{\mathrm{c}}_{n-\mathrm{1}}^{\mathrm{S}\mathrm{k}\mathrm{r}{\mathrm{s}}_n}，在扩展中发送DH轮公钥\mathrm{P}\mathrm{k}\mathrm{r}{\mathrm{s}}_n给客户端。客户端收到公钥后，生成DH共享密钥\mathrm{D}\mathrm{H}{\mathrm{c}}_n=\mathrm{P}\mathrm{k}\mathrm{r}{\mathrm{s}}_n^{\mathrm{S}\mathrm{k}\mathrm{r}{\mathrm{c}}_{n-\mathrm{1}}}。DH棘轮算法更新密钥，生成新的棘轮密钥(Skrc _n,Pkrc _n )，将\mathrm{E}\mathrm{n}{\mathrm{c}}_{\mathrm{D}\mathrm{H}{\mathrm{s}}_n}\left(\mathrm{P}\mathrm{k}\mathrm{r}{\mathrm{c}}_n\right)发送给服务器端。服务器端使用\mathrm{D}\mathrm{H}{\mathrm{s}}_n解密得到客户端更新的DH轮公钥\mathrm{P}\mathrm{k}\mathrm{r}{\mathrm{c}}_n，并存储到本地用于下轮TLS握手认证。

通过引入DH棘轮算法，在每轮认证中生成唯一的轮共享密钥，用于已注册的智能设备与服务器端的双向认证，并在每一轮认证完成后迭代更新和存储DH密钥，用于下一轮认证。确保每轮DH认证都基于上一轮的成功认证，达到只有合法用户在自己的智能设备上进行认证才能通过成功认证的目的。即使恶意软件成功远程窃取了用户的指纹和设备信息，由于缺乏上一轮的轮共享密钥，攻击者也无法冒充用户与服务器端进行身份认证，从而保护了用户的身份安全，提高了协议的安全性，有效防止了身份欺骗。

3.2　指纹注册过程

在该过程中，用户使用传统使用的认证方式(如口令)在TLS安全信道上进行用户指纹的注册，包含未注册的用户认证失败和用户注册两个环节，如图3所示。

1) 双方协商参数①~②：客户端首先发送ClientHello和扩展，扩展包含表示客户端支持指纹认证的字符串“f_hold”。服务器端回复ServerHello，扩展包含表示服务器端接受指纹认证字符串“f_accept”。同时，服务器端会生成轮密钥对(Skrc₀,Pkrc₀)，客户端收到ServerHello，完成参数的协商。

2) 认证服务器端的身份③~⑥：服务器端发送一系列加密消息，包括：扩展，即轮公钥\mathrm{P}\mathrm{k}\mathrm{r}{\mathrm{s}}_{\mathrm{0}}和指纹认证随机数\mathrm{b}\mathrm{i}\mathrm{o}\mathrm{r}，Certificate、CertVerify和Finished消息。客户端收到加密握手消息后，认证证书、签名和消息认证码。如果所有认证都成功，客户端生成轮密钥对(Skrc₀,Pkrc₀)，根据服务器端发送的扩展中的服务器端轮公钥\mathrm{P}\mathrm{k}\mathrm{r}{\mathrm{s}}_{\mathrm{0}}，生成轮共享密钥\mathrm{D}\mathrm{H}{\mathrm{c}}_{\mathrm{0}}=\mathrm{P}\mathrm{k}\mathrm{r}{\mathrm{s}}_{\mathrm{0}}^{\mathrm{S}\mathrm{k}\mathrm{r}{\mathrm{c}}_{\mathrm{0}}}。

3) 用户使用指纹认证身份⑦~⑫：客户端将随机数\mathrm{b}\mathrm{i}\mathrm{o}\mathrm{r}发送给指纹信息所在的指纹环境，使用指纹私钥对其进行签名\mathrm{S}\mathrm{i}\mathrm{g}{\mathrm{n}}_{\mathrm{F}{\mathrm{p}}_{\mathrm{s}\mathrm{k}}}\left(\mathrm{b}\mathrm{i}\mathrm{o}\mathrm{r}\right)，与设备标识符\mathrm{F}\mathrm{i}\mathrm{d}、指纹公钥\mathrm{F}{\mathrm{p}}_{\mathrm{p}\mathrm{k}}一并发送给客户端。客户端将签名、\mathrm{F}\mathrm{i}\mathrm{d}和\mathrm{F}{\mathrm{p}}_{\mathrm{p}\mathrm{k}}等信息作为扩展发送给服务器端。服务器端解密收到的信息，从扩展中获取了指纹相关信息，但是由于是首次注册，服务器端的数据库中没有用户的信息，\mathrm{F}\mathrm{i}\mathrm{d}没有存储在指纹数据库中。因此服务器端发送警告信息，告知用户认证失败，请进行注册。

4) 双方再次协商参数⑬~⑭：认证失败后，重新建立连接。并引导用户使用传统的用户名和密码完成认证和指纹的注册。客户端发送ClientHello和扩展，其中扩展中包含“f_register”字符串表示客户端要进行指纹注册。服务器端收到消息后，发送ServerHello和扩展，扩展包含表示服务器端接受指纹注册的字符串“f_regacc”。

5) 认证服务器端身份⑮：服务器端生成轮密钥\left(\mathrm{S}\mathrm{k}\mathrm{r}{\mathrm{s}}_{\mathrm{1}},\mathrm{P}\mathrm{k}\mathrm{r}{\mathrm{s}}_{\mathrm{1}}\right)并发送一系列加密消息。其中扩展包含轮公钥\mathrm{P}\mathrm{k}\mathrm{r}{\mathrm{s}}_{\mathrm{1}}、指纹认证随机数\mathrm{b}\mathrm{i}\mathrm{o}\mathrm{r}\mathrm{\text{'}}和“Enter UN PS”。

6) 用户使用传统方式认证并注册⑯~⑳：客户端完成对服务器端认证后，转发随机数\mathrm{b}\mathrm{i}\mathrm{o}\mathrm{r}\mathrm{\text{'}}，提示用户输入用户名和口令,并生成此轮非对称密钥\left(\mathrm{S}\mathrm{k}\mathrm{r}{\mathrm{c}}_{\mathrm{1}},\mathrm{P}\mathrm{k}\mathrm{r}{\mathrm{c}}_{\mathrm{1}}\right)。根据收到的服务器端轮公钥\mathrm{P}\mathrm{k}\mathrm{r}{\mathrm{s}}_{\mathrm{1}}生成轮共享密钥\mathrm{D}\mathrm{H}{\mathrm{c}}_{\mathrm{1}}=\mathrm{P}\mathrm{k}\mathrm{r}{\mathrm{s}}_{\mathrm{1}}^{\mathrm{S}\mathrm{k}\mathrm{r}{\mathrm{c}}_{\mathrm{1}}}。设备提示用户输入用户名和密码，处理器使用指纹私钥对其进行签名\mathrm{S}\mathrm{i}\mathrm{g}{\mathrm{n}}_{\mathrm{F}{\mathrm{p}}_{\mathrm{s}\mathrm{k}}}\left(\mathrm{b}\mathrm{i}\mathrm{o}\mathrm{r}\mathrm{\text{'}}\right)，并将签名、\mathrm{F}\mathrm{i}\mathrm{d}、\mathrm{U}\mathrm{N}、\mathrm{P}\mathrm{W}和\mathrm{F}{\mathrm{p}}_{\mathrm{p}\mathrm{k}}发送给客户端。客户端收到消息后，将用户信息、签名、\mathrm{P}\mathrm{k}\mathrm{r}{\mathrm{c}}_{\mathrm{1}}和\mathrm{E}\mathrm{n}{\mathrm{c}}_{\mathrm{D}\mathrm{H}{\mathrm{c}}_{\mathrm{1}}}\left(\mathrm{b}\mathrm{i}\mathrm{o}\mathrm{r}\mathrm{\text{'}}\right)发送给服务器端。服务器端解密Finished，认证用户身份后，对签名的指纹信息和共享密钥进行认证。

7) 认证完成21：认证通过后，服务器端发送新会话票据(NewSessionTicket, NST)，将〈Fid,Did,Fp_pk,Pkrc₁,NST〉与〈UN,PW〉存储在本地，并建立用户信息表。当客户端收到NST后，会将〈(Skrc₁,Pkrc₁),NST〉存储在本地用于未来会话状态的回复。其中新会话票据是TLS的扩展，用于在TLS会话期间提供会话持久性和快速恢复功能，客户端可以在将来的连接中使用这个票据，快速恢复先前的TLS会话状态。

3.3　新设备注册过程阶段

已注册指纹的用户使用新设备进行指纹认证，包含未注册的设备认证失败和注册新设备两个环节。参考3.2节指纹注册过程，本小节不再详细介绍新设备注册过程，简要注册流程如图4。

首先使用指纹请求TLS，服务器端发现该设备未在服务器端注册，此次认证失败。重新建立TLS并要求用户使用口令认证，认证通过后服务器端将新设备\mathrm{D}\mathrm{i}\mathrm{d}添加到用户信息表。

3.4　指纹认证过程

完成指纹注册的用户，使用指纹与服务器端进行TLS握手。如图5所示，过程包含：协商参数、认证服务器端和使用指纹认证用户身份三个步骤。与注册阶段不同的是，在协商之前，双方存有上轮DH轮密钥，用于本轮身份认证与DH轮密钥协商。

双方首先协商参数，其次认证服务器端的身份。服务器端生成此轮DH轮密钥对\left(\mathrm{S}\mathrm{k}\mathrm{r}{\mathrm{s}}_n,\mathrm{P}\mathrm{k}\mathrm{r}{\mathrm{s}}_n\right)，扩展包含轮公钥\mathrm{P}\mathrm{k}\mathrm{r}{\mathrm{s}}_n。客户端收到握手消息并认证成功后，根据服务器端轮公钥，生成轮共享密钥\mathrm{D}\mathrm{H}{\mathrm{c}}_n=\mathrm{P}\mathrm{k}\mathrm{r}{\mathrm{s}}_n^{\mathrm{S}\mathrm{k}\mathrm{r}{\mathrm{c}}_{n-\mathrm{1}}}，更新轮密钥对\left(\mathrm{S}\mathrm{k}\mathrm{r}{\mathrm{c}}_n\right.,\left.\mathrm{P}\mathrm{k}\mathrm{r}{\mathrm{c}}_n\right)。最后，使用指纹信息认证用户身份，客户端将\mathrm{S}\mathrm{i}\mathrm{g}{\mathrm{n}}_{\mathrm{F}{\mathrm{p}}_{\mathrm{s}\mathrm{k}}}\left(\mathrm{b}\mathrm{i}\mathrm{o}\mathrm{r}\right)、\mathrm{F}\mathrm{i}\mathrm{d}、\mathrm{D}\mathrm{i}\mathrm{d}和\mathrm{P}\mathrm{k}\mathrm{r}{\mathrm{c}}_n等信息作为扩展发送给服务器端。服务器端对指纹信息和共享密钥进行认证，使用轮共享密钥\mathrm{D}\mathrm{H}{\mathrm{s}}_n解密得到\mathrm{P}\mathrm{k}\mathrm{r}{\mathrm{c}}_n，更新用户信息表，将〈Fid,Did,Fp_pk,Pkrc _n,NST〉存储在本地，并发送NST给客户端。客户端也将〈(Skrc _n,Pkrc _n ),NST〉存储在本地用于未来会话状态的恢复。

4　 生物特征认证扩展的形式化分析

4.1　协议模型

本文使用Tamarin对扩展后的协议进行形式化建模与分析。建模模型将覆盖指纹注册、常规指纹认证、用户使用新设备认证以及认证失败四种不同情况下的扩展协议。

4.1.1　安全通道的分析与建模

安全通道具有保密性和真实性的特性。对手既无法修改也无法了解在安全通道发送的消息。建模规则如下所示。将Sec($A,$B,x)约束为线性事实，防止重放。通道规则通过事实Sec($A,$B,x)将发送者A和接收者B绑定到消息x，而对手无法修改该事实。

rule ChanoutS:

[OutS ($A, $B, x)]

--[ChanOutS ($A, $B, x)]->[Sec ($A, $B, x)]

rule ChaninS:

[Sec($A, $B, x)]

--[ChaninS($A, $B, x)]-> [InS($A, $B, x)]

4.1.2　DH棘轮的分析与建模

根据上节对DH棘轮算法的介绍，可知DH密钥出现在服务器端加密的扩展和客户端加密的扩展中，实现DH轮密钥的交换与更新。下面展示了DH棘轮算法首次协商的规则，仅包含与DH棘轮算法实现的相关项与事实。

rule ServerHelloSSend4msg2C:

let pkrS0=‘g’^~skrS0 dhkeyS=dhpkC^~yS

ExS=<~bior, pkrS0> in

[Fr (~skrS0, Fr(~bior), In(ClienthellologC)

]-->[Out (<…,senc (<$S, $C, ExtensionS,

CertSCA,CertVerifyS, FinishedS>, khS)>)]

rule CSendFinish2S:

let pkrC0=‘g’^~skrC0 dhrC0=pkrS0^~skrC0

ExC=<SignbiorD, pkrC0, senc (~bior,dhrC0)>

in [Fr(~skrC0), InS ($D, $C, <SignbiorD,

~id_D, ~id_F, pk_Fp,…>)]-->

[Out (senc (<…,ExtensionC>, khC ))]

在ServerHelloSSend4msg2C规则中，服务器端生成棘轮DH密钥对<~skrS0,pkrS0>。服务器端将pkrS0封装成扩展信息，与加密消息一起发送。在CSendFinish2S规则中，客户端生成轮DH公私钥对(skrC0,pkrC0)，并根据收到的服务器端轮DH公钥pkrC0，计算生成轮共享密钥dhrC0，并将pkrC0和用dhkeyS加密的指纹认证挑战值bior发送给服务器端。最后，服务器端利用pkrC0和自己的私钥skrS0计算轮共享密钥dhrS0，验证bior，从而完成首次棘轮密钥的同步。

4.1.3　CA和发放S证书的分析与建模

建模证书分发机制包含服务器端\mathrm{S}和证书颁发机构CA两个实体，CA使用自签名证书并为服务器端签发证书。假设证书分发信道是安全的，攻击者不能干扰证书分发的过程。下面的规则定义了注册CA和为S颁发证书。

rule InitCA:

let pkCA=pk(~skCA)

SignSCA=sign(<$S, pkS, $CA>,~skCA)

CertSCA=<$S, pkS,$CA,SignSCA>

SignCA=sign(<$CA, pk(~skCA)>,~skCA)

CertCA=<$CA, pk(~skCA), SignCA> in

[Fr(~skCA), !PkS($S,pkS)]

--[OnlyOnceInitCA($CA), Neq($S, $CA),

CAfinish($CA, $S,CertSCA)]->

[InitCAState2S(…, CertCA, SignSCA),

Out(<$CA, pkCA>),OutS($CA,$S,

<CertSCA,‘SRegisterCert’>)]

InitCA规则中，CA首先生成公钥pkCA和私钥~skCA，为服务器端S签发证书CertSCA，同时，CA通过自签名为自己生成证书CertCA。OnlyOnceInitCA限制了S和CA在一次握手过程只注册一次，只为S签发一次证书。

4.2　攻击者能力的分析与建模

除了Tamarin提供的DY攻击者能力，本文对攻击者的额外能力进行了建模，在完成握手后允许攻击者妥协用户，获取指纹信息；允许攻击者妥协通信参与方，获取长期私钥。以妥协服务器为例。规则RevealltkS定义当攻击者妥协服务器并长期密钥ltk，会将其发送在公开信道。当不对攻击者的能力进行限制时，攻击者可以任意运行这些规则。

rule RevealltkS:

[!LtkS(A, ~ltk)]

--[RevealltkS(A) ]-> [Out(~ltk)]

4.3　安全属性的分析与建模

Tamarin运用归谬法，对描述安全属性的谓词逻辑公式取否，将问题转化为约束求解问题。它依据否定公式与协议规则生成一系列约束条件，描述协议执行中的各种关系与限制。Tamarin搜索所有可能的执行轨迹，查看是否存在满足这些约束条件的路径。若找到满足否定公式约束条件的执行轨迹，即发现反例，意味着否定公式成立，证明协议不满足该安全属性。反之，若Tamarin遍历完所有可能的执行轨迹，都未找到满足否定公式约束条件的路径，则否定公式不成立，证明协议满足该安全属性。

根据1.3小节TLS要求的安全目标和2.3小节新增的安全目标，将分为机密性和认证性两种安全属性，对其进行安全分析和建模。

4.3.1　机密性

本文考虑了会话密钥的前向保密、指纹信息的保密性和会话的后妥协安全。部分属性的介绍如下。

1） 会话密钥前向保密属性引理：如果参与者认为自己已经与经过身份认证的对等方建立了会话密钥，则攻击者无法得知该密钥。除非在会话密钥建立前，攻击者已妥协参与者或对等方的长期密钥。这也就意味着，该引理允许攻击者在会话密钥建立后破坏对等方的长期密钥。引理的具体内容如下。

lemma SecretsessionKeys:

“All C S tid kh #i #j.

SessionKeyC(C,S,tid,‘auth’,kh)@i &

SessionKeyS(S,C,tid,‘auth’,kh)@j &j<i &

not (Ex #r1.RevealltkC(C)@r1 &r1<j)&

not (Ex #r2.RevealltkS(S)@r2 &r2<j)

==> not Ex #k. K(kh)@k”

SessionKeyC(…)@i和SessionKeyS(…)@j表示客户端和服务器端在时间点@i和@j生成会话密钥。j<i限制服务器端的密钥生成时刻晚于客户端，保证认证过程顺序性。该引理通过not(Ex #r1.RevealltkC(C)@r1 &r1<j)和not(Ex #r.RevealltkS(S)@r2 &r2<j)条件，确保在会话密钥生成之前，客户端和服务器端的长期密钥没有被泄露。同时，not Ex #k.K(kh)@k确保会话密钥在任何时刻都不会被公开，即使长期密钥被攻击者窃取，历史的会话密钥仍是安全的。

2） 会话的后妥协安全属性引理：后妥协安全意味着在每次TLS会话中，当客户端完成一次治愈并随后发送消息时，攻击者无法学习到这个消息，除非它再次对客户端进行妥协。因此，攻击者能够解密消息的唯一方法是在客户端最近一次治愈后重新执行妥协。引理具体内容如下。

lemma SessionPSC :

“All C, S, tid, k_C, #i,#j, #k.

Sent(tid, C, S, k_C)@i & K(k_C)@ j &

Heal(tid, C, S)@k & k < i

==>Ex #l. Compromise(C, S)@l & k < l”

该引理SessionPSC定义了，假如在时刻i客户端用会话密钥kC向服务器S发送应用消息Sent(tid,C,S,k_C)，并且客户端在发送该消息之前已经完成了治愈操作Heal(tid,C,S)@k。同时，假设攻击者在时刻j获得了会话密钥k_C。攻击者必须在治愈阶段之后，才可能通过妥协操作Compromise(C,S)获得会话密钥，且该妥协必须发生在时刻k之后。确保即使攻击者在某个时刻成功窃取了会话密钥，也无法解密未来会话内容，除非攻击者在治愈之后再次妥协客户端或服务器密钥。

4.3.2　认证性

本文采取Lowe^[24]提出的身份认证规范层次结构，综合Bio-TLS协议扩展后指纹认证需满足的安全目标与RFC所要求的安全目标，实现了比RFC要求更强的认证性，部分认证引理的介绍如下。

1） 会话密钥和会话标识符的单射认证性引理：若客户端和服务器端完成握手，根据双方一致的会话标识符，它们必须就会话密钥达成一致，并且不存在另外一个时间节点，存在相同的会话密钥和会话标识符。限制是双方不妥协长期密钥。在这里引理证明了会话密钥和会话标识符的非单射一致性。引理具体内容如下。

lemma SessionkeyagreementUniqueness:

“All C S tid key #i .

CommitSessionKeyAgree(C, S, tid, key)@i

==>(Ex #j.RunningSessionKeyAgree(S,C,tid,

key)@j &j<i & not (Ex C2 S2 #i.

CommitSessionKeyAgree(C,S,tid,key)@i2

& not (#i=#i2)))

| (Ex #r.RevealltkC(C)@r)

| (Ex #k.RevealltkS(S)@k)”

该引理规定以客户端完成TLS握手过程为出发点，事实CommitSessionKeyAgree(…)@i表示协议中的客户端在特定时间i完成了TLS握手并接受了会话密钥和会话标识符时，服务器端必然在更早的时间节点j与该客户端执行了协议，定义为RunningSessionKeyAgree(…)@j。

2） 指纹的单射认证引理：引理表达的含义是服务器端验证了指纹响应值的正确性，则客户端的确之前发送了指纹响应值，并且双方都同意了指纹的身份。引理具体内容如下。

lemma FingerAuthentication:

“All C S tid bior signbior #i.

CommitFingerAgree(S,C,bior,Signbior,tid)@i

& not (Ex #r1. RevealltkC(C)@r1)

& not (Ex #r2. RevealltkS(S)@r2 )

==> (Ex #j. RunningFingerAgree(C,S,bior,

Signbior,tid)@j &j<i)”

该引理定义了动作事实和单射性。动作事实CommitFingerAgree(…)@i表示在时间点i，服务器端S已验证指纹响应信息，完成了对用户的身份认证。另一个动作事实RunningFingerAgree(…)@j代表客户端C在更早的时间点j真实参与了协议。在这个过程中，客户端向服务器端发送了与相同的指纹响应信息和会话标识符。该引理特别明确了单射性，排除了同一指纹响应值和相同会话标识符在其他实例中被再次使用的可能性。

4.4　安全证明与分析

4.4.1　实验环境

本文实验在操作系统Ubuntu18.04完成，处理器为Intel Core i5-8400.8 GHz，内存为8 GB，验证工具为Tamarin 1.8.0。

4.4.2　实验结果与分析

本文对4个场景进行了建模与验证，包含：注册并认证、添加新设备并认证、正常认证和认证失败4个模型。表1展示了所有模型下安全属性的认证结果，其中模型①、②，在注册阶段考虑TLS1.3要求的安全属性，认证阶段涉及TL1.3要求的安全属性和指纹认证的安全属性。

实验结果表明，①、②模型在注册和添加新设备阶段，保证了TLS协议和用户指纹的安全性，包括会话密钥前向保密性、指纹信息的保密性、服务器的认证性以及会话一致性、唯一性。在完成用户和设备注册后，协议进一步确保了会话的后妥协安全和指纹的认证性。后妥协安全的实现证明了协议允许攻击者在获取用户身份信息和妥协长期密钥条件下，通过DH棘轮，实现后妥协安全。而认证失败模型验证了在用户提交未注册的指纹的情况下，TLS握手流程在认证指纹的阶段中止的场景，证明了协议的安全性。

综上可知：① 扩展后的协议不会影响TLS1.3协议安全性；② 所有与指纹认证相关的新安全属性都得到了验证，证明了Bio-TLS的安全性。

4.4.3　性能分析

本小节对比本文方案与其他现有身份认证方案，从安全性、硬件设备、无感认证和安全证明等维度，突出本文模型的特点与贡献，表2展示了本文模型和其他身份认证模型的性能分析。

由表2可知，文献均保证了会话的基本安全性，包括会话前向保密、完整性、相互认证性。例如，前向保密性的实现，本文和文献[26]均采用密钥协商机制，本文使用DH密钥交换，文献[26]使用密钥封装机制，确保会话密钥彼此独立，实现前向保密性。同时，文献均提供了安全证明，使用符号模型工具Tamarin、ProVerif等工具验证了方案的安全性。

在实现后妥协安全性上各文献之间存在显著差异。本文通过DH棘轮密钥协商与更新实现后妥协安全；文献[11]在用户未被妥协的条件下可以实现对未来通信的后妥协安全，但其攻击者的能力弱于本文；文献[25]支持用户主动选择更新密钥，这可能导致当用户不知密钥已泄露时，无法提供有效恢复机制以保障未来会话的安全性；文献[27]存在类似安全风险，密钥定期更新，而非每次认证更新，当密钥泄露后，会话的安全性难以得到保障。在硬件依赖性方面，本文方案设计不依赖特殊硬件设备，用户可利用支持指纹识别的设备通过TLS协议进行认证，使得Bio-TLS在不同环境下能灵活部署。而文献[11-12]为实现多因素认证，需要绑定智能卡，当智能卡丢失，用户无法进行身份认证；文献[25]要求设备出厂前集成FIDO。在用户体验方面，Bio-TLS实现支持多设备和无感认证，提升了用户的体验。文献[11-12，25，27]使用智能卡和密码认证方式，未实现无感认证，用户操作复杂，维护成本高。

综上，本文方案在安全性和硬件支持方面有较好的表现，尤其是在棘轮算法和无感认证的设计上，相较于其他方案提供了更完善的安全性保障和更优的用户体验。

5　 结 语

本文设计了一种基于TLS协议的生物特征认证扩展Bio-TLS，包含注册指纹、增添新设备、常规认证三个阶段。设计并实现了DH棘轮算法，用于保证指纹认证的后妥协安全。利用Tamarin对所有场景进行建模，根据TLS1.3协议的安全目标和新构建的安全目标，进行了验证与分析。结果表明，扩展后的TLS协议是安全的，在保证TLS的会话保密性和完整性等属性基础上，提供了生物特征的保密性、真实性和认证。此外，在攻击者远程妥协用户指纹信息的情况下，Bio-TLS能够保证会话的后妥协安全。在未来的工作中，笔者将考虑更广泛的TLS变体协议（0-RTT、PSK），并致力于在TLS协议库中实现该扩展，从而将基于生物特征的认证应用于TLS。

参考文献

[1] JAIN A K， SAHOO S R， KAUBIYAL J. Online social networks security and privacy： Comprehensive review and analysis［J］. Complex & Intelligent Systems， 2021， 7（5）： 2157-2177. DOI：10.1007/s40747-021-00409-7 .

[2] RESCORLA E. The transport layer security protocol version 1.3［EB/OL］. ［2018-08-30］.DOI: 10.17487/rfc8446 .

[3] VANDERSLOOT B， AMANN J， BERNHARD M， et al. Towards a complete view of the certificate ecosystem［C］//Proceedings of the 2016 Internet Measurement Conference. New York： ACM， 2016： 543-549. DOI：10.1145/2987443.2987462 .

[4] KHAN S， LUO F， ZHANG Z J， et al. A survey on X.509 public-key infrastructure， certificate revocation， and their modern implementation on blockchain and ledger technologies［J］. IEEE Communications Surveys & Tutorials， 2023， 25（4）： 2529-2568. DOI：10.1109/COMST.2023.3323640 .

[5] WANG Z， LIN J Q， CAI Q W， et al. Blockchain-based certificate transparency and revocation transparency［C］// Financial Cryptography and Data Security. Berlin： Springer， 2019： 144-162. DOI：10.1007/978-3-662-58820-8_11 .

[6] XIA W， WANG W， HE X， et al. Old habits die hard： A sober look at TLS client certificates in the real world［C］//2021 IEEE 20th International Conference on Trust， Security and Privacy in Computing and Communications （TrustCom）. New York： IEEE Press， 2021： 83-90. DOI：10.1109/TrustCom53373.2021.00029 .

[7] DONG H Y， ZHANG Y Z， LEE H， et al. Mutual TLS in practice： A deep dive into certificate configurations and privacy issues［C］//Proceedings of the 2024 ACM on Internet Measurement Conference. New York： ACM， 2024：214-229. DOI：10.1145/3646547.3688415 .

[8] BOONKRONG S. Multi-factor authentication［J］. Authentication and Access Control： Practical Cryptography Methods and Tools， 2020： 133-162. DOI： 10.1007/978-1-4842-6570-3_6 .

[9] YIN Z Y， ZHOU Q， QU J Q， et al. How far is user privacy leakage： A revisit of client certificate usage［C］//2023 8th International Conference on Cloud Computing and Big Data Analytics （ICCCBDA）. New York： IEEE Press， 2023：279-284. DOI：10.1109/ICCCBDA56900.2023.10154744 .

[10] D’ORAZIO C J， CHOO K R. A technique to circumvent SSL/TLS validations on iOS devices［J］. Future Generation Computer Systems， 2017， 74： 366-374. DOI：10.1016/j.future.2016.08.019 .

[11] GUPTA B B， PRAJAPATI V， NEDJAH N， et al. Machine learning and smart card based two-factor authentication scheme for preserving anonymity in telecare medical information system （TMIS）［J］. Neural Computing and Applications， 2023， 35（7）： 5055-5080. DOI：10.1007/s00521-021-06152-x .

[12] KIM H. Security enhancement of biometric-based authentication systems using smart card［J］. IEEE Access， 2024， 12： 174053-174065. DOI：10.1109/ACCESS.2024.3502632 .

[13] ALWEN J， CORETTI S， DODIS Y. The double ratchet： Security notions， proofs， and modularization for the signal protocol［M］//Advances in Cryptology — EUROCRYPT 2019. Cham： Springer International Publishing， 2019： 129-158. DOI：10.1007/978-3-030-17653-2_5 .

[14] KRAWCZYK H. SIGMA： The ‘SIGn-and-MAc’ approach to authenticated diffie-Hellman and its use in the IKE protocols［M］//Advances in Cryptology — CRYPTO 2003. Berlin： Springer， 2003： 400-425. DOI：10.1007/978-3-540-45146-4_24 .

[15] BLAKE-WILSON S， NYSTROM M， HOPWOOD D， et al. Transport layer security extensions［EB/OL］.［2006-04-30］. DOI: 10.17487/rfc4366 .

[16] VARO Q， LARDIER W， YAN J. Dynamic reduced-round TLS extension for secure and energy-saving communication of IoT devices［J］. IEEE Internet of Things Journal， 2022， 9（23）： 23366-23378. DOI：10.1109/JIOT.2022.3206667 .

[17] TANGE K， HOWARD D， SHANAHAN T， et al. rTLS： Lightweight TLS session resumption for constrained IoT devices［M］//Information and Communications Security. Cham： Springer International Publishing， 2020： 243-258. DOI：10.1007/978-3-030-61078-4_14 .

[18] LEE H， SMITH Z， LIM J， et al. maTLS： How to make TLS middlebox-aware？［C］//Proceedings 2019 Network and Distributed System Security Symposium. San Diego： Internet Society， 2019：1-15. DOI：10.14722/ndss.2019.23547 .

[19] AHN T， KWAK J， KIM S. mdTLS： How to make middlebox-aware TLS more efficient？［M］//Information Security and Cryptology — ICISC 2023. Singapore： Springer Nature Singapore， 2024： 39-59. DOI：10.1007/978-981-97-1238-0_3 .

[20] MEIER S， SCHMIDT B， CREMERS C， et al. The TAMARIN prover for the symbolic analysis of security protocols［M］//Computer Aided Verification. Berlin： Springer， 2013： 696-701. DOI：10.1007/978-3-642-39799-8_48 .

[21] 刘镝， 王梓屹， 李大伟， 等. 基于Tamarin的5G AKA协议形式化分析及其改进方法［J］. 密码学报， 2022， 9（2）： 237-247. DOI： 10.13868/j.cnki.jcr.000515 .

[22] LIU D， WANG Z Y， LI D W， et al. Formal analysis and improvement methods of 5G AKA protocol based on tamarin［J］. Journal of Cryptologic Research， 2022， 9（2）： 237-247. DOI： 10.13868/j.cnki.jcr.000515（Ch ）.

[23] BASIN D， SASSE R， TORO-POZO J. The EMV standard： Break， fix， verify［C］//2021 IEEE Symposium on Security and Privacy （SP）. New York： IEEE Press， 2021： 1766-1781. DOI：10.1109/SP40001.2021.00037 .

[24] SHI M， CHEN J， HE K， et al. Formal analysis and patching of ｛BLE-SC｝ pairing［C］//32nd USENIX Security Symposium. Anaheim： USENIX Association， 2023： 37-52.

[25] LOWE G. A hierarchy of authentication specifications［C］//Proceedings 10th Computer Security Foundations Workshop. New York： IEEE Press， 1997： 31-43. DOI：10.1109/CSFW.1997.596782 .

[26] FENG H N， GUAN J J， LI H， et al. FIDO gets verified： A formal analysis of the universal authentication framework protocol［J］. IEEE Transactions on Dependable and Secure Computing， 2023， 20（5）： 4291-4310. DOI：10.1109/TDSC.2022.3217259 .

[27] CELI S， HOYLAND J， STEBILA D， et al. A tale of two models： Formal verification of KEMTLS via tamarin［M］//Computer Security — ESORICS 2022. Cham： Springer Nature， 2022： 63-83. DOI：10.1007/978-3-031-17143-7_4 .

[28] SIKARWAR H， DAS D. A novel MAC-based authentication scheme （NoMAS） for Internet of vehicles （IoV）［J］. IEEE Transactions on Intelligent Transportation Systems， 2023， 24（5）： 4904-4916. DOI：10.1109/TITS.2023.3242291 .

基金资助

国家重点研发计划(2022YFB3103300)

国家自然科学基金(62172303)

国家自然科学基金(62076187)