A Framework for Analyzing Probabilistic Protocols and Its Application to the Partial Secrets Exchange

  • Konstantinos Chatzikokolakis
  • Catuscia Palamidessi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3705)


We propose a probabilistic variant of the pi-calculus as a framework to specify randomized security protocols and their intended properties. In order to express an verify the correctness of the protocols, we develop a probabilistic version of the testing semantics. We then illustrate these concepts on an extended example: the Partial Secret Exchange, a protocol which uses a randomized primitive, the Oblivious Transfer, to achieve fairness of information exchange between two parties.


Model Check Security Protocol Security Property Probabilistic Choice Oblivious Transfer 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Rabin, M.: How to exchange secrets by oblivious transfer. Technical Memo TR-81, Aiken Computation Laboratory, Harvard University (1981)Google Scholar
  2. 2.
    Even, S., Goldreich, O., Lempel, A.: A randomized protocol for signing contracts. Commun. ACM 28, 637–647 (1985)CrossRefMathSciNetGoogle Scholar
  3. 3.
    Naor, M., Pinkas, B., Sumner, R.: Privacy preserving auctions and mechanism design. In: Proceedings of the 1st ACM conference on Electronic commerce, Colorado, pp. 129–139. ACM Press, New York (1999)CrossRefGoogle Scholar
  4. 4.
    Aldini, A., Gorrieri, R.: Security analysis of a probabilistic non-repudiation protocol. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol. 2399, p. 17. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  5. 5.
    Herescu, O.M., Palamidessi, C.: Probabilistic asynchronous π-calculus. In: Tiuryn, J. (ed.) FOSSACS 2000. LNCS, vol. 1784, pp. 146–160. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  6. 6.
    Nicola, R.D., Hennessy, M.C.B.: Testing equivalences for processes. Theoretical Computer Science 34, 83–133 (1984)CrossRefzbMATHMathSciNetGoogle Scholar
  7. 7.
    Abadi, M., Gordon, A.: A calculus for cryptographic protocols: The spi calculus. Information and Computation 148, 1–70 (1999)CrossRefzbMATHMathSciNetGoogle Scholar
  8. 8.
    Chatzikokolakis, K., Palamidessi, C.: A framework for analyzing probabilistic protocols and its application to the partial secrets exchange. Report version (2005), available at
  9. 9.
    Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. Nordic Journal of Computing 2, 250–273 (1995)zbMATHMathSciNetGoogle Scholar
  10. 10.
    Palamidessi, C., Herescu, O.M.: A randomized encoding of the pi-calculus with mixed choice. In: Proceedings of the 2nd IFIP International Conference on Theoretical Computer Science, pp. 537–549 (2002)Google Scholar
  11. 11.
    Jonsson, B., Larsen, K.G., Yi, W.: Probabilistic extensions of process algebras. In: Handbook of Process Algebras (2001)Google Scholar
  12. 12.
    Norman, G., Shmatikov, V.: Analysis of probabilistic contract signing. In: Abdallah, A.E., Ryan, P.Y.A., Schneider, S. (eds.) FASec 2002. LNCS, vol. 2629, pp. 81–96. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  13. 13.
    Norman, G., Shmatikov, V.: Analysis of probabilistic contract signing. Formal Aspects of Computing (2005) (to appear) Google Scholar
  14. 14.
    Christoff, L., Christoff, I.: Efficient algorithms for verification of equivalences for probabilistic processes. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, Springer, Heidelberg (1992)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Konstantinos Chatzikokolakis
    • 1
  • Catuscia Palamidessi
    • 1
  1. 1.LIX, École PolytechniquePalaiseauFrance

Personalised recommendations