We show how any protocol in our class can be compiled to a symbolic representation expressed as a process in an abstract process calculus, and prove a general computational soundness theorem implying that if the protocol realises a given ideal functionality in the symbolic setting, then the original version also realises the ideal functionality in the standard computational UC setting. In other words, the theorem allows us to transfer a proof in the abstract symbolic setting to a proof in the standard UC model.
Finally, we show that the symbolic interpretation is simple enough in a number of cases for the symbolic proof to be partly automated using the ProVerif tool.
Category / Keywords: foundations / Cryptographic protocols, Security analysis, Symbolic analysis, Automated analysis, Computational soundness, Universal composition, Homomorphic encryption Date: received 17 May 2013 Contact author: mdahl at cs au dk Available format(s): PDF | BibTeX Citation Version: 20130525:133304 (All versions of this report) Short URL: ia.cr/2013/296