Cryptographic security of reactive systems: (Extended abstract)

We describe some general relations between cryptographic and abstracted security definitions, and we present a novel model of security for reactive systems, generalizing previous definitions relying on the simulatability paradigm. The larger context is the goal to provide cryptographic semantics for "abstract" specifications, so that the "reality" of the former can be combined with the brevity or, if a formal language is used, the precision and tool-support, of the latter. The novel aspects of our specific definition are a separate treatment of honest users, a precise synchronous switching model, and easy inclusion of various trust models. We also believe to have the first general strategy to deal abstractly with accepted vulnerabilities (such as leakage of traffic patterns), and the first worked-out serious-size examples within a general model. Most importantly, our model has the first general composition theorem, and a link to requirements formulated in logics. © 2000 Published by Elsevier Science B.V.