This talk is composed by two fairly independent but related parts. In the first part I will make a brief introduction to the problem of anonymity. Then I will introduce an information-theoretic framework in which these protocols are interpreted as noisy channels, and I will discuss various quantitative definitions of their degree of anonymity, showing the relation with probabilistic definitions from the literature. Further, I will show how an adversary can use Bayesian Inference to deduce the secret information from the observables, and I will discuss how the probability of error (Bayesian risk) depends on the matrix. As a case study, I will apply this framework to the problem of the Dining Cryptographers with unfair coins. I will show how to model the protocol, compute its matrix using model-checking tools, and use it to compute the loss of anonymity of the protocol.

In the second part I will discuss a problem that appears when dealing with process calculi and automata which express both nondeterministic and probabilistic behavior. In such formalisms 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. I will present a process-algebraic framework in which the control on the scheduler can be specified in syntactic terms and I show how to apply it to solve the problem mentioned above. I also consider the definition of (probabilistic) may and must preorders and show that all the operators of the language, except replication, distribute over probabilistic summation, which is a useful property for verification.

Finally the problem of the Dining Cryptographers will be considered again, this time with non-determinism taken into account. Using the above framework, I show that the protocol can be proved anonymous even if we permit the announcements to be made in any order (chosen non-deterministically).