src/HOL/Auth/OtwayRees.ML
1996-10-01 paulson 1996-10-01 Greatly simplified the proof of A_can_trust
1996-10-01 paulson 1996-10-01 Added new guarantees for A and B
1996-09-30 paulson 1996-09-30 Removed some dead wood. Transferred lemmas used to prove analz_image_newK to Shared.ML
1996-09-26 paulson 1996-09-26 Introduction of "lost" argument Changed Enemy -> Spy Ran expandshort
1996-09-25 paulson 1996-09-25 Last working version prior to introduction of "lost"
1996-09-23 paulson 1996-09-23 Correction of protocol; addition of Reveal message; proofs of correctness in its presence
1996-09-13 paulson 1996-09-13 Reformatting
1996-09-13 paulson 1996-09-13 Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs Weak liveness
1996-09-09 paulson 1996-09-09 "bad" set simplifies statements of many theorems
1996-09-09 paulson 1996-09-09 Stronger proofs; work for Otway-Rees
1996-09-03 paulson 1996-09-03 A further tidying
1996-09-03 paulson 1996-09-03 Initial working proof of Otway-Rees protocol