Inductive analysis of the Internet protocol TLS
- 1 August 1999
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Information and System Security
- Vol. 2 (3) , 332-351
- https://doi.org/10.1145/322510.322530
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.Keywords
All Related Versions
This publication has 6 references indexed in Scilit:
- The TLS Protocol Version 1.0Published by RFC Editor ,1999
- The inductive approach to verifying cryptographic protocolsJournal of Computer Security, 1998
- An attack on a recursive authentication protocol A cautionary taleInformation Processing Letters, 1998
- Kerberos Version IV: Inductive analysis of the secrecy goalsPublished by Springer Nature ,1998
- Prudent engineering practice for cryptographic protocolsIEEE Transactions on Software Engineering, 1996
- IsabellePublished by Springer Nature ,1994