Relay attacks (and, more generally, man-in-the-middle attacks) are a serious threat against many access control and payment schemes. In this work, we present distance-bounding protocols, how these can deter relay attacks, and the security models formalizing these protocols. We show several pitfalls making existing protocols insecure (or at least, vulnerable, in some cases). Then, we introduce the SKI protocol which enjoys resistance to all popular attack-models and features provable security. As far as we know, this is the first protocol with such all-encompassing security guarantees.