什么样的协议才安全

身份认证旨在确定通信双方的身份。没有身份认证，协议就容易受到冒充攻击：攻击者可以伪装成受信任的服务器并拦截通信。协议通常通过数字证书、预共享密钥或挑战—响应机制来实现身份认证，这些机制可以在不泄露秘密的情况下证明通信方掌握该秘密。

机密性确保只有预期接收者才能访问消息内容。它通过加密实现，所用密钥只有相关通信方知晓。机密性失效意味着窃听者可以读取传输中的消息。仅有机密性并不能阻止攻击者篡改消息或发起重放攻击；它必须与完整性保护结合使用。

完整性保护确保接收到的消息与发送者传输的内容完全一致，没有添加、删除或修改。消息认证码和认证加密模式可以提供完整性保护。没有完整性保护时，即使攻击者无法读取密文，也可能以可预测的方式翻转特定位，从而改变解密后的明文；填充预言机攻击就利用了这一点。

不可否认性意味着发送者之后无法否认自己发送过某条消息。它通过使用非对称密钥的数字签名实现：只有私钥持有者才能生成该签名，而对应的公钥可以验证签名。MAC 不提供不可否认性，因为发送者和接收者都知道共享秘密，双方都可能生成该 MAC。

新鲜性确保攻击者无法重放一条过去有效的消息，以再次触发相同效果。新鲜性机制包括随机数（消息中包含且不得重复的随机值）、具有严格有效时间窗口的时间戳，以及必须严格递增的序列号。没有新鲜性保护时，重放截获的身份认证消息可能完全绕过身份认证。

完美前向保密可确保长期密钥遭到泄露时不会暴露过去的会话密钥。通过使用 Diffie-Hellman 为每个会话生成临时密钥对，可以实现这一点。会话密钥由临时密钥计算得出，并在使用后丢弃。即使服务器的长期私钥后来被窃取，攻击者也无法解密此前记录的会话，因为临时密钥已经不存在。

单向认证只验证一方：在 HTTPS 中，服务器会出示由客户端验证的证书，但服务器通常不会验证客户端的身份。双向认证（也称双向 TLS，即 mTLS）要求双方都出示并验证证书。在微服务架构、API 网关和企业 VPN 中，mTLS 十分常见，因为双方端点在交换敏感数据之前都必须经过验证。

协议设计者不能仅凭直觉进行判断。看似显然安全的协议也可能以微妙的方式失效。Needham-Schroeder 公钥协议于 1978 年发布，当时被认为是安全的。1995 年，Gavin Lowe 使用形式化验证工具发现了其中的漏洞，该漏洞允许攻击者发起冒充攻击。如今，使用 Tamarin 或 ProVerif 等模型检查器进行形式化验证，已经成为安全关键协议设计中的标准实践。

Dolev-Yao 模型是分析密码协议的标准威胁模型。该模型假设攻击者控制整个网络：可以拦截、阻断、修改、重放和注入任何消息。模型假设密码学原语是完美的（不存在数学弱点）。在此模型中，只有当协议即使在攻击者完全控制所有通信的情况下仍能实现其目标时，才认为该协议是安全的。

密码协议设计之所以出了名地困难，是因为其中的漏洞往往微妙且不易察觉。多条消息、随机数、时间戳和密钥之间的交互可能会产生意料之外的攻击路径。各参与方可能对协议状态有不同的理解。并发会话可能相互干扰。包括 SSL、TLS、WPA2 和 802.11 在内的每个重要已部署协议，都曾在部署后被发现存在严重漏洞。

SSL 3.0 被 POODLE 攻击攻破。TLS 1.0 和 1.1 因存在多项弱点而被弃用。WEP WiFi 加密在部署后的第一年内就被完全攻破。PPTP VPN 因 MS-CHAPv2 的弱点而被认为不安全。每次失败都让安全社区更加了解非正式安全直觉与基于 Dolev-Yao 模型、可证明正确的协议设计之间的差距。

哪种安全属性可以确保攻击者今天记录的消息，日后无法成功重新发送给服务器以重复执行某项操作？

安全协议必须实现认证、保密性、完整性、不可否认性和新鲜性。完美前向保密可以保护过去的会话免受未来密钥泄露的影响。双向认证可以验证双方身份。Dolev-Yao 模型假设网络完全处于对手控制之下。协议设计需要形式化验证，而不能只依赖直觉。每个重要协议都曾在部署后被发现存在漏洞，这推动了密码学标准持续演进。