Score:1

Formal Verification for Multiparty Computation and Homomorphic Encryption?

cn flag

I've recently found some work on the use of Formal Verification Software, like ProVerif for enclaves. I wonder is if its feasible to have something similar for MPC and Homomorphic Encryption and their applications?

I always thought there were limitations adopting simulation based proofs and Universal Composability, in general, in Formal Verification, but as of late I'm thinking there must be more powerful reasons.

cn flag
I think there are many aspects to your question. I will only comment on MPC. The proofs are often written in the UC framework because it allows arbitrary composition. As far as I know, formal verification tools do not support this.
DaWNFoRCe avatar
cn flag
Ok, now imagine if we work in the context of Secure Function Evaluation, would that make things easier with respect of Formal Verification?
Vadym Fedyukovych avatar
in flag
"How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation", 1805.12482 on arxiv
DaWNFoRCe avatar
cn flag
Hi.. so there is some work from people like Maurer: "Abstract Modeling of System Communication in Constructive Cryptography using CryptHOL" but if you see the kind of venues they appear.. I wonder what are the main motivations not to embrace formal verification
DaWNFoRCe avatar
cn flag
If you guys notice.. these works are quite adamant on what they could do... like improving simulation for secure channels.. not what cannot be done.. so that is still my question.. what is really blocking the use of Formal Verification?
cn flag
I stand corrected, there are tools that allows formal verification of UC-based proofs https://eprint.iacr.org/2019/582.pdf. I imagine there's nothing that's fundamentally stopping you from using formal verification for MPC, it's just there's not enough people and not enough time to do this kind of work.
mangohost

Post an answer

Most people don’t grasp that asking a lot of questions unlocks learning and improves interpersonal bonding. In Alison’s studies, for example, though people could accurately recall how many questions had been asked in their conversations, they didn’t intuit the link between questions and liking. Across four studies, in which participants were engaged in conversations themselves or read transcripts of others’ conversations, people tended not to realize that question asking would influence—or had influenced—the level of amity between the conversationalists.