Analysis of security protocols with security properties based on distance
GIL PONS, Reynaldo · Open Repository and Bibliography (University of Luxembourg) · 2024
Security protocols are commonplace in current digital communications.Achieving secure, private and efficient communications has sparked the expansion of many fields in Computer Science at the intersection between cryptography, formal methods and the theory of computation.History has shown the first steps to achieve security are to model the problem, state its desired properties, and prove them correct with mathematical rigour.Several methods have been demonstrated useful for such tasks, from pen and paper proofs in the standard model, to semi-automated proofs in the symbolic model.Recently, protocols that depend on proximity have gained much popularity and importance.They are used in contactless technologies such as contactless payment, Near Field Communication (NFC) on smartphones and e-passports.These protocols assume the agents participating in the protocol are physically close during the execution.When this condition is not enforced, they become vulnerable to the so-called relay attacks.This type of attack occurs when an attacker relays the communication between agents, thus making them believe that they are communicating directly.In some cases this is a vulnerability, as direct communication indicates acceptance to execute a transaction.Distance-bounding protocols are an important class of protocols which aim to guarantee that the agents executing the protocol are physically close.These have been thoroughly studied in the last decade.Nevertheless, there are several protocols which are not in this class, but still use proximity notions in order to achieve security.One example is peer-to-peer key-exchange protocols where authentication is achieved solely through physical proximity.The first objective of this thesis is to study these protocols.First, we develop a symbolic framework to generically analyse protocols that consider attackers far away from the agents executing the protocol.We call this condition the distant-attacker assumption.These protocols usually utilize time measurements to guarantee that the partner of communication is nearby, similar to what is done in distance bounding.The key difference though, is that the security property sought is different, as their aim is to achieve other properties such as secrecy, authentication or memory-erasure.Using the proposed framework we show how these properties can be proved semi-automatically using standard tools.Finally, we evaluate the security of several protocols in the literature that had not been formally verified yet.Second, we study software-based memory-erasure protocols.These protocols are useful to guarantee small devices are in a safe state (for example free of malware) without having to physically access the device.In these protocols the prover aims to convince the verifier that it has erased its memory.In the literature, software-based erasure protocols have typically assumed that the prover is isolated during the execution.We show how this restriction can be lifted using distancebounding techniques.To this end, we propose new protocols and prove them secure within a computational model assuming an attacker that is distant rather than absent.Finally, we solve an open problem related to the probability of success of attackers against lookup-based distance-bounding protocols.We propose a new protocol and prove it optimal with respect to mafia-fraud and distance-fraud attacks using probabilistic analysis in a computational model.iii Personal achievements are seldom obtained in solitude.Most human beings, no matter their origin or culture, depend on others for the most part of their life.These words are my sincere attempt to say thank you to everyone who deserves it.I would like to thank Sjouke for his accurate advice and guidance in the last four years, specially for sharing insights about the human side of research and work.It has been a great pleasure to be his teaching assistance in TCS I. Thanks Rolando for the uncountable hours spent making this thesis move forward from the start to the end.Specially for having the patience to work with me continuously for such a long period of time.I want to deeply express my gratitude to the rest of the defence committee: Prof. Dr. Peter Ryan, Dr. Sasa Radomirovic, and Dr. Ralf Sasse.Thank you all for taking the time to review my thesis, your inputs made the thesis and its defence a much nicer and interesting work.I would certainly not be here without having had the family I had.The teachings and love of my grandparents Aurora, Antonio, Isabel and Reinaldo gave meaning to my life from the very start.I will always remember the joyful moments shared with and the support given by my sister Aurorita, my father "Pepe", my aunts, my uncles and my cousins