src/HOL/Auth/TLS.ML
1997-07-01 paulson 1997-07-01 Baby TLS. Proofs work, but model seems unrealistic