Sciweavers

FC
2010
Springer

A Formal Approach for Automated Reasoning about Off-Line and Undetectable On-Line Guessing

14 years 1 months ago
A Formal Approach for Automated Reasoning about Off-Line and Undetectable On-Line Guessing
Abstract. Starting from algebraic properties that enable guessing lowentropy secrets, we formalize guessing rules for symbolic verification. The rules are suited for both off-line and on-line guessing and can distinguish between them. We add our guessing rules as state transitions to protocol models that are input to model checking tools. With our proof-of-concept implementation we have automatically detected guessing attacks in several protocols. Some attacks are especially significant since they are undetectable by protocol participants, as they cause no abnormal protocol behavior, a case not previously addressed by automated techniques. 1 Motivation and related work As password-based authentication continues to be used in practice and weak passwords are still chosen by users, detecting protocols subject to guessing attacks is a topic of high interest in security. In this paper we address the problem of formalizing a previously introduced approach to detect guessing attacks in a mann...
Bogdan Groza, Marius Minea
Added 02 Sep 2010
Updated 02 Sep 2010
Type Conference
Year 2010
Where FC
Authors Bogdan Groza, Marius Minea
Comments (0)