Sciweavers

ENTCS
2007

A Probabilistic Scheduler for the Analysis of Cryptographic Protocols

13 years 11 months ago
A Probabilistic Scheduler for the Analysis of Cryptographic Protocols
When modelling cryto-protocols by means of process calculi which express both nondeterministic and probabilistic behavior, it is customary to view the scheduler as an intruder. It has been established that the traditional scheduler needs to be carefully calibrated in order to more accurately reflect the intruder’s capabilities for controlling communication channels. We propose such a class of schedulers through a semantic variant called PPCνσ, of the Probabilistic Poly-time Calculus (PPC) of Mitchell et al. [11] and we illustrate the pertinence of our approach by an extensive study of the Dining Cryptographers (DCP) [8] protocol. Along these lines, we define a new characterization of Mitchell et al.’s observational equivalence [11] more suited for taking into account any observable trace instead of just a single action as required in the analysis of the DCP.
Srecko Brlek, Sardaouna Hamadou, John Mullins
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2007
Where ENTCS
Authors Srecko Brlek, Sardaouna Hamadou, John Mullins
Comments (0)