Formal Verification of Multi-Party Privacy Protocols Using Probabilistic Automata and Symbolic Abstraction in High-Stakes Data Environments
Keywords:
Formal Verification, Probabilistic Automata, Symbolic Abstraction, Multi-Party Computation, Privacy Protocols, High-Stakes Data, Secure Communication, Protocol AnalysisAbstract
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.
References
Baier, C., & Katoen, J.-P. (2008). Principles of Model Checking, Springer.
McLean, J. (1994). Security Models and Information Flow, IEEE S&P, Vol. 12, No. 1.
Kwiatkowska, M., Norman, G., & Parker, D. (2011). PRISM 4.0: Verification of Probabilistic Real-Time Systems, CAV, Vol. 6806, Springer.
Backes, M., Pfitzmann, B., & Waidner, M. (2004). A Universal Composition Theorem for Secure Reactive Systems, TCC, Vol. 2951, Springer.
Blanchet, B. (2001). An Efficient Cryptographic Protocol Verifier Based on Prolog Rules, CSFW, Vol. 14, IEEE.
Delaune, S., & Kremer, S. (2012). Symbolic Models for the Analysis of Security Protocols, Journal of Logic and Algebraic Programming, Vol. 81, No. 7.
Lowe, G. (1996). Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR, TACAS, Vol. 1055, Springer.
Abadi, M., & Gordon, A. D. (1999). A Calculus for Cryptographic Protocols, Information and Computation, Vol. 148, No. 1.
Mitchell, J. C., Ramanathan, M., & Scedrov, A. (2004). A Probabilistic Polynomial-Time Calculus for the Analysis of Cryptographic Protocols, TCS, Vol. 1, No. 1.
Ryan, P. Y. A., Schneider, S. A., Goldsmith, M., Lowe, G., & Roscoe, A. W. (2001). Modelling and Analysis of Security Protocols, Addison-Wesley, Vol. 2.
Bella, G. (2007). Formal Correctness of Security Protocols, Springer, Vol. 1.
Millen, J. K., & Shmatikov, V. (2001). Symbolic Protocol Analysis with an Application to TLS, CSFW, Vol. 14, IEEE.
Durgin, N. A., Lincoln, P., Mitchell, J. C., & Scedrov, A. (2004). Multiset Rewriting and the Complexity of Bounded Security Protocol Analysis, JCS, Vol. 7, No. 2.
Meadows, C. (1996). The NRL Protocol Analyzer: An Overview, Journal of Logic Programming, Vol. 26, No. 2.
Basin, D., Cremers, C., Dreier, J., & Sasse, R. (2018). Automated Symbolic Proofs of Observational Equivalence, Journal of Computer Security, Vol. 26, No. 5.
