Bangalore, INDIA, 25 Jan  4 Feb 2005
Title: Specification and verification of randomized security
protocols
Abstract: Randomization is used often in security for achieving
the intended results. Examples include protocols for contractsigning
based on Oblivious Transfer, and certain protocols for guarranteeing
anonimity. In these lectures I will show how these protocols and the
desired properties can be expressed and verified using the
probablistic picalculus.
Lectures and Slides
 Lecture 1 (Feb 1, 2005): Background on Probability theory and
Probabilistic Automata [ppt]
 Lecture 1 (Feb 2, 2005): The probabilistic picalculus [ppt]
 Lecture 3 (Feb 3, 2005): Applications to security:
 Probabilistic Anonymity [openoffice , ps]
 Partial secret exchange
[ps]
Bibliography
Most of the relevant references are indicated in the slides. In
addition, The third lecture is based on the following material:

Mohit Bhargava and Catuscia Palamidessi. Probabilistic Anonymity.
Technical report [ps].

Kostas Chatzikokolakis and Catuscia Palamidessi. A Framework for
Analyzing Probabilistic Protocols and its Application to the Partial Secrets Exchange.
Technical report [pdf].
For further reading, we can recommend the following works

Martín Abadi, Andrew D. Gordon.
A Calculus for Cryptographic Protocols: The Spi Calculus.
Information and Computation, 148(1), pp. 170, 1999.
[ps of report version].
 P. Mateus, J.C. Mitchell, and A. Scedrov.
Composition of cryptographic protocols
in a probabilistic polynomialtime process calculus.
In: R. Amadio and D. Lugiez, eds.,
"CONCUR 2003  Concurrency Theory",
14th International Conference, Marseille, France, September 2003,
Springer LNCS Volume 2761, SpringerVerlag, 2003, pp. 327349.
[
ps]
 G. Norman and V. Shmatikov. Analysis of probabilistic contract signing.
In BCSFACS Formal Aspects of Security (FASec '02), 2002.
[ps]
Last update Feb 6, 2005, by
Catuscia
Palamidessi