<  Back to the Polytechnique Montréal portal

Bisimulation-based non-deterministic admissible interference and its application to the analysis of cryptographic protocols

Stéphane Lafrance and John Mullins

Conference or Workshop Item - Paper (2002)

[img]
Preview
Published Version
Terms of Use: Creative Commons Attribution Non-commercial No Derivatives.
Download (564kB)
Cite this document: Lafrance, S. & Mullins, J. (2002, January). Bisimulation-based non-deterministic admissible interference and its application to the analysis of cryptographic protocols. Paper presented at Computing: the Australasian Theory Symposium (CATS 2002), Monash University, Melbourne, Australia (24 pages). doi:10.1016/s1571-0661(04)00311-1
Show abstract Hide abstract

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.

Open Access document in PolyPublie
Subjects: 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
Department: Département de génie électrique
Research Center: Non applicable
Funders: CRSNG/NSERC
Grant number: 138321-01
Date Deposited: 12 Mar 2021 10:34
Last Modified: 13 Mar 2021 01:20
PolyPublie URL: https://publications.polymtl.ca/4983/
Document issued by the official publisher
Conference Title: Computing: the Australasian Theory Symposium (CATS 2002)
Conference Location: Monash University, Melbourne, Australia
Conference Date(s): 2002-01-28 - 2002-02-01
Journal Title: Electronic Notes in Theoretical Computer Science (vol. 61)
Publisher: Elsevier
Official URL: https://doi.org/10.1016/s1571-0661(04)00311-1

Statistics

Total downloads

Downloads per month in the last year

Origin of downloads

Dimensions

Repository Staff Only