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.
Since its oficial patenting in the 1980s, the Radio-Frequency Identification (RFID) technology has been experiencing relentless advancement due to its extreme versatility and usability in a wide range of contexts such as access control, logistics, retail, and supply chain management [1]. Moreover, as an enabling technology for the IoT computing paradigm, RFID today underpins new systems and protocols for object identification/data acquisition in smart environments [ 2]. At the same time, RFID-based systems are proving vulnerable to attacks conducted against RFID technology, such as cloning, replaying, relaying, and even backend attacks that exploit RFID vulnerabilities to inject commands to the backend of the system, including middleware and database management systems [3, 4, 5].
Despite a large number of contributions to the formal description and verification of RFID-based systems and protocols, to the best of our knowledge, no foundational framework has yet been proposed for the explicit formalization of information flow policies for RFID systems in terms of hyperproperties [6]. The need for studies in this direction has emerged especially, though not always explicitly, in the area of information security (see, e.g., [7, 8, 9, 10, 11]).
This paper aims to be a first step toward a taxonomy of hyperproperties for RFID systems, laying the foundation for a general framework for their formalization. To this end, we introduce a low-level, trace-based model suitable for representing a large portion of existing RFID systems (both with passive and battery-powered tags) implementing tree protocols for tag collision arbitration [12]. Our model features a component-oriented, event-based notion of state allowing us to express hyperproperties in terms of event satisfaction by component configurations. Our model assumes a prior high-level specification in terms of Kripke structures, automata, or labeled transition systems, which is not provided in this paper. The notions of state and trace are therefore intended to derive from such a specification. Moreover, system executions are assumed to be synchronous and discrete-time.
Within this framework, we introduce three classes of hyperproperties for the analysis of tree-based anti-collision protocols for RFID tags, and we discuss the safety and security conditions they allow us to investigate. The three classes are hyper-reachability, hyper-adaptivity, and generalized non-interference. While generalized non-interference is an instance of the general template introduced in [13], hyperreachability and hyper-adaptivity are novel and specifically designed for RFID systems. For each class, we provide a classical definition in the style of [ 6] and a formalization in a suitable hyperlogic [14]. It turns out that hyper-reachability and generalized non-interference are expressible in HyperLTL, while hyper-adaptivity requires the first-order logic FO[<, ]. On the basis of the quantifier prefix of each formula obtained, we provide information on decidability and complexity results with respect to the problems of satisfiability and model checking in the combined input Kripke structure/HyperLTL formula (the latter problem in the cases of hyper-reachability and generalized non-interference only).
The paper is organized as follows. In Section 2, we provide some background information about RFID technology and tree-based anti-collision protocols for RFID tags. In Sections 3 and 4, we present our abstract model of an RFID system and set up the machinery for hyperproperty formalization. In Section 5, we propose our three classes of hyperproperties for RFID verification. In Section 6, we provide some closing remarks and indicate possible directions for future research.
2.1. RFID systems An RFID system is made up of three main components: a controller, a reader, and a batch of tags. A tag is a transponder consisting of a microchip connected to an antenna. The microchip can store and process (a small amount of) data, which can be transmitted by the antenna in the form of radio signals. RFID tags can be either passive, semi-passive or active. Passive tags do not have an embedded power source. Semi-passive and active tags, on the other hand, are provided with an internal battery, but difer in an important respect: in the former, the battery powers the microchip and possibly some additional on-board component (e.g., a sensor), but does not supply energy for signal transmission; in the latter, it performs both functions. The reader is a device (also equipped with its own antenna) capable of uniquely identifying, tracking or locating tags by generating an electromagnetic field. The controller is a backend workstation connected to the reader via a network interface (either wired or wireless). Depending on the particular infrastructure the RFID system is integrated into, the controller carries out a number of diferent tasks. First and foremost, it is responsible for collecting and somehow processing the raw data captured by the reader.
An RFID system is activated each time the reader emits a data request signal through its antenna. In the case of passive and semi-passive systems, if a tag is within the reader’s interrogation zone, the signal transmitted by the reader is picked up by the tag’s antenna and converted into electrical energy for the microchip’s circuitry. At this point, the tag transmits the requested information to the reader via load/backscatter modulation. In the case of active systems, the tag responds to the reader using its own power source. 2.2. The symmetry problem In this paper, we only consider systems where the communication between the reader and the tags takes place on a single multiple access channel. In such a context, tag-to-reader collisions [15] can occur whenever two or more tags respond to a data request from the reader at the same time. Indeed, simultaneous reply transmissions interfere with each other and, as a result, the reader cannot distinguish between the tags. This situation is commonly referred to as the symmetry problem. As for collision arbitration, we assume that the system implements a well-known tree algorithm based on random bit extraction by the tags and identification via binary address by the reader. Originally developed in the broader context of conflict resolution techniques in shared communication channels, this protocol was independently introduced and studied in [16, 17, 18]. Over time, it has undergone several modifications and optimizations, many of which have been successfully applied to the RFID context [12].
In the event of a collision, the protocol states that the reader sends negative feedback to all tags in its interrogation zone, asking them to extract a random bit. After that, the reader interrogates all tags that extracted, say, 0. If a collision still occurs, then this splitting procedure is iterated until the reader successfully communicates with every tag in the first group. The procedure is then repeated for tags that initially extracted 1. At the end of the protocol, each tag has its own unique identifying bitstring (address) consisting of the sequence of outcomes of all its extractions.
In this section, we introduce our model of an RFID system and specify its essential architecture by detailing the input and output ports relevant to our analysis. On this basis, we define the notions of event, state, and trace. 3.1. Components and interfaces We represent an RFID system as a triple S = ⟨C, R, T⟩, where C is the backend controller, R is the reader, and T = {tag}∈ is a batch of tags indexed over a finite integer set of cardinality || > 1. We denote input and output ports of S using the notation port, where port is a port name and ∈ {, } is a port type (see Table 1). Each component tag is equipped with an input port data_request to receive instructions from R and an output port reply to send back information. Clearly, R is provided with the corresponding ports data_request and reply. The raw data that the reader acquires from the tags are sent to C via data and received at data. Once the data have been processed, the controller outputs them in their final form through the port p_data. Since the total number of tags is ||, a tag collision of multiplicity at most || can occur every time the reader sends a request. In each round of communication, the reader assesses whether the transmissions were successful or not and sends feedback to the tags in its interrogation zone via the port feedback. In particular, feedback returns the values 0 (idle), 1 (success) and 2+ (collision). Feedback is received by the tags at feedback. In the case of a collision, the tags and the reader enable, respectively, the ports r_bit (used for random bit extraction) and address (used for tag identification and transmission attempt authorization during the execution of the anti-collision protocol). The address bitstring and the random bit are sent to the input port address of the tag, which compares the last bit of the address with the extracted random bit, possibly authorizing a new data transmission via reply (the information flows among the ports are depicted in Figure 1). 3.2. Events, states and traces Our model is based on the primitive notion of event. An event represents the activity state of a single port of the system. In our framework, events are atomic entities, so they cannot be combined into more “complex” events, nor can they describe the activity of more than one port. We use ad-hoc notations for three diferent types of events. The first one is port : , where ∈ {0, 1} is a Boolean value. We write port : to express the fact that, depending on , an input or an output value for port is present ( = 1) or absent ( = 0) and, accordingly, the information flows or does not flow through the port. Sometimes, we will also need to make explicit what input or output values are present for a certain reply feedback address
reply feedback address r_bit port. So we write port ▷ and port ◁ to mean that port is taking the value as input and port is returning the value as output, respectively.
Events are the building blocks of the notions of configuration and state. Let X be a component of S. An event set (e-set) for X is any set of events related to the ports of X. We say that an e-set for X is well-defined if it contains exactly one event port : for each port of X and, whenever = 1, it possibly contains an event making explicit the value present for port. A configuration of X is a well-defined e-set for X. A state of S is a tuple of configurations of the form = ⟨︀ C, R, tag1 , . . . , tag|| ︀⟩ . For a state and a component X, we write . X to denote the configuration X at . The state space of S is denoted by Σ S. A trace is an -word over Σ S. We denote by S the set of execution traces of S.
Finally, we define event satisfaction. We say that an event is satisfied by the configuration of X at state (notation: . X ⊨ ) whenever ∈ . X. 3.3. The anti-collision protocol Following [12], we present below two pseudocodes illustrating the anti-collision protocol from the perspective of both the reader (Algorithm 1) and a generic tag (Algorithm 2). The instructions are formulated in accordance with our modeling framework.
Algorithm 1 The protocol run at R 1 = [ ]; 2 = 0; 3 while == 0: 4 data_request ◁ 5 address ◁ 6 if reply ▷ × : // collision 7 feedback ◁ 2+ 8 .ℎ(0) 9 else if reply ▷ : 10 feedback ◁ 1 11 while .() == 1: 12 .() 13 if == [ ]: 14 = 1 15 else: 16 .() 17 .ℎ(1) 18 else: feedback ◁ 0 Algorithm 2 The protocol run at tag 1 = [ ]; 2 = 0; 3 while == 0; 4 data_request ▷ 5 address ▷ 6 if == : 7 reply ◁ 8 if feedback ▷ 2+: 9 r_bit ◁ 10 .ℎ() 11 else if feedback ▷ 1: 12 = 1
A standard approach for describing and reasoning about the behavior of a computational system is to represent it as the set of all its execution traces, i.e., the sequences of states corresponding to the computations that the system performs. This method allows to model many policies satisfied by the system in terms of trace properties (in this perspective, a policy is nothing more than the set of execution traces complying with it), ofering a natural framework for a classification based on the safety-liveness dichotomy [19]. However, in this context, one cannot specify those policies whose modeling and verification must take into account the interaction between a system and its environment. Non-interference [20] and many other fundamental information flow security policies [ 21] typically fall into this category.
In their celebrated paper [6], Clarkson and Schneider introduced hyperproperties, a powerful formalism for expressing such policies. Hyperproperties specify conditions under which the behavior of a system in certain runs does or does not depend on the characteristics of certain alternative executions. It is precisely because of this major diference from trace properties that hyperproperties must be formally modeled as properties of systems. So, if a trace property is a set of execution traces, a hyperproperty is a set of trace properties. Accordingly, if the definitions of nontrivial trace properties require quantification on instants of time, those of hyperproperties require an additional level of quantification on traces in order to impose conditions on diferent executions and to relate them to each other.
In the following, we show how to formalize hyperproperties for RFID systems in light of our eventbased model. 4.1. Hyperproperties We start by discussing the modeling of a classical trace property for S, namely reachability, prescribing that whenever the reader sends a request to the tags, after some time the -th tag sends back a successful response. This is an example of liveness policy, and as such it is expressible in Linear Temporal Logic (LTL) [22]. Indeed this policy corresponds to the trace property PS[] ⊆ Σ S consisting of all traces satisfying the LTL formula 2( → ◇ ) where: := [R ⊨ data_request : 1], and := [tag ⊨ reply : 1] ∧ ##[R ⊨ feedback ◁ 1].
Note that we assume the reader returns feedback two states after the tag’s response. Let be a set of atomic propositions. Observe that the standard semantic clause for ∈ in LTL is formulated as , |= ⇔ ∈ [], where is a trace and ∈ N. In our case, every such an is the counterpart of a satisfaction statement of the form [].X ⊨ . Since states and traces become explicit only at the semantic level, we unfold the internal structure of atomic propositions using the notation [X ⊨ ]. Thus, according to our event-based framework, we obtain
, |= [X ⊨ ] ⇔ ∈ [].X ⇔ [].X ⊨ .
By Kamp’s Theorem [23] (see also [24, 25, 26]), we know that LTL is expressively equivalent to FO[<], the fragment of first-order logic (with equality) over the class of Dedekind complete linearly ordered structures with monadic predicates {}∈ (in this paper, our reference model is clearly built over N). With a slight abuse of notation, we write [X ⊨ ]() for the atomic open FO[<] formula corresponding to [X ⊨ ] in LTL. We can therefore redefine PS[] as the class of all traces ∈ Σ S satisfying the FO[<] formula ∀.( () → ∃ > . ()), where: () := [R ⊨ data_request : 1](), and () := [tag ⊨ reply : 1]() ∧ [R ⊨ feedback ◁ 1]( + 2).
In [6], Clarkson and Schneider’s formalization assumes, though does not always explicitly use, a twosorted first-order notation allowing quantification both over traces and over instants of time. In this setting, elementary facts about system behaviors are expressed by binary predicates of the form (, ). We can think of each of these predicates as being associated with an atomic proposition ∈ . So, in our context, for = [X ⊨ ], we have (, ) := [].X ⊨ .
Going back to the previous example, suppose we want to model an information flow policy based on PS[] requiring that for every execution in which the reader globally fails to communicate with the -th tag, there is at least one in which communication is successful. For ∈ {1, 2}, let us define: ( , ) := [].R ⊨ data_request : 1 ( , ) := ( [].tag ⊨ reply : 1) ∧ ( [ + 2].R ⊨ feedback ◁ 1) := ∀.∃ > .( ( , ) → ¬ ( , )) := ∀.∃ > .( ( , ) → ( , )) So we can define a hyperproperty HPS[] consisting of all ⊆ Σ S satisfying:
∀ 1.∃ 2.︀( 1 → 2︀) .
The hyperproperties we introduce in Section 5 are defined in this way. 4.2. Hyperlogics In recent years, much efort has been devoted to the development of logics for verifying hyperproperties for both linear and branching time systems. The wide variety of formalisms introduced (known as hyperlogics) has led to the construction of an expressiveness hierarchy [14] that is constantly being enriched with new elements. In this paper, we formalize our hyperproperties using the well-known linear time hyperlogics HyperLTL and FO[<, ].
HyperLTL [27] extends LTL with an additional layer of syntax enabling quantification over trace variables from a denumerable set = { 1, 2, . . . }. Further, atomic propositions are annotated with the trace variables with respect to which they are to be evaluated. Well-formed formulas are defined by the following grammar: ::= | ∀. | ∃. ::= | ¬ | ∧ | # | Evaluation of HyperLTL formulas is defined with respect to a set of traces ⊆ ℘( ) and a (partial) trace assignment Π : → . In the following list, we denote by Π[ ↦→ ] the assignment that coincides with Π except for the trace assigned to .
Π , |= Π , |= ¬ Π , |= ∀. Π , |= ∃. ⇔ ∈ Π( )[] ⇔ Π , ̸|= ⇔ ∀ ∈ .Π[ ↦→ ], |= ⇔ ∃ ∈ .Π[ ↦→ ], |= Π , |= 1 ∧ 2 ⇔ Π , |= 1 and Π , |= 2 Π , |= #
⇔ Π , + 1 |= Π , |= 1 2 ⇔ ∃ ≥ .Π , |= 2 and ∀ ∈ [, ).Π , |= 1 The temporal modalities ◇ (eventually) and 2 (globally) are defined in the usual way, with ◇ := true and 2 := ¬◇¬ . Note that, as regards our case study, the semantic clause for atomic propositions becomes:
Π , |= [X ⊨ ] ⇔ ∈ Π( )[].X ⇔ Π( )[].X ⊨ .
Although HyperLTL allows for the description of a wide variety of hyperproperties, this logic lacks suficient syntactic resources to express equality/non-equality statements between instants of time. This problem does not arise in the first-order logic FO[<, ] [28], which is obtained by extending the syntax of FO[<] with the addition of a new binary predicate symbol that expresses equality between instants of time (with respect to either the same or diferent traces). Starting from a denumerable set of variables = {1, 2, . . . }, well-formed FO[<, ] formulas are given by the following grammar: ::= | ¬ | 1 ∧ 2 | ∀. | ∃. ::= () | < | = | (, ) The intended models of FO[<, ] are structures with universe × N, where ⊆ ℘( ) is a set of traces. For ⟨, ⟩ ∈ × N and ∈ {1, 2}, we denote by (⟨, ⟩) the projection on the -th component of ⟨, ⟩. The semantics of FO[<, ] is defined with respect to (partial) pair assignments : → × N, according to the following clauses: |= () |= < |= = |= ¬ |= ∀. |= ∃. |= (, ) ⇔ 2( ()) = 2( ())
⇔ ̸|= |= 1 ∧ 2 ⇔ |= 1 and |= 2 ⇔ ∀ ∈ .∀ ∈ N. [ ↦→ ⟨, ⟩] |= ⇔ ∃ ∈ .∃ ∈ N. [ ↦→ ⟨, ⟩] |= ⇔ ∈ [], where = 1( ()) and = 2( ()) ⇔ 1( ()) = 1( ()) and 2( ()) < 2( ()) ⇔ () = () FO[<, ] has been shown to be strictly more expressive than HyperLTL [28, Thm. 8]. Nevertheless, an analog of Kamp’s theorem for HyperLTL has been proved for a fragment of FO[<, ] [28, Thm. 9]. Finally, recall that, with respect to sets of infinite traces, FO[<, ] is expressively equivalent to the recently introduced Hypertrace Logic [29], whose syntax incorporates and extends the twosorted notation of Clarkson and Schneider. All definitions of our hyperproperties can thus be seen as formalizations in this hyperlogic.
In this section, we introduce three hyperproperty templates for RFID systems: hyper-reachability, hyper-adaptivity, and generalized non-interference. This choice is not accidental. In fact, all three policies can be related to both safety and security contexts, so that compliance with them represents a prerequisite for the optimal operation of any system that fits the model presented in Section 3. 5.1. Hyper-reachability Among the policies our system has to comply with in order to have full functionality, there should be one prescribing that, for every execution where the reader is able to successfully communicate with only tags (for < ||), there exist other executions where it manages to communicate with all the remaining || − tags. However, since the tag-to-reader data transmissions can be compromised by several problems that the system itself cannot solve, this policy is too strong to be enforced in real cases. We thus propose a weaker version thereof by relaxing the condition on the existence of the alternative runs. In particular, our policy prescribes that there exists at least one execution where the reader successfully communicates with at least one nonempty subset of the remaining || − tags. Since we are reasoning in terms of pairs of disjoint sets of tags, we are actually defining a class of hyperproperties for S, each one defined with respect to a two-element partition of . Definition 1 (Hyper-reachability). Let Π 2() be the set of all the two-element partitions of . For ∈ Π 2() with blocks , , the hyper-reachability property for S with respect to is the set HRS[] of all ⊆ Σ S satisfying:
⎛⎛ ∀ 1.∃ 2. ⎜⎜⎝ ⋀︁∃. ( 1, ) ∧⋀︁¬∃′. ( 1, ′)⎠ → ⎝ ∈ ∈
⎞ ⎞
⎞ ⊆ ∈ ̸=∅ ⋁︁ ⋀︁ ∃. ( 2, )⎟⎟
⎠ ⎞ ⊆ ∈ ̸=∅ ⋁︁ ⋀︁ ◇ ( 2)⎟⎟ ⎠ ⎛⎛ ∀ 1.∃ 2. ⎜⎜⎝⎝⋀∈︁◇ ( 1) ∧⋀∈︁¬◇ ( 1)⎠ → where, for ∈ {1, 2}, ∈ , and ∈ N:
( , ) := ( [].tag ⊨ reply : 1) ∧ ( [ + 2].R ⊨ feedback ◁ 1).
We say that S satisfies the weak (resp., the strong) hyper-reachability property if S ∈ ⋃︀∈Π2() HRS[] (resp., S ∈ ⋂︀∈Π2() HRS[]).
Hyper-reachability admits the following formalization in HyperLTL: where, for ∈ {1, 2} and ∈ :
( ) := [tag ⊨ reply : 1] ∧ ##[R ⊨ feedback ◁ 1] .
It is well known that the satisfiability problem for the class of HyperLTL formulas with quantifier prefix ∀∃ is undecidable [30, Thm. 14]. The model checking problem for the same class is instead expspace-complete [27, 31].
In summary, hyper-reachability ensures that no environmental factor can prevent a given set of tags from communicating with the reader in any possible system execution. To further clarify this point, let us take a concrete example. In the RFID context, read reliability is defined as the probability that a tag is recognized when it is placed within the reader’s interrogation zone. Experimental results have shown that reliability depends, among other things, on the orientation of the tag’s antenna relative to the reader’s one [32]. Thus, an improper spatial arrangement of tags, either due to random factors or malicious tampering, could compromise the success of some transmissions by lowering the read reliability value for some tags. An RFID system satisfying hyper-reachability must therefore be part of an infrastructure that is appropriately designed to prevent the above problem from occurring with respect to the same tags in every possible situation. Hyper-reachability is therefore a policy that must be enforced at the physical layer. 5.2. Hyper-adaptivity Very often, the environmental conditions in which the reader queries tags are not static. The spatial layout of components and the order in which transmissions occur can vary from execution to execution, potentially resulting in diferent data acquisitions by the reader and processing outcomes by the controller. We introduce an adaptivity policy for S stating that, for any system execution in which the controller outputs a value (assumed to be a real number), there are distinct alternative executions in each of which the reader successfully makes distinct acquisitions and the controller outputs an approximated value of the form ± , with a tolerance parameter. This is an adaptive policy because its satisfaction would show that the system can adapt to a dynamic context while still ensuring mutually consistent results. Clearly, , , and represent indices of robustness: the larger , and the smaller , the more robust the system.
︃( respect to , , and is the set HAS[, , ] of all ⊆ Σ S satisfying: Definition 2 (Hyper-adaptivity). For , ∈ N and ∈ R, the hyper-adaptivity property for S with =1
)︃)︃ ̸=′ =1 =1 ̸=′ ̸=′ (︃ ⋀︁ =1 ⎛ ∀⟨, ⟩.∃=1⟨ , ⟩.∃⟨ , ℎ ⟩.∃=1⟨ , ⟩. ⋀︁ ⟨ , ⟩ ̸= ⟨ ′ , ′ ⟩ ∧ ⋀︁⟨ , ⟩ < ⟨ , ℎ ⟩ ∧ ⋀︁¬ ︁( ⟨ , ⟩, ⟨ , ′ ⟩ ∧ ⎝ (⟨, ⟩) → )︁ ⋀︁ (⟨ , ℎ ⟩) ∧ ⋀︁ (⟨ , ⟩) )︃⎞
⎠ . ̸=′ (︃ =1 (, ) := [].C ⊨ p_data ◁ , ( , ℎ ) := [ℎ ].C ⊨ p_data ◁ ± , ( , ) := [ ].R ⊨ feedback ◁ 1.
Section 4):
A hyperlogic characterization of HAS[, , ] can be provided by the following FO[<, ] formula (where (⟨, ⟩), (⟨ , ℎ ⟩), and (⟨ , ⟩) are defined according to the conventions adopted in where (, ), ( , ℎ ), and ( , ) are defined as follows: It can be easily checked that this formula belongs to the Ackermann class with equality, i.e., the fragment be decidable with complexity ntime(2/ log ), for some constant [33, Cor. 6.3.30]. [∃* ∀∃* , ]= of first order logic with equality, for which the satisfiability problem has been shown to
Hyper-adaptivity is designed for all those infrastructures where tags transmit data acquired from some sensing device. Consider an RFID system where each tag has an on-board sensor for temperature measurement. Suppose that the reader collects temperature data and sends them to the controller, which returns an arithmetic mean of the received values. In such a scenario, hyper-adaptivity ensures that, for any system execution where the controller computes a mean at the end of a communication round, there are suficient
(at least ) and relevant distinct alternative runs (each with distinct temperature acquisitions) where the controller obtains the same mean up to a tolerance parameter . Suppose, for instance, that some tags are temporarily disabled due to a jamming attack or a passive interference, or that after a cloning attack on some tags, the counterfeit tags transmit incorrect data. In both cases, the mean may be either incorrect or based on too few data acquisitions. Therefore, the sensitivity analysis with respect to the choices of the indices , , and is helpful to provide insights about the impact of such kinds of situations. 5.3. Generalized non-interference Non-interference provides one of the most important families of information flow security policies. Developed in the context of multilevel security, it was introduced by Goguen and Meseguer [20] in a deterministic setting and generalized to nondeterministic systems by McCullough [34] and McLean [13]. Subsequently, non-interference has been widely studied in many diferent frameworks, such as, e.g., the semantics of concurrent programs [35], language-based static analysis [36], abstract interpretation [37], property compositionality in process algebra [38], and reversible computing [39].
Here we show how a generalized notion of non-interference can be adapted to a specific condition of interest (with respect to both safety and security aspects) for RFID systems. During the execution of an anti-collision protocol, random bit extractions by tags are events that should under no circumstances compromise the transmission of data to the reader. We express this policy as a generalized noninterference hyperproperty [13] parameterized with respect to a single component tag. Our policy prescribes that, for any two traces, there exists a third interleaved trace that is globally equivalent to the first with respect to random extractions by tag and to the second with respect to the successful detection of tag by the reader. This condition guarantees that, at every possible instant of time, successful detection is independent of random extraction.
Definition 3 (Generalized non-interference). For ∈ , the generalized non-interference property for S with respect to is the set GNIS[] of all ⊆ Σ S satisfying:
∀ 1.∀ 2.∃ 3.∀.( ( 1, ) ↔ ( 3, ) ∧ ( 2, ) ↔ ( 3, )) where, for ∈ {1, 2, 3} and ∈ N, ( , ) := [].tag ⊨ r_bit : 1 and
( , ) := [].tag ⊨ reply : 1 ∧ [ + 2].R ⊨ feedback ◁ 1.
We say that S satisfies the strong generalized non-interference property if S ∈ ⋂︀∈ GNIS[].
GNIS[] can be expressed in HyperLTL:
∀ 1.∀ 2.∃ 3.2( ( 1) ↔ ( 3) ∧ ( 2) ↔ ( 3)) where, for ∈ {1, 2, 3}, ( ) := [tag ⊨ r_bit : 1] and:
( ) := [tag ⊨ reply : 1] ∧ ##[R ⊨ feedback ◁ 1] .
Decidability results are the same as in the hyper-reachability case.
Notice that GNIS[] describes a safety condition as its satisfaction is a prerequisite for the correct execution of collision arbitration. However, it can also be used to formalize a security property to verify whether the system mitigates attacks intended to alter the random extraction and invalidate the protocol. While this is just an instance of generalized non-interference, an analogous template can formalize several security aspects of RFID systems [7], including confidentiality and integrity [ 40], authentication [41], and even trust [42] for decentralized systems [43, 44, 45].
In this paper, we initiated a taxonomy of hyperproperties allowing to address both safety and security issues in RFID-based infrastructures. As future work, we plan to extend our classification with information flow policies relevant for the IoT context, also in view of applications to the analysis and verification of systems and protocols based on wireless sensor networks and mobile ad-hoc networks. We then intend to proceed to the algorithmic vericfiation of the hyperproperties obtained in existing model checkers1. Finally, it would be interesting to investigate counterexamples in case of policy violations [47].
This work has been funded by the European Union - NextGenerationEU within the framework of PNRR Mission 4 - Component 2 - Investment 1.1 under the Italian Ministry of University and Research (MUR) programme "PRIN 2022" - grant number 2022598LMZ - AsCoT-SCE - CUP: H53D23003430006. [1] K. Finkenzeller, RFID Handbook: Fundamentals and Applications in Contactless Smart Cards,
Radio Frequency Identification and near-Field Communication, 3rd ed., Wiley, Hoboken, 2010. 1For instance, MCHyper [46], available at https://finkbeiner.groups.cispa.de/tools/mchyper/.