Asynchronous Process Calculi for Specification and Verification of Information Hiding Protocols
type: Dataset
description: The work presented in this document in an account of my work as a PhD student at LIX, Ecole Polytechnique, in the COMETE team under the supervision of Catuscia Palamidessi. During these studies, I have been in interested in the various aspects of concurrency covered by the COMETE team activities. The initial goal of my thesis was to investigate the aspects related to process calculi based formalisms to express and analyze Security Protocols. The ultimate goal was to makes some advances towards the automatic verification of security properties. In particular, I was interested in information-hiding protocols which require no cryptography, but normally use randomized mechanisms and therefore exhibit probabilistic behavior. Information hiding protocols are used typically in networks, and they are run by parties that reside in different locations of the system, and therefore interact asynchronously. The first work that I did was to try to give a correct meaning to the various notions of formal asynchronous communications used in various models, in particular between the field of concurrency and the field of distributed computing, where this was a recurrent question. These results are presented in the first part of this document. Being interested in the formal aspects of information-hiding problems, I took part in the preparation of the journal version of [BP09], and started preparing an automated probabilistic anonymity checker based on the formalism presented in this document. This lead to an initial draft of an implementation presented in http://vamp.gforge.inria.fr/. The formalism for this analysis is presented in the fourth part of this document. Another aspect of the verification of information hiding properties is that it requires to compute the probabilities of the possible outcomes for each scheduler. For this reason, this application quickly turned out to be highly inefficient. However, in an asynchronous system, a lot of transitions are confluent, which means t…
issued: 2026-05-15T10:18:34.050170
language: en
modified: 2026-05-15T10:18:34.050176
contact point: Organization
  fn: CCSD
keyword: anonymity
keyword: concurrency-theory
keyword: infoeu-reposemanticsdoctoralthesis
keyword: infoinfo-crcomputer-science-cscryptography-and-security-cscr
keyword: infoinfo-locomputer-science-cslogic-in-computer-science-cslo
keyword: process-calculi
keyword: theses
landing page: https://pastel.hal.science/tel-00772693

Asynchronous Process Calculi for Specification and Verification of Information Hiding Protocols
type: Distribution
format: HTML
issued: 2026-05-15T10:18:34.079015
modified: 2026-05-15T10:18:34.034703
access URL: https://pastel.hal.science/tel-00772693

test_moissonnage_selune
type: Agent