Seminars

Automated Detection of Guessing and Denial of Service Attacks in Security Protocols PDF

Marius Minea
Politehnica University of Timisoara, Romania

3/18/2011, 1:30 PM, GHC-6501

Abstract

This talk presents an approach to modeling two types of security flaws for which limited or no prior support for automated detection exists.

We formalize symbolic rules for detecting off-line and on-line guessing attacks starting from algebraic properties that enable guessing low-entropy secrets. For denial of service, we propose a set of cost-based rules that formalize resource exhaustion by excessive or malicious use. Using the model checkers of the AVANTSSAR validation platform, where protocols are modeled with rewrite rules and Horn clauses, we have found several known and some previously unreported attacks.

This is joint work with Bogdan Groza.

Biography

Marius Minea is an associate professor at the Politehnica University of Timisoara, Romania. He received his PhD from Carnegie Mellon in 1999, working with Ed Clarke on partial-order reduction for timed systems, and was a postdoctoral researcher at the University of California, Berkeley, in 2000-01. His research interests are in formal methods for real-time systems and security, and on software analysis and testing.