In secure multi-party computation, mutually distrusting parties cooperatively compute functions of their private data; in the process, they only learn certain results as per the protocol (e.g., the final output). The realization of these protocols uses cryptographic techniques to avoid leaking information between the parties. A protocol for a secure computation can sometimes be optimized without changing its security guarantee: when the parties can use their private data and the revealed output to infer the values of other data, then this other data need not be concealed from them via cryptography.
In the context of automatically optimizing secure multi-party computation, we define two related problems, knowledge inference and constructive knowledge inference. In both problems, we attempt to automatically discover when and if intermediate variables used in a protocol will (eventually) be known to the parties involved in the computation. Provably-known variables offer optimization opportunities.
We formally state the problem of knowledge inference (and its constructive variant); we describe our solutions, which are built atop existing, standard technology such as SMT solvers. We show that our approach is sound, and further, we characterize the completeness properties enjoyed by our approach. We have implemented our approach, and present a preliminary experimental evaluation.
@INPROCEEDINGS{rastogi13knowledge, AUTHOR = {Aseem Rastogi and Piotr Mardziel and Michael Hicks and Matthew A. Hammer}, TITLE = {Knowledge Inference for Optimizing Secure Multi-party Computation}, BOOKTITLE = {Proceedings of the {ACM SIGPLAN} Workshop on Programming Languages and Analysis for Security (PLAS)}, MONTH = JUN, YEAR = 2013 }