Formal Computational Unlinkability Proofs of RFID Protocols
Hubert Comon, Adrien Koutsos
TL;DR
This paper develops a formal framework for proving RFID protocols are computationally unlinkable, introducing axioms for hash functions and demonstrating the first formal unlinkability proofs in the computational model.
Contribution
It introduces a sound axiomatic framework for formal proofs of RFID protocol unlinkability in the computational model, filling a gap in formal security analysis.
Findings
First formal proofs of RFID unlinkability in the computational model
Development of axioms for hash function properties
Formalization of computational unlinkability
Abstract
We set up a framework for the formal proofs of RFID protocols in the computational model. We rely on the so-called computationally complete symbolic attacker model. Our contributions are: i) To design (and prove sound) axioms reflecting the properties of hash functions (Collision-Resistance, PRF); ii) To formalize computational unlinkability in the model; iii) To illustrate the method, providing the first formal proofs of unlinkability of RFID protocols, in the computational model.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Formal Computational Unlinkability Proofs of RFID Protocols
Hubert Comon1, Adrien Koutsos1
1 LSV, CNRS & ENS Paris-Saclay
Abstract
We set up a framework for the formal proofs of RFID protocols in the computational model. We rely on the so-called computationally complete symbolic attacker model. Our contributions are:
To design (and prove sound) axioms reflecting the properties of hash functions (Collision-Resistance, PRF). 2. 2.
To formalize computational unlinkability in the model. 3. 3.
To illustrate the method, providing the first formal proofs of unlinkability of RFID protocols, in the computational model.
I Introduction
It is important to increase our confidence in the security of protocols. Using formal methods to prove a formal security property is the best way to get a strong confidence. There is however a difficulty: we need not only to specify formally the programs and the security properties, but also the attacker.
One of the most popular attacker model, sometimes called the “Dolev-Yao” attacker, consists in assuming that, in between any message emission and the corresponding reception, the attacker may apply a fixed set of rules modifying the message. In addition, the attacker schedules the communications. More precisely, the messages are terms in a formal algebra and the rules are given by a fixed set of combination abilities, together with a rewrite system specifying how to simplify the terms.
There are several more or less automatic verification tools that rely on such a model. Let us cite ProVerif [8], Tamarin [22] and APTE [11] for instance. Completing a proof with one of these tools will however only prove the security in the corresponding DY model.
Another popular attacker model, the computational attacker, gives the same network control to the attacker as in the Dolev-Yao model, but does not limit the attacker computations to the combination of a fixed set of operations: any probabilistic polynomial time computation is possible. More precisely, messages are bitstrings, random numbers are typically bitstrings in (where is the security parameter) and the attacker’s computation time is bounded by a polynomial in . This model reflects more accurately a real-world attacker than the Dolev-Yao model, but formal proofs are harder to complete and more error-prone.
There exist several formal verification tools in the computational model. For example EasyCrypt [6] can be used for the construction of provably secure cryptographic primitives, and CryptoVerif [9] and F [5] have been used for the study of security protocols (e.g. [10, 7]). As expected, such tools are less automatic than the verification tools in the DY model. Using such tools, we may also fail to find a proof while there is one.
We advocate the use of another approach, sketched in [3, 4], which allows to complete formal proofs in the computational model that can be automated and formally checked. This method has many other advantages, some of which are given in these papers: it could be applied, in principle, to more powerful attacker models (such as attackers having access to some side-channels); it can be used to derive “minimal” properties of the primitives that are sufficient to entail the security of the protocol (we will come back to this feature later).
The main technique, which we will recall, is to express the security of a protocol as the unsatisfiability of a formula in first-order logic. The formula contains axioms, reflecting the assumed computational properties of the security primitives, and the negation of the security property, applied to terms reflecting the execution(s) of the protocol. This approach is, we believe, simpler than formally specifying computational security games, probabilistic machines and simulations: there is no security parameter, no probabilities, no timing constraints, no Turing machines …Nonetheless, in case of success, the proof is valid in any model of the axioms, including the computational model.
Compared to EasyCrypt, our logic works at a more abstract level, using only first-order formulas and targeting full automation and a form of completeness (saturating the axioms and the negation of the security property implies that there is an attack).
As it is now, this approach does not provide any quantitative information: the protocol is computationally secure or it is not. We could however extract from a security proof a bound on the success probability of the attacker, depending on its computational power: we would only have to compose the adversary’s advantages corresponding to each clause. Also, because the logic does not include the security parameter, we can only prove the security of a number of sessions of the protocol that does not depend on the security parameter (while there is no such limitation in CryptoVerif for instance). Still, it subsumes the symbolic approach, in which the number of sessions is also independent of the security parameter.
A related logic for reachability security properties has been introduced in [3] and is implemented in the prototype tool Scary [25]. It has been used for a few experiments. The logic for indistinguishability properties, introduced in [4], is not (yet) implemented. There is only one toy example provided in [4], another one in [2] and a more significant case study developed in [26].
We investigate in this paper the application of this approach to security proofs of RFID protocols, typically proofs of unlinkability. There are a lot of such protocols that appeared in the literature, most of which are very simple, due to the low computing capabilities of a RFID tag: the protocols often use only primitives such as hashing, xoring, pairing and splitting. These protocols have been studied, attacked, patched and automatically proved in the DY model (see for instance [17]). On the computational side, [28] investigates the computational definitions of unlinkability, together with examples of RFID protocols that satisfy (or not) the definitions. There are however very few proofs of security in the computational model and no (up to our knowledge) formal security proof. For instance, an RFID protocol is proposed in [20], together with a universally composable (claimed) proof. The proof is however quite informal, and attacks were found on this protocol (see [23]). Admittedly, such attacks can be easily circumvented, but this shows that a formal approach is useful, if not necessary. Similarly, as reported in [18], other RFID protocols that were claimed secure turned out to be broken.
A large fraction of RFID protocols, the so-called Ultralightweight RFID protocols (e.g. [12, 24]), aim at ensuring only weak security properties, and against passive attackers, because of the strong constraints on the number of gates embedded in the RFID tags. We do not consider such protocols in this paper.
Contributions
The contributions of this paper are:
To design axioms that reflect security assumptions on the primitives that are used in the RFID protocols (typically hash functions, pseudo-random generators and xor), and to prove their correctness. 2. 2.
To express formally the computational unlinkability. There are various definitions; we chose to formalize one of them (from [18]). Most other definitions can be expressed in a similar way. The security property is expressed as the indistinguishability of two sequences of terms. These terms are computed from the protocol specification extended with corruption capabilities. We use a specific technique inspired by the folding of transition systems described in [4]. 3. 3.
To illustrate the proof technique on two examples taken from [27]: kcl and lak. As far as we know, all published RFID protocols, that do not rely on encryption, are computationally insecure. This is also the case of these two protocols. We propose small modifications of the protocols, which prevent the known attacks. Some of the modified versions are secure in the DY model. Depending on the assumptions on the primitives, they may however be insecure in the computational model. For instance, if we assume the hash function to be pre-image resistant and one-way, the corrected version of lak, proved in [17], is not necessarily computationally secure: there might be attacks on both authentication and unlinkability. We actually need a family of keyed hash functions, which satisfies the pseudo-random functions (PRF) property. With the appropriate implementation assumptions, we formally prove the security of the two protocols. Up to our knowledge, these are the first formal security proofs of RFID protocols in the computational model.
Outline
In Section II, we briefly recall the methodology described in [4] and we propose some axioms for the hashing and exclusive or, that depend on the assumptions on the cryptographic libraries. In Section III we recall the definition of privacy of a RFID protocol given by Juels and Weis in [18], and we show how this property translates in the logic. In Section IV we recall the two protocols kcl and lak, known attacks on them and formally prove the security of fixed versions of the protocols. We also show that relaxing the assumptions yields some attacks. Finally, in Section V, we show (as expected) that abstracting pseudo-random numbers with random numbers is sound, provided that the seed is not used for any other purpose.
II The logic
Our goal is to formally study the protocols in the computational model. In order to do this we follow the directions described in [4]: we specify in a first-order logic what the attacker cannot do, which yields a set of axioms . We also compute from the protocol and the security property a formula expressing that there is an attack on the protocol. We know that if is unsatisfiable, then the protocol is secure in any model of . If, in addition, every axiom is computationally sound, then the protocol is computationally secure.
In this section we recall the first-order (indistinguishability) logic and provide a set of axioms , some of which are valid in any computational model while others require some security assumptions on the cryptographic primitives.
II-A Syntax of the logic
Terms
In the logic terms are built on a set of function symbols , a set of function symbols (used to represent the attacker’s computations), a set of names and a set of variables .
In the examples that are considered in this paper, contains at least the following function symbols:
[TABLE]
Each variable and term has a sort, which is either bool, short, or message. Every term of sort bool or short, has also the sort message. The typing rules for function symbols are defined as follows:
- •
- •
- •
- •
- •
Names have type short
- •
In the computational interpretation of the terms, we will only need to xor bitstrings of a fixed length: the length of the random numbers. We therefore restrict the type of to:
- •
has three types:
\begin{array}[]{l}\textsf{bool}\times\textsf{message}\times\textsf{message}\rightarrow\textsf{message}\\ \textsf{bool}\times\textsf{bool}\times\textsf{bool}\rightarrow\textsf{bool}\\ \textsf{bool}\times\textsf{short}\times\textsf{short}\rightarrow\textsf{short}\end{array}
- •
In our examples, hash values will have a length equal to the security parameter, so H returns a value of sort short. Furthermore, we need a keyed hash function, otherwise we cannot state any computationally sound property over the hash function H:
- •
We can also use arbitrary additional symbols in if needed. Each term has always a least sort (w.r.t. the ordering ), which we call the sort of the term.
Formulas
Atomic formulas aim at representing the indistinguishability of two experiment. They are expressions :
[TABLE]
where are terms and, for every , and have the same sort. More formally, for every , we are using a predicate symbol with arguments. Formulas then are obtained by combining atomic formulas with Boolean connectives and (first-order) quantifiers.
Syntactic shorthands
Displaying the formulas and axioms, we use the notation for a sequence of terms of the appropriate type. We also use “” as a syntactic sugar: is a shorthand for . We may also use logical connectives in the conditions, as a shorthand. For instance “” is a shorthand for “”.
II-B Semantics of the logic
We rely on classical first-order interpretations: function symbols are interpreted as functions on an underlying interpretation domain and predicate symbols are interpreted as relations on this domain.
Though, we assume that the interpretation satisfies the generic axioms of the Figure 1, which do not depend on the actual cryptographic libraries. These axioms are computationally valid, as we will see.
One particular class of interpretations of the logic are the so-called computational semantics. We recall here the main features (the complete definition can be found in [4]):
- •
The domain of a computational model is the set of deterministic polynomial time Turing machines equipped with an input (and working) tape and two random tapes (one for honestly generated random values, the other for random values directly available to the attacker). The length of the machine input is the security parameter .
- •
A name is interpreted as a machine that, on input of length , extracts a word of length from the first random tape . Furthermore, different names extract disjoint parts of .
- •
true, false, , , are always interpreted in the expected way. For instance, , takes three machines and returns a machine such that, on input , returns if and returns otherwise.
- •
Other function symbols in (including H and , ) are interpreted as arbitrary deterministic polynomial time Turing machines. Though, we may restrict the class of interpretations using assumptions on the implementations of the primitives. This is discussed in the next section.
- •
A function symbol with arguments is interpreted as a function , such that there is a polynomial time Turing machine such that for every machines in the interpretation domains, and for every inputs ,
[TABLE]
In particular, the machine does not use directly the random tape .
- •
The interpretation is lifted to terms: given an assignment of the variables of a term to the domain values, we write the computational interpretation of the term, with respect to . The assignment is omitted when empty. We may also omit the other parameters when they are irrelevant.
- •
The predicates are interpreted as computational indistinguishability , defined by:
[TABLE]
iff, for every deterministic polynomial time Turing machine ,
[TABLE]
is negligible when are drawn according to the uniform distribution.
II-C Computationally valid axioms
We only consider the purely universal fragment of first-order logic: every variable is implicitly universally quantified. A formula is computationally valid if it is valid in all computational interpretations.
Proposition 1**.**
The axioms displayed in the figure 1 are computationally valid.
Most of the axioms have already been proven valid elsewhere (for instance in [4, 2]). Only the axioms and are new, but their computational validity is quite straightforward to prove (e.g. for every , the distributions and are both uniform distributions). EasyCrypt is using a similar rule through the rnd tactic. A formal proof of these two axioms is given in Appendix A.
II-D Assumptions on primitives
Some of our axioms reflect implementation assumptions, that is, identities that must be satisfied by any implementation of these functions. For example we will assume that the projections of a pair return the components of the pair:
[TABLE]
We do not make any further assumption on the implementation of pairing.
Other axioms reflect cryptographic assumptions on the primitives. For example, for hash functions, we need to express some computational hardness properties. An example of such a property is the Collision Resistance property, that we recall below:
Definition 1** (CR-HK [16]).**
A hash function H is said to be collision resistant under hidden-key attacks if and only if for all probabilistic polynomial time adversary with access to an oracle returning the keyed hash value of the request,
[TABLE]
is negligible, where k is drawn uniformly at random in and is the random tape of the attacker.
This property can be expressed in the logic by the following axiom:
If the only occurrences of k in are as a second argument of H:
Remark 1*.*
Note that we need the conditional here: we cannot simply state that when and are distinct,
[TABLE]
For instance, take and where are distinct and is an attacker’s function. Then even though and are syntactically distinct, the function can be interpreted as a function that discards its argument and always return the same value. In such a case, the computational interpretations of and are identical.
Proposition 2**.**
The axiom is sound in any computational model where the hash function H is collision resistant under hidden-key attacks.
Proof:
Let be the following term:
[TABLE]
Let be a computational model such that H is interpreted by a collision-resistant keyed hash function, and assume that there exists an adversary such that:
[TABLE]
is not negligible in . Since is a boolean term, , hence the existence of is equivalent to
is non-negligible
We are going to define a probabilistic polynomial time adversary with access to an hash oracle with a non negligible chance of winning the CR-HK game.
Since the only occurrences of k in are as a second argument of H, we can define to be the CR-HK-adversary that computes and returns and (names different from k are computed by uniform sampling, and subterms of the form are computed by calling the hash oracle on the inductively computed ). Then we have:
[TABLE]
which we assumed to be non negligible in .
∎
Unfortunately, this property is not sufficient to prove the security of the RFID protocols considered in this paper (we will show attacks when only CR-HK is assumed). Therefore we need to consider a stronger property:
Definition 2** (PRF[14, 15]).**
A family of keyed hash functions: is a Pseudo Random Function family if, for any PPT adversary with access to an oracle :
[TABLE]
is negligible. Where
- •
is drawn uniformly in .
- •
is the random tape of the attacker (drawn uniformly).
- •
is drawn uniformly in the set of all functions from to .
We express this property in the logic using the following recursive schema of axioms:
where:
•
the occurrences of H (and k) in are
•
n is a name, that does not occur in
•
.
Proposition 3**.**
For any , is computationally sound if is a PRF family.
The proof can be found in Appendix B, and is a little more complicated than the previous one. Note that k cannot appear in itself, unless is a subterm of for some ; the statement of the axiom does not cover “key cycles” such as in the expression . Extending the axiom to cover such situations would require a Random Oracle assumption for the hash function.
III Security properties
Radio Frequency IDentification (RFID) systems allow to wirelessly identify objects. These systems are composed of readers and tags. Readers are radio-transmiters connected through a secure channel to a single server hosting a database with all the tracked objects information. Tags are wireless transponders attached to physical objects that have a limited memory and computational capacity (so as to reduce costs). For the sake of simplicity we will assume that there is only one reader, which will represent the database server as well as all the physical radio-transmitters.
Example 1*.*
In order to illustrate the properties, we introduce a very simple version of the protocol kcl. The original protocol from [19] is (informally) described in Figure 2. The key is a shared secret key between the tag and the reader . For simplicity we assume, for now, that names are randomly generated by each party (\overset{\}{\leftarrow}$ is used to denote random sampling); this will be justified in Section V. The protocol is expected to ensure both authentication and unlinkability.
III-A Privacy of RFID protocols
We use the notion of Privacy for RFID protocols defined in [18], that we informally recall here. This is a game-based definition, in which the adversary is a probabilistic polynomial time Turing machine and interacts with a reader and a finite set of tags (also probabilistic Turing machines) through fixed communication interfaces, which are informally described below and in Figure 3:
- •
A tag can store a secret key , an id , a session identifier and the previous challenge-response pairs of the current session. It has the following interface:
- –
SetKey: Corrupts the tag by returning its old key and id , and allows the adversary to send a new key and a new id of its choice.
- –
TagInit: Initialize a tag with a session identifier . The tag deletes the previous session identifier and the logged challenge-response pairs.
- –
TagMsg: The tag receives a challenge and returns a response (that was computed using the key, the session identifier and the logged challenge-response pairs). Additionally the tag logs the challenge-response pair .
- •
The reader stores some private key material (for example a master secret key, the tags private keys …) and entries of the form where is either or depending on whether the session is completed or on-going. It has the following interface:
- –
ReaderInit: Returns a fresh session identifier along with the first challenge . The reader also stores a new entry of the form .
- –
ReaderMsg: The reader receives a session identifier and a response . It looks for a data entry of the form , appends the message to the data entry, and either closes the session (by changing the status from to ) and outputs a new challenge message (possibly [math]) and appends it to the data entry.
The adversary is allowed to corrupt (by a SetKey command) up to tags. At the end of a first phase of computations and interactions with the reader and tags , the adversary chooses two uncorrupted tags and , which are removed from the set of available tags. Then one of these tags is chosen uniformly at random by sampling a bit and made accessible to the adversary as an oracle. The adversary performs a second phase of computations and interactions with the reader , the tags , as well as the randomly selected tag (obviously the adversary is not allowed to corrupt ). Finally the adversary outputs a bit , and wins if it guessed the chosen tag (that is if ). A protocol is said to verify -Privacy if any adversary using at most calls to the interfaces, has a probability of winning the game bounded by , where is a negligible function in the security parameter.
Remark 2*.*
Our definition of privacy is slightly different from the one in [18]:
- •
We do not assume that the reader answers “reject” or “accept” when a session is completed. We can easily encode this feature by adding an answer from the reader at the end of the protocol with the corresponding message. Not taking this as the default behavior allows to model adversaries that are less powerful and do not have access to the result of the protocol.
- •
We use -Privacy, whereas they use -Privacy where and are a bound on the number of calls to ReaderInit and TagInit respectively, and is a bound on the running time. We dropped the explicit mention of as we are only interested in proving privacy against any polynomial time adversary. Moreover using or is equivalent, as, for a given protocol, the number of calls to the interfaces is bounded by the number of calls to ReaderInit and to TagInit, and conversely.
III-B Bounded Session Privacy
Protocol Description
We let be the set of possible actions of an adversary interacting with tags:
[TABLE]
We are going to use a substitution to save the state of the reader and the tags internal memories. For instance, for each tag , we use two locations to store respectively the values of the key and of the id.
For every adversarial frame , for every action and for every internal memory state we can build from the protocol description a term , which represents the answer of the reader or tag to the action . We also build a internal memory update such that represents the updated memory of the reader and tags after the action has been performed. We also build from the protocol description the initial internal memory .
For the sake of simplicity, we assume that all names appearing in a term are fresh. If one wants to reuse a name (e.g. in the lak protocol the reader uses the same name in the first and second challenge), then we will store it in the internal memory .
Folding of the Protocol
Given a subset of actions of , we construct a term and a substitution representing (respectively) the message sent over the network and the memory update, depending on the action chosen by the attacker in (under memory and frame ). Intuitively, such terms gather together all possible interleavings of actions using the folding technique explained in [4].
Given an (arbitrary) enumeration of , and are defined using intermediate terms and (for all ), relying on an attacker function symbol (representing the scheduling choice of the attacker):
[TABLE]
where denotes the substitution defined by: for every variable , .
We then let and .
Example 2*.*
Let us return to the example 1.
Each tag has an identifier and a key . In the kcl protocol the call is useless because the tag has only one message to send in a round of the protocol ( is used to tell a tag to stop the current round of the protocol and to start a new one). Since we consider a finite number of interface calls, there is at most sessions executed in parallel. We will use a variable nb to store the index of the next session to start (initialized to ), and variables and (initialized to [math]) where and store respectively the first challenge and the second challenge of session .
- •
: the data of the tag are disclosed.
- •
: the key and id of the tag are set to values chosen by the attacker ().
- •
[TABLE]
The reply of the tag follows the protocol, according to its local store. is the message, forged by the adversary, replacing the expected name ; .
- •
: there is no update in this case (nothing is stored for further verifications in this particular protocol)
- •
: when starting a new session, the reader sends a new challenge
- •
[TABLE]
The local memory of the reader is updated.
We now express the Privacy game as a set of equivalence properties. After the first phase, once the attacker has chosen the corrupted tags, we rename the tags in such a way that the challenged tags are and . In the definition below, is the number of interactions of the adversary during the first phase and is the number of interactions of the adversary during the second phase.
Definition 3** (-Bounded Session Privacy).**
Given a (computational) interpretation of the function symbols in , a protocol satisfies -Bounded Session Privacy if for every such that and for every computational model that extends , we have:
[TABLE]
where , and for all :
- •
- •
and are defined similarly, except that the chosen tag is and not (that is the key substitution used is instead of in the case ). is the attacker’s function guessing with which tag the interaction took place.
Theorem 1**.**
Given a computational interpretation of function symbols in , a protocol satisfies -Bounded Session Privacy iff it satisfies -Privacy.
Proof:
If there is an attacker on -privacy, we can construct an interpretation of the attacker’s function symbols that yields a counter-model of the equivalence property. Conversely, if there is a counter-model we can build an attacker that performs the actions and computations specified by the interpretations of these function symbols. These constructions correspond basically to the proofs in [4]. ∎
III-C Fixed Trace Privacy
The -Bounded Session Privacy definition is a bit cumbersome, since the terms gather together all possible trace interleavings of the protocol with tags and calls to the interfaces. It is easier to use the following definition, that we call -Fixed Trace Privacy, that considers equivalence formulas between executions of the protocol with a fixed sequence of actions chosen by the adversary. Basically we split a big equivalence into an exponential number (in ) of smaller formulas.
Definition 4** (-Fixed Trace Privacy).**
Given an interpretation of function symbols in , a protocol satisfies -Fixed Trace Privacy if for all such that , for all , for all computational models that extend , we have:
[TABLE]
where , and for all :
- •
- •
- •
- •
Proposition 4**.**
-Fixed Trace Privacy is equivalent to -Bounded Session Privacy.
Proof:
We start by showing that -Bounded Session Privacy implies -Fixed Trace Privacy by contraposition: let be two integers such that , and be a computational model such that:
[TABLE]
Let be an adversary with a non negligible probability of distinguishing between the two distributions (interpreted in ). We define the model to be with a signature extended by the function symbols : for all , is interpreted by a machine returning on all input, and the function symbol is interpreted by a machine satisfying:
[TABLE]
This only depends on the size of and , and is therefore possible to do with a polynomial time probabilistic Turing Machine, hence is a computational model. Moreover by construction has a non negligible probability of breaking -Bounded Session Privacy in , which concludes the proof.
Conversely we show that -Fixed Trace Privacy implies -Bounded Session Privacy by contraposition: using notation of Definition 3, let be such that and assume a model and an adversary with a non negligible probability of distinguishing between and (we remove since can compute it himself). We let and for all , is the event . We then have:
[TABLE]
where denotes the -th frame obtained for the fixed trace (it is the from Definition 4 renamed to avoid notations clash). Similarly we let is the event and we have:
[TABLE]
Since , and bounding the absolute value of the sum by the sum of the absolute values we get that:
[TABLE]
is upper bounded by:
[TABLE]
Since distinguishes and with non negligible probability, and since is finite we know that there exists such that:
[TABLE]
is non negligible. Therefore -Fixed Trace Privacy does not hold, which concludes this proof.
∎
As explained in [4], indistinguishability properties can be expressed in the logic for arbitrary determinate protocols. For such protocols, observational equivalence and trace equivalence coincide [13]. The above proposition is a similar result in the computational model. It can be extended to other equivalence properties, as long as does not depend on the security parameter.
IV Two RFID protocols
We are now going to describe the lak and kcl RFID protocols, as well, attacks, patches and formal (computational) security proofs of the fixed versions.
We first consider that names are randomly generated numbers, even though, because of the limited computing capabilities of the tags, they have to be implemented using a Cryptographic Pseudo Random Number Generator (prng). This issue will be discussed in the section V: we will show that we can always safely abstract the pseudo random numbers as random numbers, provided that a prng is used and the random seed is never used for other purposes.
IV-A A known attack on kcl
Let us return to the simple example described in Figure 2:
[TABLE]
As reported in [27], there is a simple attack that we depict in Figure 4. In this attack the tag is challenged twice with the same name: observing the exchanges between the tag and the reader, the adversary can replay the name. Finally the adversary checks if he is talking with the same tag by xoring the two components of the message sent by the second tag, and verifies whether the result is the same as what he obtained with the same operation in the first session.
In the left execution, the xor of the two part of the tag answers will be the same:
[TABLE]
Whereas in the right execution we will obtain two values and which will be different with high probability.
IV-B kcl+*, a revised version of *kcl
We propose a simple correction to the kcl protocol: we replace the first occurrence of the name with its hash, breaking the algebraic property that was used in the attack. This protocol is depicted in Figure 5, and to our knowledge there exists no formal study of this revised version.
We are now going to illustrate our method by showing that the kcl+ protocol verifies -Fixed Trace Privacy with two tags A and B. Assuming collision resistance only, there is actually an attack on the protocol kcl+ (exactly the same attack as the one described in Section IV-D). We therefore assume the PRF property.
Theorem 2** (Unlinkability for an arbitrary number of rounds).**
Assuming PRF for the keyed hash function, the kcl+ protocol verifies -Fixed Trace Privacy for two agents and all .
In the proof below, the primed version of a term is the term , in which the names appearing in have been replaced by . We will use (where or B) to denote the response of the tag to a challenge:
[TABLE]
Since the axioms are Horn clauses, we can view them as inference rules, in which the premises of the inferences are the negative literals of the clause. This is easier to display and read.
Proof:
We prove this by induction on (induction is outside our logic). Let be two sequences of terms from the -Fixed Trace Privacy definition. By induction hypothesis, we assume that we have a derivation of (in the base case, this is the reflexivity of ). We consider two cases.
If the adversary decides to start a new session with the reader, we need to show that where is fresh in . This case is easy, we only need to apply the axiom:
Otherwise, the adversary decides to interact with the tags, e.g. A on the left and B on the right (the other cases are identical). We want to show that . We let n be a fresh name and be defined by:
[TABLE]
We start (from the root) our proof by applying the axiom (breaking the pair) and then to introduce an intermediate term since, intuitively, (resp. ) should be indistinguishable from a random number.
where is a derivation of .
Left Derivation
We have to find first a a derivation of . The ultimate goal is to apply the axioms. For that, we need to introduce, on both sides of the predicate, equality tests between the last message hashed under key (i.e. ), and all the previous hashed messages under key . We let be the set of messages hashed with in . We know that these messages are either names , or of the form where is a strict prefix of .
Let , . For all we let , and be the term:
[TABLE]
We observe that, for every term , is derivable from the equality axioms. We are now going to use the axiom to split the proof. To do so we introduce for every the term :
[TABLE]
And the term :
[TABLE]
By repeatedly applying the axiom we obtain:
First note that, using the axiom, we derive, for every , . This allows us to deal with cases to , since this implies that is derivable. Therefore we have for all :
Consider now the case . The conditions on the occurrences of H and are satisfied, thanks to the choice of . We may use the axiom:
Right Derivation ()
Now, we have to derive . We start by replacing A with B, splitting again the proof in two subgoals:
For the right part, we first decompose the goal:
Then, the derivation of is similar to the derivation of .
For the left part, we start by using the axiom on :
It only remains to show that . We do this using the and axioms:
[TABLE]
LSim
MSim
RSim
Which concludes the inductive step proof. ∎
In this result we consider only two tags, for simplicity reasons. In particular they cannot be corrupted tags. Our framework is expressive enough for multiple tags, including corrupted one, though we did not complete the proof in that case.
IV-C The lak protocol
Description
We describe in Figure 6 the original protocol from [21]. As we mentioned before, the protocol we consider is a simplified version of the lak protocol, without the key server. In the lak protocol, the reader shares a private key with each of its tags . h is an hash function. This is a stateful protocol: the key is updated after each successful completion of the protocol, and the reader keeps in the previous value of the key. This value is used as a backup in case has not completed the protocol (for example because the last message was lost) and therefore not updated its version of the key. The protocol allows to recover from such a desynchronization: the reader can use the previous version of at the next round (which is the version used by ) and finish the protocol.
The protocol is supposed to achieve mutual authentication and unlinkability. Even though such properties can be defined in various ways, we recall below a known attack against the lak protocol, which will force us to modify it.
An attack on lak
An attack on authentication is described in [27] and sketched below:
[TABLE]
In this attack, the adversary simply observes the beginning of an honest execution of the protocol (without completing the protocol, so that the reader and the tag do not update the key) between a tag and the reader. The adversary obtains and the names . He then interacts with the reader to get a new name and impersonates the tag by choosing the returned tag such that .
IV-D A stateless revised version of lak
In [17], the authors consider a corrected (and stateless) version of the protocol, which they proved secure. This version of the protocol is described below:
[TABLE]
This new version avoids the previous attack, which relied on the algebraic properties of exclusive-or. Formally, the protocol is described in the applied pi-calculus in [17], in which they prove the strong unlinkability property of [1] in the Dolev-Yao model for an unbounded number of session.
Attack against stateless lak
Since the stateless version of lak was proved in the symbolic model, no computational security assumptions were made on h. We show in Figure 7 that choosing h to be a one-way cryptographic hash function (OW-CPA and Strongly Collision Resistant for example) is not enough to guarantee unlinkability.
The attack is quite simple: it suffices that the hash function h leaks a few bits of the hashed message (which is possible for an one-way hash function). This means that, when hashing a message of the form , the hash function h will leak some bits of the agent key k. Since the keys are drawn uniformly at random, there is a non negligible probability for the leaked bits to be different when hashing messages with different keys. In particular an adversary will be be able to distinguish from with high probability.
Observe that this attack would still work if we modified the protocol to update the keys after a successful execution of the protocol (in other word, if we consider the original lak protocol with concatenation instead of xor), because the attacker could start executions of the protocol without finishing them, preventing the keys from being updated.
Remark 3*.*
In the original paper introducing lak [21], the hash function is described as a one-way cryptographic hash function, which a priori does not prevent the attack described above. However, in the security analysis section, the authors assume the function to be indistinguishable from a random oracle, which prevents the attack. It is actually sufficient to assume PRF, for which there are effective constructions (subject to hardness assumptions).
IV-E The lak+ protocol
We describe here a stateless version of the lak protocol, that we call lak+. As in the lak protocol, the reader shares with each tag a secret key k. We use a keyed-hash function that is assumed to be PRF to prevent the attack depicted in Section IV-D. This protocol uses a function that combines the names. It could be a priori a xor, as in the original protocol, or a pairing, as in the revised version of [17] or something else. We will look for sufficient conditions on this function , such that the protocol is secure.
[TABLE]
We start by describing two different attacks that rely on some properties of the function . In each case, we give a sufficient condition on that prevents the attack. Next, we show that these two conditions are sufficient to prove that the lak+ protocol verifies the Bounded Session Privacy property.
First Attack:
The attack depicted below is a generalization of the attack from [27]. It works when there exists a function (computable in probabilistic polynomial time) such that the quantity below is not negligible:
[TABLE]
This condition is satisfied if is the xor operation (choose ).
[TABLE]
The attacker starts by sending a name to the tag, and gets the name chosen by the tag as well as the hash . Then the attacker initiates a second round of the protocol with the reader. The reader sends first a name . The attacker is then able to answer, re-using the hash sent by the tag in the first round, choosing as a replacement of the name . Using Equation (1), there is a non negligible probability for the reader to accept the forged message as genuine.
This attack can be prevented by requiring to be injective on its first argument:
[TABLE]
Second Attack:
We have an unlinkability attack if we can distinguish between the answers of the tags, even though the hash function is assumed to be a PRF. This is possible if there exists a constant and a function such that:
[TABLE]
If this is the case, then the unlinkability attack described below has a non negligible probability of success in distinguishing two consecutive rounds with the same tag A from one round with the tag A and one round with the tag B.
The attack works as follows: it starts by impersonating the reader, sends to the tag and gets the response . Then the attacker initiates a new round of the protocol by sending to the second tag. Using Equation 2, there is a non negligible probability that the hash in the response from the tag A in the second round of the protocol is the same as in the first round, whereas this will not be the case if the second round is initiated with B.
This attack can be prevented by asking to be right injective on its second argument:
[TABLE]
Unlinkability of the lak+ protocol
To prevent all the attacks against lak+ described above, we are going to require to be right and left injective. This can easily be expressed in the logic using the two axioms in Figure 9, which are satisfied, for instance, when is a pairing.
Three messages are sent in a complete session of the lak+ protocol: two by the reader and one by the tag. Therefore, if we want to show interesting properties of the lak+ protocol, we need to consider at least 6 terms in the trace (two full sessions, e.g. twice with the same tag or with the tag and the tag ). This leads us to consider the -Fixed Trace Privacy of the lak+ protocol.
Theorem 3**.**
The lak+ protocol verifies -Fixed Trace Privacy. In particular, the following formula is derivable using the axioms from Section II and the axioms in Figure 9:
[TABLE]
Where:
[TABLE]
The proof of this theorem is given in Appendix C. As for the kcl+ protocol, by induction on , it should be possible to generalize the result to an arbitrary -Fixed Trace Privacy (if is independent of the security parameter), although we did not complete this generalization formally.
V Pseudo Random Number Generator
A prng uses an internal state, which is updated at each call, and outputs a pseudo random number. This can be modeled by a function taking the internal state as input, and outputing a pair with the new internal state and the generated pseudo random number (retrieved using the projections and ). Besides, a function is used to initialized the internal state with a random seed (which can be hard-coded in the tag).
Definition 5**.**
A prng is a tuple of polynomial functions such that for every PPT adversary and for every , the following quantity is negligible in :
[TABLE]
where and for all .
This can be translated in the logic by the axioms:
where and .
The soundness of these axioms is an immediate consequence of Definition 5:
Proposition 5**.**
The axioms are sound in any computational model where is interpreted as a prng.
For each protocol where a strict separation exists between the cryptographic material used for random number generation and the other primitives (e.g. encryption keys), pseudo random numbers generated using a prng can be abstracted as random numbers using the following proposition (the proof can be found in Appendix D):
Proposition 6**.**
For every names and contexts that do not contain these names, the following formula is derivable using the axioms in Figure 1 and :
[TABLE]
where and .
Remark 4* (Forward Secrecy).*
We did not study forward secrecy of RFID protocols, but this could easily be done. The standard forward secrecy assumption on a prng states that leaking the internal state of the prng (e.g. with a physical attack on the RFID chip) does not allow the adversary to gain any information about the previously generated names . This could be expressed in the logic using, for example, the following formula:
where and .
VI Conclusion
We gave a framework for formally proving the security of RFID protocols in the computational model: we expressed cryptographic assumptions on hash functions and an unlinkability property as formulas of the Complete Symbolic Attacker logic. We then illustrated this method on two examples, providing formal security proofs. We also showed that the security assumptions used in the proofs of these two protocols cannot be weakened (at least not in an obvious way).
What our framework is missing is an automatic tool for the logic, since the formal proofs are already heavy for simple protocols. Building such a tool would help streamline the design of formally verified protocols, and is the goal of our future research.
Compiling the process equivalence in our logic has already been explained in [4]. In principle, we could use any automatic first order theorem prover to complete the proofs. However, the search space may be too large on our examples. This is why the focus of our current research is on the design of appropriate strategies.
Appendix A Proof of Proposition 1
If terms and have no name in common then the distribution obtained when interpreting is the product of the distribution of and the distribution . This generalized to interpretations under substitution fixing all names common to and .
Proposition 7**.**
If then .
If there is a set of names such that the distributions obtained when interpreting and are the same for all valuation of the names in then distributions obtained when interpreting and are the same.
Proposition 8**.**
If and if for all such that we have then we have .
We use the two proposition above to prove the soundness of the and axioms:
- •
: Assume that for all computational model we have . Using the axiom we know that . Therefore for all computational adversary the following quantity is negligible:
[TABLE]
Let be an arbitrary substitution fixing all names except n. Then we have:
[TABLE]
Since this holds for all we have . Similarly . Therefore the following quantity is negligible:
[TABLE]
- •
: For all computational model :
[TABLE]
Since n does not appear in we have by independence:
[TABLE]
Appendix B Proof of Proposition 3
We give here and show a simpler version of the Proposition 3. The proof below can then easily be generalized.
Proposition 9**.**
*The following axiom:
where:
•
the only occurrence of H in is in a subterm
•
k does not occur in and only in key position in .
•
n is a name, that does not occur in
is computationally sound if is a PRF family.*
Proof:
Let be an attacker that distinguishes the two sequences of terms. We construct an attacker on the PRF property as follows:
draws all names appearing in , except k. Let be the resulting sampling. 2. 2.
computes (bottom-up) the distribution:
[TABLE]
calling the oracle each time there is an occurrence of . ( is the extension of with a sampling of k and attacker’s random tape ). This is possible, thanks to the occurrences assumptions on k. 3. 3.
simulates on the result.
Given a fixed we have:
[TABLE]
Hence,
[TABLE]
On the other hand, consider the term sequences, in which each occurrence is replaced with a function symbol : let be the result of such a replacement in . Let be an extension of with ,where is uniformly sampled from .
[TABLE]
Hence, letting ,
[TABLE]
Since is assumed not to contain any occurrence of and is drawn uniformly at random,
[TABLE]
Now, distinguishing cases,
[TABLE]
Now, since the only occurrences of in are in expressions , when we fix , and do not depend on , but only on : we write them and respectively. The above probability can then be written:
[TABLE]
Given and assuming and , the distribution of is uniform; in other words, if is the set of functions from to such that , for any , for any
[TABLE]
Therefore, given such that ,
[TABLE]
Using this in the expression of , we get:
[TABLE]
If, extending with a sampling of k, , then and . Since, now, only occurs in the conditional,
[TABLE]
Folding back, we get:
[TABLE]
And summing :
[TABLE]
This, together with Equation 3, shows that the advantage of is equal to the advantage of : we can break the PRF property. A contradiction. ∎
Remark 5*.*
In the proposition 9, the conditions on occurrences of k are necessary, unless we work in the random oracle model.
The proofs of the axioms are identical to the previous one, fixing (instead of ) the values of .
Appendix C Proof of Theorem 3
Unsurprisingly, it turns out that left and right injectivity of implies the injectivity of :
Proposition 10**.**
The following formula is derivable using the axioms from Section II and the axioms in Figure 9:
[TABLE]
The proof is straightforward rewriting using left and right injectivity and the if then else axioms.
We are now ready to give the proof of Theorem 3. Most of the formulas are easy to prove, so we are going to focus on the formula explicitly given in the theorem statement, which is in our opinion the hardest case.
Before starting, we define several new terms in Figure 10.
We have similar definition for the tilded versions . We start by applying the axiom several times:
We are now going to use the axiom on the conditional to split the proof. To do so we introduce the term:
[TABLE]
and the terms:
[TABLE]
Similarly we introduced the tilded versions of these terms. We observe that for all term we have and . Therefore we can apply the axiom, which gives us:
\forall i\in\{1,\dots,4\},\;\;\begin{array}[c]{l}\phi_{2},e_{4},e_{5},u_{i}^{\alpha},u_{i}^{\beta},u_{i}^{\gamma}\\ \qquad\sim\phi_{2},\tilde{e}_{4},\tilde{e}_{5},\tilde{u}_{i}^{\tilde{\alpha}},\tilde{u}_{i}^{\tilde{\beta}},\tilde{u}_{i}^{\tilde{\gamma}}\end{array}
We let and .
- •
Case : Let n be a fresh name, we start by the derivation displayed in Figure 11. Using we know that , and using the left injectivity of this shows that . Therefore we know that:
[TABLE]
[TABLE]
Hence we can apply the axiom, which shows that:
Similarly we show that:
It remains to show that . We do this exactly like we did to get rid of the and . First we use , and to get the derivation displayed in Figure 11.
The formulas and are dealt with exactly like we did for , introducing the corresponding conditional tests. We do not detail these two cases, but notice that the right injectivity of is needed for them.
We now need to show that , which is done by applying the axiom several time:
\begin{array}[]{l}\phi_{2},\textsf{n}_{R}^{\prime},\textsf{n}_{T}^{\prime},\textsf{H}(\mathsf{c}(g(\phi_{2}),\textsf{n}^{\prime}_{T}),\textsf{k}_{\textsf{A}})\\ \qquad\qquad\sim\phi_{2},\textsf{n}_{R}^{\prime},\textsf{n}_{T}^{\prime},\textsf{H}(\mathsf{c}(g(\phi_{2}),\textsf{n}^{\prime}_{T}),\textsf{k}_{\textsf{B}})\end{array}
Let , it is then easy to show that is derivable using the fact that is fresh in , the right injectivity of and the axiom.
- •
Case and : These case are very similar to the case , except that we need to use the axiom at some point to get rid of the double occurrence of (in case ) or (in case ).
- •
Case : Using Proposition 10 we know that
[TABLE]
Since booleans \epsilon_{4}^{\prime}\equiv\textsf{EQ}\big{(}\pi_{1}(g(\phi_{3}));\textsf{n}_{T}^{\prime}\big{)} and \epsilon_{5}\equiv\textsf{EQ}\big{(}\textsf{n}_{R}^{\prime};\pi_{1}(g(\phi_{3}))\big{)} we have:
[TABLE]
And therefore, for all term we have . Similarly we have This means that we have:
We already showed in the case that is derivable.
Appendix D Proof of Proposition 6
Let and be such that do not contain . Let and . We want to give a derivation of:
[TABLE]
using the axioms in Figure 1 and .
For all , we let the context and the names be such that and does not contain any name (only function applications and holes). Then using the axiom we have:
Now, we can use the axiom to get rid of multiple occurrences of the same name: indeed if there exists a name m such that and then we can keep only one occurrence of m. Let be such that for all and , then:
Now by assumptions we know that , therefore we can apply the axiom for all to get rid of . Finally we conclude with the axiom:
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] M. Arapinis, T. Chothia, E. Ritter, and M. Ryan. Analysing unlinkability and anonymity using the applied pi calculus. In Proceedings of IEEE Conf. Computer Security Foundations , 2010.
- 2[2] Gergei Bana and Rohit Chadha. Verification methods for the computationally complete symbolic attacker based on indistinguishability. IACR Cryptology e Print Archive , 2016:69, 2016.
- 3[3] Gergei Bana and Hubert Comon-Lundh. Towards unconditional soundness: Computationally complete symbolic attacker. In Pierpaolo Degano and Joshua D. Guttman, editors, Proceedings of the 1st International Conference on Principles of Security and Trust (POST’12) , volume 7215 of Lecture Notes in Computer Science , pages 189–208. Springer, March 2012.
- 4[4] Gergei Bana and Hubert Comon-Lundh. A computationally complete symbolic attacker for equivalence properties. In Proc. ACM Conference on Computers and Communications Security , 2014.
- 5[5] Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, and Santiago Zanella-Béguelin. Probabilistic relational verification for cryptographic implementations. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages , POPL ’14, pages 193–205, New York, NY, USA, 2014. ACM.
- 6[6] Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, and Santiago Zanella Béguelin. Computer-Aided Security Proofs for the Working Cryptographer , pages 71–90. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011.
- 7[7] K. Bhargavan, C. Fournet, M. Kohlweiss, A. Pironti, and P. Y. Strub. Implementing tls with verified cryptographic security. In 2013 IEEE Symposium on Security and Privacy , pages 445–459, May 2013.
- 8[8] Bruno Blanchet. Pro Verif : Cryptographic protocols verifier in the formal model . available at http://proseccco.gforge..inria.fr/personal/bblanchet/proverif/ .