| 2006-01-04 |
paulson |
2006-01-04 |
a few more named lemmas
|
file | diff | annotate |
| 2005-10-07 |
nipkow |
2005-10-07 |
changes due to new neq_simproc in simpdata.ML
|
file | diff | annotate |
| 2005-09-15 |
wenzelm |
2005-09-15 |
fixed document;
|
file | diff | annotate |
| 2005-06-17 |
haftmann |
2005-06-17 |
migrated theory headers to new format
|
file | diff | annotate |
| 2003-10-16 |
paulson |
2003-10-16 |
improved presentation
|
file | diff | annotate |
| 2003-10-10 |
paulson |
2003-10-10 |
better presentation
|
file | diff | annotate |
| 2003-09-26 |
paulson |
2003-09-26 |
Conversion of all main protocols from "Shared" to "Public".
Removal of Key_supply_ax: modifications to possibility theorems.
Improved presentation.
|
file | diff | annotate |
| 2003-09-23 |
paulson |
2003-09-23 |
Removal of the Key_supply axiom (affects many possbility proofs) and minor
changes
|
file | diff | annotate |
| 2003-04-09 |
paulson |
2003-04-09 |
tidying
|
file | diff | annotate |
| 2002-08-17 |
paulson |
2002-08-17 |
tidying of Isar scripts
|
file | diff | annotate |
| 2001-10-03 |
wenzelm |
2001-10-03 |
tuned parentheses in relational expressions;
|
file | diff | annotate |
| 2001-04-12 |
paulson |
2001-04-12 |
converted many HOL/Auth theories to Isar scripts
|
file | diff | annotate |
| 2001-03-29 |
paulson |
2001-03-29 |
misc tidying; changing the predicate isSymKey to the set symKeys
|
file | diff | annotate |
| 2001-02-27 |
paulson |
2001-02-27 |
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
Streamlining of Yahalom proofs
Removal of redundant proofs
|
file | diff | annotate |
| 1999-03-10 |
paulson |
1999-03-10 |
deleted obsolete comments
|
file | diff | annotate |
| 1999-03-09 |
paulson |
1999-03-09 |
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
Changing "spies" to "knows Spy", etc. Retaining the constant "spies" as a
translation.
|
file | diff | annotate |
| 1998-09-08 |
paulson |
1998-09-08 |
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
|
file | diff | annotate |
| 1998-08-21 |
paulson |
1998-08-21 |
Tidying
|
file | diff | annotate |
| 1998-01-08 |
paulson |
1998-01-08 |
Expressed most Oops rules using Notes instead of Says, and other tidying
|
file | diff | annotate |
| 1997-09-18 |
paulson |
1997-09-18 |
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 |
| 1997-09-05 |
paulson |
1997-09-05 |
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
|
file | diff | annotate |
| 1997-07-14 |
paulson |
1997-07-14 |
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 |
| 1997-06-26 |
nipkow |
1997-06-26 |
set_of_list -> set
|
file | diff | annotate |
| 1997-03-25 |
paulson |
1997-03-25 |
Trivial renamings (for consistency with CSFW papers)
|
file | diff | annotate |
| 1997-01-17 |
paulson |
1997-01-17 |
Now with Andy Gordon's treatment of freshness to replace newN/K
|
file | diff | annotate |
| 1996-12-19 |
paulson |
1996-12-19 |
Extensive tidying and simplification, largely stemming from
changing newN and newK to take an integer argument
|
file | diff | annotate |
| 1996-12-13 |
paulson |
1996-12-13 |
Removed needless quotation marks
|
file | diff | annotate |
| 1996-11-29 |
paulson |
1996-11-29 |
Swapped arguments of Crypt (for clarity and because it is conventional)
|
file | diff | annotate |
| 1996-10-28 |
paulson |
1996-10-28 |
Minor corrections
|
file | diff | annotate |
| 1996-10-18 |
paulson |
1996-10-18 |
Important correction to comment
|
file | diff | annotate |
| 1996-10-07 |
paulson |
1996-10-07 |
Simple tidying
|
file | diff | annotate |
| 1996-09-26 |
paulson |
1996-09-26 |
Introduction of "lost" argument
Changed Enemy -> Spy
Ran expandshort
|
file | diff | annotate |
| 1996-09-23 |
paulson |
1996-09-23 |
Correction of protocol; addition of Reveal message; proofs of
correctness in its presence
|
file | diff | annotate |
| 1996-09-11 |
paulson |
1996-09-11 |
Reformatting
|
file | diff | annotate |
| 1996-09-03 |
paulson |
1996-09-03 |
Initial working proof of Otway-Rees protocol
|
file | diff | annotate |