Searching for just a few words should be enough to get started. If you need to make more complex queries, use the tips below to guide you.
Issue title: Security Issues in Concurrency (SecCo'07)
Guest editors: Daniele GorlaGuest-Editor and Catuscia PalamidessiGuest-Editor
Article type: Research Article
Authors: Hamadou, Sardaouna | Mullins, John; *; **
Affiliations: Department of Computer and Software Engineering, École Polytechnique de Montréal, Canada. E-mails: sardaouna.hamadou@polymtl.ca, john.mullins@polymtl.ca
Correspondence: [*] Corresponding author.
Note: [**] Research partially supported by an individual NSERC research grant (Canada) of the author.
Abstract: It is customary to view the scheduler as an intruder when modelling security protocols by means of process calculi that express both nondeterministic and probabilistic behavior. It has been established that traditional schedulers need to be carefully calibrated in order to more accurately reflect an intruder's real power. We propose such a class of schedulers through a variant of the Probabilistic Poly-time Calculus (PPC) of Mitchell et al. (Theoretical Computer Science 353 (2006), 118–164) called PPCνσ. We define two levels of schedulers: adversarial schedulers which schedule a class of indistinguishable actions i.e. actions that we do not want an attacker to distinguish, and internal schedulers, called task schedulers, which resolve the remaining nondeterminism within a chosen class. We also show how to apply them in order to design schedulers for the analysis of cryptographic protocols that accurately reflect an intruder's capacity for controlling communication networks, without allowing it to control the internal reactions of the protocol under attack. We give a new characterization of the asymptotic observational equivalence of Mitchell et al. (Theoretical Computer Science 353 (2006), 118–164) that is more suited for taking into account any observable trace rather than just one single action. This asymptotic observational equivalence is a congruence in accordance with these new schedulers. We illustrate the aptness of our approach by an extensive study of the Dining Cryptographers (DCP) (J. Cryptology 1 (1988), 65–75) protocol.
Keywords: Process algebra, observational equivalence, probabilistic scheduling, analysis of cryptographic protocols
DOI: 10.3233/JCS-2010-0362
Journal: Journal of Computer Security, vol. 18, no. 2, pp. 265-316, 2010
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
USA
Tel: +1 703 830 6300
Fax: +1 703 830 2300
sales@iospress.com
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
IOS Press
Nieuwe Hemweg 6B
1013 BG Amsterdam
The Netherlands
Tel: +31 20 688 3355
Fax: +31 20 687 0091
info@iospress.nl
For editorial issues, permissions, book requests, submissions and proceedings, contact the Amsterdam office info@iospress.nl
Inspirees International (China Office)
Ciyunsi Beili 207(CapitaLand), Bld 1, 7-901
100025, Beijing
China
Free service line: 400 661 8717
Fax: +86 10 8446 7947
china@iospress.cn
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
如果您在出版方面需要帮助或有任何建, 件至: editorial@iospress.nl