群组密钥协议攻击分析与改进

### 群组密钥协议攻击分析与改进 #### 1. Asokan–Ginzboorg 协议概述 Asokan 和 Ginzboorg 提出了一种适用于蓝牙设备的应用层协议。场景是一群人在会议室中，使用支持蓝牙的笔记本电脑建立安全会话，且电脑之间无共享先验知识，也没有可信第三方或公钥基础设施。该协议的步骤如下： 1. 选择并展示一个短的群组密码（如写在白板上），参与者使用该密码建立安全的密钥。 2. 协议流程： - 设群组规模为 \(n\)（\(n \in N\)，\(n \geq 2\)），成员记为 \(M_i\)（\(1 \leq i \leq n\)），其中 \(M_n\) 作为群组领导者。 - \(M_n \to ALL : M_n, \{| E \}|_P\)：\(M_n\) 广播包含新鲜公钥 \(E\) 的消息，该公钥使用密码 \(P\) 加密。 - \(M_i \to M_n : M_i, \{| R_i, S_i \}|_E\)（\(i = 1, \ldots, n - 1\)）：其他参与者 \(M_i\) 向 \(M_n\) 发送对最终密钥的贡献 \(S_i\) 和新鲜对称密钥 \(R_i\)，使用公钥 \(E\) 加密。 - \(M_n \to M_i : \{| \{S_j, j = 1, \ldots, n\} \}|_{R_i}\)（\(i = 1, \ldots, n - 1\)）：\(M_n\) 收集所有 \(S_i\) 并加上自己的贡献 \(S_n\)，然后向每个参与者发送包含 \(S_1, \ldots, S_n\) 的消息，使用相应的对称密钥 \(R_i\) 加密。 - \(M_i \to M_n : M_i, \{| S_i, h(S_1, \ldots, S_n) \}|_K\)（某个 \(i\)，\(K = f(S_1, \ldots, S_n)\)）：一个参与者 \(M_i\) 向 \(M_n\) 响应，将收到的包通过单向哈希函数 \(h()\) 处理，并使用新的群组密钥 \(K\) 加密。 该协议有三个目标： - 防止外部间谍获取密钥。 - 抵御干扰攻击，攻击者可添加虚假消息，但不能阻止或延迟消息。 - 通过贡献式密钥建立，防止不诚实参与者将密钥限制在特定范围内。 #### 2. 建模 Asokan–Ginzboorg 协议 在 Coral 的模型中，将跟踪信息视为变量，可实例化为任意数量的消息，从而可以针对群组规模进行通用建模。建模方法与固定 2 或 3 主体协议类似，为每个协议消息生成一个规则，描述跟踪信息如何通过该消息扩展，并考虑控制条件。 然而，消息 3 带来了问题。对于 \(n\) 个参与者的群组，会同时发送 \(n - 1\) 个不同的消息 3，且群组领导者必须检查是否收到了 \(n - 1\) 个消息 2。这个问题通过在模型中添加两个子句解决，递归定义了一个新函数，用于检查跟踪信息中是否所有消息 2 都已发送，并返回包含协议规定响应的新跟踪信息。该函数在所有实例化模式下都有效，允许在反驳搜索过程中为不同规模的群组构建协议运行。 #### 3. 攻击 Asokan–Ginzboorg 协议 为了测试协议的安全性，考虑了两种攻击者：室内间谍和室外间谍。室外间谍尝试进行干扰攻击，室内间谍试图控制室内通信，例如让所有参与者同意只有他知道的不同密钥。由于是无线场景，间谍只能插入额外的虚假消息，不能阻止特定消息的接收。 通过寻找安全属性的反例来发现攻击，这些反例的表述方式与 Paulson 的方法类似，需要根据可能的消息跟踪集来表述所需的属性。 ##### 3.1 干扰攻击检查 使用以下猜想检查干扰攻击： ```plaintext %% some honest xi has sent message 4, so has key f(Package): eqagent(XI,spy)=false ∧ member(sent(XI,XK,pair(principal(XI), encr(pair(nonce(SI ), h(Package)), f (Package)))), Trace) = true∧ %% genuine messages 3 and 1 are in the trace to some agent XJ: member(sent(MN,XJ,encr(Package,nonce(RJ))),Trace)=true ∧ member(sent(MN,all,pair(principal(MN),encr(key(E),key(P)))) ∧ ,Trace)=true %% but XJ never sent a message 2 under public key E with nonces SJ %% (which is in Package) and RJ (which the message 3 meant for %% him was sent under). That means he doesn’t have RJ, and so can’t %% get the key from his message 3. member(nonce(SJ),Package)=true ∧ member(sent(XJ,MN,pair(principal(XJ),encr(pair(nonce(RJ),nonce(SJ)), key(E)))),Trace)=false → ``` 这个猜想表示协议运行已完成（即发送了消息 4），但存在某个代理没有获得密钥（即无法读取他的消息 3）。 当首次使用该猜想运行时，Cora