Modeling partial attacks with alloy (transcript of discussion)

Abstract

The reason we went into this research, was that we found that partial attacks were extremely hard to model in terms of a language that could be used by an automated tool. Now there are three reasons why this is so. The first is that it is hard to identify these attacks even by hand, because you have to be really creative in thinking, what constitutes a reduction in entropy of the secret, that is significant, because a partial attack is really anything that reduces entropy, it's just that it does not reduce the entropy to zero, which would be a case of a complete attack. Next, it's hard to describe that in a formal language, part of that problem comes from the definition, you have to define what you want to be the goal, if the secret is the entire password, then getting one letter is pretty much a partial attack, but if the secret is that one letter, then getting that one letter is a complete attack. And lastly, applying that logic, how do you measure entropy, how do you measure information leakage, that's also very difficult. © 2010 Springer-Verlag.