Dolev-Yao 攻击者模型与符号密码学

Dolev-Yao 模型由 Danny Dolev 和 Andrew Yao 于 1983 年提出，是符号协议分析中标准的对手模型。攻击者控制整个网络。

Dolev-Yao 攻击者可以：拦截任何消息、存储消息、重放旧消息、根据已知组件伪造新消息，但无法破解底层密码学原语。

在符号模型中，加密是一个完美的黑盒：攻击者无法在没有密钥的情况下解密，无法分解大整数，也无法伪造签名。这简化了分析，但可能会遗漏实现层面的攻击。

消息被建模为项：enc(k, m)、sig(sk, m)、hash(m)、pair(a, b)。攻击者知道某些项，并使用已定义的规则（演绎规则）推导出新的项。

攻击者的知识在演绎下是闭合的：如果攻击者知道 enc(k,m) 和 k，就可以推导出 m。如果攻击者知道 pair(a,b)，就可以推导出 a 和 b。初始知识的闭包 = 攻击者能够学习到的一切内容。

协议安全性表述为：“在任何可达状态中，攻击者的知识都不包含秘密 s。”保密性 = 可达性。身份认证 = 不存在某些不良轨迹模式。

双方协议：A→B: {Na, A}_{K_B}；B→A: {Na, Nb}_{K_A}；A→B: {Nb}_{K_B}。在项代数中：Alice 发送 enc(pubkey_B, pair(Na, A))。我们验证执行完成后，只有 B 知道 Na。

应用 π 演算（Abadi & Fournet 2001）是一种用于协议建模的进程代数。进程通过信道通信；攻击者控制公共信道。ProVerif 和 Tamarin 使用这种形式化方法。

在 Dolev-Yao 模型中安全的协议，如果其密码学实例较弱，仍可能在计算上不安全。计算可靠性定理（Cortier 等人）为特定的原语类别弥合了这一差距。

Dolev-Yao 无法建模：代数性质（例如 XOR 的交换律）、侧信道攻击、实现错误或概率性失败。等式理论模型等扩展可以处理部分代数性质。

Dolev-Yao 攻击者 NOT 具备哪项能力？

Dolev-Yao 赋予攻击者对网络的完全控制权，但假设密码学是完美的。消息是代数中的项；安全性是一种可达性属性。应用 π 演算提供了形式化语言。局限性：无法建模代数关系、侧信道或实现错误。