安全与密码学2016eprint.iacr.org编辑精选
Signal 消息协议的形式化安全分析
A Formal Security Analysis of the Signal Messaging Protocol
专业 · 约 120 分钟读完前置知识：密码学基础、密钥交换协议（DH/3DH）、形式化验证方法
导读
这篇论文用形式化方法分析 Signal 消息协议（TextSecure）的安全性：作者在多阶段密钥交换模型下，借助自动化证明工具对协议的密钥协商与 Double Ratchet 密钥更新机制进行建模和验证，论证其密钥保密性与前向保密等性质在给定密码学假设下成立。论文同时把协议本身的安全性与实现、终端环境的信任问题区分开来，这也是讨论的起点。
HN 关注点：的焦点不是在协议数学本身，而是协议验证通过之后：终端操作系统不可信、App 权限过大、服务器可靠性不足以及用户规模太小，使端到端加密的实际收益被打折扣。
后来怎么样
这是首个对 Signal 协议的完整形式化安全分析，确立了 Double Ratchet 的符号化证明范式，后续多篇形式化分析工作（如对 XSalsa/MLS 等的研究）沿用了其建模方法，Signal 协议也被 WhatsApp 等主流消息应用广泛采用。
HN 评论精选
这几条评论里：支持 1 质疑 1 补充 2
支持从技术角度指出攻击面在 KDF 派生组件而非握手本身，并强调协议的最大价值是让大规模被动监控不经济，最现实的攻击是入侵终端。
这篇论文很好，周末要花时间读了。初步印象是，若要在实现层面寻找攻击点，应同时针对 KDF 中的派生组件（const0、const1）——它们似乎是迭代链密钥以生成消息密钥的基础（而不只是对上一个密钥做 HMAC），以及针对由初始 3DH 密钥协商内容派生出链根密钥的环节。如果我要破坏某个实现，大概会考察降低这些组件熵值会造成什么影响。即便如此，你还得为每个发送方/接收方组合预先计算消息密钥链。在 KDF 中用上一个密钥的 HMAC 来推进消息密钥和链密钥是很妙的做法，它摆脱了对静态计数器或跨所有客户端实例的全局计数器种子的依赖。不管这些直觉对不对，该协议实际上（很好地）做到的是：迫使攻击者针对单个用户设备才能拿到明文；即使实现者犯了一堆错误，发送方与接收方之间密钥的多样性也使被动大规模监控变得不切实际。在我看来，最经济的“大规模”攻击是：在网络上识别出它的报文，然后自动利用终端设备漏洞、安装截屏间谍软件并收割数据。这已经算不上被动，也很难在大规模下不被发现。不错。
motohagiography查看英文原文
Great paper, there goes my weekend. Initial impression is that theoretical place to look for attacks on an implementation would be simultaneously against the derivation components in the KDFs, (const0, 1), which appear to be the basis for iterating the chain keys to gen msg keys (other than the hmac of the previous one) - and on the derivation of a chains root key from (I think) the contents of that initial 3DH key agreement. If I were sabotaging an implementation, I would probably examine the impact of reducing the entropy of these components. Even then, you would have to precompute chains of message keys for each sender/recipient combination. Using the previous key HMAC in the KDF to increment message and chain is a really nice touch as it removes the dependency on a static counter or a universal GF counter seed across all client instances. Whether these intuitions are correct or not, what the protocol effectively does (very well) is force an attacker to target an individual users device to get message cleartext, as even if an implementor made a bunch of mistakes, the diversity of keys across senders and recipients makes passive mass surveillance impractical. IMHO, the most economical "mass," attack against it would be to identify its messages on the wire, then auto-exploit the endpoint devices, install screen grabbing spyware, and harvest that data. Hardly passive or scaleably undetectable. Nice.
质疑提问：首次通信是否仍可能被 MITM，只能靠带外验证安全号码来防御。
我的理解对吗：一种从最初几条消息就开始的中间人攻击可能奏效，而唯一防范办法是在带外核对安全号码（safety number）？
badrabbit查看英文原文
Am I correct in my understanding that a mitm attack that starts with the initial messages could work and the only way to prevent this is to verify the safety number out of band?
补充批评 Signal Android 客户端索取过多敏感权限，主张用插件化拆分权限。
协议或许没问题，但对一款处理敏感数据的应用来说，Signal 的权限模型是有缺陷的。过度权限的例子：禁用锁屏、定位权限、设置壁纸（这是把什么都塞进来的功能）、外部存储（为什么不用应用专属的内部存储）、系统日志。Android 沙箱会尽力保护用户免受被攻陷应用的危害，但如果应用本身已拿到全部权限，沙箱也保护不了你。从近期事件看，我认为 Signal 用户整体上就是被瞄准的风险群体——他们对隐私的诉求使其成为情报机构和执法部门眼中的有趣目标。很多成功应用采用插件模式，把侵入性权限拆分到单独的可选应用中。Signal 也应该这么做。
iamnothere查看英文原文
The protocol may be in good shape, but Signal's permission model is flawed for an application that handles sensitive data. A few examples of excessive permissions: * Disable your screen lock * Location permissions * Set wallpaper ("kitchen sink" feature here) * External storage (why not use internal "app only" storage?) * System log data Android's sandbox will do its best to protect the user from compromised applications, but it can't do anything to protect you if the application already has full permissions. Based on recent events, I would assume that Signal users are at risk of targeting as a block -- their desire for privacy makes them interesting targets from an intelligence and LEO perspective. Many successful applications follow a plugin model, where intrusive permissions are split off into separate, optional applications. Signal should do the same.
补充从产品与运维角度：用户规模小、服务器每月约 710/720 小时可用，呼吁支持自建托管。
底层 Signal 协议是安全的，这很好，但我最担心的是怎么让更多人用它、怎么让它更可靠。现状是 Signal 基本只被技术倾向中等偏上的人群使用，用户刚过一百万。理想情况下它应该比 WhatsApp 更大——WhatsApp 用了 libsignal，但有大量元数据问题，在美国也错过了很多年长人群。另外服务器可靠性大约是每月 720 小时里有 710 小时可用，上周六 19:51 到 22:08 PST 就发生过一次除 ZRTP 通话外全部中断的故障。我知道在 CyanogenMod WhisperPush 互操作那场混乱之后，Moxie 大概永远不会允许与他的服务器互通，但我们需要某种支持自建或替代托管的东西：Signal 的服务器并非万无一失，偏远地区的一台本地服务器可能是无价的，而目前在这个领域我们只有 XMPP 加 Conversations。
moyta查看英文原文
Its great that the underlying Signal protocol is secure, my major worry is how do we get more people to use it, and how do we make it more reliable? As it stands right now, Signal is used exclusively by the moderately technically inclined, with a little over 1 million users. In a perfect world, it would be bigger than Whatsapp, which uses libsignal but has many metadata related issues, and also misses many older demographics in the US. Additionally, server reliability has been something like 710hrs out of 720hrs usually every month, with an outage just this last Saturday from 19:51 to 22:08 PST for everything but ZRTP calls. I know Moxie will likely never allow interoperability with his servers after the cluster that was CyanogenMod WhisperPush interop, but we need something to allow for self hosting or alternative hosting, Signal's servers are not bulletproof and a local server in remote areas can be invaluble, essentially XMPP with Conversations is all we have in this arena right now.
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
历次讨论
- 2016Hacker News 讨论帖253 分 · 220 评
- 2018Hacker News 讨论帖100 分 · 10 评
同领域还值得读
如何入侵一台已关机的电脑：在 Intel ME 中运行未签名代码
How to hack a turned-off computer, or running unsigned code in Intel ME
这篇 Black Hat 2017 白皮书讨论 Intel Management Engine（ME）的安全问题：如何在 ME 中运行未签名代码，以及攻破处于关机状态的电脑的相关…
安全与密码学2017 · 543 分 · 107 评专业 · 约 40 分钟编辑精选比特币：一种点对点的电子现金系统（2008）
Bitcoin: A Peer-to-Peer Electronic Cash System (2008)
中本聪 2008 年发表的比特币白皮书，提出了无需可信第三方的点对点电子现金系统。
安全与密码学2017 · 536 分 · 394 评入门 · 约 45 分钟编辑精选GPRS 加密算法 GEA-1 的密码分析表明存在故意弱点
Cryptanalysis of GPRS Encryption Algorithms GEA-1 suggest intentional weakness
首次公开了对 GPRS 加密算法 GEA-1 和 GEA-2 的密码分析攻击。
安全与密码学2021 · 487 分 · 107 评专业 · 约 90 分钟编辑精选A2：模拟恶意硬件
A2: Analog Malicious Hardware
论文研究如何在芯片设计阶段植入模拟电路形式的恶意硬件后门，使其难以被常规检测发现。
安全与密码学2016 · 315 分 · 94 评专业 · 约 75 分钟编辑精选Air-FI：从气隙隔离计算机生成隐蔽 Wi-Fi 信号
Air-FI: Generating Covert Wi-Fi Signals from Air-Gapped Computers
研究如何从物理隔离（air-gapped）的计算机中隐蔽地外泄数据：利用内存总线产生的电磁泄漏，在 2.4 GHz Wi-Fi 频段内编码信息，使附近的普通 Wi-Fi 网卡（如…
安全与密码学2020 · 294 分 · 105 评 · 引用 3进阶 · 约 45 分钟编辑精选