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 
New proof of respond_Spy_not_see_session_key

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 
19970701 
paulson 
19970701 
Tidying; also simplified the lemma Says_Server_not

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 
19970215 
oheimb 
19970215 
reflecting my recent changes of the simplifier and classical reasoner

file  diff  annotate 
19970127 
paulson 
19970127 
Tidied unicity theorems

file  diff  annotate 
19970123 
paulson 
19970123 
Reordering of certificates so that session keys appear in decreasing order

file  diff  annotate 
19970121 
paulson 
19970121 
Simplified proofs

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

file  diff  annotate 
19970107 
paulson 
19970107 
Simplification of some proofs, especially by eliminating
the equality in RA2

file  diff  annotate 
19970107 
paulson 
19970107 
Now uses HPair

file  diff  annotate 
19961220 
paulson 
19961220 
Simplification and generalization of the guarantees.
Nonces are not required for binding, merely for freshness.

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 
19961218 
paulson 
19961218 
Recursive Authentication Protocol

file  diff  annotate 