|Home \ External Talks & Seminars \ External Talk Page||Login|
A Spatial-Epistemic Logic for Reasoning about Security Protocols(Research Talk)
By: Bernardo Toninho
Security protocols are notoriously difficult to design and analyze, which frequently leads to serious security flaws in systems. Thus, it becomes necessary to develop techniques to analyze and verify the correctness of a security protocol, given some high-level, abstract specification. In this talk, we present a framework for security protocol analysis based on process models and logic specifications that explores 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 (a process calculus) and a modeling language for properties (dynamic spatial epistemic logic), that may be used to mechanically determine if a protocol conforms to a specification. The talk will cover some introductory notions on process calculi and dynamic spatial logic and present in detail the two key components of the framework: a process calculus for security and a dynamic spatial epistemic logic for our calculus, for which model-checking is decidable for the class of bounded processes.
Date: 12 Feb 2010
Location/Event: Carnegie Mellon University