<  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

Paper (2002)

Open Acess document in PolyPublie and at official publisher
[img] Open Access to the full text of this document
Published Version
Terms of Use: Creative Commons Attribution Non-commercial No Derivatives
Download (564kB)
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.

Subjects: 2700 Information technology > 2700 Information technology
2700 Information technology > 2714 Mathematics of computing
2700 Information technology > 2717 Modelling and simulation studies
Department: Department of Electrical Engineering
Funders: CRSNG/NSERC
Grant number: 138321-01
PolyPublie URL: https://publications.polymtl.ca/4983/
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
DOI: 10.1016/s1571-0661(04)00311-1
Official URL: https://doi.org/10.1016/s1571-0661%2804%2900311-1
Date Deposited: 12 Mar 2021 10:34
Last Modified: 07 May 2023 10:56
Cite in APA 7: Lafrance, S., & Mullins, J. (2002, January). Bisimulation-based non-deterministic admissible interference and its application to the analysis of cryptographic protocols [Paper]. Computing: the Australasian Theory Symposium (CATS 2002), Monash University, Melbourne, Australia (24 pages). Published in Electronic Notes in Theoretical Computer Science, 61. https://doi.org/10.1016/s1571-0661%2804%2900311-1

Statistics

Total downloads

Downloads per month in the last year

Origin of downloads

Dimensions

Repository Staff Only

View Item View Item