Date Added: Oct 2009
As mobile devices pervade physical space, the familiar authentication patterns are becoming insufficient: besides entity authentication, many applications require, e.g. location authentication. While many interesting and subtle protocols have been proposed and implemented to provide such strengthened authentication, there are very few proofs that such protocols satisfy the required properties. The authors consider the problem of adapting the Dolev-Yao-style reasoning methods for pervasive security. They show how the notion of guards, previously used for symbolic reasoning about secrecy, can be extended into a tool for analyzing pervasive authentication. It supports a simple form of probabilistic reasoning, necessary for situations where the authentication cannot be achieved in absolute sense, and needs to be quantified.