Abstract
We use properties of observational equivalence for a probabilistic process calculus to prove an authentication property of a cryptographic protocol. The process calculus is a form of π-calculus, with probabilistic scheduling instead of nondeterminism, over a term language that captures probabilistic polynomial time. The operational semantics of this calculus gives priority to communication over private channels, so that the presence of private communication does not affect the observable probability of visible actions. Our definition of observational equivalence involves asymptotic comparison of uniform process families, only requiring equivalence to within vanishing error probabilities. This definition differs from previous notions of probabilistic process equivalence that require equal probabilities for corresponding actions; asymptotics fit our intended application and make equivalence transitive, thereby justifying the use of the term “equivalence.” Our security proof uses a series of lemmas about probabilistic observational equivalence that may well prove useful for establishing correctness of other cryptographic protocols.
Partially supported by DoD MURI “Semantic Consistency in Information Exchange,’ ONR Grant N00014-97-1-505
Additional support from NSF CCR-9629754
Additional support from Stanford University Fellowship
Additional support from NSF Grant CCR-9800785
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 A. Gordon. A calculus for cryptographic protocols: the spi calculus. In Proc. 4th ACM Conference on Computer and Communications Security, pages 36–47, 1997. Revised and expanded versions to appear in Information and Computation and 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.
G. Berry and G. Boudol. The chemical abstract machine. In Proc. 17th ACM Symp. Principles of Programming Languages, pages 81–94, 1990.
M. Bellare and P. Rogaway. Entity authentication and key distribution. In Advances in Cryptology-CRYPTO’ 93, Lecture Notes in Computer Science, Vol. 773, 1994.
M. Bellare and P. Rogaway. Provably secure session key distribution the three party case. In Proc. 27th ACM Symposium on the Theory of Computing, 1995.
D. Dolev and A. Yao. On the security of public-key protocols. IEEE Transactions on Information Theory, 2(29), 1983.
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.
D. Kozen. Semantics of probabilistic programs. Journal of Computer and System Sciences, 22:328–350, 1981.
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.
G. Lowe. Breaking and xing the Needham-Schroeder public-key protocol using CSP and FDR. In 2 nd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems. Springer-Verlag, 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.
R. Milner. Functions as processes. Math. Structures in Computer Science, 2(2):119–141, 1992.
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.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.
D. Volpano and G. Smith. Probabilistic noninterference in a concurrent language. In 11th IEEE Computer Security Foundations Workshop, pages 34–43. IEEE Computer Soc Press, 1998.
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
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lincoln, P., Mitchell, J., Mitchell, M., Scedrovy, A. (1999). Probabilistic Polynomial-Time Equivalence and Security Analysis. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1708. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48119-2_43
Download citation
DOI: https://doi.org/10.1007/3-540-48119-2_43
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66587-8
Online ISBN: 978-3-540-48119-5
eBook Packages: Springer Book Archive