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

24106 f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	1	(* Title: HOL/Auth/ROOT.ML
1944 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
24106 f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	11	use_thys [
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)
24106 f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	17	"NS_Shared",
f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	18	"Kerberos_BAN",
f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	19	"Kerberos_BAN_Gets",
f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	20	"KerberosIV",
f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	21	"KerberosIV_Gets",
f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	22	"KerberosV",
f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	23	"OtwayRees",
f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	24	"OtwayRees_AN",
f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	25	"OtwayRees_Bad",
f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	26	"OtwayReesBella",
f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	27	"WooLam",
f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	28	"Recur",
f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	29	"Yahalom",
f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	30	"Yahalom2",
f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	31	"Yahalom_Bad",
f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	32	"ZhouGollmann",
14145 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)
24106 f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	35	"NS_Public_Bad",
f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	36	"NS_Public",
f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	37	"TLS",
f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	38	"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
24106 f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	43	"Smartcard/ShoupRubin",
f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	44	"Smartcard/ShoupRubinBella",
18886 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)
24106 f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	47	"Guard/P1",
f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	48	"Guard/P2",
f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	49	"Guard/Guard_NS_Public",
f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	50	"Guard/Guard_OtwayRees",
f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	51	"Guard/Guard_Yahalom",
f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	52	"Guard/Proto"
f2965bf954dc simultaneous use_thys; wenzelm parents: 18886 diff changeset	53	];

author	haftmann
	Fri, 07 Dec 2007 15:07:59 +0100
changeset 25571	c9e39eafc7a0
parent 24106	f2965bf954dc
child 28098	c92850d2d16c
permissions	-rw-r--r--