安全多方计算与形式化证明

安全多方计算的安全模型默认假设参与方运行的安全多方计算软件是正确的，然而在现实中复杂的程序常会有安全漏洞。为了进一步推动安全多方计算的发展和部署，安全多方计算与形式化证明的结合是发展的必然趋势。形式化证明可以辅助密码学家进行证明的构造，也可以在一定层面上确保程序相对于协议的正确性。这与近期对OpenSSL正确性的形式化证明类似。由于安全多方计算的复杂性，该过程将引入更多的挑战和机遇。设计简单易证明的协议比设计仅有高效率的协议更具吸引力。

大数据的隐私保护计算等需求给密码学带来了前所未有的挑战。作为密码学的前沿领域，安全多方计算给大数据安全和隐私保护计算提供了一条重要的技术路径。经过密码学家30多年的不懈探索，安全多方计算正朝着高效可用和高安全保障的方向持续高速发展。