Making Random Choices Invisible to the Scheduler

TL;DR

This paper introduces a process-algebraic framework that allows explicit control over schedulers in probabilistic process models, enhancing security analysis by preventing scheduler influence on random choices.

Contribution

It proposes a syntactic method to restrict schedulers in probabilistic process calculi, ensuring security properties are preserved and operators distribute over probabilistic summation.

Findings

The framework enables specifying scheduler restrictions syntactically.

May and must preorders are shown to be precongruences under restrictions.

Operators distribute over probabilistic summation, aiding verification.

Abstract

When dealing with process calculi and automata which express both nondeterministic and probabilistic behavior, it is customary to introduce the notion of scheduler to solve the nondeterminism. It has been observed that for certain applications, notably those in security, the scheduler needs to be restricted so not to reveal the outcome of the protocol's random choices, or otherwise the model of adversary would be too strong even for ``obviously correct'' protocols. We propose a process-algebraic framework in which the control on the scheduler can be specified in syntactic terms, and we show how to apply it to solve the problem mentioned above. We also consider the definition of (probabilistic) may and must preorders, and we show that they are precongruences with respect to the restricted schedulers. Furthermore, we show that all the operators of the language, except replication, distribute over probabilistic summation, which is a useful property for verification.