Lawrence C. Paulson
Abstract
Internet browsers use security protocols to protect sensitive messages. An inductive analysis of TLS (a descendant of SSL 3.0) has been performed using the theorem prover Isabelle. Proofs are based on higher-order logic and make no assumptions concerning beliefs of finiteness. All the obvious security goals can be proved; session resumption appears to be secure even if old session keys are compromised. The proofs suggest minor changes to simplify the analysis.
TLS, even at an abstract level, is much more complicated than most protocols verified by researchers. Session keys are negotiated rather than distributed, and the protocol has many optional parts. Netherless, the resources needed to verify TLS are modest: six man-weeks of effort and three minutes of processor time.
- ABADI, M. AND NEEDHAM, R. 1996. Prudent engineering practice for cryptographic protocols. IEEE Trans. Softw. Eng. 22, I, 6-15. Google Scholar
- BELLA, G. AND PAULSON, L. C. 1998. Kerberos version IV: Inductive analysis of the secrecy goals. In Computer Security (ESORICS '98), J.-J. Quisquater, Y. Deswarte, C. Meadows, and D. Gollmann, Eds. Springer-Verlag, New York, 361-375. Google Scholar
- DIERKS, T. AND ALLEN, C. 1999. The TLS protocol: Version 1.0. Request for Comments: 2246. ftp ://ftp.isi. edu/in-notes/rfc2246.txt. Google Scholar
- DIETRICH, S. 1997. A formal analysis of the secure sockets layer protocol. Ph.D. Dissertation. Adelphi Univ., Garden City, NY.Google Scholar
- FREIER, A. O., KARLTON, P., AND KOCHER, P. C. 1996. The SSL protocol version 3.0. Internet-draft draft-freier-ssl-version3-02.txtGoogle Scholar
- GOLLMANN, D. 1996. What do we mean by entity authentication?. In Proceedings of the IEEE Symposium on Security and Privacy (Oakland, CA, May). IEEE Press, Piscataway, NJ, 46 -54. Google Scholar
- MITCHELL, J. C., SHMATIKOV, V., AND STERN, U. 1997. Finite-state analysis of SSL 3.0 and related protocols. In Proceedings of the Workshop on Design and Formal Verification of Security Protocols (DIMACS, Sept.), H. Orman and C. Meadows, Eds. Google Scholar
- PAULSON, L. C. 1994. Isabelle: A generic theorem prover. In Lecture Notes in Computer Science. Lecture Notes in Computer Science, vol. 828. Springer-Verlag, New York.Google Scholar
- PAULSON, L. C. 1999. Relations between secrets: Two formal analyses of the Yahalom protocol. J. Comput. Secur. 7 (To appear). Google Scholar
- PAULSON, L. C. 1998. The inductive approach to verifying cryptographic protocols. J. Comput. Secur. 6, 85-128. Google Scholar
- RYAN, P. Y. A. AND SCHNEIDER, S.A. 1998. An attack on a recursive authentication protocol. A cautionary tale. Inf. Process. Lett. 65, 1, 7-10. Google Scholar
- WAGNER, D. AND SCHNEIER, B. 1996. Analysis of the SSL 3.0 protocol. In Proceedings of the USENIX Conference on Electronic Commerce. USENIX Assoc., Berkeley, CA, 29-40. Google Scholar
Index Terms
- Inductive analysis of the Internet protocol TLS
Recommendations
Accountability protocols: Formalized and verified
Classical security protocols aim to achieve authentication and confidentiality under the assumption that the peers behave honestly. Some recent protocols are required to achieve their goals even if the peer misbehaves. Accountability is a protocol ...
Inductive study of confidentiality: for everyone
AbstractThe Inductive Method is among the most established tools to analyse security protocols formally. It has successfully coped with large, deployed protocols, and its findings are widely published. However, perhaps due to its embedding in a theorem ...
Mechanised Assessment of Complex Natural-Language Arguments Using Expressive Logic Combinations
Frontiers of Combining SystemsAbstractWe present and illustrate an approach to combining logics based on shallow semantical embeddings, a technique that harnesses the high expressive power of classical higher-order logic (HOL) as a meta-language in order to embed the syntax and ...
Comments