isabelle: src/HOL/Auth/Auth_Shared.thy@5ae2a2e74c93 (annotated)

32632 8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	1	(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory
1944 ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	2	Copyright 1996 University of Cambridge
ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	3	*)
ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	4
58889 5b7a9633cfa8 modernized header uniformly as section; wenzelm parents: 32632 diff changeset	5	section {* Conventional protocols: rely on conventional Message, Event and Public -- Shared-key protocols *}
1944 ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	6
32632 8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	7	theory Auth_Shared
8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	8	imports
8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	9	"NS_Shared"
8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	10	"Kerberos_BAN"
8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	11	"Kerberos_BAN_Gets"
8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	12	"KerberosIV"
8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	13	"KerberosIV_Gets"
8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	14	"KerberosV"
8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	15	"OtwayRees"
8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	16	"OtwayRees_AN"
8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	17	"OtwayRees_Bad"
8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	18	"OtwayReesBella"
8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	19	"WooLam"
8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	20	"Recur"
8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	21	"Yahalom"
8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	22	"Yahalom2"
8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	23	"Yahalom_Bad"
8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	24	"ZhouGollmann"
8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	25	begin
14145 2e31b8cc8788 ZhouGollmann: new example (fair non-repudiation protocol) paulson parents: 13922 diff changeset	26
32632 8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	27	end

author	wenzelm
	Sat, 23 May 2015 17:19:37 +0200
changeset 60299	5ae2a2e74c93
parent 58889	5b7a9633cfa8
child 61830	4f5ab843cf5b
permissions	-rw-r--r--