Automatic verification of cryptographic protocols : privacy-type properties
type: Dataset
description: Many tools have been developed to automatically verify security properties on cryptographic protocols. But until recently, most tools focused on trace properties (or reachability properties) such as authentication and secrecy. However, many security properties cannot be expressed as trace properties, but can be written as equivalence properties. Privacy, unlinkability, and strong secrecy are typical examples of equivalence properties. Intuitively, two protocols P, Q are equivalent if an adversary can not distinguish P from Q by interacting with these processes. In the literature, several notions of equivalence were studied, e.g. trace equivalence or a stronger one, observational equivalence. However, it is often very difficult to prove by hand any of these equivalences, hence the need for efficient and automatic tools. We first worked on an approach that rely on constraint solving techniques and that is well suited for bounded number of sessions. We provided a new algorithm for deciding the trace equivalence between processes that may contain negative tests and non-determinism. We applied our results on concrete examples such as anonymity of the Private Authentication protocol and the E-passport protocol. We also investigated composition results. More precisely, we focused on parallel composition under shared secrets. We showed that under certain conditions on the protocols, the privacy type properties are preserved under parallel composition and under shared secrets. We applied our result on the e-passport protocol. At last this work presents an extension of the automatic protocol verifier ProVerif in order to prove more observational equivalences. This extension have been implemented in ProVerif and allows us to automatically prove anonymity in the private authentication protocol.
identifier: NNT: 2012DENS0075
issued: 2026-05-09T18:29:55.095014
language: en
modified: 2026-05-09T18:29:55.095018
contact point: Organization
  fn: CCSD
keyword: formal-verification
keyword: infoeu-reposemanticsdoctoralthesis
keyword: infoinfo-ohcomputer-science-csother-csoh
keyword: modele-symbolique
keyword: securite-des-protocoles-cryptographiques
keyword: security-of-cryptographic-protocol
keyword: symbolic-model
keyword: theses
keyword: verification-formelle
landing page: https://theses.hal.science/tel-00861389

Automatic verification of cryptographic protocols : privacy-type properties
type: Distribution
format: HTML
issued: 2026-05-09T18:29:55.096238
modified: 2026-05-09T18:29:55.085076
access URL: https://theses.hal.science/tel-00861389

test_moissonnage_selune
type: Agent