Previously:
The YubiKey is a simple physical authentication device with a unique button. This device, manufactured by Yubico, allows users to securely authenticate to their accounts by issuing a one-time password (OTP).
In its typical configuration, the YubiKey generates a random OTP by encrypting a secret value and a counter. This message is accepted by the server only if it decrypts under the correct key to a valid secret value containing a counter whose value is larger than the last value accepted by the server for that YubiKey.
In this model, we analyze the security of the protocol as described in [1], assuming that the server remains secure.
Yubico assigns a key k, as well as a public and a secret identifier pid, sid to each YubiKey. The counter cpt inside the YubiKey is incremented whenever the YubiKey is plugged in, as well as when an OTP is generated, i.e. when the button of the YubiKey is pressed. This OTP is obtained by encrypting the counter value and the sid of the YubiKey with the key k.
Here, npr is the encryption randomness. The server accepts this message if it decrypts with a legitimate key k, and leads to a valid secret value sid. Lastly, the counter value obtained through decryption has to be larger than the current value stored in the server database. After this exchange, the server updates its counter with the value just received.
The OTP is an encryption of a triple <sid, cpt, npr>. It is modelled here as a randomized encryption of a pair <sid, cpt>. According to the specification in [1], AES is used.
In [1], they “over-approximate in the case that the Yubikey increases the session token by allowing the adversary to instantiate the rule for any counter value that is higher than the previous one”. Here, we model the incrementation by 1 of the counter.
The 3 security properties as stated in [1].
[1] R. Künnemann, "Foundations for analyzing security APIs in the symbolic and computational model’, 2014.
abstract startplug : messagePublic constants (abstract) and names used in the protocol.
Symmetric encryption scheme, using the secret key k (with index arity 1 so that each YubiKey is associated to a key) and the random npr (with index arity 2 so that each session of a YubiKey uses a new random name).
Public constants and public functions used to model counter values.
mutable YCpt(i:index): message = myzeroMutable cells for the YubiKey and the server, initialized with myzero.
Communication channels used in the protocol.
process yubikeyplug(i:index,j:index) =When the key is plugged, its counter is incremented.
process yubikeypress(i:index,j:index) =When the key is pressed, an OTP is sent with the current value of the counter and the counter is incremented.
process server(ii:index) =When the server receives a message, it checks whether it corresponds to a pid in its database, and checks also that the counter inside the OTP is strictly greater than the counter associated to the token. If so, the value inside the OTP is used to update the database. Now, the counter value associated to this token is this new value.
systemIn the final system, processes can play in parallel an unbounded number of sessions.
include Basic. Goal eq_sym :We include here some libraries, useful to help the tool with automated reasoning.
The following axioms are used to reason on counter values.
We now prove some properties on the counter on the server side, used later in the proofs of the security properties.
The counter SCpt(i) strictly increases at each action S performed by the server with tag i.
The proof is automatically done by Squirrel.
auto. [> Line 180: autoThe counter SCpt(i) increases (not strictly) between pred(t) and t.
After having introduced the hypotheses, we perform a case analysis on all possible values that the timestamp t can take. Most cases are trivial and automatically handled by Squirrel (=> //) because most actions do not update SCpt(i) so we automatically have that SCpt(i)@t = SCpt(i)@pred(t).
Case where t = S(ii,i0): This is the interesting case, where t is an action that updates the mutable cell SCpt(i0). We distinguish two cases: i = i0 and i <> i0.
The case i = i0 corresponds to the left disjunct, which is a direct consequence of the condition of the action SCpt(i). This is done automatically by Squirrel.
The case i <> i0 corresponds to the right disjunct. When expanding the macro SCpt(i)@t, we notice that it is an if _ then _ else _ term with a condition that is always false. This can be simplified using the rewrite tactic with lemma if_false (which is included in the Basic library.
The two previous tactics can be merged into a single one: by rewrite /SCpt if_false.
goal counterIncreaseBis:The counter SCpt(i) increases (not strictly) between t' and t when t' < t.
This proof is done by induction, relying on the previous counterIncrease lemma to prove the induction step.
We introduce a case disjunction t'. Since we already have that t' < t then the constraints tactic allows to close the goal showing that (t' = pred(t) || t' < pred(t)) is indeed satisfied.
Case t’ = pred(t). We first rewrite the conclusion using the equality in H0. The ! mark is here to indicate that the rewriting must be done as much as possible and at least once. Then, it is a direct consequence of the counterIncrease lemma.
Case t’ < pred(t). We first apply the induction hypothesis with t' < pred(t) to obtain a relation between SCpt(i)@t' and SCpt(i)@pred(t). We then use the counterIncrease lemma, this time to obtain a relation between SCpt(i)@pred(t) and SCpt(i)@t. We will then be able to conclude by transitivity.
It remains to show that the premises of the induction hypothesis IH0 were satisfied, relying on the fact that exec@t => exec@pred(t).
We now state and prove the 3 following security properties:
This property states that the server never accepts for the same YubiKey the same counter twice, i.e. if the trace is executable up until S(ii1,i), then there cannot exist a previous action S(ii,i) in the trace such that ii <> ii1 and SCpt(i)@S(ii,i) = SCpt(i)@S(ii1,i).
Note that proving this property does not rely on any assumption on cryptographic primitives: it relies only on reasonings about counter values.
We start by proving an invariant (noreplayInv) that will be useful in the main proof. This intermediate lemma states that whenever the server accepts for a given YubiKey (represented by the index i), the counter value must have increased compared to the last time the server accepted for this YubiKey.
The proof relies on the previous helping lemmas reasoning on counter values.
The case where S(ii,i) = S(ii1,i) is trivial and automatically handled by Squirrel. For the case where S(ii,i) < S(ii1,i), we use the invariant to show that there is a contradiction with the hypothesis Meq.
This property states that a successful login for the YubiKey pid(i) (i.e. the execution of action S(ii,i)) must have been preceded by a button press on this YubiKey for the same counter value (P(i,j) with cpt(i,j)@Press(i,j) = SCpt(i)@S(ii,i)), and this counter value is not involved in another successful login.
Proving this property requires to reason on counter values, but also requires the use of the INT-CTXT cryptographic assumption.
Proof. [> Line 365: ((executable S(ii,i));(intro //))The high-level idea of this proof is to use the INT-CTXT assumption: if the message received by the server is a valid ciphertext, then it must be equal to an encryption that took place before.
Since the action Press(i,j) is the only one that outputs an encryption, we thus have the existence of such an action before in the trace. Then, the unicity is proved using lemmas on counter values.
We apply the INT-CTXT assumption, which directly gives the existence of an action Press(i,j) that happens before S(ii,i).
The two first conjucts of the conclusion are automatically proved by Squirrel (the equality of counter values is a consequence of M1 once we have expanded the macros cpt and SCpt.
It now remains to show that the counter value cpt(i,j)@Press(i,j) is not involved in another successful login. We first show if this second successful login S(ii',i) had happened, then we must have SCpt(i)@S(ii,i) = SCpt(i)@S(ii',i).
The proof now relies only on lemmas about counter values to show that we cannot have SCpt(i)@S(ii,i) = SCpt(i)@S(ii',i) and S(ii,i) <> S(ii',i). We therefore a case disjunction (the first case corresponds to what we want to prove, and we will show that the 2 other cases are impossible).
This property states that the counter values associated to successful logins are monotonically increasing in time.
Note that proving this property does not rely on any assumption on cryptographic primitives: it relies only on reasonings about counter values.
We introduce a case disjunction, and we will show that the cases S(ii,i) = S(ii1,i) and S(ii,i) > S(ii1,i) are not possible, relying on previous lemmas and axioms on counter values.