We devise an abstraction of secure multi-party computations in the applied $pi$-calculus. Based on this abstraction, we propose a methodology to mechanically analyze the security of cryptographic protocols employing secure multi-party computations. We exemplify the applicability of our framework by analyzing the SIMAP sugar-beet double auction protocol. We finally study the computational soundness of our abstraction, proving that the analysis of protocols expressed in the applied $pi$-calculus and based on our abstraction provides computational security guarantees.
展开▼
机译：我们在应用的$ pi $-演算中设计了安全的多方计算的抽象。基于此抽象，我们提出了一种使用安全的多方计算来机械分析密码协议安全性的方法。我们通过分析SIMAP甜菜双拍卖协议来举例说明我们框架的适用性。最后，我们研究了抽象的计算安全性，证明对应用的$ pi $演算中表示的协议以及基于我们的抽象的协议的分析提供了计算安全性保证。
展开▼
