Abstract
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.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
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.
M. Abadi and A. Gordon. A bisimulation method for cryptographic protocol. In Proc. ESOP’98, Springer Lecture Notes in Computer Science, 1998.
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).
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.
M. Bellare and P. Rogaway. Entity authentication and key distribution. In Advances in Cryptology-CRYPTO’ 93, Lecture Notes in Computer Science, Vol. 773, 1994.
D. Dolev and A. Yao. On the security of public-key protocols. IEEE Transactions on Information Theory, 2(29), 1983.
T. ElGamal. A public-key cryptosystem and a signature scheme based on discrete logarithms. IEEE Transactions on Information Theory, IT-31:469–472, 1985.
A. Freier, P. Karlton, and P. Kocher. The SSL protocol version 3.0. draft-ietf-tls-ssl-version3-00.txt, November 18 1996.
R. Kemmerer, C. Meadows, and J. Millen. Three systems for cryptographic protocol analysis. J. Cryptology, 7(2):79–130, 1994.
J.T. Kohl and B.C. Neuman. The Kerberos network authentication service (version 5). Internet Request For Comment RFC-1510, September 1993.
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.
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.
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.
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.
M. Luby. Pseudorandomness and Cryptographic Applications. Princeton Computer Science Notes, Princeton University Press, 1996.
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.
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.
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.
R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, part i. Information and Computation, 100(1):1–40, 1992.
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.
L.C. Paulson. Mechanized proofs for a recursive authentication protocol. In 10th IEEE Computer Security Foundations Workshop, pages 84–95, 1997.
L.C. Paulson. Proving properties of security protocols by induction. In 10th IEEE Computer Security Foundations Workshop, pages 70–83, 1997.
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.
S. Schneider. Security properties and CSP. In IEEE Symp. Security and Privacy, 1996.
A. Yao. Theory and applications of trapdoor functions. In IEEE Foundations of Computer Science, pages 80–91, 1982.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mitchell, J.C. (2001). Probabilistic Polynomial-Time Process Calculus and Security Protocol Analysis. In: Sands, D. (eds) Programming Languages and Systems. ESOP 2001. Lecture Notes in Computer Science, vol 2028. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45309-1_2
Download citation
DOI: https://doi.org/10.1007/3-540-45309-1_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41862-7
Online ISBN: 978-3-540-45309-3
eBook Packages: Springer Book Archive