Computational and symbolic analysis of distance-bounding protocols

Doctoral thesis (2019)

Contactless technologies are gaining more popularity everyday. Credit cards enabled with contactless payment, smart cards for transport ticketing, NFC-enabled mobile phones, and e-passports are just a few ... [more ▼]

Contactless technologies are gaining more popularity everyday. Credit cards enabled with contactless payment, smart cards for transport ticketing, NFC-enabled mobile phones, and e-passports are just a few examples of contactless devices we are familiar with nowadays. Most secure systems meant for these devices presume physical proximity between the device and the reader terminal, due to their short communication range. In theory, a credit card should not be charged of an on-site purchase if the card is not up to a few centimeters away from the payment terminal. In practice, this is not always true. Indeed, some contactless payment protocols, such as Visa's payWave, have been shown vulnerable to relay attacks. In a relay attack, a man-in-the-middle uses one or more relay devices in order to make two distant devices believe they are close. Relay attacks have been implemented also to bypass keyless entry and start systems in various modern cars. Relay attacks can be defended against with distance-bounding protocols, which are security protocols that measure the round-trip times of a series of challenge/response rounds in order to guarantee physical proximity. A large number of these protocols have been proposed and more sophisticated attacks against them have been discovered. Thus, frameworks for systematic security analysis of these protocols have become of high interest. As traditional security models, distance-bounding security models sit within the two classical approaches: the computational and the symbolic models. In this thesis we propose frameworks for security analysis of distance-bounding protocols, within the two aforementioned models. First, we develop an automata-based computational framework that allows us to generically analyze a large class of distance-bounding protocols. Not only does the proposed framework allow us to straightforwardly deliver computational (in)security proofs but it also permits us to study problems such as optimal trade-offs between security and space complexity. Indeed, we solve this problem for a prominent class of protocols, and propose a protocol solution that is optimally secure amongst space-constrained protocols within the considered class. Second, by building up on an existing symbolic framework, we develop a causality-based characterization of distance-bounding security. This constitutes the first symbolic property that guarantees physical proximity without modeling continuous time or physical location. We extend further our formalism in order to capture a non-standard attack known as terrorist fraud. By using our definitions and the verification tool Tamarin, we conduct a security survey of over 25 protocols, which include industrial protocols based on the ISO/IEC 14443 standard such as NXP's MIFARE Plus with proximity check and Mastercard's PayPass payment protocol. For the industrial protocols we find attacks, propose fixes and deliver security proofs of the repaired versions. [less ▲]

Distance-Bounding Protocols: Verification without Time and Location

in Proceedings of IEEE Symposium on Security and Privacy (SP), San Francisco 21-23 May 2018 (2018)

Distance-bounding protocols are cryptographic protocols that securely establish an upper bound on the physi- cal distance between the participants. Existing symbolic verification frameworks for distance ... [more ▼]

Distance-bounding protocols are cryptographic protocols that securely establish an upper bound on the physi- cal distance between the participants. Existing symbolic verification frameworks for distance-bounding protocols consider timestamps and the location of agents. In this work we introduce a causality-based characterization of secure distance-bounding that discards the notions of time and location. This allows us to verify the correct- ness of distance-bounding protocols with standard pro- tocol verification tools. That is to say, we provide the first fully automated verification framework for distance- bounding protocols. By using our framework, we con- firmed known vulnerabilities in a number of protocols and discovered unreported attacks against two recently published protocols. [less ▲]

Multiobjective variable mesh optimization

in Annals of Operations Research (2016)

In this article we introduce a new multiobjective optimizer based on a recently proposed metaheuristic algorithm named Variable Mesh Optimization (VMO). Our proposal (multiobjective VMO, MOVMO) combines ... [more ▼]

In this article we introduce a new multiobjective optimizer based on a recently proposed metaheuristic algorithm named Variable Mesh Optimization (VMO). Our proposal (multiobjective VMO, MOVMO) combines typical concepts from the multiobjective optimization arena such as Pareto dominance, density estimation and external archive storage. MOVMO also features a crossover operator between local and global optima as well as dynamic population replacement. We evaluated MOVMO using a suite of four wellknown benchmark function families, and against seven state-of-the-art optimizers: NSGA-II, SPEA2,MOCell, AbYSS,SMPSO,MOEA/DandMOEA/D.DRA. The statistically validated results across the additive epsilon, spread and hypervolume quality indicators confirm that MOVMO is indeed a competitive and effective method for multiobjective optimization of numerical spaces. [less ▲]

A class of precomputation-based distance-bounding protocols

Presentation (2016, March 16)

Distance-bounding protocols serve to thwart various types of proximity-based attacks, such as relay attacks. A particular class of distance-bounding protocols measures round trip times of a series of one ... [more ▼]

Distance-bounding protocols serve to thwart various types of proximity-based attacks, such as relay attacks. A particular class of distance-bounding protocols measures round trip times of a series of one-bit challenge-response cycles, during which the proving party must have minimal computational overhead. This can be achieved by precomputing the responses to the various possible challenges. We formalize this class of precomputation-based distance-bounding protocols. By designing an abstract model for these protocols, we can study their generic properties, such as security lower bounds in relation to space complexity. Further, we present a novel family of protocols in this class that resists well to mafia fraud attacks. [less ▲]

Detección de ruido y aprendizaje basado en información actual

in Computación y Sistemas (2014), 18(1), 153-167

Methods for noise cleaning have great significance in classification tasks and in situations when it is necessary to carry out a semi-supervised learning due to importance of having well-labeled samples ... [more ▼]

Methods for noise cleaning have great significance in classification tasks and in situations when it is necessary to carry out a semi-supervised learning due to importance of having well-labeled samples (prototypes) for classification of the new patterns. In this work, we present a new algorithm for detecting noise in data streams that takes into account changes in concepts over time (concept drift). The algorithm is based on the neighborhood criteria and its application uses the construction of a training set. In our experiments we used both synthetic and real databases, the latter were taken from UCI repository. The results support our proposal of noise detection in data streams and classification processes. [less ▲]