Page d'accueil // Recherche // FSTC // Computer Sci... // Projets de r... // Symbolic verification of distance-bounding and multiparty authentication protocols

Symbolic verification of distance-bounding and multiparty authentication protocols

Financement: Fonds National de la Recherche > Aide à la Formation Recherche PhD
Date de début: 1 juin 2015
Date de fin: 31 mai 2018


Formal methods are the most reliable approach to exhaustively verify the security of cryptographic protocols. As new applications arise, new security goals and protocols may be required and ultimately, new formal approaches aimed at verifying those protocols ought to be proposed. With the boom of wireless technologies, distance bounding protocols have gained in popularity as a countermeasure against different types of distance-based attacks, such as mafia fraud, distance fraud, terrorist fraud, and distance hijacking. That is why recent efforts have been made on the development of formal approaches for the security analysis of distance bounding protocols. All these approaches have in common that distance is modeled by introducing either timestamps or a global clock into the model. We claim that most (or maybe all) distance-based attacks proposed up-to-date can be modeled in a symbolic partially-ordered approach, that is to say, in a model that does not explicitly introduce time or location in absolute terms. In this project we will extend the security model and operational semantics of the protocol verification tool Scyther in order to capture different types of distance-based attacks. Differently to previous models, we plan to define the notion of proximity as an ordering predicate on the trace of messages during a protocol session. We will thus study the relation between classical security properties, e.g., aliveness and agreement, and distance-based attacks. The extended model will be used for the formal analysis of both distance bounding and multiparty authentication protocols. Finally, we will design and implement model-checking algorithms so as to provide the Scyther tool with the ability to verify distance-based attacks.