University of Tartu - ©2011 Rafik Chaabouni - Last update: 08.04.2013 15:13
Date: 11/04/2013 Location: J. Liivi 2, room 317 (next to the coffee room)
Speaker: Dominique Unruh
Title: Symbolic Universal Composability
Abstract:
The definition of Universal Composability (UC; Canetti, FOCS 2001) is a cryptographic security definition that is both simple and gives very strong security guarantees. In particular, it ensures that the composition of secure protocols stays secure. The idea of UC is not, however, restricted to the cryptographic (computational) setting; instead, one can see it as a refinement relation on protocols and programs that preserves security and is composable. We show how UC can be applied in a symbolic security setting. We also show a new design technique (virtual primitives). This design technique allows to circumvent, in a symbolic UC setting, various impossibility results that apply in the cryptographic setting. Finally, we discuss the problem of automated verification in this setting.