Probabilistic Polynomial-Time Process Calculus and Security Protocol Analysis

  • John C. Mitchell
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2028)


We propose a formal framework for analyzing security protocols. This framework, which differs from previous logical methods based on the Dolev-Yao model, is based on a process calculus that captures probabilistic polynomial time. Protocols are written in a restricted form of π-calculus and security is expressed as a form or observational equivalence, a standard relation from programming language theory that involves quantifying over possible additional processes that might interact with the protocol. Using an asymptotic notion of probabilistic equivalence, we may relate observational equivalence to polynomial-time statistical tests. Several example protocols have been analyzed. We believe that this framework offers the potential to codify and automate realistic forms of protocol analysis. In addition, our work raises some foundational problems for reasoning about probabilistic programs and systems.


Authentication Protocol Security Protocol Public Channel Encryption Function Cryptographic Primitive 
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.


  1. [AF01]
    M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In 28th ACM Symposium on Principles of Programming Languages, pages 104–115, 2001.Google Scholar
  2. [AG98]
    M. Abadi and A. Gordon. A bisimulation method for cryptographic protocol. In Proc. ESOP’98, Springer Lecture Notes in Computer Science, 1998.Google Scholar
  3. [AG99]
    M. Abadi and A. Gordon. A calculus for cryptographic protocols: the spi calculus. Information and Computation, 143:1–70, 1999. Expanded version available as SRC Research Report 149 (January 1998).CrossRefMathSciNetGoogle Scholar
  4. [BAN89]
    M. Burrows, M. Abadi, and R. Needham. A logic of authentication. Proceedings of the Royal Society, Series A, 426(1871):233–271, 1989. Also appeared as SRC Research Report 39 and, in a shortened form, in ACM Transactions on Computer Systems 8, 1 (February 1990), 18-36.zbMATHCrossRefMathSciNetGoogle Scholar
  5. [BR94]
    M. Bellare and P. Rogaway. Entity authentication and key distribution. In Advances in Cryptology-CRYPTO’ 93, Lecture Notes in Computer Science, Vol. 773, 1994.Google Scholar
  6. [DY83]
    D. Dolev and A. Yao. On the security of public-key protocols. IEEE Transactions on Information Theory, 2(29), 1983.Google Scholar
  7. [ElG85]
    T. ElGamal. A public-key cryptosystem and a signature scheme based on discrete logarithms. IEEE Transactions on Information Theory, IT-31:469–472, 1985.zbMATHCrossRefMathSciNetGoogle Scholar
  8. [FKK96]
    A. Freier, P. Karlton, and P. Kocher. The SSL protocol version 3.0. draft-ietf-tls-ssl-version3-00.txt, November 18 1996.Google Scholar
  9. [KMM94]
    R. Kemmerer, C. Meadows, and J. Millen. Three systems for cryptographic protocol analysis. J. Cryptology, 7(2):79–130, 1994.zbMATHCrossRefGoogle Scholar
  10. [KN93]
    J.T. Kohl and B.C. Neuman. The Kerberos network authentication service (version 5). Internet Request For Comment RFC-1510, September 1993.Google Scholar
  11. [KNT94]
    J.T. Kohl, B.C. Neuman, and T.Y. Ts’o. The evolution of the Kerberos authentication service, pages 78–94. IEEE Computer Society Press, 1994.Google Scholar
  12. [LMMS98]
    P.D. Lincoln, J.C. Mitchell, M. Mitchell, and A. Scedrov. A probabilistic poly-time framework for protocol analysis. In ACM Conf. Computer and Communication Security, 1998.Google Scholar
  13. [LMMS99]
    P.D. Lincoln, J.C. Mitchell, M. Mitchell, and A. Scedrov. Probabilistic polynomial-time equivalence and security protocols. In FM’99 World Congress On Formal Methods in the Development of Computing Systems, 1999.Google Scholar
  14. [Low96]
    G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using CSP and FDR. In 2nd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems. Springer-Verlag, 1996.Google Scholar
  15. [Lub96]
    M. Luby. Pseudorandomness and Cryptographic Applications. Princeton Computer Science Notes, Princeton University Press, 1996.Google Scholar
  16. [Mea96]
    C. Meadows. Analyzing the Needham-Schroeder public-key protocol: a comparison of two approaches. In Proc. European Symposium On Research In Computer Security. Springer Verlag, 1996.Google Scholar
  17. [MMS97]
    J.C. Mitchell, M. Mitchell, and U. Stern. Automated analysis of cryptographic protocols using Murϕ. In Proc. IEEE Symp. Security and Privacy, pages 141–151, 1997.Google Scholar
  18. [MMS98]
    J. Mitchell, M. Mitchell, and A. Scedrov. A linguistic characterization of bounded oracle computation and probabilistic polynomial time. In IEEE Symp. Foundations of Computer Science, 1998.Google Scholar
  19. [MPW92]
    R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, part i. Information and Computation, 100(1):1–40, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  20. [NS78]
    R.M. Needham and M.D. Schroeder. Using encryption for authentication in large networks of computers. Communications of the ACM, 21(12):993–999, 1978.zbMATHCrossRefGoogle Scholar
  21. [Pau97a]
    L.C. Paulson. Mechanized proofs for a recursive authentication protocol. In 10th IEEE Computer Security Foundations Workshop, pages 84–95, 1997.Google Scholar
  22. [Pau97b]
    L.C. Paulson. Proving properties of security protocols by induction. In 10th IEEE Computer Security Foundations Workshop, pages 70–83, 1997.Google Scholar
  23. [Ros95]
    A. W. Roscoe. Modelling and verifying key-exchange protocols using CSP and FDR. In 8th IEEE Computer Security Foundations Workshop, pages 98–107. IEEE Computer Soc Press, 1995.Google Scholar
  24. [Sch96]
    S. Schneider. Security properties and CSP. In IEEE Symp. Security and Privacy, 1996.Google Scholar
  25. [Yao82]
    A. Yao. Theory and applications of trapdoor functions. In IEEE Foundations of Computer Science, pages 80–91, 1982.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • John C. Mitchell
    • 1
  1. 1.Stanford UniversityStanford

Personalised recommendations