References of "Trujillo Rasua, Rolando 50003226"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailSecurity of Distance−Bounding: A Survey
Gildas, Avoine; Muhammed, Ali Bingöl; Ioana, Boureanu et al

in ACM Computing Surveys (in press)

Distance bounding protocols allow a verifier to both authenticate a prover and evaluate whether the latter is located in his vicinity. These protocols are of particular interest in contactless systems, e ... [more ▼]

Distance bounding protocols allow a verifier to both authenticate a prover and evaluate whether the latter is located in his vicinity. These protocols are of particular interest in contactless systems, e.g. electronic payment or access control systems, which are vulnerable to distance-based frauds. This survey analyzes and compares in a unified manner many existing distance bounding protocols with respect to several key security and complexity features. [less ▲]

Detailed reference viewed: 125 (4 UL)
Full Text
Peer Reviewed
See detailAttribute evaluation on attack trees with incomplete information
Buldas, Ahto; Gadyatskaya, Olga UL; Lenin, Aleksandr et al

in Computers and Security (2020), 88(101630),

Attack trees are considered a useful tool for security modelling because they support qualitative as well as quantitative analysis. The quantitative approach is based on values associated to each node in ... [more ▼]

Attack trees are considered a useful tool for security modelling because they support qualitative as well as quantitative analysis. The quantitative approach is based on values associated to each node in the tree, expressing, for instance, the minimal cost or probability of an attack. Current quantitative methods for attack trees allow the analyst to, based on an initial assignment of values to the leaf nodes, derive the values of the higher nodes in the tree. In practice, however, it shows to be very difficult to obtain reliable values for all leaf nodes. The main reasons are that data is only available for some of the nodes, that data is available for intermediate nodes rather than for the leaf nodes, or even that the available data is inconsistent. We address these problems by developing a generalisation of the standard bottom-up calculation method in three ways. First, we allow initial attributions of non-leaf nodes. Second, we admit additional relations between attack steps beyond those provided by the underlying attack tree semantics. Third, we support the calculation of an approximative solution in case of inconsistencies. We illustrate our method, which is based on constraint programming, by a comprehensive case study. [less ▲]

Detailed reference viewed: 42 (2 UL)
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: 83 (2 UL)
Full Text
Peer Reviewed
See detailRobust active attacks on social graphs
Mauw, Sjouke UL; Ramirez Cruz, Yunior UL; Trujillo Rasua, Rolando UL

in Data Mining and Knowledge Discovery (2019), 33(5), 1357-1392

Detailed reference viewed: 84 (6 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: 120 (8 UL)
Full Text
Peer Reviewed
See detailAnonymising social graphs in the presence of active attackers
Mauw, Sjouke UL; Ramirez Cruz, Yunior UL; Trujillo Rasua, Rolando UL

in Transactions on Data Privacy (2018), 11(2), 169-198

Detailed reference viewed: 52 (4 UL)
Full Text
Peer Reviewed
See detailNew Directions in Attack Tree Research: Catching up with Industrial Needs
Gadyatskaya, Olga UL; Trujillo Rasua, Rolando UL

in Mauw, Sjouke (Ed.) Proceedings of the 4th International Workshop on Graphical Models for Security (2018, January)

Attack trees provide a systematic way of characterizing diverse system threats. Their strengths arise from the combination of an intuitive representation of possible attacks and availability of formal ... [more ▼]

Attack trees provide a systematic way of characterizing diverse system threats. Their strengths arise from the combination of an intuitive representation of possible attacks and availability of formal mathematical frameworks for analyzing them in a qualitative or a quantitative manner. Indeed, the mathematical frameworks have become a large focus of attack tree research. However, practical applications of attack trees in industry largely remain a tedious and error-prone exercise. Recent research directions in attack trees, such as attack tree generation, attempt to close this gap and to improve the attack tree state-of-thepractice. In this position paper we outline the recurrent challenges in manual tree design within industry, and we overview the recent research results in attack trees that help the practitioners. For the challenges that have not yet been addressed by the community, we propose new promising research directions. [less ▲]

Detailed reference viewed: 221 (6 UL)
Full Text
Peer Reviewed
See detailConditional adjacency anonymity in social graphs under active attacks
Mauw, Sjouke UL; Ramirez Cruz, Yunior UL; Trujillo Rasua, Rolando UL

in Knowledge and Information Systems (2018)

Detailed reference viewed: 128 (28 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: 143 (12 UL)
Full Text
Peer Reviewed
See detailRefinement-Aware Generation of Attack Trees
Gadyatskaya, Olga UL; Ravi, Jhawar; Mauw, Sjouke UL et al

in Livraga, Giovanni; Mitchell, Chris J. (Eds.) Security and Trust Management - 13th International Workshop (2017, September)

Detailed reference viewed: 154 (4 UL)
Full Text
Peer Reviewed
See detailSimilarities and Differences Between the Vertex Cover Number and the Weakly Connected Domination Number of a Graph
Lemanska, Magdalena; Rodríguez-Velázquez, Alberto; Trujillo Rasua, Rolando UL

in Fundamenta Informaticae (2017), 152(3), 273-287

Detailed reference viewed: 110 (18 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: 66 (5 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: 139 (13 UL)
Full Text
Peer Reviewed
See detailAttack trees for practical security assessment: ranking of attack scenarios with ADTool 2.0
Gadyatskaya, Olga UL; Jhawar, Ravi UL; Kordy, Piotr UL et al

in Quantitative Evaluation of Systems - 13th International Conference (2016)

Detailed reference viewed: 168 (8 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: 115 (9 UL)
Full Text
Peer Reviewed
See detailCounteracting active attacks in social network graphs
Mauw, Sjouke UL; Trujillo Rasua, Rolando UL; Xuan, Bochuan

in Proceedings of Data and Applications Security and Privacy - 30th Annual IFIP WG 11.3 Conference (DBSec 2016) (2016)

Detailed reference viewed: 90 (1 UL)
Full Text
Peer Reviewed
See detailCharacterizing 1-metric antidimensional trees and unicyclic graphs
Trujillo Rasua, Rolando UL; Yero, Ismael G.

in Computer Journal (2016), 59(8), 1264--1273

Detailed reference viewed: 83 (4 UL)
Full Text
Peer Reviewed
See detailUsing attack-defense trees to analyze threats and countermeasures in an ATM: a case study
Fraile, Marlon; Ford, Margaret; Gadyatskaya, Olga UL et al

in IFIP Working Conference on The Practice of Enterprise Modeling (2016)

Detailed reference viewed: 154 (1 UL)
Full Text
Peer Reviewed
See detailk-Metric antidimension: A privacy measure for social graphs
Trujillo Rasua, Rolando UL; Yero, Ismael G.

in Information Sciences (2016), 328

Detailed reference viewed: 59 (0 UL)
Full Text
Peer Reviewed
See detailThe Fréchet/Manhattan distance and the trajectory anonymisation problem
Ferreira Torres, Christof UL; Trujillo Rasua, Rolando UL

in Proceedings of Data and Applications Security and Privacy - 30th Annual IFIP WG 11.3 Conference (DBSec 2016) (2016)

Detailed reference viewed: 111 (10 UL)