Paper deep dive
Privacy-Preserving Robustness Verification for Neural Networks
Nianyun Song, Xiaokun Luan, Yu Guo, Rongfang Bie, Meng Sun, Xiyue Zhang
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 91%
Last extracted: 7/7/2026, 5:27:45 PM
Summary
The paper introduces SecureCROWN, a novel framework for privacy-preserving neural network robustness verification. It leverages secure two-party computation (2PC) to enable a model owner and data owner to jointly compute certified robustness bounds without exposing private data. The framework addresses challenges like data-dependent branching in Linear Bound Propagation by reformulating conditional logic into continuous arithmetic operations using Function Secret Sharing (FSS) and enhances numerical stability with a Newton-Raphson refinement method. Experiments demonstrate that SecureCROWN matches plaintext verification results while maintaining efficiency across various network sizes and communication settings.
Entities (7)
Relation Signals (6)
SecureCROWN → uses → Secure Two-Party Computation (2PC)
confidence 95% · Built upon secure two-party computation (2PC), our framework enables a model owner and a data owner to jointly compute certified robustness bounds
SecureCROWN → operatesunder → Semi-Honest Security Model
confidence 93% · provably protecting both parties' private data under the semi-honest security model.
SecureCROWN → implementes → Linear Bound Propagation (LBP)
confidence 92% · we develop (i) a secure implementation of Linear Bound Propagation (LBP) that computes certified robustness bounds under privacy constraints
SecureCROWN → employs → Function Secret Sharing (FSS)
confidence 90% · a unified branch-free reformulation of the conditional logic in ReLU relaxation and bound propagation, efficiently realized via function secret sharing (FSS)
SecureCROWN → uses → Newton-Raphson Refinement
confidence 88% · Additionally, we introduce a Newton–Raphson refinement method to improve numerical stability.
Linear Bound Propagation (LBP) → handles → ReLU Activation
confidence 85% · Convex relaxation of ReLU activations requires distinct parameters depending on secret-shared activation states.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Neural network verification and data privacy are inherently in tension: verification demands full access to model parameters and input data, yet both are increasingly restricted by privacy regulations and intellectual property constraints. This tension has left robustness verification impractical in privacy-sensitive domains. In this work, we address this gap with SecureCROWN, the first framework for privacy-preserving neural network robustness verification. Built upon secure two-party computation (2PC), our framework enables a model owner and a data owner to jointly compute certified robustness bounds -- revealing only the final result while provably protecting both parties' private data under the semi-honest security model. A key challenge is securely computing the conditional operations in Linear Bound Propagation, where the data-dependent branching is incompatible with standard secure computation protocols. We eliminate branching by formulating conditional logic as continuous arithmetic operations. Additionally, we introduce a Newton--Raphson refinement method to improve numerical stability. Extensive analysis and experiments show that SecureCROWN strictly matches plaintext verification results, while completing in 0.1--200s across varied model sizes and communication settings (LAN/WAN), demonstrating the feasibility of privacy-preserving neural network verification.
Tags
Links
- Source: https://arxiv.org/abs/2607.05251v1
- Canonical: https://arxiv.org/abs/2607.05251v1
PDF not stored locally. Use the link above to view on the source site.
Full Text
109,710 characters extracted from source content.
Expand or collapse full text
Privacy-Preserving Robustness Verification for Neural Networks Nianyun Song School of Artificial Intelligence, Beijing Key Laboratory of Artificial Intelligence for Education, Engineering Research Center of Intelligent Technology and Educational Application (Ministry of Education), Beijing Normal University, Beijing, China School of Computer Science University of Bristol Bristol, UK Xiaokun Luan School of Mathematical Sciences Peking University Beijing, China Yu Guo School of Artificial Intelligence, Beijing Key Laboratory of Artificial Intelligence for Education, Engineering Research Center of Intelligent Technology and Educational Application (Ministry of Education), Beijing Normal University, Beijing, China Rongfang Bie School of Artificial Intelligence, Beijing Key Laboratory of Artificial Intelligence for Education, Engineering Research Center of Intelligent Technology and Educational Application (Ministry of Education), Beijing Normal University, Beijing, China Meng Sun School of Mathematical Sciences Peking University Beijing, China Xiyue Zhang Correspondence to XZ (xiyue.zhang@bristol.ac.uk) School of Computer Science University of Bristol Bristol, UK Abstract Neural network verification and data privacy are inherently in tension: verification demands full access to model parameters and input data, yet both are increasingly restricted by privacy regulations and intellectual property constraints. This tension has left robustness verification impractical in privacy-sensitive domains. In this work, we address this gap with SecureCROWN, the first framework for privacy-preserving neural network robustness verification. Built upon secure two-party computation (2PC), our framework enables a model owner and a data owner to jointly compute certified robustness bounds—revealing only the final result while provably protecting both parties’ private data under the semi-honest security model. A key challenge is securely computing the conditional operations in Linear Bound Propagation, where the data-dependent branching is incompatible with standard secure computation protocols. We eliminate branching by formulating conditional logic as continuous arithmetic operations. Additionally, we introduce a Newton–Raphson refinement method to improve numerical stability. Extensive analysis and experiments show that SecureCROWN strictly matches plaintext verification results, while completing in 0.1–200s across varied model sizes and communication settings (LAN/WAN), demonstrating the feasibility of privacy-preserving neural network verification. 1 Introduction The field of deep learning (DL) has experienced enormous growth recently, with deep neural networks (DNNs) now deployed in a variety of safety-critical applications, including medical diagnosis [Litjens et al., 2017, Esteva et al., 2017] and healthcare [Esteva et al., 2019, Davenport and Kalakota, 2019]. In these domains, safety and robustness of DNNs are essential. However, DNNs are susceptible to perturbations in their inputs [Szegedy et al., 2014], such as noise and illumination variations [Goodfellow et al., 2015, Hendrycks and Dietterich, 2019]. To ensure DNN robustness with worst-case guarantees, significant progress in verification approaches [Wu et al., 2024, Wang et al., 2021, Singh et al., 2019] has been made, which can certify that a model’s prediction remains stable regardless of data noise or environmental changes. Despite these advances, existing verification techniques assume centralized access to both model parameters and input data in plaintext. This assumption is often unrealistic in privacy-sensitive deployments. In practice, user data may be subject to strict privacy regulations, such as the General Data Protection Regulation (GDPR) [Voigt and Von dem Bussche, 2017]. Meanwhile, proprietary model parameters constitute valuable intellectual property and may not be disclosed to third parties. Thus, the standard verification setting, where both model and data are fully accessible, is incompatible with many privacy-regulated collaborative scenarios. We consider a two-party verification setting in which a model owner P0P_0 holds a proprietary DNN, while a data owner P1P_1 holds sensitive input data. We aim to verify the robustness of the model on the given input such that only the verification result is revealed, while both the model parameters and the input data remain private. Achieving this requires jointly performing robustness verification without exposing either party’s confidential information. Secure multi-party computation (MPC) [Evans et al., 2018] provides a principled cryptographic approach that enables multiple parties to jointly evaluate functions on their private inputs without revealing their data to one another. While MPC has been successfully applied to privacy-preserving inference and training [Knott et al., 2021, Tan et al., 2021, Wagh et al., 2021, Kumar et al., 2020, Gupta et al., 2025, Zhang et al., 2021], extending it to robustness verification faces two fundamental challenges: (i) Data-dependent branching: Convex relaxation of ReLU activations requires distinct parameters depending on secret-shared activation states. In MPC, resolving these conditionals requires a secure comparison for every neuron, scaling linearly with the total number of neurons and rendering naïve implementations computationally prohibitive. (i) Precision sensitivity in deep recursion: Unlike MPC-based inference, which tolerates minor numerical errors during a single forward pass, verification computes certified bounds via deep backward recursion that amplifies numerical errors. Because safety guarantees depend strictly on the sign of the final margin, these compounded errors can invert near-zero bounds, compromising verification soundness. To bridge this gap, we propose SecureCROWN, the first privacy-preserving framework for neural network robustness verification built on secure two-party computation (2PC). It enables verification of DNNs while ensuring that sensitive input data remains confidential and proprietary model parameters are not disclosed. Specifically, we develop (i) a secure implementation of Linear Bound Propagation (LBP) that computes certified robustness bounds under privacy constraints; (i) a unified branch-free reformulation of the conditional logic in ReLU relaxation and bound propagation, efficiently realized via function secret sharing (FSS); and (i) a Newton–Raphson-based refinement method for reciprocal computation to improve numerical precision and stability. Furthermore, we provide formal security guarantees in the semi-honest adversary model and conduct extensive experiments validating that our protocol achieves verification precision comparable to the plaintext verifier while incurring moderate cryptographic overhead. 2 Related Work Modern neural network verification methods primarily address robustness analysis in a plaintext setting, where both model parameters and user inputs are assumed to be fully accessible. Representative verifiers include α,βα,β-CROWN [Zhang et al., 2018, Xu et al., 2020, 2021, Wang et al., 2021], CORA [Althoff, 2015], Marabou [Wu et al., 2024, Katz et al., 2019], and NeuralSAT [Duong et al., 2024, 2025]. These approaches rely on techniques such as convex relaxation [Salman et al., 2019], abstract interpretation [Singh et al., 2019], and constraint-solving [Duong et al., 2023] to compute certified robustness bounds or to solve verification queries exactly. Meanwhile, substantial progress has been made in privacy-preserving machine learning through cryptographic protocols. A prominent line of work employs MPC to enable secure inference. CrypTen [Knott et al., 2021] supports private inference over secret-shared inputs and models in a two-party setting, assuming a semi-honest threat model. CryptGPU [Tan et al., 2021] extends this framework to a three-party system with optimized GPU-based protocols under semi-honest security. Falcon [Wagh et al., 2021] implements strengthened malicious security in a three-party setting and combines SecureNN [Wagh et al., 2019] and ABY3 [Mohassel and Rindal, 2018] to improve protocol efficiency. ObliviGate [Song et al., 2026] further achieves maliciously secure inference while concealing the model architecture. CrypTFlow [Kumar et al., 2020] proposes an end-to-end toolchain that compiles predefined TensorFlow inference code into MPC protocols, supporting both semi-honest and malicious adversaries. Beyond MPC, zero-knowledge proof systems have been leveraged to provide verifiable inference without revealing model parameters or inputs [Lee et al., 2024, Maheri et al., 2025], while homomorphic encryption (HE) enables neural network inference directly over encrypted data [Lee et al., 2022, Lou and Jiang, 2021]. However, these cryptographic methods focus exclusively on secure or verifiable inference. They do not address robustness verification, which requires computing and propagating symbolic bounds beyond forward inference alone. In contrast, we establish a privacy-preserving framework for neural network robustness verification. To the best of our knowledge, our work is the first to integrate formal robustness verification with cryptographic privacy guarantees. 3 Preliminaries 3.1 Local Robustness Verification Consider an L-layer feedforward neural network classifier f:ℝd0→ℝKf:R^d_0 ^K, where d0d_0 is the input dimension and K is the number of classes. The network is parameterized by weight matrices (l)∈ℝdl×dl−1W^(l) ^d_l× d_l-1 and bias vectors (l)∈ℝdlb^(l) ^d_l for layers l∈1,…,Ll∈\1,…,L\, with dL=Kd_L=K. The pre-activation at each layer is defined as (1)=(1)+(1)z^(1)=W^(1)x+b^(1) for l=1l=1, and (l)=(l)σ((l−1))+(l)z^(l)=W^(l)σ(z^(l-1))+b^(l) for l≥2l≥ 2. In this work, we consider the ReLU activation σ(⋅)=max(0,⋅)σ(·)= (0,·). The network output is f()=(L)f(x)=z^(L), with predicted class y=argmaxkfk()y= *argmax_kf_k(x). Given an input 0x_0 correctly classified as class y, the network is locally robust within an ℓp _p-ball of radius ϵε if: fy,j≜min∈ℬp(0,ϵ)(fy()−fj())>0,∀j≠y,f_y,j _x _p(x_0,ε) (f_y(x)-f_j(x) )>0, ∀\,j≠ y, (1) where ℬp(0,ϵ)=:‖−0‖p≤ϵB_p(x_0,ε)=\x:\|x-x_0\|_p≤ε\. Since exactly verifying Eq. (1) is NP-hard for ReLU networks [Katz et al., 2017], verification methods typically compute a certified lower bound f¯y,j f_y,j via linear relaxation [Salman et al., 2019]. Linear Relaxation. Consider robustness verification under ℓp _p input perturbations ∈ℬp(0,ϵ)x _p(x_0,ε). Let z¯,z¯∈ℝ z, z be the pre-activation lower and upper bounds for a neuron z, i.e., z¯≤z≤z¯ z≤ z≤ z. To handle the nonlinearity of the activation function, linear relaxation constructs a pair of linear bounding functions—a lower bound α¯z+β¯ αz+ β and an upper bound α¯z+β¯ αz+ β—satisfying α¯z+β¯≤σ(z)≤α¯z+β¯ αz+ β≤σ(z)≤ αz+ β for all z∈[z¯,z¯]z∈[ z, z]. A commonly used bounding strategy for ReLU in CROWN [Zhang et al., 2018] sets the upper-bound parameters (α¯,β¯)( α, β) as: (α¯,β¯)=(1,0),if z¯≥0,(0,0),if z¯≤0,(α∗,−α∗z¯),otherwise,where α∗=z¯z¯−z¯,( α, β)= cases(1,0),&if z≥ 0,\\ (0,0),&if z≤ 0,\\ (α^*,-α^* z ),&otherwise, cases α^*= z z- z, (2) and the lower bound shares the same slope with zero intercept: (α¯,β¯)=(α¯,0)( α, β)=( α,0). Linear Bound Propagation. LBP in CROWN-series verifiers computes certified bounds by propagating backward linear relaxations through the network. To bound (l)z^(l) for any layer l∈1,…,Ll∈\1,…,L\, LBP constructs linear functions such that (0)+¯(0)≤(l)≤(0)+¯(0),∀∈ℬp(0,ϵ),A^(0)x+ c^(0) ^(l) ^(0)x+ c^(0),\ \ _p(x_0,ε), (3) where (0)∈ℝdl×d0A^(0) ^d_l× d_0 and ¯(0),¯(0)∈ℝdl c^(0), c^(0) ^d_l. Since our relaxation uses identical slopes α¯=α¯ α= α, the coefficient matrix (0)A^(0) is shared for both bounds, while distinct intercepts β¯≠β¯ β≠ β yield separate constants ¯(0) c^(0) and ¯(0) c^(0). For l=1l=1, since (1)=(1)+(1)z^(1)=W^(1)x+b^(1) is purely an affine transformation of x, we directly obtain (0)=(1)A^(0)=W^(1) and ¯(0)=¯(0)=(1) c^(0)= c^(0)=b^(1). For l≥2l≥ 2, the backward recursion requires relaxation parameters ((t),¯(t),¯(t))( α^(t), β^(t), β^(t)) for each intermediate layer t∈1,…,l−1t∈\1,…,l-1\, where (t)∈ℝdt α^(t) ^d_t denotes slopes and ¯(t),¯(t)∈ℝdt β^(t), β^(t) ^d_t intercepts; these are determined by the pre-activation bounds via Eq. (2). The recursion maintains (t)∈ℝdl×dtA^(t) ^d_l× d_t and ¯(t),¯(t)∈ℝdl c^(t), c^(t) ^d_l such that (t)(t)+¯(t)≤(l)≤(t)(t)+¯(t)A^(t)z^(t)+ c^(t) ^(l) ^(t)z^(t)+ c^(t). Starting with (l)=dlA^(l)=I_d_l and ¯(l)=¯(l)= c^(l)= c^(l)=0, the backward updates for t=l,…,2t=l,…,2 are given by: ^(t) A^(t) =(t)(t), =A^(t)W^(t), (4) (t−1) ^(t-1) =^(t)diag((t−1)), = A^(t)diag( α^(t-1)), (5) ¯(t−1) c^(t-1) =¯(t)+(t)(t)+¯(t−1), = c^(t)+A^(t)b^(t)+ δ^(t-1), (6) ¯(t−1) c^(t-1) =¯(t)+(t)(t)+¯(t−1), = c^(t)+A^(t)b^(t)+ δ^(t-1), (7) where the i-th element (for i∈1,…,dli∈\1,…,d_l\) of the intercept contribution is δ¯i(t−1)=∑j:A^ij(t)>0A^ij(t)β¯j(t−1)+∑j:A^ij(t)≤0A^ij(t)β¯j(t−1) δ^(t-1)_i= _j:\, A^(t)_ij>0 A^(t)_ij β^(t-1)_j+ _j:\, A^(t)_ij≤ 0 A^(t)_ij β^(t-1)_j, and ¯(t−1) δ^(t-1) is defined analogously with β¯ β and β¯ β swapped. The recursion terminates at the input layer yielding (0)=(1)(1)A^(0)=A^(1)W^(1), ¯(0)=¯(1)+(1)(1) c^(0)= c^(1)+A^(1)b^(1), and ¯(0)=¯(1)+(1)(1) c^(0)= c^(1)+A^(1)b^(1). By applying Hölder’s inequality over the ℓp _p-ball ℬp(0,ϵ)B_p(x_0,ε) (where 1/p+1/q=11/p+1/q=1), the symbolic bounds in Eq. (3) are converted into concrete element-wise bounds: z¯i(l) z^(l)_i =i,:(0)0+c¯i(0)−ϵ‖i,:(0)‖q, =A^(0)_i,:x_0+ c^(0)_i-ε\|A^(0)_i,:\|_q, (8) z¯i(l) z^(l)_i =i,:(0)0+c¯i(0)+ϵ‖i,:(0)‖q. =A^(0)_i,:x_0+ c^(0)_i+ε\|A^(0)_i,:\|_q. (9) Margin verification. For margin verification between classes y and j, we apply LBP to the output layer (l=Ll=L) by setting (L)←y,:(L)−j,:(L)∈ℝ1×dL−1W^(L) ^(L)_y,:-W^(L)_j,: ^1× d_L-1 and b(L)←by(L)−bj(L)∈ℝb^(L)← b^(L)_y-b^(L)_j . With dL=1d_L=1, the coefficient matrix (t)A^(t) reduces to a row vector and c¯(t) c^(t) to a scalar. The certified lower bound is: f¯y,j=(0)0+c¯(0)−ϵ‖(0)‖q. f_y,j=A^(0)x_0+ c^(0)-ε\|A^(0)\|_q. (10) Local robustness is verified if f¯y,j>0 f_y,j>0. 3.2 Secure Computation Primitives In the standard 2PC setting [Yao, 1982, Goldreich et al., 1987], two parties (P0P_0 and P1P_1) jointly compute a function over their private inputs, revealing nothing beyond the prescribed output. Computations are performed in the ring ℤ2kZ_2^k of bit-length k (modulo 2k2^k is omitted for brevity). A real value v∈ℝv is encoded in two’s complement fixed-point format with nfn_f fractional bits as v~=⌊v⋅2nf⌋∈ℤ2k v= v· 2^n_f _2^k. Additive Secret Sharing (ASS). A value x∈ℤ2kx _2^k is additively shared as ⟨x⟩=⟨x⟩0,⟨x⟩1 x =\ x _0, x _1\ such that x=⟨x⟩0+⟨x⟩1x= x _0+ x _1. To generate shares, P0P_0 samples ⟨x⟩0∈ℤ2k x _0 _2^k uniformly at random and sets ⟨x⟩1=x−⟨x⟩0 x _1=x- x _0; each individual share is information-theoretically independent of x. ASS supports linear operations locally. Given shares ⟨x⟩,⟨y⟩ x , y and a public value c∈ℤ2kc _2^k, party PiP_i (i∈0,1i∈\0,1\) computes ⟨x+y⟩i=⟨x⟩i+⟨y⟩i,⟨c⋅x⟩i=c⋅⟨x⟩i. x+y _i= x _i+ y _i, c· x _i=c· x _i. For adding a public constant, one party (e.g., P0P_0) absorbs it locally: ⟨x+c⟩0=⟨x⟩0+c x+c _0= x _0+c and ⟨x+c⟩1=⟨x⟩1 x+c _1= x _1. Secure Multiplication via Beaver Triples. Nonlinear operations require interaction. A standard technique uses a Beaver triple (⟨a⟩,⟨b⟩,⟨c⟩)( a , b , c ) with c=a⋅bc=a· b. Given ⟨x⟩,⟨y⟩ x , y , parties compute masked differences e=x−ae=x-a and d=y−bd=y-b by locally forming ⟨e⟩=⟨x⟩−⟨a⟩ e = x - a and ⟨d⟩=⟨y⟩−⟨b⟩ d = y - b , then opening e and d (i.e., exchanging shares and reconstructing the public values). They then output product shares ⟨x⋅y⟩i=⟨c⟩i+d⋅⟨a⟩i+e⋅⟨b⟩i+(1−i)⋅e⋅d, x· y _i= c _i+d· a _i+e· b _i+(1-i)· e· d, where i∈0,1i∈\0,1\. This yields ⟨x⋅y⟩0+⟨x⋅y⟩1=xy x· y _0+ x· y _1=xy, followed by a truncation procedure to restore the fixed-point scale, i.e., ⟨xy~⟩=⟨⌊x~⋅y~/2nf⌋⟩ xy = x· y/2^n_f . Function Secret Sharing. FSS generalizes secret sharing from values to functions [Boyle et al., 2015]. A two-party FSS scheme for a function family G consists of: • (1λ,g)→(k0,k1) Gen(1^λ,g)→(k_0,k_1): a randomized key generation algorithm that, given a security parameter λ and a function g∈g , outputs two correlated keys (k0,k1)(k_0,k_1). • (i,ki,x)→yi Eval(i,k_i,x)→ y_i: a deterministic evaluation algorithm run by PiP_i on input x (typically a public masked value in MPC), producing an output share yiy_i such that y0+y1=g(x)y_0+y_1=g(x) (over an appropriate output ring). Intuitively, each key kik_i hides the function g, yet the two evaluations add up to the correct value. A key instantiation is the Distributed Comparison Function (DCF), computing gθ,ρ<(x)=ρ⋅x<θg^<_θ,ρ(x)=ρ·I\x<θ\ for threshold θ and payload ρ, where I is the indicator function. DCF is a basic primitive for secure comparison and is commonly used to build higher-level operators such as ReLU and fixed-point truncation. FSS-Based Secure Evaluation on Masked Values. Many FSS-based 2PC protocols maintain a masking invariant on intermediate values. Consequently, for a private value x∈ℤ2kx _2^k, the parties hold a public masked value x^=x+rin x=x+r_in, where rinr_in is a preprocessed random mask unknown to either party. To evaluate y=g(x)y=g(x) while preserving the invariant, the parties generate FSS keys for a shifted function: grin,rout(x^)=g(x^−rin)+rout,g_r_in,r_out( x)=g( x-r_in)+r_out, where routr_out is a fresh output mask. Each party evaluates its key on x x to obtain shares of grin,rout(x^)g_r_in,r_out( x), which reconstruct to y^=g(x)+rout y=g(x)+r_out. Thus the output remains masked in the same form, enabling secure composition of function evaluations without revealing intermediate plaintexts. 4 Problem Formulation System Setup. We study privacy-preserving robustness verification in a 2PC setting with a model owner (P0P_0) and a data owner (P1P_1). The network architecture (number of layers L and layer dimensions dll=0L\d_l\_l=0^L) is assumed to be public. The model owner P0P_0 holds a trained neural network f with private parameters (l),(l)l=1L\W^(l),b^(l)\_l=1^L, which represent proprietary intellectual property. The data owner P1P_1 holds a verification query consisting of input 0∈ℝd0x_0 ^d_0, robustness perturbation radius ϵ>0ε>0 (the magnitude of worst-case perturbations to certify against), and the classification target pair (true label y, target label j). During setup, P0P_0 secret-shares the model parameters, retains ⟨(l)⟩0,⟨(l)⟩0l=1L\ ^(l) _0, ^(l) _0\_l=1^L, and sends ⟨(l)⟩1,⟨(l)⟩1l=1L\ ^(l) _1, ^(l) _1\_l=1^L to P1P_1. To avoid the O(K)O(K) overhead associated with secure array indexing, P1P_1 encodes the verification target as a difference vector =y−j∈−1,0,1Kd=e_y-e_j∈\-1,0,1\^K (where ye_y and je_j are one-hot vectors). P1P_1 then secret-shares these encoded inputs, retaining (⟨0⟩1,⟨ϵ⟩1,⟨⟩1)( _0 _1, ε _1, _1) and sending (⟨0⟩0,⟨ϵ⟩0,⟨⟩0)( _0 _0, ε _0, _0) to P0P_0. Threat Model. We consider the semi-honest (honest-but-curious) adversarial model, where both parties follow the protocol specification but may attempt to infer the other party’s private input from their view. The protocol operates in a preprocessing model with a trusted dealer D that distributes correlated randomness (Beaver triples, FSS keys) during an offline phase. The preprocessing depends only on public parameters, so D learns nothing about private inputs. We assume D does not collude with either party. In practice, D can be instantiated via trusted hardware or replaced by a two-party preprocessing protocol. Problem Statement. Given secret shares of a neural network f and a verification query (0,ϵ,)(x_0,ε,d) held by the two parties (where y and j are encoded in the difference vector d), design a 2PC protocol that enables P1P_1 to determine whether the network is certifiably ℓ∞ _∞-robust at (0,ϵ)(x_0,ε) for the margin between classes y and j. The parties jointly compute secret shares of the certified lower bound f¯y,j f_y,j (Eq. (10)). Upon completion, P0P_0 sends ⟨f¯y,j⟩0 f_y,j _0 to P1P_1, who reconstructs f¯y,j=⟨f¯y,j⟩0+⟨f¯y,j⟩1 f_y,j= f_y,j _0+ f_y,j _1 and concludes robust if f¯y,j>0 f_y,j>0, or unknown otherwise. While the problem formulation above is general, our current protocol instantiates it for fully connected ReLU networks; extensions to other architectures are discussed in Appendix D. Design Goals. SecureCROWN targets two objectives: (1) Input and Model Privacy: The protocol satisfies semi-honest security. P0P_0 learns nothing about (0,ϵ,)(x_0,ε,d) beyond public parameters, and P1P_1 learns only f¯y,j f_y,j. All intermediate quantities remain secret-shared throughout. (2) Faithful Verification Semantics: The protocol preserves the decision behavior of the plaintext verifier (Section 3.1). Any numerical error introduced by fixed-point arithmetic must be bounded to prevent unsound certifications. Security Definition. We formalize semi-honest security in the real/ideal paradigm. Let 0=(l),(l)l=1L inp_0=\W^(l),b^(l)\_l=1^L and 1=(0,ϵ,) inp_1=(x_0,ε,d) denote the private inputs of P0P_0 and P1P_1, respectively. The ideal functionality is defined as ℱ(0,1)=(⊥,f¯y,j)F( inp_0, inp_1)=( , f_y,j), where P0P_0 receives no output (⊥ ) and P1P_1 receives the certified lower bound. Definition 1 (Semi-Honest Security). Protocol Π securely computes ℱF if for each i∈0,1i∈\0,1\, there exists a probabilistic polynomial-time (PPT) simulator i Sim_i such that: i(1λ,i,ℱi(0,1))≡ciΠ(1λ,0,1) \ Sim_i(1^λ, inp_i,F_i( inp_0, inp_1)) \ c≡ \ View _i(1^λ, inp_0, inp_1) \ (11) where iΠ View _i denotes the view of PiP_i (input, randomness, received messages), ℱiF_i denotes the output to PiP_i, and ≡c c≡ denotes computational indistinguishability. 5 Methodology 5.1 Overview Challenges. Implementing the robustness verification (Section 3.1) in MPC presents two fundamental challenges. (1) Data-dependent branching: The relaxation slope α depends on neuron activation state—inactive (z¯≤0 z≤ 0), active (z¯≥0 z≥ 0), or unstable—each requiring distinct computation (Eq. (2)). Similarly, intercept terms ¯ δ and ¯ δ (Eqs. (6)–(7)) depend on coefficient signs. In MPC, such data-dependent branching requires costly secure comparison, preventing efficient batching across neurons. (2) Precision sensitivity in deep recursion: The backward recursion in Eq. (5) updates the coefficient matrix (t)A^(t) across layers, with relaxation slopes (t) α^(t) computed via division (Eq. (2)). In fixed-point MPC, division has limited precision, and truncation errors accumulate through the propagation chain, potentially compromising verification accuracy in deep networks. Our Approach. We address these challenges through two key techniques. (1) Branch Elimination via ReLU: We observe that all branching conditions in the verifier are fundamentally sign tests. Since ReLU inherently encodes sign information, we reformulate conditional logic into unified arithmetic expressions where ReLU outputs naturally select the correct terms. This eliminates branching entirely, enabling identical computation paths for all neurons and facilitating efficient vectorized execution in MPC. These ReLU operations are efficiently realized via FSS-based protocols with constant-round communication. (2) Newton–Raphson Refinement: To address precision loss in secure division, we apply Newton–Raphson iterations to refine reciprocal estimates, approximately doubling the precision bits per iteration at minimal additional cost. Protocol Overview. The protocol operates in the preprocessing model: correlated randomness is generated offline based on the public network architecture, reducing the online phase to local computations and share exchanges. Specifically, in the offline phase, the trusted dealer D generates correlated randomness based on the network architecture d0,…,dL\d_0,…,d_L\, including Beaver triples for multiplication, FSS keys with associated input masks for function evaluations, and other correlated randomness required by the sub-protocols. This phase is data-independent, so D learns nothing about private inputs. The online phase begins with input sharing, where the parties secret-share their private inputs as described in Section 4. Next, in the secure computation phase, the parties jointly execute ΠVerify _Verify (Algorithm 2): for each hidden layer l∈1,…,L−1l∈\1,…,L-1\, compute pre-activation bounds ⟨¯(l)⟩,⟨¯(l)⟩ z^(l) , z^(l) via ΠBackward _Backward (Algorithm 1) and derive relaxation slopes ⟨(l)⟩ α^(l) via Π _ α; then execute a final backward pass using ⟨⟩ to compute ⟨f¯y,j⟩ f_y,j (Eq. (10)). Finally, in the output phase, P0P_0 sends ⟨f¯y,j⟩0 f_y,j _0 to P1P_1, who reconstructs the certified lower bound f¯y,j f_y,j and concludes local robustness if f¯y,j>0 f_y,j>0. 5.2 Secure Building Blocks Secure Multiplication ( SecMul, SecMatMul). Secure scalar multiplication (⟨x⟩,⟨y⟩)→⟨xy⟩ SecMul( x , y )→ xy follows the standard Beaver triple protocol (Section 3.2). For matrix multiplication, given inputs ∈ℤ2km×nX _2^k^m× n and ∈ℤ2kn×pY _2^k^n× p, the protocol computes (⟨⟩,⟨⟩)→⟨⟩ SecMatMul( , )→ by consuming matrix-level Beaver triples (⟨⟩,⟨⟩,⟨⟩)( , , ), thereby avoiding the overhead of scalar-wise decomposition. Secure Arithmetic Right Shift ( SecARS). To realign the radix point after fixed-point multiplications—which inherently yield 2nf2n_f fractional bits—we must restore the standard nfn_f-bit precision. We achieve this via (⟨x⟩,nf)→⟨⌊x/2nf⌋⟩ SecARS( x ,n_f)→ x/2^n_f , efficiently instantiated using the DCF-based protocol of Gupta et al. [2025]. Secure ReLU and Absolute Value ( SecReLU, SecAbs). Both primitives are built on securely computing the sign indicator μ=[x<0]μ=I[x<0] via DCF. Parties evaluate preprocessed DCF keys to obtain the secret-shared bit ⟨μ⟩ μ , and subsequently compute (⟨x⟩)→(⟨1−μ⟩,⟨x⟩) SecReLU( x )→ SecMul( 1-μ , x ) and (⟨x⟩)→(⟨1−2μ⟩,⟨x⟩) SecAbs( x )→ SecMul( 1-2μ , x ). Each primitive strictly requires one DCF evaluation followed by one SecMul operation. Secure Reciprocal ( SecRecip). We implement the reciprocal protocol (⟨x⟩)→⟨1/x⟩ SecRecip( x )→ 1/x in two stages. First, we adapt the FSS-based approach from Gupta et al. [2025] to generate an initial approximation. The input magnitude is decomposed as |x|≈(1+m2ℓm)⋅2e|x|≈(1+ m2 _m)· 2^e, and a seed w0≈1/|x|w_0≈ 1/|x| is computed via w0=2−e⋅2ℓm2ℓm+mw_0=2^-e· 2 _m2 _m+m, where the terms are retrieved via spline and lookup tables. Second, since the lookup-based initialization provides limited precision, we perform nitern_iter Newton–Raphson iterations wi+1=wi⋅(2−|x|⋅wi)w_i+1=w_i·(2-|x|· w_i) to refine the result to the target precision. Each iteration roughly doubles the number of accurate bits, ensuring sufficient numerical stability for subsequent verification steps. 5.3 Secure Slope Computation Π _ α The relaxation slope vector (l) α^(l) in Eq. (2) is essential for constructing the linear propagation matrices in LBP. Although the definition is simple, securely evaluating the piecewise logic in Eq. (2) is costly in MPC, as it requires secure comparisons and data-dependent branching per neuron to distinguish active, inactive, and unstable states. To circumvent these overheads and enable efficient execution, we reformulate the piecewise logic into a unified, data-independent arithmetic expression applied element-wise across all neurons in the layer: =ReLU(¯)ReLU(¯)+ReLU(−¯)+ϵs. α= ReLU( z)ReLU( z)+ReLU(- z)+ _s. (12) This formulation naturally encapsulates the three theoretical cases within a single data-independent execution path: for inactive neurons where z¯≤0 z≤ 0, the vanishing numerator ReLU(z¯)=0ReLU( z)=0 yields a slope of α=0α=0; for active neurons where z¯≥0 z≥ 0, the term ReLU(−z¯)=0ReLU(- z)=0 results in α≈1α≈ 1; and for unstable neurons, the expression simplifies to the optimal chord slope z¯/(z¯−z¯) z/( z- z). To ensure numerical robustness during the MPC execution, we introduce a small public stability constant ϵs _s into the denominator of Eq. (12). This safeguard prevents potential division-by-zero errors that may arise when pre-activation bounds [z¯,z¯][ z, z] vanish near zero—a common phenomenon in deep neural networks due to the accumulation of conservative bounds during propagation. A theoretical analysis of its impact on the certified bounds is provided in Appendix B.3. The detailed vectorized protocol Π _ α, which achieves branching-free computation using SecReLU, SecRecip, and SecMul primitives, is presented in Algorithm 3 in Appendix A. 5.4 Secure Intercept Accumulation Π _ δ As established in Eqs. (6)–(7), the intercept contribution vectors ¯(t−1),¯(t−1)∈ℝdl δ^(t-1), δ^(t-1) ^d_l depend on the element-wise signs of the intermediate coefficient matrix ^(t)∈ℝdl×dt−1 A^(t) ^d_l× d_t-1. From Eq. (2), the lower relaxation intercept is β¯j(t−1)=0 β^(t-1)_j=0 for all neurons, while the upper intercept is β¯j(t−1)=−αj(t−1)z¯j(t−1) β^(t-1)_j=-α^(t-1)_j z^(t-1)_j for unstable neurons (and zero otherwise). Since β¯j(t−1)=0 β^(t-1)_j=0, the accumulations simplify significantly: only terms involving β¯ β contribute. By substituting Aij(t−1)=A^ij(t)αj(t−1)A^(t-1)_ij= A^(t)_ijα^(t-1)_j (Eq. (5)) and noting that αj(t−1)≥0α^(t-1)_j≥ 0 preserves signs, the i-th elements of the lower and upper contributions reduce to δ¯i(t−1)=∑j:Aij(t−1)≤0Aij(t−1)(−z¯j(t−1)) δ^(t-1)_i= _j:\,A^(t-1)_ij≤ 0A^(t-1)_ij(- z^(t-1)_j) and δ¯i(t−1)=∑j:Aij(t−1)>0Aij(t−1)(−z¯j(t−1)) δ^(t-1)_i= _j:\,A^(t-1)_ij>0A^(t-1)_ij(- z^(t-1)_j), respectively. To avoid expensive secure comparisons in MPC, these conditional summations can be elegantly reformulated into unified matrix-vector multiplications using ReLU operations: ¯(t−1) δ^(t-1) =−ReLU(−(t−1))ReLU(−¯(t−1)), =-ReLU(-A^(t-1))ReLU(- z^(t-1)), (13) ¯(t−1) δ^(t-1) =ReLU((t−1))ReLU(−¯(t−1)), =ReLU(A^(t-1))ReLU(- z^(t-1)), (14) The protocol Π _ δ is given in Algorithm 4 (Appendix A). Algorithm 1 ΠBackward _Backward: Secure Linear Bound Propagation 1:Target layer l; ⟨(t)⟩,⟨¯(t)⟩t=1l−1\ α^(t) , z^(t) \_t=1^l-1; ⟨0⟩ _0 ; ⟨ϵ⟩ ε 2:Concrete bounds ⟨¯(l)⟩,⟨¯(l)⟩ z^(l) , z^(l) 3:⟨⟩←⟨dl⟩ ← _d_l ; ⟨¯⟩←⟨⟩ c ← 0 ; ⟨¯⟩←⟨⟩ c ← 0 4:for t=l,…,2t=l,…,2 do 5: ⟨^⟩←(⟨⟩,⟨(t)⟩) A ← SecMatMul( , ^(t) ) ⊳ Eq. (4) 6: ⟨⟩←(⟨^⟩,⟨diag((t−1))⟩) ← SecMatMul( A , ( α^(t-1)) ) 7:⊳ Eq. (5) 8: ⟨¯⟩,⟨¯⟩←Π(⟨⟩,⟨¯(t−1)⟩) δ , δ ← _ δ( , z^(t-1) ) ⊳ Eqs. (13)–(14) 9: ⟨¯⟩←⟨¯⟩+(⟨⟩,⟨(t)⟩)+⟨¯⟩ c ← c + SecMatMul( , ^(t) )+ δ 10:⊳ Eq. (6) 11: ⟨¯⟩←⟨¯⟩+(⟨⟩,⟨(t)⟩)+⟨¯⟩ c ← c + SecMatMul( , ^(t) )+ δ 12:⊳ Eq. (7) 13:⟨(0)⟩←(⟨⟩,⟨(1)⟩) ^(0) ← SecMatMul( , ^(1) ) 14:⟨¯(0)⟩←⟨¯⟩+(⟨⟩,⟨(1)⟩) c^(0) ← c + SecMatMul( , ^(1) ) 15:⟨¯(0)⟩←⟨¯⟩+(⟨⟩,⟨(1)⟩) c^(0) ← c + SecMatMul( , ^(1) ) 16:⟨⟩←RowSum((⟨(0)⟩)) ( SecAbs( ^(0) )) 17:⊳ Row-wise ℓ1 _1-norm 18:⟨⟩←(⟨(0)⟩,⟨0⟩) ← SecMatMul( ^(0) , _0 ); 19:⟨⟩←(⟨ϵ⟩,⟨⟩) ← SecMul( ε , ) 20:⟨¯(l)⟩←⟨⟩+⟨¯(0)⟩−⟨⟩ z^(l) ← + c^(0) - ; 21:⟨¯(l)⟩←⟨⟩+⟨¯(0)⟩+⟨⟩ z^(l) ← + c^(0) + 22:return ⟨¯(l)⟩,⟨¯(l)⟩ z^(l) , z^(l) Algorithm 2 ΠVerify _Verify: Secure Robustness Verification 1:Shares ⟨(l)⟩ ^(l) , ⟨(l)⟩ ^(l) for l∈[L]l∈[L]; ⟨0⟩ _0 ; ⟨ϵ⟩ ε ; ⟨⟩ 2:Certified lower bound ⟨f¯y,j⟩ f_y,j 3:/* Iterative Bound and Slope Computation */ 4:⟨(1)⟩←(⟨(1)⟩,⟨0⟩)+⟨(1)⟩ ^(1) ← SecMatMul( ^(1) , _0 )+ ^(1) 5:⟨(1)⟩←RowSum((⟨(1)⟩)) ^(1) ( SecAbs( ^(1) )) ⊳ Row-wise ℓ1 _1-norm 6:⟨¯(1)⟩←⟨(1)⟩+(⟨ϵ⟩,⟨(1)⟩) z^(1) ← ^(1) + SecMul( ε , ^(1) ) 7:⟨¯(1)⟩←⟨(1)⟩−(⟨ϵ⟩,⟨(1)⟩) z^(1) ← ^(1) - SecMul( ε , ^(1) ) 8:⟨(1)⟩←Πα(⟨¯(1)⟩,⟨¯(1)⟩) α^(1) ← _α( z^(1) , z^(1) ) 9:for l=2,…,L−1l=2,…,L-1 do 10: ⟨¯(l)⟩,⟨¯(l)⟩←ΠBackward(l,⟨(t)⟩,⟨¯(t)⟩t=1l−1) z^(l) , z^(l) ← _Backward(l,\ α^(t) , z^(t) \_t=1^l-1) 11: ⟨(l)⟩←Πα(⟨¯(l)⟩,⟨¯(l)⟩) α^(l) ← _α( z^(l) , z^(l) ) 12:/* Margin Certification */ 13:⟨(L)⟩←(⟨⟩⊤,⟨(L)⟩) ^(L) ← SecMatMul( , ^(L) ) 14:⟨b(L)⟩←(⟨⟩⊤,⟨(L)⟩) b^(L) ← SecMatMul( , ^(L) ) 15:⟨f¯y,j⟩,_←ΠBackward(L,⟨(t)⟩,⟨¯(t)⟩t=1L−1) f_y,j ,\_← _Backward(L,\ α^(t) , z^(t) \_t=1^L-1) 16:return ⟨f¯y,j⟩ f_y,j 5.5 Secure Verification Protocol Building on the sub-protocols Π _ α and Π _ δ, we now present the complete secure verification protocol. Algorithm 1 (ΠBackward _Backward) securely implements the backward recursion (Eqs. (4)–(7)) for a target layer l. Starting with ⟨⟩=⟨dl⟩ = _d_l and ⟨¯⟩=⟨¯⟩=⟨⟩ c = c = 0 , the protocol iterates for t=l,…,2t=l,…,2, performing coefficient propagation ( SecMatMul), slope multiplication ( SecMul), intercept accumulation (Π _ δ), and bias addition. Final bounds follow from Hölder’s inequality (Eqs. (8)–(9)), with the ℓ1 _1-norm computed via SecAbs and local summation (for ℓ∞ _∞-perturbations). Iterative Bound and Slope Computation. As described in Section 3.1, computing bounds at layer l requires slopes from all preceding layers, so the parties compute bounds and slopes iteratively from l=1l=1 to L−1L-1. For l=1l=1, bounds are computed directly: the linear term ⟨(1)0⟩ ^(1)x_0 via SecMatMul and the row-wise norm via SecAbs; slopes ⟨(1)⟩ α^(1) then follow from Π _ α. For l≥2l≥ 2, the parties invoke ΠBackward _Backward with previously computed slope shares to obtain ⟨¯(l)⟩,⟨¯(l)⟩ z^(l) , z^(l) , and then derive ⟨(l)⟩ α^(l) via Π _ α. Margin Certification. After obtaining all slope shares ⟨(1)⟩,…,⟨(L−1)⟩ α^(1) ,…, α^(L-1) , the parties compute the certified margin ⟨f¯y,j⟩ f_y,j via a final backward pass. To avoid O(K)O(K) overhead from secure array indexing, P1P_1 provides a difference vector ⟨⟩ where =y−j∈−1,0,1Kd=e_y-e_j∈\-1,0,1\^K. The backward pass initializes ⟨(L)⟩←(⟨⟩⊤,⟨(L)⟩)∈ℝ1×dL−1 ^(L) ← SecMatMul( , ^(L) ) ^1× d_L-1 and ⟨b(L)⟩←(⟨⟩⊤,⟨(L)⟩)∈ℝ b^(L) ← SecMul( , ^(L) ) . This reduces the coefficient (t)A^(t) to a row vector in ℝ1×dtR^1× d_t, lowering per-layer communication from O(d2)O(d^2) to O(d)O(d). The parties then invoke ΠBackward _Backward with target layer L to obtain ⟨(0)⟩ ^(0) and ⟨c¯(0)⟩ c^(0) , from which the certified margin ⟨f¯y,j⟩ f_y,j follows via Eq. (10). 6 Theoretical Analysis Security. The security of SecureCROWN is analyzed under the semi-honest adversary model (Definition 1). The proof constructs a simulator via a hybrid argument over L layers, reducing security to the underlying FSS and ASS primitives. The complete proof of Theorem 6.1 is provided in Appendix B.1. A pathway for upgrading to malicious security, together with an empirical cost estimate, is discussed in Appendix C. Theorem 6.1 (Security). Protocol Πverify _verify securely computes ℱverifyF_verify in the ℱF_D-hybrid model against semi-honest adversaries. Complexity. For an L-layer network with maximum width d, SecureCROWN requires O(L2)O(L^2) rounds, O(L2d2k)O(L^2d^2k) communication, and O(L2d3)O(L^2d^3) computation (Appendix B.2). Error Analysis. Fixed-point arithmetic introduces error in f¯y,j f_y,j bounded by a network-depth-dependent multiple of the per-operation rounding unit εq=2−nf _q=2^-n_f(Appendix B.3). With maximum weight norm ρ=maxi‖(i)‖∞ρ= _i\|W^(i)\|_∞, the absolute error in each output bound entry scales as O(L)εqO(L)\, _q, O(L2)εqO(L^2)\, _q, and O(ρL)εqO(ρ^L)\, _q for the stable (ρ<1ρ<1), unit-norm (ρ=1ρ=1), and unstable (ρ>1ρ>1) regimes, respectively. 7 Experimental Evaluation 7.1 Experimental Setup Implementation. We implement SecureCROWN in C++, with k=64k=64-bit fixed-point representation, nf=26n_f=26 fractional bits, stability constant ϵs=10−4 _s=10^-4, and niter=1n_iter=1 Newton–Raphson refinement iteration in SecRecip (the FSS-based seed provides approximately ⌈nf/2⌉ n_f/2 accurate bits, and one iteration doubles this to ≥nf≥\,n_f bits). Experiments are run on a machine with an Intel Xeon w7-3445 CPU and 64 GB of RAM, using four CPU threads. We simulate network conditions via Linux tc: LAN (10 Gbps bandwidth, 0.05ms round-trip time (RTT)) and WAN (370/600 Mbps, 40/60 ms RTT). Results are averaged over 10 trials. Our replication package is available at https://github.com/songzhibo1/SecureCROWN. Table 1: Fidelity analysis of SecureCROWN. m×[n]m×[n]: m layers, n neurons each. R: Robust (f¯y,j>0 f_y,j>0); U: Unknown (f¯y,j≤0 f_y,j≤ 0). Avg. Data Model Rob. ϵε Result MRE Cons. MNIST 2×[20]2×[20] 0.0448 0.0150.015 All R (99) 4.45×−4.45× 10^-7 %100\% 0.0450.045 R (43) 9.52×−9.52× 10^-7 %100\% U (56) 8.70×10−78.70× 10^-7 %100\% 0.10.1 All U (99) 3.27×10−73.27× 10^-7 %100\% 3×[20]3×[20] 0.0304 0.0150.015 R (93) 1.41×−1.41× 10^-6 %100\% U (1) 1.08×10−41.08× 10^-4 %100\% 0.0300.030 R (44) 7.18×−7.18× 10^-6 %100\% U (50) 3.68×10−63.68× 10^-6 %100\% 0.10.1 All U (94) 6.85×10−76.85× 10^-7 %100\% 3×[256]3×[256] 0.0159 0.0150.015 R (49) 6.20×−6.20× 10^-6 %100\% U (51) 1.14×10−51.14× 10^-5 %100\% 0.10.1 All U (100) 9.29×10−79.29× 10^-7 %100\% 5×[256]5×[256] 0.0149 0.0150.015 R (50) 7.78×−7.78× 10^-6 %100\% U (50) 1.21×10−51.21× 10^-5 %100\% 0.10.1 All U (100) 6.16×10−56.16× 10^-5 %100\% 7×[256]7×[256] 0.0132 0.0150.015 R (30) 2.66×−2.66× 10^-5 %100\% U (69) 1.32×10−21.32× 10^-2 %100\% 0.10.1 All U (99) 9.18×10−29.18× 10^-2 %100\% CIFAR-10 5×[100]5×[100] 0.0021 0.0020.002 R (24) 5.23×−5.23× 10^-5 %100\% U (21) 7.78×10−57.78× 10^-5 %100\% 0.00780.0078 All U (45) 5.65×10−55.65× 10^-5 %100\% 7×[100]7×[100] 0.0013 0.0010.001 R (32) 2.82×−2.82× 10^-4 %100\% U (14) 1.50×10−41.50× 10^-4 %100\% 10×[200]10×[200] 0.0010 0.0010.001 R (28) 1.73×−1.73× 10^-3 %100\% U (24) 1.67×10−41.67× 10^-4 %100\% Figure 1: Online latency breakdown across network conditions and model architectures. Baseline. As no prior work addresses privacy-preserving robustness verification, we compare against the plaintext CROWN algorithm (Section 3.1), implemented in Python and executed single-threaded. This serves as the correctness oracle for validating numerical fidelity. Models and Datasets. We evaluate on MNIST [LeCun et al., 1998] and CIFAR-10 [Krizhevsky, 2009] using fully-connected ReLU networks. MNIST models (2×[20]2×[20] to 7×[256]7×[256]) are from [Zhang et al., 2018] and VNN-COMP [Brix et al., 2023]; CIFAR-10 models (5×[100]5×[100] to 10×[200]10×[200]) are from ERAN [Singh et al., 2019]. For each configuration, we randomly sample 100 test images, verify those that are correctly classified, and test multiple ϵε values under ℓ∞ _∞ perturbations—including values near the robustness boundary (mixed Robust/Unknown outcomes) and extreme values (all Robust or all Unknown). 7.2 Results RQ1: Fidelity. We validate SecureCROWN’s correctness by measuring numerical fidelity against the plaintext baseline using two metrics. The first is Mean Relative Error (MRE): MRE=1N∑i=1N|(f¯y,jsec,(i)−f¯y,jplain,(i))/f¯y,jplain,(i)|MRE= 1N _i=1^N|( f_y,j^sec,(i)- f_y,j^plain,(i))/ f_y,j^plain,(i)|, where f¯y,jsec f_y,j^sec and f¯y,jplain f_y,j^plain denote the SecureCROWN and plaintext certified lower bounds, respectively. The second is Verification Consistency, the percentage of samples with identical verification outcomes. As shown in Table 1, SecureCROWN achieves high numerical fidelity, with MRE scaling predictably with network depth. Our evaluation specifically examines challenging cases near the robustness boundary, as reflected by the mixed Robust/Unknown outcomes in Table 1. For shallow networks (MNIST 2×[20]2×[20]), MRE remains at ≈10−7≈ 10^-7. As depth increases, cumulative rounding errors in recursive bound propagation lead to higher MRE—from 6.20×10−66.20× 10^-6 (MNIST 3×[256]3×[256]) to 1.73×10−31.73× 10^-3 for CIFAR-10 10×[200]10×[200]. Despite this, SecureCROWN maintains 100% verification consistency with the plaintext baseline across all 8 architectures and multiple ϵε configurations, confirming that our approach faithfully preserves the decision behavior of the plaintext verifier. Table 2: Online communication volume breakdown (MB). Dataset Model Communication (MB) Input Comp. E2E MNIST 2×[20]2×[20] 0.130.13 0.640.64 0.770.77 3×[20]3×[20] 0.140.14 1.781.78 1.921.92 3×[256]3×[256] 2.072.07 30.1630.16 32.2332.23 5×[256]5×[256] 3.073.07 109.95109.95 113.02113.02 7×[256]7×[256] 4.074.07 234.80234.80 238.88238.88 CIFAR-10 5×[100]5×[100] 2.632.63 83.7683.76 86.3986.39 7×[100]7×[100] 2.782.78 140.92140.92 143.71143.71 10×[200]10×[200] 7.207.20 596.97596.97 604.17604.17 RQ2: Online Efficiency. We evaluate online efficiency by analyzing runtime latency and communication volume across network conditions and model architectures. We break down the end-to-end (E2E) execution into two phases: (1) Input Processing, encompassing secure input sharing and constraint setup; (2) Computation, the secure backward bound propagation with FSS-based nonlinear primitives. Figure 1 and Table 2 summarize the results. Latency. As shown in Figure 1, E2E latency ranges from 0.1s to 200.5s across network conditions and model architectures. Smaller models (MNIST 2×[20]2×[20] to 3×[256]3×[256]) complete within 0.1–9.9s, while CIFAR-10 10×[200]10×[200] requires 151.1–200.5s. The computation phase dominates total latency, with input processing contributing only 0.0–0.3s. Bandwidth variation at fixed RTT (370 vs 600 Mbps, 40ms) yields <<2% difference, whereas increasing RTT from 40ms to 60ms incurs ∼ 5% overhead. This indicates that round-trip latency accumulates over O(L2)O(L^2) communication rounds, making RTT the dominant network factor. FSS evaluations are embarrassingly parallel across neurons, so exploiting more cores would further reduce latency for larger models. Communication. Table 2 details communication volume. E2E communication scales linearly with network complexity: from 0.77 MB (MNIST 2×[20]2×[20]) to 604.17 MB (CIFAR-10 10×[200]10×[200]). The computation phase dominates, accounting for ≈ 98.8% of total volume in the largest model. Input processing remains negligible (≤ 7.20 MB even for CIFAR-10), confirming that communication overhead scales with secure operations rather than input dimensions, ensuring scalability to higher-dimensional data. RQ3: Offline Preprocessing Overhead. As shown in Table 3, both time and storage scale with network complexity, ranging from 0.17 s / 39 MB (MNIST 2×[20]2×[20]) to 71.16 s / 31 GB (CIFAR-10 10×[200]10×[200]). While storage costs are substantial for deep networks, the preprocessing phase is one-time and data-independent—generated offline without access to private inputs. In practical deployment, preprocessing material can be prepared as a batch for multiple planned verification queries; each query consumes a fresh portion of the batch during execution, amortizing the generation cost across those queries. Table 3: Offline preprocessing overhead (one-time, data-independent). Dataset Model Time (s) Data (MB) MNIST 2×[20]2×[20] 0.170.17 3939 3×[20]3×[20] 0.410.41 100100 3×[256]3×[256] 4.204.20 16441644 5×[256]5×[256] 13.9313.93 56775677 7×[256]7×[256] 29.2129.21 11 89811\,898 CIFAR-10 5×[100]5×[100] 12.0312.03 45474547 7×[100]7×[100] 19.2519.25 75417541 10×[200]10×[200] 71.1671.16 31 06031\,060 RQ4: Sensitivity to the Stability Constant. We vary the stability constant ϵs _s (Eq. (12)) to examine its impact on verification outcomes. Specifically, ϵs _s is varied from 10−410^-4 (our default) to 10−110^-1 on MNIST 5×[256]5×[256] (ϵ=0.015ε=0.015). As shown in Table 4, verification consistency remains 100% across all tested values. At the same time, the reported MREs increase approximately linearly with ϵs _s, indicating that larger stability constants introduce larger numerical deviations from the plaintext bounds. On this benchmark, verification decisions remain unchanged even when ϵs _s is increased to 1000×1000× the default value. Table 4: Sensitivity to the stability constant ϵs _s on MNIST 5×[256]5×[256] (ϵ=0.015ε=0.015). ϵ _s Cons. Avg. MRE R (50) U (50) 10−110^-1 100% 5.86×10−25.86× 10^-2 1.40×10−11.40× 10^-1 10−210^-2 100% 6.47×10−36.47× 10^-3 1.50×10−21.50× 10^-2 10−310^-3 100% 6.49×10−46.49× 10^-4 1.52×10−31.52× 10^-3 10−410^-4 100% 7.05×10−57.05× 10^-5 1.62×10−41.62× 10^-4 8 Conclusion We propose SecureCROWN, the first privacy-preserving framework for neural network robustness verification in a 2PC setting. Our protocol addresses the key challenges of performing linear relaxation and backward bound computation on protected model parameters and inputs. We provided formal privacy guarantees in the semi-honest adversary model and analyzed the protocol’s computational complexity. Experiments on standard benchmarks validate that our method achieves verification fidelity comparable to plaintext verification with moderate cryptographic overhead, representing a promising step toward efficient privacy-preserving verification. Acknowledgements.This work was supported by the National Science and Technology Major Project (Grant 2022ZD0115901), the University of Bristol Engineering and Physical Sciences Research Council Impact Acceleration Account, and the National Natural Science Foundation of China (Grant Nos. 92582102, 62572013, and 62172019). Nianyun Song is supported by the China Scholarship Council (Grant 202506040106). We thank the anonymous reviewers for their constructive feedback. References Althoff [2015] Matthias Althoff. An introduction to CORA 2015. In 1st and 2nd International Workshop on Applied Verification for Continuous and Hybrid Systems, volume 34 of EPiC Series in Computing, pages 120–151. EasyChair, 2015. Boyle et al. [2015] Elette Boyle, Niv Gilboa, and Yuval Ishai. Function secret sharing. In Advances in Cryptology, EUROCRYPT 2015, volume 9057 of Lecture Notes in Computer Science, pages 337–367. Springer, 2015. Brix et al. [2023] Christopher Brix, Mark Niklas Müller, Stanley Bak, Taylor T. Johnson, and Changliu Liu. First three years of the international verification of neural networks competition (VNN-COMP). Int. J. Softw. Tools Technol. Transf., 25(3):329–339, 2023. Davenport and Kalakota [2019] Thomas Davenport and Ravi Kalakota. The potential for artificial intelligence in healthcare. Future Healthcare Journal, 6(2):94–98, 2019. Duong et al. [2023] Hai Duong, Linhan Li, ThanhVu Nguyen, and Matthew B. Dwyer. A DPLL(T) framework for verifying deep neural networks. CoRR, abs/2307.10266, 2023. Duong et al. [2024] Hai Duong, Dong Xu, ThanhVu Nguyen, and Matthew B. Dwyer. Harnessing neuron stability to improve DNN verification. Proc. ACM Softw. Eng., 1(FSE):859–881, 2024. Duong et al. [2025] Hai Duong, ThanhVu Nguyen, and Matthew B. Dwyer. NeuralSAT: A high-performance verification tool for deep neural networks. In Computer Aided Verification, CAV 2025, volume 15932 of Lecture Notes in Computer Science, pages 409–423. Springer, 2025. Esteva et al. [2017] Andre Esteva, Brett Kuprel, Roberto A Novoa, Justin Ko, Susan M Swetter, Helen M Blau, and Sebastian Thrun. Dermatologist-level classification of skin cancer with deep neural networks. Nature, 542(7639):115–118, 2017. Esteva et al. [2019] Andre Esteva, Alexandre Robicquet, Bharath Ramsundar, Volodymyr Kuleshov, Mark DePristo, Katherine Chou, Claire Cui, Greg Corrado, Sebastian Thrun, and Jeff Dean. A guide to deep learning in healthcare. Nature Medicine, 25(1):24–29, 2019. Evans et al. [2018] David Evans, Vladimir Kolesnikov, and Mike Rosulek. A pragmatic introduction to secure multi-party computation. Found. Trends Priv. Secur., 2(2-3):70–246, 2018. Goldreich et al. [1987] O. Goldreich, S. Micali, and A. Wigderson. How to play ANY mental game. In Proceedings of the Annual ACM Symposium on Theory of Computing, STOC 1987, pages 218–229. ACM, 1987. Goodfellow et al. [2015] Ian J. Goodfellow, Jonathon Shlens, and Christian Szegedy. Explaining and harnessing adversarial examples. In International Conference on Learning Representations, ICLR 2015, 2015. Gupta et al. [2025] Kanav Gupta, Nishanth Chandran, Divya Gupta, Jonathan Katz, and Rahul Sharma. SHARK: actively secure inference using function secret sharing. In IEEE Symposium on Security and Privacy, SP 2025, pages 2472–2490. IEEE, 2025. Hendrycks and Dietterich [2019] Dan Hendrycks and Thomas G. Dietterich. Benchmarking neural network robustness to common corruptions and perturbations. In International Conference on Learning Representations, ICLR 2019, 2019. Katz et al. [2017] Guy Katz, Clark Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. In Computer Aided Verification, CAV 2017, volume 10426 of Lecture Notes in Computer Science, pages 97–117. Springer, 2017. Katz et al. [2019] Guy Katz, Derek A. Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljic, David L. Dill, Mykel J. Kochenderfer, and Clark W. Barrett. The Marabou framework for verification and analysis of deep neural networks. In Computer Aided Verification, CAV 2019, volume 11561 of Lecture Notes in Computer Science, pages 443–452. Springer, 2019. Knott et al. [2021] Brian Knott, Shobha Venkataraman, Awni Y. Hannun, Shubho Sengupta, Mark Ibrahim, and Laurens van der Maaten. CrypTen: Secure multi-party computation meets machine learning. Advances in Neural Information Processing Systems, 34:4961–4973, 2021. Krizhevsky [2009] Alex Krizhevsky. Learning multiple layers of features from tiny images. Technical Report TR-2009, Department of Computer Science, University of Toronto, 2009. Kumar et al. [2020] Nishant Kumar, Mayank Rathee, Nishanth Chandran, Divya Gupta, Aseem Rastogi, and Rahul Sharma. CrypTFlow: Secure TensorFlow inference. In IEEE Symposium on Security and Privacy, SP 2020, pages 336–353. IEEE, 2020. LeCun et al. [1998] Yann LeCun, Léon Bottou, Yoshua Bengio, and Patrick Haffner. Gradient-based learning applied to document recognition. Proceedings of the IEEE, 86(11):2278–2324, 1998. Lee et al. [2022] Eunsang Lee, Joon-Woo Lee, Junghyun Lee, Young-Sik Kim, Yongjune Kim, Jong-Seon No, and Woosuk Choi. Low-complexity deep convolutional neural networks on fully homomorphic encryption using multiplexed parallel convolutions. In International Conference on Machine Learning, ICML 2022, volume 162 of Proceedings of Machine Learning Research, pages 12403–12422. PMLR, 2022. Lee et al. [2024] Seunghwa Lee, Hankyung Ko, Jihye Kim, and Hyunok Oh. vCNN: Verifiable convolutional neural network based on zk-SNARKs. IEEE Trans. Dependable Secur. Comput., 21(4):4254–4270, 2024. Litjens et al. [2017] Geert Litjens, Thijs Kooi, Babak Ehteshami Bejnordi, Arnaud Arindra Adiyoso Setio, Francesco Ciompi, Mohsen Ghafoorian, Jeroen Awm Van Der Laak, Bram Van Ginneken, and Clara I Sánchez. A survey on deep learning in medical image analysis. Medical Image Analysis, 42:60–88, 2017. Lou and Jiang [2021] Qian Lou and Lei Jiang. HEMET: A homomorphic-encryption-friendly privacy-preserving mobile neural network architecture. In International Conference on Machine Learning, ICML 2021, volume 139 of Proceedings of Machine Learning Research, pages 7102–7110. PMLR, 2021. Maheri et al. [2025] Mohammad Mahdi Maheri, Hamed Haddadi, and Alex Davidson. TeleSparse: Practical privacy-preserving verification of deep neural networks. Proc. Priv. Enhancing Technol., 2025(4):861–880, 2025. Mohassel and Rindal [2018] Payman Mohassel and Peter Rindal. ABY3: A mixed protocol framework for machine learning. In Proceedings of the ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, pages 35–52. ACM, 2018. Salman et al. [2019] Hadi Salman, Greg Yang, Huan Zhang, Cho-Jui Hsieh, and Pengchuan Zhang. A convex relaxation barrier to tight robustness verification of neural networks. Advances in Neural Information Processing Systems, 32:9835–9846, 2019. Shi et al. [2025] Zhouxing Shi, Qirui Jin, Zico Kolter, Suman Jana, Cho-Jui Hsieh, and Huan Zhang. Neural network verification with branch-and-bound for general nonlinearities. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2025, volume 15696 of Lecture Notes in Computer Science, pages 315–335. Springer, 2025. Singh et al. [2019] Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certifying neural networks. Proc. ACM Program. Lang., 3(POPL):1–30, 2019. Song et al. [2026] Nianyun Song, Fuyi Wang, Rongfang Bie, Yu Guo, Leo Yu Zhang, and Xiaohua Jia. ObliviGate: Towards architecture-oblivious privacy-preserving inference for malicious security. IEEE Transactions on Services Computing, 2026. Szegedy et al. [2014] Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian J. Goodfellow, and Rob Fergus. Intriguing properties of neural networks. In International Conference on Learning Representations, ICLR 2014, 2014. Tan et al. [2021] Sijun Tan, Brian Knott, Yuan Tian, and David J. Wu. CryptGPU: Fast privacy-preserving machine learning on the GPU. In IEEE Symposium on Security and Privacy, SP 2021, pages 1021–1038. IEEE, 2021. Voigt and Von dem Bussche [2017] Paul Voigt and Axel Von dem Bussche. The EU General Data Protection Regulation (GDPR): A Practical Guide. Springer International Publishing, 2017. Wagh et al. [2019] Sameer Wagh, Divya Gupta, and Nishanth Chandran. SecureNN: 3-party secure computation for neural network training. Proc. Priv. Enhancing Technol., 2019(3):26–49, 2019. Wagh et al. [2021] Sameer Wagh, Shruti Tople, Fabrice Benhamouda, Eyal Kushilevitz, Prateek Mittal, and Tal Rabin. Falcon: Honest-majority maliciously secure framework for private deep learning. Proc. Priv. Enhancing Technol., 2021(1):188–208, 2021. Wang et al. [2021] Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. Beta-CROWN: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. Advances in Neural Information Processing Systems, 34:29909–29921, 2021. Wu et al. [2024] Haoze Wu, Omri Isac, Aleksandar Zeljic, Teruhiro Tagomori, Matthew L. Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekaterina Komendantskaya, Guy Katz, and Clark W. Barrett. Marabou 2.0: A versatile formal analyzer of neural networks. In Computer Aided Verification, CAV 2024, volume 14682 of Lecture Notes in Computer Science, pages 249–264. Springer, 2024. Xu et al. [2020] Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neural Information Processing Systems, 33:1129–1141, 2020. Xu et al. [2021] Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. Fast and Complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In International Conference on Learning Representations, ICLR 2021, 2021. Yao [1982] Andrew C Yao. Protocols for secure computations. In Proceedings of the Annual Symposium on Foundations of Computer Science, FOCS 1982, pages 160–164. IEEE, 1982. Zhang et al. [2018] Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. Advances in Neural Information Processing Systems, 31:4939–4948, 2018. Zhang et al. [2021] Qiao Zhang, Chunsheng Xin, and Hongyi Wu. Privacy-preserving deep learning based on multiparty secure computation: A survey. IEEE Internet Things J., 8(13):10412–10429, 2021. Appendix Appendix A Detailed Protocols A.1 Secure Relaxation Slope Computation Algorithm 3 details the secure protocol Π _ α for computing the relaxation slope vector (l) α^(l), directly implementing the unified arithmetic expression derived in Eq. (12) of the main text. As discussed in Section 5.3, securely evaluating the piecewise conditions of the standard ReLU relaxation introduces prohibitive communication overhead due to data-dependent branching and secure comparisons. By formulating the slope computation as a continuous, data-independent function, our protocol evaluates all neurons uniformly. The protocol first extracts the required positive bounds and the magnitudes of the negative bounds using standard SecReLU operations. After locally incorporating the public stability constant ϵs _s to prevent numerical instability, the division is securely resolved by computing the reciprocal of the denominator via SecRecip, followed by an element-wise SecMul. This branching-free design ensures deterministic execution time and minimizes the use of heavy cryptographic primitives. Algorithm 3 Π _ α: Secure Slope Computation 1:Secret shares of pre-activation lower bounds ⟨¯(l)⟩∈ℤ2kdl z^(l) _2^k^d_l, upper bounds ⟨¯(l)⟩∈ℤ2kdl z^(l) _2^k^d_l, and public stability constant ϵs∈ℝ+ _s ^+ 2:Secret shares of the relaxation slope vector ⟨(l)⟩∈ℤ2kdl α^(l) _2^k^d_l 3:⟨⟩←(⟨¯(l)⟩) ← SecReLU( z^(l) ) ⊳ Numerator: ReLU(¯(l))ReLU( z^(l)) 4:⟨sub⟩←(−⟨¯(l)⟩) _sub ← SecReLU(- z^(l) ) ⊳ Partial denominator: ReLU(−¯(l))ReLU(- z^(l)) 5:⟨⟩←⟨⟩+⟨sub⟩+ϵs ← + _sub + _s ⊳ Full denominator via local addition (zero communication) 6:⟨⟩←(⟨⟩) ← SecRecip( ) ⊳ Element-wise secure reciprocal: 1/1/d 7:⟨(l)⟩←(⟨⟩,⟨⟩) α^(l) ← SecMul( , ) ⊳ Element-wise secure multiplication for division 8:return ⟨(l)⟩ α^(l) A.2 Secure Intercept Accumulation Algorithm 4 details the secure protocol Π _ δ for computing the intercept contribution vectors ¯(t−1) δ^(t-1) and ¯(t−1) δ^(t-1), implementing the reformulated expressions in Eqs. (13)–(14). As discussed in Section 5.4, directly evaluating the conditional summations would necessitate expensive secure comparison protocols. By leveraging the property that the relaxation slopes satisfy (t−1)≥0 α^(t-1)≥ 0, the updated coefficients (t−1)A^(t-1) preserve the necessary sign information. The protocol efficiently isolates the positive and negative components of the coefficient matrix ⟨(t−1)⟩ ^(t-1) and the negative components of the pre-activation bounds ⟨¯(t−1)⟩ z^(t-1) using three parallel SecReLU evaluations. The final vectors ⟨¯(t−1)⟩ δ^(t-1) and ⟨¯(t−1)⟩ δ^(t-1) are then obtained via SecMatMul. Algorithm 4 Π _ δ: Secure Intercept Accumulation 1:Secret shares of coefficients ⟨(t−1)⟩∈ℤ2kdl×dt−1 ^(t-1) _2^k^d_l× d_t-1 and pre-activation lower bounds ⟨¯(t−1)⟩∈ℤ2kdt−1 z^(t-1) _2^k^d_t-1 2:Secret shares of intercept contributions ⟨¯(t−1)⟩,⟨¯(t−1)⟩∈ℤ2kdl δ^(t-1) , δ^(t-1) _2^k^d_l 3:⟨A−⟩←(−⟨(t−1)⟩) _A^- ← SecReLU(- ^(t-1) ) ⊳ ReLU(−(t−1))ReLU(-A^(t-1)), element-wise 4:⟨A+⟩←(⟨(t−1)⟩) _A^+ ← SecReLU( ^(t-1) ) ⊳ ReLU((t−1))ReLU(A^(t-1)), element-wise 5:⟨z⟩←(−⟨¯(t−1)⟩) _z ← SecReLU(- z^(t-1) ) ⊳ ReLU(−¯(t−1))ReLU(- z^(t-1)) 6:⟨¯(t−1)⟩←−(⟨A−⟩,⟨z⟩) δ^(t-1) ←- SecMatMul( _A^- , _z ) ⊳ Eq. (13) 7:⟨¯(t−1)⟩←(⟨A+⟩,⟨z⟩) δ^(t-1) ← SecMatMul( _A^+ , _z ) ⊳ Eq. (14) 8:return ⟨¯(t−1)⟩,⟨¯(t−1)⟩ δ^(t-1) , δ^(t-1) Appendix B Detailed Analysis B.1 Security Proof Proof. We prove security via a hybrid argument. Let the verification circuit consist of L layers corresponding to the neural network’s bound propagation. For each layer l, let l F_l denote the FSS scheme used (either for SecReLU, SecMul, or SecRecip), with associated simulator l Sim_l. We construct simulator 0 Sim_0 for corrupted model owner P0P_0; the case for data owner P1P_1 is symmetric. Hybrid Definitions. • 0H_0: The simulator knows all inputs and executes the real protocol honestly. This is identical to the real execution. • lH_l (for l∈1,…,Ll∈\1,…,L\): Execute the real protocol for layers 1,…,L−l1,…,L-l. For layers L−l+1,…,L-l+1,…,L, use the FSS simulator l Sim_l to generate keys and simulate protocol messages. • L+1H_L+1: Same as LH_L, but additionally replace P1P_1’s inputs with dummy values. This is the ideal-world execution. Indistinguishability of Adjacent Hybrids. l≈cl+1H_l _cH_l+1 for l∈0,…,L−1l∈\0,…,L-1\: These hybrids differ only in layer j=L−lj=L-l. Suppose a distinguisher D distinguishes lH_l from l+1H_l+1 with non-negligible advantage. We construct an adversary A that breaks the security of FSS scheme j F_j: 1. A runs the protocol for layers 1,…,j−11,…,j-1 honestly. 2. A receives an FSS key kbk_b from the FSS challenger (either real or simulated). 3. A uses kbk_b to execute layer j and simulates layers j+1,…,Lj+1,…,L. 4. A outputs D’s guess. If D distinguishes, then A breaks FSS security—a contradiction. L≈sL+1H_L _sH_L+1: In both hybrids, P1P_1’s inputs are masked by uniform random shares. Since additive secret sharing is information-theoretically secure, replacing real inputs with dummy inputs produces an identical distribution of shares. Thus these hybrids are statistically indistinguishable. Conclusion. By the hybrid argument, 0≈cL+1H_0 _cH_L+1, which establishes that the real and ideal executions are computationally indistinguishable. ∎ B.2 Complexity Analysis We analyze the theoretical complexity of SecureCROWN for an L-layer network with maximum width d. Table 5 summarizes the costs of the underlying building blocks. Table 5: Complexity of secure building blocks. Rounds and Comm. denote online costs; Preproc. denotes offline costs. Parameters: bit-width k=64k=64, fractional bits nf=26n_f=26, security parameter λ=128λ=128, Newton–Raphson iterations niter=1n_iter=1. Primitive Rounds Comm. (bits) Preproc. (bits) SecMul 1 2k2k (128) 3k3k (192) SecMatMulm×n×p 1 2(mn+np)k2(mn+np)k (mn+np+mp)k(mn+np+mp)k SecARS 2 k+2k+2 (66) (k+nf)λ+O(k)(k+n_f)λ+O(k) SecReLU 2 k+1k+1 (65) kλ+O(k)kλ+O(k) SecAbs 2 k+1k+1 (65) kλ+O(k)kλ+O(k) SecRecip 6 O(k)O(k) O(kλ)O(kλ) Sub-protocol Complexity. The complexity of our specialized sub-protocols is derived as follows: • Protocol Πα _ α (Algorithm 3): This involves two parallel SecReLU operations (2 rounds), one SecRecip (4+2niter4+2n_iter rounds, including nitern_iter Newton–Raphson iterations), and a final multiplication (1 round). The total is 7+2niter7+2n_iter rounds, with communication O(dk)O(dk). • Protocol Πδ _ δ (Algorithm 4): This protocol executes three parallel SecReLU evaluations (2 rounds) followed by two parallel SecMatMul operations (1 round). The total is 3 rounds with O(d2k)O(d^2k) communication. End-to-End Complexity. The complete SecureCROWN protocol (Algorithm 2) proceeds layer-by-layer. For a target layer l, Algorithm 1 iterates l−1l-1 times. Each iteration involves: SecMatMul (1 round) → slope multiplication (1 round) → Π _ δ (3 rounds), yielding 5 rounds per iteration. The bias accumulation in Lines 6-7 overlaps with Π _ δ: the (⟨⟩,⟨⟩) SecMatMul( , ) executes in parallel with the SecReLU operations, and the final addition of δ is a local operation. Summing over all layers, the total complexity is: • Rounds: O(L2)O(L^2). The iterative bound computation contributes ∑l=2L−15(l−1)=5(L−2)(L−1)2≈52L2 _l=2^L-15(l-1)= 5(L-2)(L-1)2≈ 52L^2 rounds. The final margin certification adds 5(L−1)=O(L)5(L-1)=O(L) rounds. Additionally, Π _ α is invoked L−1L-1 times, contributing (L−1)(7+2niter)(L-1)(7+2n_iter) rounds. • Communication: O(L2d2k)O(L^2d^2k). This is dominated by the dense matrix multiplications in the iterative backward pass. • Computation: O(L2d3)O(L^2d^3), dominated by O(L2)O(L^2) matrix multiplications of size d×d× d. • Preprocessing: O(L2d2k)O(L^2d^2k) bits for matrix Beaver triples and O(Ldkλ)O(Ldkλ) bits for FSS keys. B.3 Error Analysis We analyze the LBP bound computation, which constructs an affine form bound by backward propagation of a coefficient matrix A and a bias vector c, accumulating constants and relaxation terms layer by layer, and then forms the final upper/lower bound of the target quantity as a function of the input. The final step is to maximize/minimize this affine form over the input perturbation set X, which yields closed-form expressions for the bounds. We denote by r()r(M) the vector of row-wise sums of absolute values of a matrix M, i.e., r()i=∑j|ij|r(M)_i= _j|M_ij|. We denote by ‖∞=maxir()i\|M\|_∞= _ir(M)_i the induced infinity norm of a matrix M, and by ‖1=∑i|vi|\|v\|_1= _i|v_i| the ℓ1 _1 norm of a vector v. Let Qnf:ℝ→ℝQ_n_f:R denote the fixed-point quantization function that maps a real number to its fixed-point representation with nfn_f fractional bits, i.e., Qnf(y)=2−nf⌊2nfy⌋Q_n_f(y)=2^-n_f 2^n_fy . For each layer i, the algorithm uses a diagonal matrix of slopes diag((i))diag( α^(i)) with entries αk(i)∈[0,1] _k^(i)∈[0,1] to relax the ReLU activation, applied during backward propagation. For a fixed fractional precision parameter nfn_f, let ARSnf(⋅)ARS_n_f(·) denote the arithmetic-right-shift scaling operation that divides its input by 2nf2^n_f and rounds towards −∞-∞ (i.e., takes the floor). We model each call to ARSnfARS_n_f as introducing an additive element-wise rounding error bounded by a constant εq _q in real units, where typically εq=2−nf _q=2^-n_f. Assumptions Our analysis makes the following assumptions: • Assumption 1 (Range safety): During execution, every intermediate integer value remains within the representable range of the fixed-point format, i.e., no overflow occurs. Equivalently, the fixed-point computation is a faithful representation of the corresponding real arithmetic plus truncation errors. • Assumption 2 (Quantization error model): Each call to ARSnfARS_n_f corresponds to applying QnfQ_n_f to the intended real-valued quantity, and thus introduces an additive error bounded by εq _q in real units: Qnf(y)=y+η(y)with|η(y)|≤εq.Q_n_f(y)=y+η(y) |η(y)|≤ _q. F Backward propagation operator For the target bound computation, define the ideal backward propagation of coefficient matrices (i)\A^(i)\ by (i−1)=(i)(i)diag((i−1)),i=1,…,m,A^(i-1)=A^(i)W^(i)diag( α^(i-1)), i=1,…,m, where m is the number of backward steps performed by the algorithm (e.g., m=L−1m=L-1 for the full backward propagation from the last layer). The starting coefficient (m)A^(m) is initialized as the weight matrix of the current layer. Let (i)\ ^(i)\ be the corresponding coefficients computed by the fixed-point implementation, which applies the ARSnfARS_n_f operation at each multiplication step. The coefficient error at layer i is defined as (i)=(i)−(i)E^(i)= ^(i)-A^(i). Theorem B.1. Under assumptions 1 and 2, given the slopes (i)∈[0,1] α^(i)∈[0,1] element-wise, the coefficient error satisfies the recurrence ‖(i−1)‖∞≤‖(i)‖∞‖(i)‖∞+Δi,i=1,…,m,\|E^(i-1)\|_∞≤\|W^(i)\|_∞\|E^(i)\|_∞+ _i, i=1,…,m, (15) where Δi _i is an upper bound on the ℓ∞ _∞ norm of the local rounding injection at step i, induced by the truncations performed at that step. In particular, if step i produces a matrix with qiq_i columns before truncation, then one may take the conservative bound Δi≤qiεq _i≤ q_i _q. Consequently, if the initial coefficient is computed exactly (i.e., (m)=E^(m)=0), then the final coefficient error after m steps is bounded by ‖(0)‖∞≤∑i=1m(∏j=1i−1‖(j)‖∞)Δi.\|E^(0)\|_∞≤ _i=1^m ( _j=1^i-1\|W^(j)\|_∞ ) _i. (16) If, furthermore, ‖(i)‖∞≤ρ\|W^(i)\|_∞≤ρ for all relevant layers, then the error bound simplifies to ‖(0)‖∞≤(∑k=0m−1ρk)maxiΔi=O(m)⋅maxiΔi,if ρ=1,O(ρm)⋅maxiΔi,if ρ>1,O(1)⋅maxiΔi,if ρ<1.\|E^(0)\|_∞≤ ( _k=0^m-1ρ^k ) _i _i= casesO(m)· _i _i,&if ρ=1,\\ O(ρ^m)· _i _i,&if ρ>1,\\ O(1)· _i _i,&if ρ<1. cases (17) Proof. Fix i∈1,…,mi∈\1,…,m\. The ideal update is (i−1)=(i)(i)diag((i−1))A^(i-1)=A^(i)W^(i)diag( α^(i-1)), while the actual update is (i−1)=Qnf((i)(i)diag((i−1))), ^(i-1)=Q_n_f( ^(i)W^(i)diag( α^(i-1))), (18) where we have used the fact that αk(i−1) _k^(i-1) is computed to lie in [0,1][0,1] and treated it as the same slope vector used in both the ideal and actual computations. If one wishes to include quantized αk(i−1) _k^(i-1) in the error analysis, it appears as an additional additive term. By Assumption 2, we have (i−1)=(i)(i)diag((i−1))+(i), ^(i-1)= ^(i)W^(i)diag( α^(i-1))+ ^(i), (19) where (i) ^(i) is the rounding error matrix injected by the ARSnfARS_n_f operation, with |j,k(i)|≤εq| ^(i)_j,k|≤ _q for all entries. Therefore, (i−1)=(i−1)−(i−1)=((i)−(i))(i)diag((i−1))+(i)=(i)(i)diag((i−1))+(i).E^(i-1)= ^(i-1)-A^(i-1)=( ^(i)-A^(i))W^(i)diag( α^(i-1))+ ^(i)=E^(i)W^(i)diag( α^(i-1))+ ^(i). (20) Taking ∥⋅∥∞\|·\|_∞ on both sides and using the sub-multiplicative property gives ‖(i−1)‖∞≤‖(i)‖∞‖(i)‖∞‖diag((i−1))‖∞+‖(i)‖∞.\|E^(i-1)\|_∞≤\|E^(i)\|_∞\|W^(i)\|_∞\|diag( α^(i-1))\|_∞+\| ^(i)\|_∞. (21) Since αk(i−1)∈[0,1] _k^(i-1)∈[0,1] for all k, we have ‖diag((i−1))‖∞=maxkαk(i−1)≤1\|diag( α^(i-1))\|_∞= _k _k^(i-1)≤ 1, hence ‖(i−1)‖∞≤‖(i)‖∞‖(i)‖∞+‖(i)‖∞.\|E^(i-1)\|_∞≤\|W^(i)\|_∞\|E^(i)\|_∞+\| ^(i)\|_∞. (22) Define Δi=‖(i)‖∞ _i=\| ^(i)\|_∞ to be the local error bound at step i, yielding the stated recurrence. To bound Δi _i, note that ‖(i)‖∞=maxj∑k|j,k(i)|≤maxj∑kεq=qiεq\| ^(i)\|_∞= _j _k| ^(i)_j,k|≤ _j _k _q=q_i _q, where qiq_i is the number of columns of the matrix. Finally, unrolling the recurrence with (m)=E^(m)=0 gives the stated bound on (0)E^(0): ‖(0)‖∞ \|E^(0)\|_∞ ≤‖(1)‖∞‖(1)‖∞+Δ1 ≤\|W^(1)\|_∞\|E^(1)\|_∞+ _1 ≤‖(1)‖∞(‖(2)‖∞‖(2)‖∞+Δ2)+Δ1 ≤\|W^(1)\|_∞(\|W^(2)\|_∞\|E^(2)\|_∞+ _2)+ _1 =‖(1)‖∞‖(2)‖∞‖(2)‖∞+‖(1)‖∞Δ2+Δ1 =\|W^(1)\|_∞\|W^(2)\|_∞\|E^(2)\|_∞+\|W^(1)\|_∞ _2+ _1 ⋯ ·s ≤∑i=1m(∏j=1i−1‖(j)‖∞)Δi. ≤ _i=1^m ( _j=1^i-1\|W^(j)\|_∞ ) _i. The ρ-based bound follows directly from the above by substituting ‖(j)‖∞≤ρ\|W^(j)\|_∞≤ρ for all j. ∎ Based on Theorem B.1, we now derive the error bound for the final upper/lower bound vectors. Write the ideal final bounds over X as UB=(0)0+¯(0)+ϵ⋅r((0)),LB=(0)0+¯(0)−ϵ⋅r((0)),UB=A^(0)x_0+ c^(0)+ε· r(A^(0)), LB=A^(0)x_0+ c^(0)-ε· r(A^(0)), where r((0))r(A^(0)) is the row-wise ℓ1 _1-norm vector of (0)A^(0). During backward propagation, the ideal update is ¯(i−1) c^(i-1) =¯(i)+(i)(i)+¯(i−1), = c^(i)+A^(i)b^(i)+ δ^(i-1), (23) ¯(i−1) c^(i-1) =¯(i)+(i)(i)+¯(i−1), = c^(i)+A^(i)b^(i)+ δ^(i-1), (24) where ¯(i−1) δ^(i-1) and ¯(i−1) δ^(i-1) are the ReLU relaxation intercept contribution terms. Define uk(i−1)=(−z¯k(i−1))+≥0u_k^(i-1)=(- z^(i-1)_k)_+≥ 0 for all k, where (x)+=max(0,x)(x)_+= (0,x) denotes the positive part, with the convention uk(0)=0u_k^(0)=0 since layer 0 is the input layer with no ReLU. Then the intercept contributions are: ¯j(i−1) δ^(i-1)_j =∑k(j,k(i−1))+uk(i−1), = _k(A^(i-1)_j,k)_+u_k^(i-1), (25) ¯j(i−1) δ^(i-1)_j =∑k(−j,k(i−1))+uk(i−1). = _k(-A^(i-1)_j,k)_+u_k^(i-1). (26) The actual update performed by the fixed-point implementation is ¯(i−1) γ^(i-1) =Qnf(¯(i)+(i)(i)+¯^(i−1)), =Q_n_f( γ^(i)+ ^(i)b^(i)+ δ^(i-1)), (27) ¯(i−1) γ^(i-1) =Qnf(¯(i)+(i)(i)+¯^(i−1)), =Q_n_f( γ^(i)+ ^(i)b^(i)+ δ^(i-1)), (28) where ¯^(i−1) δ^(i-1) and ¯^(i−1) δ^(i-1) are computed using the actual coefficient matrix (i−1) ^(i-1): ¯^j(i−1) δ^(i-1)_j =∑k(j,k(i−1))+uk(i−1), = _k( ^(i-1)_j,k)_+u_k^(i-1), (29) ¯^j(i−1) δ^(i-1)_j =∑k(−j,k(i−1))+uk(i−1). = _k(- ^(i-1)_j,k)_+u_k^(i-1). (30) Therefore, the error in the bias term at layer i−1i-1, denoted as ¯(i−1)≔¯(i−1)−¯(i−1) ν^(i-1) γ^(i-1)- c^(i-1), can be decomposed component-wise (for index j) as ¯j(i−1) ν^(i-1)_j =¯j(i)+[(i)(i)]j+¯^j(i−1)+Θj(i)−(¯j(i)+[(i)(i)]j+¯j(i−1)) = γ^(i)_j+[ ^(i)b^(i)]_j+ δ^(i-1)_j+ ^(i)_j- ( c^(i)_j+[A^(i)b^(i)]_j+ δ^(i-1)_j ) =¯j(i)+[(i)(i)]j+∑k[(j,k(i−1))+−(j,k(i−1))+]uk(i−1)+Θj(i), = ν^(i)_j+[E^(i)b^(i)]_j+ _k [( ^(i-1)_j,k)_+-(A^(i-1)_j,k)_+ ]u_k^(i-1)+ ^(i)_j, (31) where Θ(i) ^(i) is the rounding error injected by the ARSnfARS_n_f operation, with ‖Θ(i)‖∞≤εq\| ^(i)\|_∞≤ _q. Using the 1-Lipschitz property of (⋅)+(·)_+, we can bound the error in the intercept contribution: |¯^j(i−1)−¯j(i−1)|≤∑k|(j,k(i−1))+−(j,k(i−1))+|uk(i−1)≤∑k|j,k(i−1)|uk(i−1)≤‖j,:(i−1)‖1‖u(i−1)‖∞.| δ^(i-1)_j- δ^(i-1)_j|≤ _k|( ^(i-1)_j,k)_+-(A^(i-1)_j,k)_+|u_k^(i-1)≤ _k|E^(i-1)_j,k|u_k^(i-1)≤\|E^(i-1)_j,:\|_1\|u^(i-1)\|_∞. (32) Taking the infinity norm over j, we get: ‖¯^(i−1)−¯(i−1)‖∞≤‖(i−1)‖∞‖u(i−1)‖∞.\| δ^(i-1)- δ^(i-1)\|_∞≤\|E^(i-1)\|_∞\|u^(i-1)\|_∞. (33) Unrolling the recurrence for ¯(0) ν^(0) (with ¯(m)= ν^(m)=0) gives ‖¯(0)‖∞=‖¯(0)−¯(0)‖∞≤∑i=1m(‖(i)‖∞‖(i)‖∞+‖(i−1)‖∞‖u(i−1)‖∞)+mεq.\| ν^(0)\|_∞=\| γ^(0)- c^(0)\|_∞≤ _i=1^m (\|E^(i)\|_∞\|b^(i)\|_∞+\|E^(i-1)\|_∞\|u^(i-1)\|_∞ )+m _q. (34) A symmetric bound holds for the lower bound bias error ‖¯(0)‖∞=‖¯(0)−¯(0)‖∞\| ν^(0)\|_∞=\| γ^(0)- c^(0)\|_∞ (replacing (⋅)+(·)_+ by (−⋅)+(-·)_+ throughout). Theorem B.2. Let UB^,LB UB, LB be the fixed-point outputs, and define (0)=(0)−(0)E^(0)= ^(0)-A^(0). Under Assumptions 1 and 2, the absolute errors of the final bounds are bounded by: ‖UB^−UB‖∞ \| UB-UB\|_∞ ≤(‖0‖∞+ϵ)‖(0)‖∞+∑i=1m(‖(i)‖∞‖(i)‖∞+‖(i−1)‖∞‖u(i−1)‖∞)+ζu, ≤(\|x_0\|_∞+ε)\|E^(0)\|_∞+ _i=1^m (\|E^(i)\|_∞\|b^(i)\|_∞+\|E^(i-1)\|_∞\|u^(i-1)\|_∞ )+ _u, (35) ‖LB^−LB‖∞ \| LB-LB\|_∞ ≤(‖0‖∞+ϵ)‖(0)‖∞+∑i=1m(‖(i)‖∞‖(i)‖∞+‖(i−1)‖∞‖u(i−1)‖∞)+ζl, ≤(\|x_0\|_∞+ε)\|E^(0)\|_∞+ _i=1^m (\|E^(i)\|_∞\|b^(i)\|_∞+\|E^(i-1)\|_∞\|u^(i-1)\|_∞ )+ _l, (36) where u(i−1)=(−¯(i−1))+≥0u^(i-1)=(- z^(i-1))_+≥ 0 with u(0)=0u^(0)=0 (no ReLU at the input layer), and ζu,ζl _u, _l are assembly-level quantization residuals bounded by (m+1)εq(m+1) _q. Therefore, by substituting Theorem B.1 bounds for ‖(i)‖∞\|E^(i)\|_∞, one obtains an explicit depth-dependent absolute error bound for both UB UB and LB LB. Proof. We prove the upper-bound case; the lower-bound case is identical. The ideal final upper bound is given by UB=(0)0+¯(0)+ϵ⋅r((0)).UB=A^(0)x_0+ c^(0)+ε· r(A^(0)). The fixed-point implementation computes the final bound as UB^=(0)0+¯(0)+ϵ⋅r((0))+ξu, UB= ^(0)x_0+ γ^(0)+ε· r( ^(0))+ _u, where ξu _u represents the rounding error introduced during the final assembly operations (e.g., dot products and additions), with ‖ξu‖∞≤εq\| _u\|_∞≤ _q. Decomposing the difference yields UB^−UB=(0)0+ϵ(r((0))−r((0)))+¯(0)+ξu. UB-UB=E^(0)x_0+ε (r( ^(0))-r(A^(0)) )+ ν^(0)+ _u. Taking the infinity norm and applying the triangle inequality gives ‖UB^−UB‖∞≤‖(0)0‖∞+ϵ‖r((0))−r((0))‖∞+‖¯(0)‖∞+‖ξu‖∞.\| UB-UB\|_∞≤\|E^(0)x_0\|_∞+ε\|r( ^(0))-r(A^(0))\|_∞+\| ν^(0)\|_∞+\| _u\|_∞. By norm inequalities, we have ‖(0)0‖∞≤‖(0)‖∞‖0‖∞,‖r((0))−r((0))‖∞≤‖(0)‖∞.\|E^(0)x_0\|_∞≤\|E^(0)\|_∞\|x_0\|_∞, \|r( ^(0))-r(A^(0))\|_∞≤\|E^(0)\|_∞. Substituting the bound for ‖¯(0)‖∞\| ν^(0)\|_∞ derived earlier, we obtain ‖UB^−UB‖∞ \| UB-UB\|_∞ ≤(‖0‖∞+ϵ)‖(0)‖∞+∑i=1m(‖(i)‖∞‖(i)‖∞+‖(i−1)‖∞‖u(i−1)‖∞)+mεq+εq ≤(\|x_0\|_∞+ε)\|E^(0)\|_∞+ _i=1^m (\|E^(i)\|_∞\|b^(i)\|_∞+\|E^(i-1)\|_∞\|u^(i-1)\|_∞ )+m _q+ _q =(‖0‖∞+ϵ)‖(0)‖∞+∑i=1m(‖(i)‖∞‖(i)‖∞+‖(i−1)‖∞‖u(i−1)‖∞)+ζu, =(\|x_0\|_∞+ε)\|E^(0)\|_∞+ _i=1^m (\|E^(i)\|_∞\|b^(i)\|_∞+\|E^(i-1)\|_∞\|u^(i-1)\|_∞ )+ _u, where ζu≤(m+1)εq _u≤(m+1) _q. ∎ Remark 1. The stability constant ϵs _s in Eq. (12) perturbs each relaxation slope from its ideal value, and hence the relaxation bounding functions. For every neuron k, the sup-norm deviation of the perturbed bounding functions over [z¯k,z¯k][ z_k, z_k] is at most ϵs _s: for unstable neurons this follows from max(|z¯k|,z¯k)≤z¯k−z¯k (| z_k|, z_k)≤ z_k- z_k; the active case gives deviation ϵsz¯k/(z¯k+ϵs)≤ϵs _s z_k/( z_k+ _s)≤ _s, and the inactive case is exact. Substituting the perturbed relaxations in the backward recursion therefore injects, at each step i, an additional deviation of at most ‖^(i)‖∞ϵs\| A^(i)\|_∞\, _s into the accumulated bound values, where ^(i) A^(i) is the intermediate coefficient matrix in Eq. (4) and, as in the proof of Theorem B.1, the relaxation parameters at the remaining layers are treated as fixed. The effect on the final bounds thus follows the same depth-dependent structure as Theorem B.2, with the per-step injection scale εq _q replaced by ‖^(i)‖∞ϵs\| A^(i)\|_∞\, _s. Since the perturbed relaxation deviates from the ideal one, a verification outcome could in principle change when the certified margin lies within O(ϵs)O( _s) of zero; empirically, no such change is observed even at 1000×1000× the default ϵs _s (Table 4). A slope–intercept co-adjustment that restores provable soundness of the perturbed relaxation is left for future work. Corollary B.3 (Asymptotic error bound). Under the hypotheses of Theorems B.1 and B.2, assume (m)=E^(m)=0, ‖(i)‖∞≤ρ\|W^(i)\|_∞≤ρ and Δi≤Δ _i≤ for all i. Let X=‖0‖∞+ϵ,B=maxi‖(i)‖∞,U=maxi‖u(i−1)‖∞,X\;=\;\|x_0\|_∞+ε, B\;=\; _i\|b^(i)\|_∞, U\;=\; _i\|u^(i-1)\|_∞, and let Sn=∑k=0n−1ρkS_n= _k=0^n-1ρ^k, so that the layer-t coefficient error satisfies ‖(t)‖∞≤Sm−tΔ\|E^(t)\|_∞≤ S_m-t\, . Then, as m→∞m→∞, the error in UB UB (and identically in LB LB) satisfies ‖UB^−UB‖∞≤[X⋅Sm+B∑i=1mSm−i+U∑i=1mSm−i+1]Δ+O(m)εq,\| UB-UB\|_∞\;≤\; [X· S_m\;+\;B _i=1^mS_m-i\;+\;U _i=1^mS_m-i+1 ] \;+\;O(m)\, _q, (37) where the three asymptotic regimes of the leading term (as a function of m) are: ‖UB^−UB‖∞=O(m)⋅(B+U)Δ+O(1)⋅XΔ+O(m)εq,if ρ<1,O(m2)⋅(B+U)Δ+O(m)⋅XΔ+O(m)εq,if ρ=1,O(ρm)⋅(X+B+U)Δ+O(m)εq,if ρ>1.\| UB-UB\|_∞\;=\; casesO(m)·(B+U) \;+\;O(1)· X \;+\;O(m)\, _q,&if ρ<1,\\[4.0pt] O(m^2)·(B+U) \;+\;O(m)· X \;+\;O(m)\, _q,&if ρ=1,\\[4.0pt] O(ρ^m)·(X+B+U) \;+\;O(m)\, _q,&if ρ>1. cases (38) In particular, the ζ residuals are O(m)εqO(m)\, _q in all cases. Interpretation of the unstable regime. The ρ>1ρ>1 branch in the asymptotic corollary should be read as a conservative worst-case envelope rather than as the typical numerical behavior of SecureCROWN. It is obtained by replacing every layer-dependent amplification factor with the same uniform upper bound ρ and every local rounding injection with the same upper bound Δ . The non-asymptotic analysis above is sharper and remains layer-wise. Indeed, before the conservative inequality ‖diag((i−1))‖∞≤1\|diag( α^(i-1))\|_∞≤ 1 is applied, the proof of Theorem B.1 gives ‖(i−1)‖∞≤κi‖(i)‖∞+Δi,κi≔‖(i)diag((i−1))‖∞.\|E^(i-1)\|_∞≤ _i\|E^(i)\|_∞+ _i, _i \|W^(i)diag( α^(i-1))\|_∞. (39) Thus, when (m)=E^(m)=0, ‖(0)‖∞≤∑i=1m(∏j=1i−1κj)Δi.\|E^(0)\|_∞≤ _i=1^m ( _j=1^i-1 _j ) _i. (40) This expression propagates each local error through the actual product of effective layer norms. Consequently, the simplified O(ρm)O(ρ^m) term arises only when these heterogeneous products are upper-bounded by the same worst-case factor at every layer; factors κj<1 _j<1 can attenuate errors produced at other layers with κj>1 _j>1. The diagonal relaxation matrices further reduce the effective amplification: since αk(i−1)∈[0,1] _k^(i-1)∈[0,1], the factor κi _i is a row-wise weighted sum of |(i)||W^(i)| with weights (i−1) α^(i-1), and is always at most ‖(i)‖∞\|W^(i)\|_∞. When many slopes are strictly below one, as for inactive or unstable ReLU neurons, κi _i can be substantially smaller than the raw weight norm of the layer and can even fall below one when ‖(i)‖∞>1\|W^(i)\|_∞>1. We do not rule out the vulnerability captured by this worst-case bound: if a network has consistently large effective layer norms, fixed-point rounding errors can be amplified and the numerical precision of the certified bounds can deteriorate. In standard modern training pipelines, however, small initialization, weight decay, and related regularization or normalization techniques typically limit uncontrolled growth of weight norms. Consistent with this interpretation, our experiments do not exhibit the exponential-growth regime: SecureCROWN maintains 100% verification consistency with plaintext CROWN across all evaluated architectures and perturbation settings, including near-boundary instances (Table 1). Appendix C Discussion on Malicious Security SECURECROWN currently targets the semi-honest model, which is standard for initial 2PC-based protocol designs. A malicious-secure upgrade could replace unauthenticated Beaver triples with authenticated triples and add MAC-based consistency checks, following SPDZ-style protocols. The trusted-dealer assumption can also be removed by using two-party preprocessing, such as OT-based triple generation, without changing the online verifier logic. These changes preserve the branch-free reformulation of CROWN, but increase both online communication and offline preprocessing costs. To estimate this overhead, we implemented the same verification algorithm in MP-SPDZ. On MNIST 5×[256]5×[256], replacing semi2k with spdz2k increases online time by about 3.2×3.2× (183183s to 586586s) and communication by about 8.7×8.7× (1.261.26TB to 10.8810.88TB). In comparison, our FSS-based semi-honest implementation completes the same task in 4.34.3s with 113113MB communication. This suggests that a specialized malicious-secure variant of SECURECROWN could be substantially more efficient than directly using a generic malicious 2PC backend, although designing and benchmarking such a variant is left for future work. Appendix D Extension to Other Network Architectures The current implementation targets CROWN-style LBP for fully connected ReLU networks. We discuss extensions to other network components according to the type of additional support required. D.1 Components Requiring Minimal Cryptographic Changes Batch normalization. Batch normalization (BN) can be folded into the preceding affine layer by P0P_0 before secret sharing, since all BN parameters are fixed after training. This requires no change to the secure verification protocol. Residual connections. Residual connections compute =F()+y=F(x)+x, where F()F(x) denotes the residual branch. From the secure-computation perspective, this addition is local under additive secret sharing and incurs no communication. Therefore, residual connections require no new cryptographic primitives, although the verifier implementation would need to handle skip connections and merge the propagated bounds from multiple graph branches. D.2 Linear Components with Scalability Bottlenecks Convolutional layers. Convolutions can be represented as matrix multiplications =Wtoep+y=W_toepx+b, where x and y denote vectorized input and output feature maps, and WtoepW_toep is the sparse Toeplitz matrix induced by the convolutional kernels. Therefore, convolutions are compatible with our SecMatMul interface in principle. However, a naive dense unfolding loses the sparsity of the convolutional kernel. For input and output channel counts cinc_in and coutc_out, input and output spatial sizes s and s′s , and kernel size κ, the unfolded matrix has dimension (couts′2)×(cins2)(c_outs 2)×(c_ins^2), whereas the convolution itself has only coutcinκ2c_outc_inκ^2 independent kernel parameters. Since our Beaver-based SecMatMul treats the unfolded matrix as dense, communication scales with the full matrix dimensions rather than with the number of independent kernel parameters. Practical support for CNNs would therefore require secure convolution protocols that exploit kernel sparsity or tiled/sliding-window structure. Cost projection for ResNet-18. For a CIFAR-10-scale ResNet-18, a naive Toeplitz unfolding of a 6464-channel 32×3232× 32 convolution can yield matrices up to 65,536×65,53665,536× 65,536. Repeated dense secure matrix multiplications inside LBP would therefore lead to communication on the order of terabytes over the full verification procedure. Exploiting the sparse Toeplitz structure, as done in optimized secure-inference systems such as CryptGPU [Tan et al., 2021] and CrypTFlow [Kumar et al., 2020], is a promising direction for reducing this cost. D.3 Components Requiring New Verification Relaxations Non-ReLU activations. Non-ReLU activations, such as sigmoid or tanh, require activation-specific linear relaxations. Extending SecureCROWN to these activations would therefore require new branch-free reformulations of the corresponding relaxation logic. This does not necessarily require new cryptographic primitives: the underlying FSS primitives already support operations such as spline and exponential evaluations [Gupta et al., 2025], providing a cryptographic foundation for these extensions. The main challenge is deriving secure-computation-friendly bound propagation rules that minimize secure comparisons and communication overhead. Attention layers. Attention layers compute softmax(QK⊤/dk)Vsoftmax(QK / d_k)V, where Q, K, and V denote the query, key, and value matrices, respectively, and dkd_k is the key dimension. This operation involves bilinear terms in QK⊤QK and the softmax nonlinearity. Unlike ReLU, which is a univariate piecewise-linear function, attention introduces nonlinearities whose tight and scalable verification remains substantially more complex even in plaintext verification [Shi et al., 2025]. Extending SECURECROWN to attention-based architectures would therefore first require mature CROWN-style relaxations for these operations.