Page 322 - 《软件学报》2025年第9期

韩将 等: 面向跨信任域互联网场景的拜占庭容错访问控制架构 4233

3. 将交易 v l 输入广播实例 k-RBC (r,j)
4. upon 首次接收到消息 Finish(v l ) := {Finish,v l } do
5. 进入等待状态, 直到接收到 n− f 个 Finish(v l ) := {Finish,v l } 消息
6. 将交易 v l 和外部断言 Q 加入 Opti-MVBA r
7. v l ← Opti-MVBA r
8. return v l

4.2.4 安全性分析
在安全性分析中, 需要证明: 1) k-RBC 依旧满足一致性、有效性和总体性; 2) Opti-MVBA 依旧满足一致性、
终止性和有效性; 3) Super-Dumbo 依旧满足一致性、有效性和总体性. 并且在完成证明后, 回到第 3.3 节对于安全
目标的证明.
引理 1. 当实现 k-RBC 的 RBC 是安全的, 那么 k-RBC 满足一致性、有效性和总体性.
证明:
′
v
a) 一致性: 对于某一交易切片 v i , 当一个诚实节点输出 , 另一个诚实节点输出 , 按照 RBC 的一致性, 可得
v i
i
v i = v . 当 k-RBC 输出时, 节点会按照交易切片索引值按序进行拼接, 使得一个诚实节点输出 v = {v i } k , 另一个诚实
′
i
′
′ ′ v = v , 满足一致性.
节点输出 v = {v } k , 满足
i
b) 有效性: 对于某一交易切片 v i , 当一个诚实节点输入 , 根据 RBC 的一致性, 则存在诚实节点均会输出 v i .
v i
根据 k-RBC 算法, 将交易切片按序聚合成交易后, 依旧满足当一个诚实节点输入 v = {v i } k , 则存在诚实节点会输出
v = {v i } k , 满足有效性.
c) 总体性: 对于某一交易切片 v i , 当一个诚实节点输入 , 根据 RBC 的总体性, 所有诚实节点均会输出 v i . 根
v i
据 k-RBC 算法, 将交易切片按序聚合成交易后, 依旧满足当一个诚实节点输入 v = {v i } k , 所有诚实节点均会输出
v = {v i } k , 满足总体性. 证毕.
引理 2. 当 CBC 和 ABA 均安全时, 那么 Opti-MVBA 满足终止性、外部有效性、一致性、完整性.
证明:
a) 终止性: 证明终止性, 即证明当所有的诚实节点输入了经过断言验证的值 v, 则所有诚实节点均将输出值 v.
v, 由于随机置换的策略选取并不会影响 MVBA 的安全性, 仅影
假设所有的诚实节点输入经过断言验证的值
响 MVBA 的性能, 所以 MVBA 的终止性不会受到影响, 那么根据 MVBA 的终止性, 所有诚实节点均将输出值 v.
终止性成立.
b) 外部有效性: 证明外部有效性, 即证明如果一个诚实节点输出了值 v, 则有外部断言 Q, 满足 Q(v) = True.
由于断言变为循环等待, 所以此处的断言从 MVBA 的全局、无状态断言变为本地、有状态断言. 此时的断言
是单调的, 即随着每个节点内部的状态变化, 断言函数的结果只可能从否变成真, 不能从真变成否. 为了保证本地
断言的有效性, 此处要求所有输出值 v, 以及协议节点本地断言集合 {Q i }, 满足:

∀Q ∈ {Q i }, |{Q i }| ⩾ n−2 f, Q(v) = True (2)
n−2 f 个本地断言输出为真. 而 MVBA (n−2 f,n) -门限签名, 同样需要满足: 对于值
即至少对 的外部断言使用
v 的证明, 即有效的签名分片集合 {σ}, 通过断言的条件为:

∀σ ∈ {σ i }, |{σ i }| ⩾ n−2 f (3)
与本地断言的验证条件一致. 所以满足外部有效性.
c) 一致性: 证明一致性, 即证明所有诚实节点的输出一致.
根据 Opti-MVBA 的算法, 由于外部验证和随机置换的优化对 ABA 共识阶段并不会产生影响, 与 MVBA 的
ABA 共识阶段一致, 所以 Opti-MVBA 依然满足一致性.
d) 总体性: 证明总体性, 即证明当部分诚实节点输出了值 v, 则有一些诚实节点输入了值 v.