References of "Toro Pozo, Jorge Luis 50008972"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailPost-collusion security and distance bounding
Mauw, Sjouke UL; Smith, Zachary Daniel UL; Trujillo Rasua, Rolando UL et al

in Post-collusion security and distance bounding (2019, November 11)

Verification of cryptographic protocols is traditionally built upon the assumption that participants have not revealed their long-term keys. However, in some cases, participants might collude to defeat ... [more ▼]

Verification of cryptographic protocols is traditionally built upon the assumption that participants have not revealed their long-term keys. However, in some cases, participants might collude to defeat some security goals, without revealing their long-term secrets. We develop a model based on multiset rewriting to reason about collusion in security protocols. We introduce the notion of postcollusion security, which verifies security properties claimed in sessions initiated after collusion occurred. We use post-collusion security to analyse terrorist fraud on protocols for securing physical proximity, known as distance-bounding protocols. In a terrorist fraud attack, agents collude to falsely prove proximity, whilst no further false proximity proof can be issued without further collusion. Our definitions and the Tamarin prover are used to develop a modular framework for verification of distance-bounding protocols that accounts for all types of attack from literature. We perform a survey of over 25 protocols, which include industrial protocols such as Mastercard’s contactless payment PayPass and NXP’s MIFARE Plus with proximity check. For the industrial protocols we confirm attacks, propose fixes, and deliver computer-verifiable security proofs of the repaired versions [less ▲]

Detailed reference viewed: 29 (1 UL)
Full Text
See detailComputational and symbolic analysis of distance-bounding protocols
Toro Pozo, Jorge Luis UL

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 ▲]

Detailed reference viewed: 165 (14 UL)
Full Text
Peer Reviewed
See detailAutomated Identification of Desynchronisation Attacks on Shared Secrets
Mauw, Sjouke UL; Smith, Zachary Daniel UL; Toro Pozo, Jorge Luis UL et al

in Automated Identification of Desynchronisation Attacks on Shared Secrets (2018, September)

Key-updating protocols are a class of communication protocol that aim to increase security by having the participants change encryption keys between protocol executions. However, such protocols can be ... [more ▼]

Key-updating protocols are a class of communication protocol that aim to increase security by having the participants change encryption keys between protocol executions. However, such protocols can be vulnerable to desynchronisation attacks, a denial of service attack in which the agents are tricked into updating their keys improperly, so that they are no longer able to communicate. In this work we introduce a method that can be used to automatically verify (or falsify) resistance to desynchronisation attacks for a range of protocols. This approach is then used to identify previously unreported vulnerabilities in two published RFID grouping protocols. [less ▲]

Detailed reference viewed: 114 (8 UL)
Full Text
Peer Reviewed
See detailDistance-Bounding Protocols: Verification without Time and Location
Mauw, Sjouke UL; Smith, Zachary Daniel UL; Toro Pozo, Jorge Luis UL et al

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 ▲]

Detailed reference viewed: 136 (12 UL)
Full Text
Peer Reviewed
See detailOptimality Results on the Security of Lookup-Based Protocols
Mauw, Sjouke UL; Toro Pozo, Jorge Luis UL; Trujillo Rasua, Rolando UL

in Hancke, Gerard P.; Markantonakis, Konstantinos (Eds.) Radio Frequency Identification and IoT Security - 12th International Workshop, RFIDSec 2016, Hong Kong, China, November 30 - December 2, 2016, Revised Selected Papers (2016, December)

Distance-bounding protocols use the round-trip time of a challenge-response cycle to provide an upper-bound on the distance between prover and verifier. In order to obtain an accurate upper-bound, the ... [more ▼]

Distance-bounding protocols use the round-trip time of a challenge-response cycle to provide an upper-bound on the distance between prover and verifier. In order to obtain an accurate upper-bound, the computation time at the prover’s side should be as short as possible, which can be achieved by precomputing the responses and storing them in a lookup table. However, such lookup-based distance bounding protocols suffer from a trade-off between the achieved security level and the size of the lookup table. In this paper, we study this security-memory trade-off problem for a large class of lookup-based distance bounding protocols; called layered protocols. Relying on an automata-based security model, we provide mathematical definitions for different design decisions used in previous lookup-based protocols, and perform general security analyses for each of them. We also formalize an interpretation of optimal trade-off and find a non-trivial protocol transformation approach towards optimality. That is to say, our transformation applied to any layered protocol results in either an improved or an equal protocol with respect to the optimality criterion. This transformation allows us to provide a subclass of lookup-based protocol that cannot be improved further, which means that it contains an optimal layered protocol. [less ▲]

Detailed reference viewed: 63 (5 UL)
Full Text
Peer Reviewed
See detailMultiobjective variable mesh optimization
Salgueiro, Yamisleydi; Toro Pozo, Jorge Luis UL; Bello, Rafael et al

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 ▲]

Detailed reference viewed: 117 (1 UL)
Full Text
Peer Reviewed
See detailLimpieza de ruido para clasificación basado en vecindad y cambios de concepto en el tiempo
Toro Pozo, Jorge Luis UL; Pascual González, Damaris; Vázquez Mesa, Fernando

in Revista Cubana de Ciencias Informaticas (2016), 10(2), 1-13

An important field within data mining and pattern recognition is classification. Classification is necessary in a number nowadays-world processes. Several works and methods have been proposed with the ... [more ▼]

An important field within data mining and pattern recognition is classification. Classification is necessary in a number nowadays-world processes. Several works and methods have been proposed with the goal to achieve classifiers to be more effective each time. However, most of them consider the training sets to be perfectly clustered, without having into account that incorrectly classified data might be in them. The process of removing incorrectly classified objects is called noise cleaning. Obviously, noise cleaning influences considerably in classification of new samples. In this work, we present a neighborhood-based algorithm for noise cleaning on data stream for classification. In addition, it considers the data distribution changes that may occur on the time. It was measured, by several experiments, the effect of the method on automatic building of training sets by using databases from UCI repository and two synthetic ones. The obtained results show prove the efficacy of the proposed noise cleaning strategy and its influence on the right classification of new samples. [less ▲]

Detailed reference viewed: 45 (6 UL)
Full Text
See detailA class of precomputation-based distance-bounding protocols
Mauw, Sjouke UL; Toro Pozo, Jorge Luis UL; Trujillo Rasua, Rolando UL

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 ▲]

Detailed reference viewed: 133 (13 UL)
Full Text
Peer Reviewed
See detailA Class of Precomputation-based Distance-bounding Protocols
Mauw, Sjouke UL; Toro Pozo, Jorge Luis UL; Trujillo Rasua, Rolando UL

in Proceedings of the 1st IEEE European Symposium on Security and Privacy (2016)

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. In this paper we study 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 develop a novel family of protocols in this class that resists well to mafia fraud attacks. [less ▲]

Detailed reference viewed: 111 (8 UL)
Full Text
Peer Reviewed
See detailDetección de ruido y aprendizaje basado en información actual
Pascual-González, Damaris; Vázquez-Mesa, Fernando; Toro Pozo, Jorge Luis UL

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 ▲]

Detailed reference viewed: 35 (2 UL)