19971224 
paulson 
19971224 
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort

file  diff  annotate 
19971223 
paulson 
19971223 
Tidied using more default rules

file  diff  annotate 
19971219 
wenzelm 
19971219 
tuned;

file  diff  annotate 
19971216 
paulson 
19971216 
Simplified proofs using rewrites for f``A where f is injective

file  diff  annotate 
19971103 
wenzelm 
19971103 
isatool fixclasimp;

file  diff  annotate 
19971021 
paulson 
19971021 
Many minor speedups:
1. Some use of rewriting with expand_ifs instead of addsplits[expand_if]
2. Faster proof of new_keys_not_used
3. New version of shrK_neq (no longer refers to "range")

file  diff  annotate 
19971017 
nipkow 
19971017 
setloop split_tac > addsplits

file  diff  annotate 
19970929 
paulson 
19970929 
Step_tac > Safe_tac

file  diff  annotate 
19970918 
paulson 
19970918 
Global change: lost>bad and sees Spy>spies
First change just gives a more sensible name.
Second change eliminates the agent parameter of "sees" to simplify
definitions and theorems

file  diff  annotate 
19970916 
paulson 
19970916 
Deleted the redundant simprule not_parts_not_analz

file  diff  annotate 
19970722 
paulson 
19970722 
Cosmetic changes: margins, indentation, ...

file  diff  annotate 
19970714 
paulson 
19970714 
Changing "lost" from a parameter of protocol definitions to a constant.
Advantages: no "lost" argument everywhere; fewer Vars in subgoals;
less need for specially instantiated rules
Disadvantage: can no longer prove "Agent_not_see_encrypted_key", but this
theorem was never used, and its original proof was also broken
the introduction of the "Notes" constructor.

file  diff  annotate 
19970711 
paulson 
19970711 
Removal of monotonicity reasoning involving "lost" and the theorem
Agent_not_see_encrypted_key, which (a) is never used and (b) becomes harder
to prove when Notes is available.

file  diff  annotate 
19970627 
paulson 
19970627 
Corrected indentations and margins after the renaming of "set_of_list"

file  diff  annotate 
19970626 
nipkow 
19970626 
set_of_list > set

file  diff  annotate 
19970619 
paulson 
19970619 
Made proofs more concise by replacing calls to spy_analz_tac by uses of
analz_insert_eq in rewriting

file  diff  annotate 
19970515 
oheimb 
19970515 
renamed unsafe_addss to addss

file  diff  annotate 
19970507 
paulson 
19970507 
Conversion to use blast_tac (with other improvements)

file  diff  annotate 
19970505 
paulson 
19970505 
Some blast_tac calls; more needed

file  diff  annotate 
19970325 
paulson 
19970325 
Trivial renamings (for consistency with CSFW papers)

file  diff  annotate 
19970215 
oheimb 
19970215 
reflecting my recent changes of the simplifier and classical reasoner

file  diff  annotate 
19970117 
paulson 
19970117 
Now with Andy Gordon's treatment of freshness to replace newN/K

file  diff  annotate 
19961219 
paulson 
19961219 
Extensive tidying and simplification, largely stemming from
changing newN and newK to take an integer argument

file  diff  annotate 
19961216 
paulson 
19961216 
New tactic: prove_unique_tac

file  diff  annotate 
19961213 
paulson 
19961213 
Streamlined some proofs

file  diff  annotate 
19961206 
paulson 
19961206 
Minor renamings

file  diff  annotate 
19961129 
paulson 
19961129 
Swapped arguments of Crypt (for clarity and because it is conventional)

file  diff  annotate 
19961128 
paulson 
19961128 
Weaking of injectivity assumptions for newK and newN:
they are no longer assumed injective over all traces, merely over the
length of a trace

file  diff  annotate 
19961121 
paulson 
19961121 
Minor reformatting

file  diff  annotate 
19961118 
paulson 
19961118 
Removal of an obsolete result, and authentication of
B to A

file  diff  annotate 
19961108 
paulson 
19961108 
A bit of tidying up

file  diff  annotate 
19961107 
paulson 
19961107 
Tidying up: removing redundant assumptions, etc.

file  diff  annotate 
19961105 
paulson 
19961105 
Simplified new_keys_not_seen, etc.: replaced the
union over all
agents by the Spy alone. Proofs run faster and they do not have to be
set up in terms of a previous lemma.

file  diff  annotate 
19961028 
paulson 
19961028 
Minor corrections

file  diff  annotate 
19961028 
nipkow 
19961028 
Renamed and shuffled a few thms.

file  diff  annotate 
19961018 
paulson 
19961018 
Replaced excluded_middle_tac by case_tac; tidied proofs

file  diff  annotate 
19961008 
paulson 
19961008 
Put in a simpler and *much* faster proof of no_nonce_OR1_OR2

file  diff  annotate 
19961007 
paulson 
19961007 
Simple tidying

file  diff  annotate 
19961001 
paulson 
19961001 
Greatly simplified the proof of A_can_trust

file  diff  annotate 
19961001 
paulson 
19961001 
Added new guarantees for A and B

file  diff  annotate 
19960930 
paulson 
19960930 
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
to Shared.ML

file  diff  annotate 
19960926 
paulson 
19960926 
Introduction of "lost" argument
Changed Enemy > Spy
Ran expandshort

file  diff  annotate 
19960925 
paulson 
19960925 
Last working version prior to introduction of "lost"

file  diff  annotate 
19960923 
paulson 
19960923 
Correction of protocol; addition of Reveal message; proofs of
correctness in its presence

file  diff  annotate 
19960913 
paulson 
19960913 
Reformatting

file  diff  annotate 
19960913 
paulson 
19960913 
Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs
Weak liveness

file  diff  annotate 
19960909 
paulson 
19960909 
"bad" set simplifies statements of many theorems

file  diff  annotate 
19960909 
paulson 
19960909 
Stronger proofs; work for OtwayRees

file  diff  annotate 
19960903 
paulson 
19960903 
A further tidying

file  diff  annotate 
19960903 
paulson 
19960903 
Initial working proof of OtwayRees protocol

file  diff  annotate 