6 Ultra-lightweight Authentication
109
One of the initial goals of synchronized protocols 4 is to provide forward privacy.
Forward privacy is a stronger notion than just privacy. Simply put, a protocol is said
to be forward private if an attacker, having recovered the internal state (the dynamic
values of the identifier and keys) of a tag, is not able to recognize the tag in past
interaction traces. For a more formal definition, see [453]. Forward privacy cannot
be achieved in a protocol if the secrets used in the exchange are all static. Indeed,
if the attacker knows the secrets of a tag at some point, it also knows them in the
past, since the secret does not change in the tag’s lifetime. Therefore, messages sent
by a tag in previous interactions can be recomputed, and recognized easily. Note
that a changing secret is required for forward privacy, but it does not guarantee it
(indeed, there are many synchronized protocols that are not private, and therefore
not forward private).
A positive side effect of changing the secrets is that it might make it harder to
obtain the full secret at any given time, if only a partial leakage is obtained at every
authentication round. This seems to be a good feature as it is intuitively harder to
hit a moving target than a static one. However, this does not necessarily make the
full cryptanalysis impossible, just slightly harder, as has been demonstrated with the
Tango attacks [273, 468].
6.3.6 Dubious Proofs of Security: Randomness Tests
and Automated Provers
In many instances, some degree of security is allegedly claimed by verifying that
the exchanged messages look random enough. For that, multiple sessions of the
protocol are run and the exchanged messages are recorded and later analyzed using
various randomness test batteries such as the well-known ENT [568], Diehard [394]
and NIST [509]. Unfortunately this does not prove any security level (for instance,
LMAP presented such a “proof” but was broken shortly after publication). Randomness may appear, not as a consequence of a well designed protocol, but simply as
a result of employing nonces in message mixing. Randomness is not a sufficient
condition, neither is it a necessary one. A trivial way of showing this is by thinking
about highly formatted messages and how, even if a protocol is secure, due to
formatting and padding of some or all of its messages these may not pass some
randomness test.
Another popular but flawed way of proving security of proposed ultralightweight protocols is the use of logic modeling and formal protocol verification
software.
A notable example is [492]. The scheme was broken in [464], despite being
accompanied by a formal security proof in BAN logic. The authors mistakenly
4 In synchronized protocols the parties, after each execution of the protocol, apply the same
updating function to their secret keys and state information.
109
One of the initial goals of synchronized protocols 4 is to provide forward privacy.
Forward privacy is a stronger notion than just privacy. Simply put, a protocol is said
to be forward private if an attacker, having recovered the internal state (the dynamic
values of the identifier and keys) of a tag, is not able to recognize the tag in past
interaction traces. For a more formal definition, see [453]. Forward privacy cannot
be achieved in a protocol if the secrets used in the exchange are all static. Indeed,
if the attacker knows the secrets of a tag at some point, it also knows them in the
past, since the secret does not change in the tag’s lifetime. Therefore, messages sent
by a tag in previous interactions can be recomputed, and recognized easily. Note
that a changing secret is required for forward privacy, but it does not guarantee it
(indeed, there are many synchronized protocols that are not private, and therefore
not forward private).
A positive side effect of changing the secrets is that it might make it harder to
obtain the full secret at any given time, if only a partial leakage is obtained at every
authentication round. This seems to be a good feature as it is intuitively harder to
hit a moving target than a static one. However, this does not necessarily make the
full cryptanalysis impossible, just slightly harder, as has been demonstrated with the
Tango attacks [273, 468].
6.3.6 Dubious Proofs of Security: Randomness Tests
and Automated Provers
In many instances, some degree of security is allegedly claimed by verifying that
the exchanged messages look random enough. For that, multiple sessions of the
protocol are run and the exchanged messages are recorded and later analyzed using
various randomness test batteries such as the well-known ENT [568], Diehard [394]
and NIST [509]. Unfortunately this does not prove any security level (for instance,
LMAP presented such a “proof” but was broken shortly after publication). Randomness may appear, not as a consequence of a well designed protocol, but simply as
a result of employing nonces in message mixing. Randomness is not a sufficient
condition, neither is it a necessary one. A trivial way of showing this is by thinking
about highly formatted messages and how, even if a protocol is secure, due to
formatting and padding of some or all of its messages these may not pass some
randomness test.
Another popular but flawed way of proving security of proposed ultralightweight protocols is the use of logic modeling and formal protocol verification
software.
A notable example is [492]. The scheme was broken in [464], despite being
accompanied by a formal security proof in BAN logic. The authors mistakenly
4 In synchronized protocols the parties, after each execution of the protocol, apply the same
updating function to their secret keys and state information.