Towards an awareness-based semantics for security protocol analysis

We report on work-in-progress on a new semantics for analyzing security protocols that combines complementary features of security logics and inductive methods. We use awareness to model the agents' resource-bounded reasoning and, in doing so, capture a more appropriate notion of belief than those usually considered in security logics. We also address the problem of modeling interleaved protocol executions, adapting ideas from inductive methods for protocol verification. The result is an intuitive, but expressive, doxastic logic for formalizing and reasoning about attacks. As a case study, we use awareness to characterize, and demonstrate the existence of, a man-in-the-middle attack upon the Needham-Schroeder Public Key protocol. This is, to our knowledge, not only the first doxastic analysis of this attack but also the first practical application of an awareness logic. Even though defining the awareness sets of the agents, a task that is left unspecified in formal works on awareness logics, turns out to be surprisingly subtle, initial results suggest that our approach is promising for modeling, verifying and reasoning about security protocols and their properties.