Skip to Main content Skip to Navigation
Theses

Efficient verification of observational equivalences of cryptographic processes : theory and practice

Itsaka Rakotonirina 1
1 PESTO - Proof techniques for security protocols
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : This thesis studies the analysis of cryptographic protocols. They are sequences of instructions permitting to interact with a recipient remotely while protecting the sensitive content of the communication from a potential malicious third party. Classical cases where the confidentiality and the integrity of the communication are critical are, among others, online payments and medical-service booking, or electronic voting. We study notions of security defined technically by observational equivalences (which includes among others confidentiality, anonymity or non-traceability). We designed a program, DeepSec, which, from the description of a protocol for a fixed number of participants, verifies in a fully-automated way whether the protocol offers a security guarantee of this type. We demonstrate the ability of this tool to analyse complex attack scenarios through several examples. After that, we present an optimization technique exploiting symmetries in security proofs. Typically, participants with similar roles in the protocol often have similar instructions to follow, inducing redundant work during the analysis. On several examples, using this technique allowed to reduce the analysis time of DeepSec by several orders of magnitude. Finally, we also studied the theoretical aspect the problem in order to determine to which extent DeepSec’s algorithm could be improved (can we make the tool faster?) or made more expressive (can we get rid of some of the limitations of the tool?). For that we carried out a complete analysis of the computational complexity of DeepSec’s algorithm, and integrated it to a detailed survey of the state of the art regarding complexity results in similar contexts. This meticulous survey allowed us to expose subtle variations in how the problem is formalised across the literature—sometimes impacting its complexity. We also include new results and improve some of the surveyed ones, resulting in a clearer understanding of the problem.
Document type :
Theses
Complete list of metadata

https://hal.univ-lorraine.fr/tel-03229177
Contributor : Thèses Ul Connect in order to contact the contributor
Submitted on : Tuesday, May 18, 2021 - 5:18:13 PM
Last modification on : Saturday, October 16, 2021 - 11:26:10 AM

File

DDOC_T_2021_0052_RAKOTONIRINA....
Files produced by the author(s)

Identifiers

  • HAL Id : tel-03229177, version 1

Citation

Itsaka Rakotonirina. Efficient verification of observational equivalences of cryptographic processes : theory and practice. Cryptography and Security [cs.CR]. Université de Lorraine, 2021. English. ⟨NNT : 2021LORR0052⟩. ⟨tel-03229177⟩

Share

Metrics

Record views

120

Files downloads

279