Detail

A Spatial-Epistemic Logic and Tool for Reasoning about Security Protocols

Security protocols are of great importance to the security of systems.
Unfortunately, they are notoriously difficult to design and analyze, which
frequently leads to serious design flaws. Thus, it becomes necessary to
develop techniques to analyze and verify the correctness of a security protocol, given its
high-level, abstract specification.
In this talk, we present a framework for security protocol analysis based on
process models and logic specifications that aims to verify the
correctness of security protocols in the presence of adversaries, taking
advantage of the fact that reasoning about security very often involves
reasoning about the knowledge of the several principals of a system.
The framework consists of a modeling language for systems (process calculus) and a
modeling language for properties (logic), that may be used to mechanically determine if a protocol
conforms to a specification.
To perform this automatic verification, we have also developed an implementation of a
model-checking algorithm, as an extension to the SLMC tool.