FULL PDF
Abstract
Ensuring data privacy in high-stakes, multi-party computation (MPC) environments demands formally verified protocols that accommodate uncertainty and adversarial behavior. This paper presents a formal verification framework for multi-party privacy protocols using probabilistic automata and symbolic abstraction. Probabilistic automata capture non-determinism inherent in real-world networked environments, while symbolic abstraction facilitates scalable verification of complex cryptographic operations. We validate our framework against representative healthcare and financial data-sharing scenarios, demonstrating soundness, scalability, and practical tractability. Our findings indicate improved verification efficiency and greater resilience to probabilistic inference attacks when compared with baseline non-symbolic models.
View more >>