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

file  diff  annotate 
19971223 
paulson 
19971223 
Tidied using rev_iffD1

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 
19971118 
paulson 
19971118 
Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys

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 
19970925 
paulson 
19970925 
Changed some proofs to use Clarify_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 
19970917 
paulson 
19970917 
Fixed comments

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 
19970704 
paulson 
19970704 
Changed some variables of type msg to lower case (e.g. from NB to nb

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 
19970626 
paulson 
19970626 
Trivial changes in connection with the Yahalom paper.
Changed the order of the premises in no_nonce_YM1_YM2.
Installed B_trusts_YM4_newK using bind_thm.
Improved some comments.

file  diff  annotate 
19970619 
paulson 
19970619 
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)

file  diff  annotate 
19970618 
paulson 
19970618 
Streamlined proofs of the secrecy of NB and added authentication of A and B

file  diff  annotate 
19970609 
paulson 
19970609 
Strengthened and streamlined the Yahalom proofs

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

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 
19961220 
paulson 
19961220 
Corrected comments

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 
19961213 
paulson 
19961213 
Streamlined many proofs

file  diff  annotate 
19961205 
paulson 
19961205 
Trivial renamings

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

file  diff  annotate 
19961128 
paulson 
19961128 
Extra fix needed in newN case

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 
19961108 
paulson 
19961108 
Ran expandshort

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 
19961101 
paulson 
19961101 
Minor changes to comments

file  diff  annotate 
19961028 
paulson 
19961028 
Simplified proofs

file  diff  annotate 
19961018 
paulson 
19961018 
Addition of Reveal message

file  diff  annotate 
19961007 
paulson 
19961007 
Simplified a proof

file  diff  annotate 
19961001 
paulson 
19961001 
Simplified main theorem by abstracting out newK

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 
Proof of Says_imp_old_keys is now more robust

file  diff  annotate 
19960913 
paulson 
19960913 
Reformatting; proved B_gets_secure_key

file  diff  annotate 
19960913 
paulson 
19960913 
Addition of Yahalom protocol

file  diff  annotate 
19960912 
paulson 
19960912 
Tidied many proofs, using AddIffs to let equivalences take
the place of separate Intr and Elim rules. Also deleted most named clasets.

file  diff  annotate 