Computationally Sound Abstraction and Verification of Secure Multi-Party Computations

ionally Sound Abstraction and Verification of Secure Multi-Party Computations Michael Backes Saarland University MPI-SWS Matteo Maffei Saarland University Esfandiar Mohammadi Saarland University October 7, 2010 e an abstraction of secure multi-party computations in the applied -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 soundour abstraction, proving that the analysis of protocols expressed in the applied -calculus d on our abstraction provides computational security guarantees. Contents

• Type: Journal
• Year: 2010
• Where: FSTTCS
• Authors: Michael Backes, Matteo Maffei, Esfandiar Mohammadi
• Keywords: Abstraction, FSTTCS 2010, Saarland University, Secure Multi-party Computations, Software Engineering