A symbolic framework for multi- faceted security protocol analysis

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.