src/HOL/Auth/TLS.ML
1997-12-24 ago New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-12-23 ago Tidied using rev_iffD1, etc
1997-12-19 ago tuned;
1997-12-16 ago expandshort;
1997-12-16 ago Simplified proofs using rewrites for f``A where f is injective
1997-11-11 ago Fixed indentation
1997-11-03 ago isatool fixclasimp;
1997-10-27 ago Deleted two needless theorems
1997-10-21 ago Many minor speedups:
1997-10-17 ago setloop split_tac -> addsplits
1997-10-03 ago Routine tidying up
1997-10-01 ago Strengthened the possibility property for resumption so that it could have
1997-10-01 ago Exchanged the M and SID fields of the FINISHED messages to simplify proofs;
1997-09-30 ago Client, Server certificates now sent using the separate Certificate rule,
1997-09-29 ago Renamed XA, XB to PA, PB and removed the certificate from Client Verify
1997-09-25 ago Deleted an obsolete step in TrustServerFinished
1997-09-24 ago sessionK now indexed by nat instead of bool.
1997-09-22 ago Simplified SpyKeys to use sessionK instead of clientK and serverK
1997-09-19 ago First working version with Oops event for session keys
1997-09-19 ago Full version of TLS including session resumption, but no Oops
1997-09-18 ago Global change: lost->bad and sees Spy->spies
1997-09-17 ago Now with the sessionK constant and new events ClientAccepts and ServerAccepts
1997-09-16 ago Addition of SessionIDs to the Hello and Finished messages
1997-09-16 ago TLS now with a distinction between premaster secret and master secret
1997-07-14 ago Changing "lost" from a parameter of protocol definitions to a constant.
1997-07-11 ago Now uses the Notes constructor to distinguish the Client (who has chosen M)
1997-07-07 ago New proofs involving CERTIFICATE VERIFY
1997-07-04 ago New constant "certificate"--just an abbreviation
1997-07-01 ago More realistic model: the Spy can compute clientK and serverK
1997-07-01 ago Baby TLS. Proofs work, but model seems unrealistic