Title: Specification and verification of randomized security
protocols
Abstract: Randomization is used often in security for achieving
the intended results. Examples include protocols for contract-signing
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 pi-calculus.
Lectures and Slides
- Lecture 1 (Feb 1, 2005): Background on Probability theory and
Probabilistic Automata [ppt]
- Lecture 1 (Feb 2, 2005): The probabilistic pi-calculus [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. 1-70, 1999.
[ps of report version].
- P. Mateus, J.C. Mitchell, and A. Scedrov.
Composition of cryptographic protocols
in a probabilistic polynomial-time process calculus.
In: R. Amadio and D. Lugiez, eds.,
"CONCUR 2003 - Concurrency Theory",
14-th International Conference, Marseille, France, September 2003,
Springer LNCS Volume 2761, Springer-Verlag, 2003, pp. 327-349.
[
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