7 From Relay Attacks to Distance-Bounding Protocols
123
7.4.1.2 Distance Fraud (DF) [113]
In distance fraud, a malicious prover located far away from the verifier attempts to
convince the verifier that he is close. The fraud succeeds if the authentication of the
faraway malicious prover is accepted.
7.4.1.3 Distance Hijacking (DH) [160]
Distance hijacking is a distance fraud in which honest provers are present near
the verifier. This gives the malicious prover more surface of attack, so that some
protocols are resistant to distance fraud, while being vulnerable to distance hijacking. For instance, in the Brands-Chaum protocol (Sect. 7.3.3), which is resistant to
distance fraud, a faraway prover can eavesdrop on a session played by an honest
prover P (located close to the verifier), send the final message before P does, and
be authenticated in place of P . Distance hijacking succeeds if the verifier accepts
the authentication of the faraway malicious prover.
7.4.1.4 Terrorist Fraud (TF) [178]
Terrorist fraud is an attack in which a malicious prover, located far away from the
verifier, is helped by an accomplice located near the verifier. A trivial attack in this
scenario would be that the prover simply gives all his secret keys to his accomplice.
Since this attack cannot be prevented if the prover has access to his secret key, we
make the additional assumption that the prover does not want the accomplice to
impersonate him later. Hence, a terrorist fraud succeeds if the verifier accepts the
authentication of the faraway prover through his accomplice, and the accomplice
cannot authenticate on his own in a later execution of the protocol.
7.4.2 Provable Security and Formal Verification
Provable security is the field of research which aims at building formal, mathematical proofs of the security of systems or protocols. Early distance-bounding
protocols were analyzed in an ad hoc fashion, so a call for provable security
of distance bounding was needed. A preliminary framework [41] for modelling
distance bounding paved the way to formal treatment of distance-bounding security.
In terms of formal security for distance bounding, we have: computational
formalisms [110, 193], and symbolic ones [177, 401]. Computational models treat
the messages as bitstrings and attackers as probabilistic polynomial-time algorithms
trying to defeat cryptographic goals. Symbolic security verification represents
messages as terms in a term algebra, abstracts the cryptographic primitives to black
box functions and models attackers as rules manipulating the terms and black-box
123
7.4.1.2 Distance Fraud (DF) [113]
In distance fraud, a malicious prover located far away from the verifier attempts to
convince the verifier that he is close. The fraud succeeds if the authentication of the
faraway malicious prover is accepted.
7.4.1.3 Distance Hijacking (DH) [160]
Distance hijacking is a distance fraud in which honest provers are present near
the verifier. This gives the malicious prover more surface of attack, so that some
protocols are resistant to distance fraud, while being vulnerable to distance hijacking. For instance, in the Brands-Chaum protocol (Sect. 7.3.3), which is resistant to
distance fraud, a faraway prover can eavesdrop on a session played by an honest
prover P (located close to the verifier), send the final message before P does, and
be authenticated in place of P . Distance hijacking succeeds if the verifier accepts
the authentication of the faraway malicious prover.
7.4.1.4 Terrorist Fraud (TF) [178]
Terrorist fraud is an attack in which a malicious prover, located far away from the
verifier, is helped by an accomplice located near the verifier. A trivial attack in this
scenario would be that the prover simply gives all his secret keys to his accomplice.
Since this attack cannot be prevented if the prover has access to his secret key, we
make the additional assumption that the prover does not want the accomplice to
impersonate him later. Hence, a terrorist fraud succeeds if the verifier accepts the
authentication of the faraway prover through his accomplice, and the accomplice
cannot authenticate on his own in a later execution of the protocol.
7.4.2 Provable Security and Formal Verification
Provable security is the field of research which aims at building formal, mathematical proofs of the security of systems or protocols. Early distance-bounding
protocols were analyzed in an ad hoc fashion, so a call for provable security
of distance bounding was needed. A preliminary framework [41] for modelling
distance bounding paved the way to formal treatment of distance-bounding security.
In terms of formal security for distance bounding, we have: computational
formalisms [110, 193], and symbolic ones [177, 401]. Computational models treat
the messages as bitstrings and attackers as probabilistic polynomial-time algorithms
trying to defeat cryptographic goals. Symbolic security verification represents
messages as terms in a term algebra, abstracts the cryptographic primitives to black
box functions and models attackers as rules manipulating the terms and black-box