Access Restriction

Author Canetti, Ran ♦ Herzog, Jonathan
Source CiteSeerX
Content type Text
File Format PDF
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
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 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. We exemplify the approach in the case of authentication and key-exchange 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
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Publisher Date 2009-01-01