可证明地提高Belenios选举可验证性

### 可证明地提高Belenios选举可验证性 #### 1. 选举流程与基本概念 在选举过程中，日志的一致性不仅能确保基本的完整性属性，还能防止类似的选票复制攻击。选民可以在选举期间随时在公告板（BB）上检查自己的选票。具体而言，他们应检查预期的选票 `b` 是否与他们的公共凭证 `cr` 一起公布在 `BBcast` 上。 计票阶段，会选择要计票的选票并将其标记为计票程序的输入。通常会选择每个 `cri` 最后投出的选票，得到 `BBtally: (cr1, b1), ..., (crn, bn)`。如果没有为 `cri` 投出选票，则 `bi = ⊥`。基于ElGamal加密的同态属性，将 `BBtally` 上对应非空选票的密文组合成一个密文 `c`，该密文编码了每个候选人的总票数。然后，由受托人对 `c` 进行解密以获得选举结果。 #### 2. 选举可验证性与攻击场景 选举可验证性建模为属性的合取 `Φh_iv ∧ Φeli ∧ Φcl ∧ Φ◦_res`，具体含义如下： - **个体可验证性（`Φh_iv`）**：确保如果诚实的选民成功验证了他们投出的最后一张选票，那么相应的投票应包含在最终计票中。 - **资格验证（`Φeli`）**：确保如果选民成功验证了一张选票，那么相应的公共凭证应在 `BB` 上的注册时记录。此外，任何计票的选票都应对应于注册时记录的公共凭证。 - **无冲突（`Φcl`）**：确保没有两个选民可以成功验证同一公共凭证的选票。 - **结果完整性（`Φ◦_res`）**：确保对手只有在相应选民被破坏或未对投出的任何选票执行个体验证程序时，才能为给定的公共凭证投出选票。更强的结果完整性概念 `Φ•_res` 禁止对手即使选民未验证任何投出的选票也投出选票。 违反 `Φres` 称为选票填充攻击，违反 `Φcl` 称为冲突攻击。Belenios 预计在以下对抗场景中满足选举可验证性： - **A1**：服务器和注册商均诚实。 - **A2**：服务器腐败，注册商诚实。 - **A3**：服务器诚实，注册商腐败。 当注册商诚实，安全性由私钥签名保证；当服务器诚实时，安全性由私有密码和服务器日志保证。然而，存在一些攻击，原因是服务器不知道公共凭证与相应选民身份之间的关联。腐败的选民只要对手设法获得用相应私有凭证签名的选票，就可以为任何公共凭证投出选票。 常见的攻击场景如下： - **选票重排序攻击（A1、A2 或 A3）**：假设诚实的选民 `id` 具有公共凭证 `cr`，按顺序投出选票 `b1` 和 `b2`，并且只验证了 `b2`。那么 `b2` 应该为相应的公共凭证计票。然而，对手可以使 `b1` 被计票。攻击场景如下： 1. `V(id, cr)` 投出 `b1` 和 `b2`，被对手 `A` 阻止。 2. `A` 为 `cr` 投出 `b2`（依赖于腐败的选民或投票服务器）。 3. `BBcast` 上，`(cr, b2)` 被选民 `V(id, cr)` 验证。 4. `A` 为 `cr` 投出 `b1`。 5. `BBtally: (cr, b1)`。 在正常执行中，当服务器诚实时，除非对手破坏了 `id` 的密码，否则对手不能在 `b2` 之后投出 `b1`。A1 攻击的关键点是 `b2` 由不同的腐败选民为同一公共凭证 `cr` 投出。 - **选票填充攻击（A3）**：当诚实的选民 `id1` 用 `cr1` 投出选票 `b` 时，对手可以阻止并以腐败选民 `id2` 的名义为同一公共凭证 `cr1` 投出该选票。选民 `id1` 成功验证了 `b`。随后，依赖于腐败的注册商，对手可以为 `cr1` 投出另一张选票 `bA`。这违反了结果完整性 `Φ◦_res` 和个体可验证性 `Φiv`。攻击场景如下： 1. `A` 破坏 `VR` 和 `V(id2)` 以获得 `⟨cr1, skey1, pwd2⟩`。 2. `V(id1)` 投出 `b`，被 `A` 阻止。 3. `A` 用 `⟨cr1, pwd2⟩` 投出 `b`，`VS` 在日志中存储 `(id2, cr1)`。 4. `BBcast` 上，`(cr1, b)` 被 `V(id1)` 验证。 5. `A` 用 `⟨cr1, pwd2⟩` 投出 `bA`，该选票被接受并公布。 6. `BBtally: (cr1, bA)`。 如果选民 `id2` 验证了投出的选票 `b`，这在相关定义中也被视为冲突攻击。这种攻击的一种变体可能导致较弱形式的选票填充：对手可以在 `id1` 有机会投出选票之前提交 `bA`。在这种情况下，投票服务器将不接受 `id1` 的任何进一步选票，因为这会破坏 `cr1` 日志的一致性。 #### 3. 改进选举可验证性的方法 在Belenios中，选票 `b = ⟨c, s, prR, prL⟩` 中的零知识证明 `prL = proofL(c, r, cr)` 的目的是将密文 `c = enc(v, pk, r)` 以及选票 `b` 可验证地链接到为其投出选票的公共凭证 `cr`。通过丰富标签结构可以保护选举免受上述攻击。具体步骤如下： ##### 3.1 防止选票重排序攻击 假设最初在 `BB` 上符合条件的公共凭证旁边有空选票。并且，`BB` 的特定部分用于显示每个凭证最后投出的选票： - 投票前：`BBlast : (cr1, ⊥), ..., (crn, ⊥)` - 投票期间：`BBlast : (cr1, b1), ..., (crn, bn)` 当投票平台 `VP` 为具有公共凭证 `cr` 的选民构造新选票时，它从 `BBlast` 中获取 `cr` 旁边的最后一张选票 `b′`。然后，在构造证明 `prL` 时，`VP` 使用标签 `h(cr, b′)`，其中 `h` 是一个抗碰撞哈希函数，将对 `(cr, b′)` 映射到标签的适当域： ```plaintext ℓ = h(cr, b′); prL = proofL(c, r, ℓ); b = ⟨c, s, prR, prL, ℓ⟩. ``` `BBcast` 记录为 `cr` 投出的所有选票，并且它们的顺序不能在 `BB` 上更改。选举审计员可以查看为凭证 `cr` 投出的任意两张连续选票 `b′` 和 `b`，并验证 `verL(prL, c, h(cr, b′)) = ok`，从而确保构造 `b` 的一方确实期望它跟随 `b′`。这种标签结构确保在注册商诚实的腐败场景（即 A1 和 A2）中实现选举可验证性。 ##### 3.2 防止注册商腐败攻击 在注册商腐败的场景中，选票填充和冲突攻击的主要原因是对手可以阻止诚实选民的选票 `b`，并以腐败选民的身份投出该选票，同时保持与 `b` 关联的公共凭证相同。为了防止这种情况，在选票 `b` 上附加的标签应包含对选民身份的承诺。具体操作如下： 在为选民 `id` 投出选票期间，`VP` 生成一个新的随机数 `t`，构造标签 `⟨cr, com(id, t)⟩`，并将 `t` 与选票一起发送到投票服务器 `VS`。 ```plaintext VP : ℓ = ⟨cr, com(id, t)⟩; prL = proofL(c, r, ℓ); b = ⟨c, s, prR, prL, ℓ⟩, VS : receives (cr, b, t) from VP for a given id; ℓ′ = ⟨cr, com(id, t)⟩, casts b if and only if ℓ′ = ℓ and verL(prL, c, ℓ) = ok. ``` 这种标签结构足以确保在服务器诚实的腐败场景（即 A1 和 A3）中实现选举可验证性。选举审计员仍然可以在 `BB` 上检查证明 `prL`，但只能确保选票是为预期的公共凭证 `cr` 投出的，而不会知道底层的 `id`。 ##### 3.3 组合标签 将上述两种标签组合如下： ```plaintext ℓ1 = h(cr, b′); ℓ2 = com(id, t); ℓ = ⟨ℓ1, ℓ2⟩. ``` 定义不同变体的Belenios： - `Beleniostr`：按照3.1节增强标签的变体。 - `Beleniosid`：按照3.2节设置标签的变体。 - `Belenios+`：使用组合标签 `ℓ` 的变体。 对于协议 `P`、腐败场景 `A` 和属性 `Φ`，用 `(P, A) |= Φ` 表示 `P` 在腐败场景 `A` 中满足 `Φ`。得到以下结果： | 协议 | 腐败场景 | 是否满足 `Φ◦_E2E` | | ---- | ---- | ---- | | `Beleniostr` | `A1, A2` | 是 | | `Beleniosid` | `A1, A3` | 是 | | `Belenios+` | `A1, A2, A3` | 是 | | `Belenios` | `A1, A2, A3` | 否 | `Φ◦_E2E` 对应于标准的可验证性概念，确保如果诚实的选民成功验证了公共凭证 `cr` 的选票 `b`，那么 `b` 将作为 `cr` 的贡献计入最终计票。更强的可验证性概念 `Φ•_E2E` 要求如果为对应诚实选民的公共凭证计票的选票，那么它必须是该选民投出的。在场景 A3 中，即使是 `Belenios+` 也可能违反 `Φ•_E2E`，但能满足 `Φ◦_E2E`。 #### 4. 规范与验证 ##### 4.1 使用Tamarin指定协议 使用Tamarin证明器对 `Belenios+` 进行分析，Tamarin基于多集重写框架。在Tamarin中，消息（或项）由一组函数符号构建，加密原语的属性由一组方程建模。协议状态信息和对手知识由事实表示，协议动作由多集重写规则指定，形式为 `[L] --[ M ] -> [N]`。 例如，在投票协议中，生成秘密/公钥对的多集重写规则 `Rkey` 如下： ```plaintext [ Fr(k) ] --[ !BBkey(pk(k)), Phase('setup') ] -> [ !Sk(k), !BBkey(pk(k)), Out(pk(k)) ] ``` 其中 `Fr(k)` 表示随机生成的新鲜密钥 `k` 作为前提。结论事实 `!Sk(k)` 和 `!BBkey(pk(k))` 分别记录选举的秘密密钥和公共密钥。 设置候选人和选民身份的规则如下： ```plaintext Rcand : [ In(⟨v1, v2⟩) ] --[ Phase('setup') ] -> [ !BBcand(v1), !BBcand(v2) ] Rid : [ In(id) ] --[ Phase('setup') ] -> [ !Id(id) ] ``` 选民投出选票的规则 `Rvote` 如下： ```plaintext Rvote : [ !Id(id), !BBcand(v), !BBkey(pk(k)), Fr(r) ] --[ Vote(id, v), Phase('voting') ] -> [ Out(⟨id, enc(v, pkey, r)⟩) ] ``` 加密操作通过方程指定，例如解密操作： ```plaintext dec(enc(v, pk(k), r), k) = v ``` Tamarin中的限制是约束协议规则应用的逻辑公式，例如 `∀x, y, i, j. BBkey(x) @i ∧ BBkey(y) @j ⇒ x = y` 确保不能有两个不同的选举密钥。 ##### 4.2 `Belenios+` 的规范与验证 定义一组方程用于指定解密、签名验证、范围证明验证和将标签附加到密文的证明验证： ```plaintext (1) dec(enc(x, pk(y), z), y) = x, (2) ver(sign(x, y), x, pk(y)) = ok, (3) (∀i) verR(proofR(enc(xi, y, z), z, ⟨x1, ..., xk⟩), enc(xi, y, z), y, ⟨x1, ..., xk⟩) = ok, (4) verL(proofL(enc(x, y, z), z, ℓ), enc(x, y, z), ℓ) = ok. ``` 对于协议中参与者的动作，定义了一组规则和限制。以下是投票平台 `VP` 和投票服务器 `VS` 投出选票的重要规则： 投票平台 `VP` 投出选票的规则 `RVP_vote`： ```plaintext RVP_vote : construct a ballot, authenticate and send it to VS let c = enc(v, pkey, r); s = sign(c, skey); ℓ = ⟨h(cr, b0), com(id, t)⟩; prR = proofR(c, r, vlist); prL = proofL(c, r, ℓ); b = ⟨c, s, prR, prL, ℓ⟩; a = h(⟨id, pwd, cr, b, t⟩) in [ !BBcand(v), !BBkey(pkey), Fr(r), Fr(t), !Vlist(vlist), !Reg(id, cr, skey), !Pwd(id, pwd), VPlast(cr, b0) ] --[ Vote(id, cr, v), VoteB(id, cr, b) ] -> [ !Voted(id, cr, v, b), Out(⟨id, cr, b, a, t⟩) ] ``` 投票服务器 `VS` 投出选票的规则 `RVS_cast`： ```plaintext RVS_cast : authenticate voter, verify and publish ballot let ℓ = ⟨h(cr, b0), com(id, t)⟩; b = ⟨c, s, prR, prL, ℓ⟩; a′ = h(⟨id, pwd, cr, b, t⟩) in [ In(⟨id, cr, b, a, t⟩), !BBkey(pkey), !Vlist(vlist), !BBreg(cr), !Pwd(id, pwd), BBlast(cr, b0) ] --[ a′ = a, ver(s, c, cr) = ok, verR(prR, c, pkey, vlist) = ok, verL(prL, c, ℓ) = ok, Log(id, cr), !BBcast(cr, b) ] -> [ !BBcast(cr, b), BBlast(cr, b), VPlast(cr, b) ] ``` 还定义了个体验证程序的规则和限制，以及不同的腐败场景规则，如腐败选民以揭示凭证、腐败服务器以确定密码、腐败服务器以填充选票、腐败注册公共/秘密凭证等规则。通过Tamarin的验证结果表明，`Belenios+` 在不同腐败场景下的积极结果是 `Beleniostr` 和 `Beleniosid` 积极结果的并集。 以下是Tamarin验证 `Belenios+` 时不同选票数量限制下的执行时间示例（假设）： | 每个选民的选票数量限制 | 执行时间 | | ---- | ---- | | 2 | 10分钟 | | 3 | 20分钟 | | 4 | 30分钟 | | 5 | 超过1小时 | 综上所述，通过丰富标签结构和使用Tamarin进行验证，可以有效提高Belenios选举的可验证性，抵御多种攻击场景，但在某些强可验证性要求和无选票数量限制的情况下仍存在挑战。 ### 可证明地提高Belenios选举可验证性 #### 继续深入分析选举过程与安全性 在前面我们已经了解了Belenios选举的基本流程、常见攻击场景以及一些改进可验证性的方法。接下来，我们进一步详细探讨这些内容之间的联系以及如何更好地确保选举的安全性。 ##### 选举流程的关键环节 选举流程中，计票阶段是决定最终结果的重要环节。其流程如下： 1. **选票选择**：选择要计票的选票，通常选取每个公共凭证 `cri` 最后投出的选票，形成记录 `BBtally: (cr1, b1), ..., (crn, bn)`。若未为 `cri` 投出选票，则 `bi = ⊥`。 2. **密文组合**：基于ElGamal加密的同态属性，将 `BBtally` 上对应非空选票的密文组合成一个密文 `c`，该密文编码了每个候选人的总票数。 3. **解密计票**：由受托人对密文 `c` 进行解密，从而获得选举结果。 ```mermaid graph LR A[选票选择] --> B[密文组合] B --> C[解密计票] ``` ##### 攻击场景的深入剖析 不同的攻击场景对选举的可验证性造成了不同程度的威胁。我们再次梳理这些攻击场景，以便更好地理解其原理和影响。 - **选票重排序攻击**：这种攻击利用了服务器对选票顺序控制的漏洞。对手通过阻止诚实选民的选票并重新投出，改变了选票的计票顺序。在正常情况下，服务器会根据选民身份和公共凭证的关联来确保选票顺序的正确性，但当对手破坏了这种关联（如获取选民密码）时，就可能实施攻击。 - **选票填充攻击**：在注册商腐败的场景下，对手可以阻止诚实选民的选票，并以腐败选民的名义投出，甚至后续再投出自己的选票。这不仅违反了结果完整性和个体可验证性，还可能导致冲突攻击。 #### 改进方法的综合应用与效果评估 我们已经介绍了通过丰富标签结构来防止选票重排序和注册商腐败攻击的方法。接下来，我们分析这些方法的综合应用以及其在不同腐败场景下的效果。 ##### 标签结构的综合应用 通过将防止选票重排序的标签 `h(cr, b′)` 和防止注册商腐败的标签 `com(id, t)` 组合成新的标签 `⟨h(cr, b′), com(id, t)⟩`，我们得到了 `Belenios+` 变体。这种组合标签的应用使得选举在多种腐败场景下都能更好地保证可验证性。 ##### 不同协议变体的效果对比 | 协议 | 腐败场景 | 是否满足 `Φ◦_E2E` | 是否满足 `Φ•_E2E` | | ---- | ---- | ---- | ---- | | `Beleniostr` | `A1, A2` | 是 | 否 | | `Beleniosid` | `A1, A3` | 是 | 否 | | `Belenios+` | `A1, A2, A3` | 是 | 在 A3 场景可能不满足 | | `Belenios` | `A1, A2, A3` | 否 | 否 | 从表格中可以看出，`Belenios+` 在更多的腐败场景下满足标准的可验证性概念 `Φ◦_E2E`，但对于更强的可验证性概念 `Φ•_E2E`，在某些场景下仍存在不足。 #### Tamarin验证的详细解读 Tamarin证明器在验证 `Belenios+` 的安全性方面发挥了重要作用。下面我们详细解读Tamarin验证的过程和结果。 ##### Tamarin验证的基本原理 Tamarin基于多集重写框架，通过定义消息（项）、方程、事实和规则来建模协议。协议状态信息和对手知识由事实表示，协议动作由多集重写规则指定。例如，生成密钥对、设置候选人和选民身份、投出选票等操作都可以用规则来表示。 ##### 验证规则的详细分析 - **投票平台投出选票规则 `RVP_vote`**：该规则涉及到选票的构造、认证和发送。具体步骤如下： 1. 构造密文 `c = enc(v, pkey, r)`。 2. 对密文进行签名 `s = sign(c, skey)`。 3. 生成组合标签 `ℓ = ⟨h(cr, b0), com(id, t)⟩`。 4. 生成证明 `prR = proofR(c, r, vlist)` 和 `prL = proofL(c, r, ℓ)`。 5. 构造选票 `b = ⟨c, s, prR, prL, ℓ⟩`。 6. 进行密码认证相关操作 `a = h(⟨id, pwd, cr, b, t⟩)`。 7. 发送选票信息 `Out(⟨id, cr, b, a, t⟩)`。 - **投票服务器投出选票规则 `RVS_cast`**：该规则主要进行选民认证、选票验证和公布操作。具体步骤如下： 1. 接收选票信息 `In(⟨id, cr, b, a, t⟩)`。 2. 验证密码、签名和零知识证明，如 `a′ = a`，`ver(s, c, cr) = ok`，`verR(prR, c, pkey, vlist) = ok`，`verL(prL, c, ℓ) = ok`。 3. 记录日志 `Log(id, cr)`。 4. 公布选票 `!BBcast(cr, b)`。 5. 更新最后选票记录 `BBlast(cr, b)` 和 `VPlast(cr, b)`。 ```mermaid graph LR A[投票平台 RVP_vote] --> B[构造选票] B --> C[认证操作] C --> D[发送选票] E[投票服务器 RVS_cast] --> F[接收选票] F --> G[验证操作] G --> H[记录日志] H --> I[公布选票] I --> J[更新记录] D --> F ``` ##### 腐败场景规则的影响 不同的腐败场景规则模拟了各种可能的攻击情况。例如： - **`CV_corr`**：腐败选民以揭示凭证，使对手可以获取选民的相关信息。 - **`CVS_pwd`**：腐败服务器以确定密码，让对手能够绕过密码认证。 - **`CVS_cast`**：腐败服务器以填充选票，破坏选举的公正性。 - **`CVR_reg`**：腐败注册公共/秘密凭证，影响选民的注册信息。 这些腐败场景规则的存在，使得Tamarin能够全面地验证 `Belenios+` 在不同攻击情况下的安全性。 #### 总结与展望 通过对Belenios选举的深入分析，我们可以看到，通过丰富标签结构和使用Tamarin进行验证，能够显著提高选举的可验证性，抵御多种常见的攻击场景。但我们也应该认识到，在某些强可验证性要求和无选票数量限制的情况下，仍然存在挑战。 未来，我们可以进一步研究如何优化标签结构，使其在满足强可验证性要求的同时，提高选举系统的性能。同时，也可以探索更高效的验证方法，减少Tamarin验证的执行时间，特别是在无选票数量限制的情况下，确保选举系统能够快速、准确地进行验证。此外，还可以考虑结合其他安全技术，如区块链技术，进一步增强选举的安全性和可验证性。 总之，提高Belenios选举的可验证性是一个持续的过程，需要不断地研究和改进，以确保选举的公正性和可靠性。