Formally verified authenticated query dissemination in sensor networks

We consider the problem of authenticated query dissemination in sensor networks, where each sensor node should be able to decide whether the query was injected into the network by a legitimate entity (e.g., the base station), or by an adversary that tries to gain unauthorized access to the sensor data. We present sAQF, an improved variant of the AQF protocol by Benenson et al. and verify its correctness by means of a model based on probabilistic action systems.