Verification of software systems, and security protocol analysis as a particular case, requires 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. Additionally, security protocols also present hidden assump- tions about the context, specific subtleties due to the nature of the problem and sources of complexity that tend to make ver- ification incomplete. We introduce 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 frame- work 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, more- over, transforms into executable verification tools.
|Autori:||A. BRACCIALI; FERRARI G; E. TUOSTO|
|Titolo:||A symbolic framework for multi- faceted security protocol analysis|
|Anno del prodotto:||2008|
|Digital Object Identifier (DOI):||10.1007/s10207-007-0043-9|
|Appare nelle tipologie:||1.1 Articolo in rivista|