Modelling cryptographic protocols in a theory of action

Hunter, Aaron (Aaron Hunter (Aaron_Hunter)) (author)
Delgrande, James, P. (author)
Grote, Torsten (author)
(editor)
(translator)

© 2009 James P. Delgrande, Torsten Grote and Aaron Hunter.

Proceedings of the Ninth International Symposium on Logical Formalizations of Commonsense Reasoning, Toronto, ON, June 1-3, 2009. This paper proposes a framework for analysing cryptographic protocols by expressing message passing and possible attacks as a situation calculus theory. While cryptographic protocols are usually quite short, they are nonetheless notoriously difficult to analyse, and are subject to subtle and nonintuitive attacks. Our thesis is that in previous approaches for expressing protocols, underlying domain assumptions and capabilities of agents are left implicit. We propose a declarative specification of such assumptions and capabilities in the situation calculus. A protocol is then compiled into a sequence of actions to be executed by the principals. A successful attack is an executable plan by an intruder that compromises the stated goal of the plan. We argue that not only is a full declarative specification necessary, it is also much more flexible than previous approaches, permitting among other things interleaved runs of different protocols and participants with varying abilities.

http://hdl.handle.net/10453/19495