Starting from algebraic properties that enable guessing low-entropy 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. © 2010 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Groza, B., & Minea, M. (2010). A formal approach for automated reasoning about off-line and undetectable on-line guessing. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6052 LNCS, pp. 391–399). https://doi.org/10.1007/978-3-642-14577-3_34
Mendeley helps you to discover research relevant for your work.