| #
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
| #
5385dbfa |
|
16-Jan-2018 |
wenzelm <none@none> |
standardized towards new-style formal comments: isabelle update_comments;
|
| #
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;
|
| #
f4961062 |
|
20-Nov-2011 |
wenzelm <none@none> |
eliminated obsolete "standard";
|
| #
deac04eb |
|
22-Jul-2010 |
wenzelm <none@none> |
updated some headers;
|
| #
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
|
| #
7b63d2a6 |
|
11-Jul-2007 |
berghofe <none@none> |
Adapted to new inductive definition package.
|
| #
b00c25dd |
|
07-Oct-2005 |
nipkow <none@none> |
changes due to new neq_simproc in simpdata.ML
|
| #
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
| #
658c4226 |
|
16-Oct-2003 |
paulson <none@none> |
improved presentation
|
| #
3f87abe1 |
|
10-Oct-2003 |
paulson <none@none> |
better presentation
|
| #
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.
|
| #
d66531ec |
|
23-Sep-2003 |
paulson <none@none> |
Removal of the Key_supply axiom (affects many possbility proofs) and minor
changes
|
| #
05b61f85 |
|
17-Aug-2002 |
paulson <none@none> |
tidying of Isar scripts
|
| #
4962745e |
|
03-Oct-2001 |
wenzelm <none@none> |
tuned parentheses in relational expressions;
|
| #
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
|
| #
77e2d844 |
|
10-Mar-1999 |
paulson <none@none> |
deleted obsolete comments
|
| #
5ed22e3e |
|
09-Mar-1999 |
paulson <none@none> |
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.
|
| #
9aca3040 |
|
08-Sep-1998 |
paulson <none@none> |
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
|
| #
d06dcde6 |
|
21-Aug-1998 |
paulson <none@none> |
Tidying
|
| #
e1becb53 |
|
08-Jan-1998 |
paulson <none@none> |
Expressed most Oops rules using Notes instead of Says, and other tidying
|
| #
d2cfa1cd |
|
08-Jan-1998 |
paulson <none@none> |
Restored the ciphertext in OR4 in order to make the spec closer to that in
OtwayRees.thy
|
| #
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.
|
| #
8628ff0b |
|
26-Jun-1997 |
nipkow <none@none> |
set_of_list -> set
|
| #
5f254ab7 |
|
25-Mar-1997 |
paulson <none@none> |
Trivial renamings (for consistency with CSFW papers)
|
| #
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
|
| #
ad1324da |
|
29-Nov-1996 |
paulson <none@none> |
Swapped arguments of Crypt (for clarity and because it is conventional)
|
| #
86b695a2 |
|
27-Oct-1996 |
paulson <none@none> |
Changing from the Reveal to the Oops rule
|
| #
354300e5 |
|
18-Oct-1996 |
paulson <none@none> |
Reveal -> Revl
|
| #
46a4b2b2 |
|
01-Oct-1996 |
paulson <none@none> |
Working again with new theory Shared
|
| #
e2feb658 |
|
25-Sep-1996 |
paulson <none@none> |
Introduction of "lost" argument
Changed Enemy -> Spy
Ran expandshort
|
| #
56b443d5 |
|
23-Sep-1996 |
paulson <none@none> |
Bad version of Otway-Rees and the new attack on it
|