Copyright Information
The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other
copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying
this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without
the explicit permission of the copyright holder.
Sensoria Bibliography Site A symbolic framework for multi- faceted security protocol analysis
Andrea Bracciali, Gianluigi Ferrari, Emilio Tuosto
abstract:
Software verification in general, and security protocol analysis as a particular case, require frameworks that are expressive, so as to properly capture the relevant aspects of the system and its properties, formal, so as to be provably correct, and with a computational counterpart, so as to support the (semi-)automated certification of properties. Specifically, security protocols also present hidden assumptions about the context, specific subtleties due to the nature of the problem and sources of complexity that tend to make verification incomplete. We present a verification framework that is expressive enough to capture a few relevant aspects of the problem, like symmetric and asymmetric cryptography and multi-session analysis, and to make assumptions explicit, e.g. the hypotheses about the initial sharing of secret keys among honest (and malicious) participants. It features a clear separation between the modeling of the protocol functioning and the properties it is expected to enforce, the former in terms of a calculus, the latter in terms of a logic. This framework is grounded on a formal theory that allows us to prove the correctness of the verification carried out within the fully-fledged model. It overcomes incompleteness by performing the analysis at a symbolic level of abstraction, which, moreover, transforms into executable verification tools.