#
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
#
ce5e1da3 |
|
28-Dec-2015 |
wenzelm <none@none> |
more symbols;
|
#
feca4ab8 |
|
10-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
deac04eb |
|
22-Jul-2010 |
wenzelm <none@none> |
updated some headers;
|
#
7b63d2a6 |
|
11-Jul-2007 |
berghofe <none@none> |
Adapted to new inductive definition package.
|
#
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
#
5442a36e |
|
26-Sep-2003 |
paulson <none@none> |
Conversion of all main protocols from "Shared" to "Public". Removal of Key_supply_ax: modifications to possibility theorems. Improved presentation.
|
#
05b61f85 |
|
17-Aug-2002 |
paulson <none@none> |
tidying of Isar scripts
|
#
f88893dc |
|
11-Apr-2001 |
paulson <none@none> |
converted many HOL/Auth theories to Isar scripts
|
#
22bc9d8c |
|
27-Feb-2001 |
paulson <none@none> |
Some X-symbols for <notin>, <noteq>, <forall>, <exists> Streamlining of Yahalom proofs Removal of redundant proofs
|
#
9aca3040 |
|
08-Sep-1998 |
paulson <none@none> |
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
|
#
99c390e7 |
|
18-Sep-1997 |
paulson <none@none> |
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
|
#
5f61de48 |
|
04-Sep-1997 |
paulson <none@none> |
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
|
#
5276b175 |
|
13-Jul-1997 |
paulson <none@none> |
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.
|
#
279c30cb |
|
01-Jul-1997 |
paulson <none@none> |
Deleted a redundant A~=B in rules that refer to a previous event
|
#
bdb90be2 |
|
01-Jul-1997 |
paulson <none@none> |
Added a comment
|
#
8628ff0b |
|
26-Jun-1997 |
nipkow <none@none> |
set_of_list -> set
|
#
5b1e40e3 |
|
16-Jan-1997 |
paulson <none@none> |
Now with Andy Gordon's treatment of freshness to replace newN/K
|
#
2176d339 |
|
19-Dec-1996 |
paulson <none@none> |
Extensive tidying and simplification, largely stemming from changing newN and newK to take an integer argument
|
#
d953f00f |
|
29-Nov-1996 |
paulson <none@none> |
Swapping arguments of Crypt; removing argument lost
|
#
d27fcdc1 |
|
28-Nov-1996 |
paulson <none@none> |
Addition of Woo-Lam protocol
|