Universally Composable Symbolic Security Analysis

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 complexity. We 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 system. ...

• Type: Journal
• Year: 2011
• Where: JOC
• Authors: Ran Canetti, Jonathan Herzog
• Keywords: Analysis, JOC 2011, Security, Security Analysis