src/HOL/Auth/TLS.thy
1997-07-04 paulson 1997-07-04 New constant "certificate"--just an abbreviation
1997-07-01 paulson 1997-07-01 More realistic model: the Spy can compute clientK and serverK
1997-07-01 paulson 1997-07-01 Baby TLS. Proofs work, but model seems unrealistic