Universally Composable Symbolic Security Analysis

Authors: Ran Canetti Jonathan Herzog

Publish Date: 2010/03/09

Volume: 24, Issue: 1, Pages: 83-147

PDF Link

Abstract

In light of the growing complexity of cryptographic protocols and applications it becomes highly desirable to mechanize—and eventually automate—the security analysis of protocols A natural step towards automation is to allow for symbolic security analysis However the complexity of mechanized symbolic analysis is typically exponential in the space and time complexities of the analyzed system Thus full automation via direct analysis of the entire given system has so far been impractical even for systems of modest complexityWe propose an alternative route to fully automated and efficient security analysis of systems with no a priori bound on the complexity We concentrate on systems that have an unbounded number of components where each component is of small size The idea is to perform symbolic analysis that guarantees composable security This allows applying the automated analysis only to individual components while still guaranteeing security of the overall systemWe exemplify the approach in the case of authentication and keyexchange protocols of a specific format Specifically we formulate and mechanically assert symbolic properties that correspond to concrete security properties formulated within the Universally Composable security framework As an additional contribution we demonstrate that the traditional symbolic secrecy criterion for key exchange provides an inadequate security guarantee regardless of the complexity of verification and propose a new symbolic criterion that guarantees composable concrete securityThis work was first presented at the DIMACS workshop on protocol security analysis June 2004 An extended abstract appears in the proceedings of the Theory of Cryptography Conference TCC March 2006 Most of the research was done while both authors were at CSAIL MIT

Keywords: