Abstract:
We consider a calculus for multiparty sessions enriched with security
levels for messages. We propose a monitored semantics for this
calculus, which blocks the execution of processes as soon as they
attempt to leak information. We illustrate the use of our monitored
semantics with various examples, and show that the induced safety
property implies a noninterference property studied previously.