124
G. Avoine et al.
cryptographic functions. Due to these abstractions, symbolic models are easier to
mechanize into automatic verifiers, yet generally an attack found in such models is
more a logical flaw than a cryptographic-design problem.
7.4.2.1 Symbolic Verification
The two symbolic models permit us to use semiautomatic tools, Tamarin [406] and
Proverif [93], respectively, to verify the security of distance-bounding protocols.
They slightly differ in their approach: [177] models time and distance explicitly,
while [401] abstracts this into some classification of the order of messages.
However, they find similar attacks. Moreover, both methodologies take a step
beyond the scope of previous computational models: they consider that the verifiers
can be corrupted. Also, outside formalizations, in distance bounding, verifiers were
traditionally considered honest (except when user privacy is considered).
However, as symbolic models, there are some attacks that they cannot find, due
to the abstractions they make. For instance, if a prover is within the distance bound,
it might be possible for a mafia-fraud adversary to flip challenge bits on the fly
without being detected, which allows him to recover the secret key of the provers
in some protocols [62]. This kind of attack can be found using the computational
models, but not the symbolic ones, which abstract bitstrings to terms.
7.4.2.2 Provable Security
Due to abstracting the cryptographic primitives into black-boxes, symbolic-verification mechanisms also cannot detect attacks by “PRF programming” [108].
Some protocols, such as Swiss-Knife or Hancke-Kuhn, use a PRF to compute the
response vectors. However, as noted in [108], the pseudorandomness of a PRF is
only guaranteed if the adversary does not know anything about the involved key and
if there is no oracle/reuse for/of the key anywhere else in the protocol. Yet dishonest
provers in distance-fraud attacks do know the key of the PRF. And, in distancebounding protocols such as the Swiss-Knife protocol [328], the key is re-used
outside of the PRF call in forming the responses. So, [108] exhibit “programmed
PRFs”: dishonest provers can use the PRF to mount distance fraud, and man-inthe-middle attackers can adaptively chose inputs to mount mafia fraud. In turn,
this means that in provably-secure distance bounding, care needs to be taken with
security claims resting just on pseudorandomness.
For both symbolic and computational models, modelling terrorist fraud is a
big challenge. The symbolic models for terrorist fraud are either too strong or
too weak, and the computational ones are often tailored definitions proposed
for specific protocols. For instance, SimTF [216] imposes restrictions on the
communications between the prover and his accomplice, and in [109], the prover
helps his accomplice several times instead of just once.
G. Avoine et al.
cryptographic functions. Due to these abstractions, symbolic models are easier to
mechanize into automatic verifiers, yet generally an attack found in such models is
more a logical flaw than a cryptographic-design problem.
7.4.2.1 Symbolic Verification
The two symbolic models permit us to use semiautomatic tools, Tamarin [406] and
Proverif [93], respectively, to verify the security of distance-bounding protocols.
They slightly differ in their approach: [177] models time and distance explicitly,
while [401] abstracts this into some classification of the order of messages.
However, they find similar attacks. Moreover, both methodologies take a step
beyond the scope of previous computational models: they consider that the verifiers
can be corrupted. Also, outside formalizations, in distance bounding, verifiers were
traditionally considered honest (except when user privacy is considered).
However, as symbolic models, there are some attacks that they cannot find, due
to the abstractions they make. For instance, if a prover is within the distance bound,
it might be possible for a mafia-fraud adversary to flip challenge bits on the fly
without being detected, which allows him to recover the secret key of the provers
in some protocols [62]. This kind of attack can be found using the computational
models, but not the symbolic ones, which abstract bitstrings to terms.
7.4.2.2 Provable Security
Due to abstracting the cryptographic primitives into black-boxes, symbolic-verification mechanisms also cannot detect attacks by “PRF programming” [108].
Some protocols, such as Swiss-Knife or Hancke-Kuhn, use a PRF to compute the
response vectors. However, as noted in [108], the pseudorandomness of a PRF is
only guaranteed if the adversary does not know anything about the involved key and
if there is no oracle/reuse for/of the key anywhere else in the protocol. Yet dishonest
provers in distance-fraud attacks do know the key of the PRF. And, in distancebounding protocols such as the Swiss-Knife protocol [328], the key is re-used
outside of the PRF call in forming the responses. So, [108] exhibit “programmed
PRFs”: dishonest provers can use the PRF to mount distance fraud, and man-inthe-middle attackers can adaptively chose inputs to mount mafia fraud. In turn,
this means that in provably-secure distance bounding, care needs to be taken with
security claims resting just on pseudorandomness.
For both symbolic and computational models, modelling terrorist fraud is a
big challenge. The symbolic models for terrorist fraud are either too strong or
too weak, and the computational ones are often tailored definitions proposed
for specific protocols. For instance, SimTF [216] imposes restrictions on the
communications between the prover and his accomplice, and in [109], the prover
helps his accomplice several times instead of just once.