Page 109 - 《软件学报》2026年第6期

2428 软件学报 2026 年第 37 卷第 6 期

SecRPN、SecRoIA 和 SecClassification 模块进行检测. MalOD 的正确性可以通过证明其模块的正确性来证明. 接
下来, 本文进行 MalOD 的正确性证明.
定理 A1. MalOD 的组成模块 SecBackbone、SecRPN、SecRoIA 和 SecClassification 是正确的.
证明: SecBackbone 由 Π SAdd 、SConv、 Π SMaxpool 、 Π SBN 层、 Π SLinear 层、 Π SReLU 层和 SNNI 组成. 已知 Π SAdd 、
Π SConv 、 Π SMaxpool 、 Π SBN 、 Π SLinear 和 Π SReLU 协议是正确的 [35,36] , 因此只需证明 SNNI 的正确性. 由于 SNNI 仅在本地
执行坐标计算, 其正确性显而易见. 因此, SecBackbone 是正确的. SecRPN 模块由 Π SConv 、 Π SSigmoid 、 Π SAdd 、 Π SMult 、
Π SSort 、 Π SSelect 等已证明正确性的协议以及本文提出的 SBBDec 算子组成. SBBDec 按照其计算过程 (正文中公
式 (4)–(9)) 调用 Π SMult 、 Π SAdd 和 Π SNE 构成, 因此其是正确的. 由此可证得 SecRPN 的正确性. MalOD 的第 3 个模块
由 SecRoIA、 Π SSoftmax 、 Π SConv 、 Π SLinear 、SBBDec 和 Π SReLU 组成. 只需证明 SecRoIA 协议的正确性即可证明该模块
的正确性. 除本地计算和 Π SAdd 算法, SecRoIA 还调用了 SBI 算法. SBI 由 Π SMult 、SCeil 和 Π SFloor 组成. 根据公式 (2),
Π SFloor 是正确的, 因此 SCeil 是正确的, 可得 SBI 是正确的. 因此, SecRoIA 是正确的, 进而验证了 SecRoIA 和
SecClassification 模块的正确性.
综上所述, 由 SecBackbone, SecRPN, SecRoIA 和 SecClassification 模块构成的 MalOD 是正确的.
A.2 MalOD 的安全性
本节中, 本文根据定义 A1、引理 A1、引理 A2 和引理 A3 对恶意敌手下的 MalOD 进行安全性分析.
定义 A1. 给定一个协议 π, 如果对于真实世界中的任何恶意敌手 A, 存在一个模拟器能够为 A 生成一个在计
F .
算上与真实情况不可区分的视图, 那么就可以说, 该协议在存在恶意敌手的情况下安全地实现了功能
引理 A1 [39] . 如果协议 π 中的所有子协议是可模拟的, 那么 π 也是可模拟的.
引理 A2 [40] . 如果 r 是一个与值 x 无关且敌手 A 未知的均匀分布随机数, 那么 x±r 也是一个对 A 未知的均匀
分布随机数.
引理 A3 [35,36] . 在四方计算的诚实多数恶意敌手模型中, Π SAdd 、 Π SMult 、 Π SComp 、Π SSelect 、 Π SSort 、 Π SConv 、
Π SMaxpool 、 Π SBN 、 Π SLinear 、 Π SReLU 、 Π SNE 、 Π SSoftmax 、 Π SSigmoid 和 Π SFloor 是安全的.
本文将根据上述定义和引理证明所构建协议的安全性.
定理 A2. 在四方计算的诚实多数恶意敌手模型中, SCeil 和 SNNI 协议是安全的.
证明: 在 SCeil 中, 每个服务器 S i 的视图包括 [x] i [⌊−x⌋] i 和 [⌈x⌉] i . 由于 Π SFloor 是安全的, [x] i 和 [⌊−x⌋] i 是均匀
,
分布随机数. 根据引理 A2 和公式 (2), 可以推导出 [⌈x⌉] i 也是均匀分布随机数. 在 SNNI 中, 每个服务器 S i 的视图由
′ [F] i 是由均匀分布的随机数组成, 因此各方根
[F] i 和 [F ] i 构成, 且各方仅在本地进行计算, 不涉及数据交互. 由于
[F ] i 也由均匀分布的随机数组成. 综上所述, SCeil 和 SNNI 的所有视图均可模拟且与真
′
据 [F] i 在本地计算得到的
实视图不可区分, 因此 SCeil 和 SNNI 在恶意敌手模型下是安全的.
定理 A3. 在四方计算诚实多数的恶意敌手模型中, SBI 和 SBBDec 协议是安全的.
S 3 之间的信道, 并记录每个计算子协议的输入和输出视图, 分别记
证明: 假设恶意敌手 A 窃听 S 0 、S 1 、S 2 和
作 view in 和 view out . 对于 SBI 协议, 有:
输入视图: view in = view Π SAdd ∪view Π SFloor ∪view SCeil ∪view Π SMult ;
输出视图: view out = output Π SAdd ∪output Π SFloor ∪output SCeil ∪output Π SMult .
同理, 对于 SBBDec, ; . 根据定
view in = view Π SAdd ∪view Π SNE ∪view Π SMult view out = output Π SAdd ∪output Π SNE ∪output Π SMult
理 A2、引理 A1 和引理 A3, 由于 SBI 和 SBBDec 中 view in 和 view out 的所有元素均可模拟, 因此 SBI 和 SBBDec 的
view in 和 view out 均与模拟视图不可区分. 因此 SBI 和 SBBDec 协议在恶意敌手模型中是安全的.
接下来证明 MalOD 中 SecBackbone、SecRPN、SecRoIA 和 SecClassification 的安全性.
定理 A4. SecBackbone、SecRPN、SecRoIA 和 SecClassification 在四方计算的诚实多数恶意敌手模型中是安
全的.
证明: 该定理的证明方法与定理 3 的证明类似.