Stéphane Lafrance et John Mullins
Communication écrite (2002)
![]() |
Libre accès au plein texte de ce document Version officielle de l'éditeur Conditions d'utilisation: Creative Commons: Attribution-Pas d'utilisation commerciale-Pas de modification (CC BY-NC-ND) Télécharger (564kB) |
Abstract
In this paper, we first define bisimulation-based non-deterministic admissible interference(BNAI), derive its process-theoretic characterization and present a compositional verification method with respect to the main operators over communicating processes, generalizing in this way the similar trace-based results obtained in [19] into the finer notion of observation-based bisimulation [6]. Like its trace-based version, BNAI admits information flow between secrecy levels only through a downgrader (e.g. a cryptosystem), but is phrased into a generalization of observational equivalence [18]. We then describe an admissible interference-based method for the analysis of cryptographic protocols, extending, in a non-trivial way, the non interference-based approach presented in [11]. Confidentiality and authentication for cryptoprotocols are defined in terms of BNAI and their respective bisimulation-based proof methods are derived. Finally, as a significant illustration of the method, we consider simple case studies: the paradigmatic examples of the Wide Mouthed Frog protocol [1] and the Woo and Lam one-way authentication protocol [25]. The original idea of this methodology is to prove that the intruder may interfere with the protocol only through selected channels considered as admissible when leading to harmless interference.
Sujet(s): |
2700 Technologie de l'information > 2700 Technologie de l'information 2700 Technologie de l'information > 2714 Mathématiques de l'informatique 2700 Technologie de l'information > 2717 Études de modélisation et de simulation |
---|---|
Département: | Département de génie électrique |
Organismes subventionnaires: | CRSNG/NSERC |
Numéro de subvention: | 138321-01 |
URL de PolyPublie: | https://publications.polymtl.ca/4983/ |
Nom de la conférence: | Computing: the Australasian Theory Symposium (CATS 2002) |
Lieu de la conférence: | Monash University, Melbourne, Australia |
Date(s) de la conférence: | 2002-01-28 - 2002-02-01 |
Titre de la revue: | Electronic Notes in Theoretical Computer Science (vol. 61) |
Maison d'édition: | Elsevier |
DOI: | 10.1016/s1571-0661(04)00311-1 |
URL officielle: | https://doi.org/10.1016/s1571-0661%2804%2900311-1 |
Date du dépôt: | 12 mars 2021 10:34 |
Dernière modification: | 08 avr. 2024 18:49 |
Citer en APA 7: | Lafrance, S., & Mullins, J. (janvier 2002). Bisimulation-based non-deterministic admissible interference and its application to the analysis of cryptographic protocols [Communication écrite]. Computing: the Australasian Theory Symposium (CATS 2002), Monash University, Melbourne, Australia (24 pages). Publié dans Electronic Notes in Theoretical Computer Science, 61. https://doi.org/10.1016/s1571-0661%2804%2900311-1 |
---|---|
Statistiques
Total des téléchargements à partir de PolyPublie
Téléchargements par année
Provenance des téléchargements
Dimensions