isabelle: src/HOL/Auth/ROOT.ML@2075d9027004 (annotated)

1944 ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	1	(* Title: HOL/Auth/ROOT
ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	2	ID: $Id$
ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	4	Copyright 1996 University of Cambridge
ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	5
1971 30fe5ac5c04e Now runs all Auth proofs paulson parents: 1944 diff changeset	6	Root file for protocol proofs.
1944 ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	7	*)
ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	8
14716 1846cc85ada1 tuned document; wenzelm parents: 14307 diff changeset	9	no_document use_thy "NatPair";
1846cc85ada1 tuned document; wenzelm parents: 14307 diff changeset	10
18886 9f27383426db new and updated protocol proofs by Giamp Bella paulson parents: 17394 diff changeset	11	set timing;
17394 a8c9ed3f9818 renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions; wenzelm parents: 14716 diff changeset	12
18886 9f27383426db new and updated protocol proofs by Giamp Bella paulson parents: 17394 diff changeset	13	(* Conventional protocols: rely on
9f27383426db new and updated protocol proofs by Giamp Bella paulson parents: 17394 diff changeset	14	conventional Message, Event and Public *)
1944 ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	15
2325 ea8a1fc512e6 Loads new public-key examples paulson parents: 2274 diff changeset	16	(Shared-key protocols)
2530 02ccf78ad0a3 Now requests runtimes of all theories paulson parents: 2450 diff changeset	17	time_use_thy "NS_Shared";
5053 75d20f367e94 New example Kerberos_BAN by G Bella paulson parents: 4449 diff changeset	18	time_use_thy "Kerberos_BAN";
18886 9f27383426db new and updated protocol proofs by Giamp Bella paulson parents: 17394 diff changeset	19	time_use_thy "Kerberos_BAN_Gets";
6452 6a1b393ccdc0 addition of Kerberos IV example paulson parents: 6400 diff changeset	20	time_use_thy "KerberosIV";
18886 9f27383426db new and updated protocol proofs by Giamp Bella paulson parents: 17394 diff changeset	21	time_use_thy "KerberosIV_Gets";
9f27383426db new and updated protocol proofs by Giamp Bella paulson parents: 17394 diff changeset	22	time_use_thy "KerberosV";
2530 02ccf78ad0a3 Now requests runtimes of all theories paulson parents: 2450 diff changeset	23	time_use_thy "OtwayRees";
02ccf78ad0a3 Now requests runtimes of all theories paulson parents: 2450 diff changeset	24	time_use_thy "OtwayRees_AN";
02ccf78ad0a3 Now requests runtimes of all theories paulson parents: 2450 diff changeset	25	time_use_thy "OtwayRees_Bad";
18886 9f27383426db new and updated protocol proofs by Giamp Bella paulson parents: 17394 diff changeset	26	time_use_thy "OtwayReesBella";
2530 02ccf78ad0a3 Now requests runtimes of all theories paulson parents: 2450 diff changeset	27	time_use_thy "WooLam";
02ccf78ad0a3 Now requests runtimes of all theories paulson parents: 2450 diff changeset	28	time_use_thy "Recur";
02ccf78ad0a3 Now requests runtimes of all theories paulson parents: 2450 diff changeset	29	time_use_thy "Yahalom";
02ccf78ad0a3 Now requests runtimes of all theories paulson parents: 2450 diff changeset	30	time_use_thy "Yahalom2";
6400 1f495d4d922b added new theory Yahalom_Bad paulson parents: 6349 diff changeset	31	time_use_thy "Yahalom_Bad";
14145 2e31b8cc8788 ZhouGollmann: new example (fair non-repudiation protocol) paulson parents: 13922 diff changeset	32	time_use_thy "ZhouGollmann";
2e31b8cc8788 ZhouGollmann: new example (fair non-repudiation protocol) paulson parents: 13922 diff changeset	33
2325 ea8a1fc512e6 Loads new public-key examples paulson parents: 2274 diff changeset	34	(Public-key protocols)
2530 02ccf78ad0a3 Now requests runtimes of all theories paulson parents: 2450 diff changeset	35	time_use_thy "NS_Public_Bad";
02ccf78ad0a3 Now requests runtimes of all theories paulson parents: 2450 diff changeset	36	time_use_thy "NS_Public";
3475 368206f85f4b New theory TLS paulson parents: 3207 diff changeset	37	time_use_thy "TLS";
13922 75ae4244a596 Changes required by the certified email protocol paulson parents: 13550 diff changeset	38	time_use_thy "CertifiedEmail";
13508 890d736b93a5 Frederic Blanqui's new "guard" examples paulson parents: 9000 diff changeset	39
18886 9f27383426db new and updated protocol proofs by Giamp Bella paulson parents: 17394 diff changeset	40	(*Smartcard protocols: rely on conventional Message and on new
9f27383426db new and updated protocol proofs by Giamp Bella paulson parents: 17394 diff changeset	41	EventSC and Smartcard *)
9f27383426db new and updated protocol proofs by Giamp Bella paulson parents: 17394 diff changeset	42
9f27383426db new and updated protocol proofs by Giamp Bella paulson parents: 17394 diff changeset	43	with_path "Smartcard" time_use_thy "ShoupRubin";
9f27383426db new and updated protocol proofs by Giamp Bella paulson parents: 17394 diff changeset	44	with_path "Smartcard" time_use_thy "ShoupRubinBella";
9f27383426db new and updated protocol proofs by Giamp Bella paulson parents: 17394 diff changeset	45
13508 890d736b93a5 Frederic Blanqui's new "guard" examples paulson parents: 9000 diff changeset	46	(Blanqui's "guard" concept: protocol-independent secrecy)
18886 9f27383426db new and updated protocol proofs by Giamp Bella paulson parents: 17394 diff changeset	47	with_path "Guard" (app time_use_thy)
9f27383426db new and updated protocol proofs by Giamp Bella paulson parents: 17394 diff changeset	48	["P1", "P2", "Guard_NS_Public", "Guard_OtwayRees", "Guard_Yahalom", "Proto"];

author	wenzelm
	Sat, 04 Nov 2006 12:46:40 +0100
changeset 21166	2075d9027004
parent 18886	9f27383426db
child 24106	f2965bf954dc
permissions	-rw-r--r--