Hyperproperties for Safe and Secure RFID Systems

Although there have been many contributions to the rigorous description and verification of RFID-based systems and their safety and security properties, there has yet to be much progress toward an explicit formalization of information flow policies for such systems in terms of hyperproperties. In this paper, we introduce three classes of hyperproperties related to the analysis of anti-collision protocols for RFID tags: hyper-reachability, hyperadaptivity, and generalized non-interference. As a modeling framework, we employ an event-based model (suitable for representing a large portion of existing RFID systems, both with passive and battery-powered tags) featuring a component-oriented notion of state and allowing us to express hyperproperties in terms of event satisfaction by component configurations. For each hyperproperty, we provide a formalization à la Clarkson-Schneider and a hyperlogic characterization. We also propose some insights about decidability issues.