CITI has stopped operations in 2014, to co-launch NOVA LINCS THIS SITE IS NOT BEING UPDATED SINCE 2013
citi banner
  Home  \  Seminars @ CITI  \  Seminar Page Login  
banner bottom
File Top
A Spatial-Epistemic Logic and Tool for Reasoning about Security Protocols
{ Wed, 16 Dec 2009, 14h00 }

By: Bernardo Toninho

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.

Hosted by: Software Systems

Location: DI Seminars Room

File Bottom