isabelle: src/HOL/Auth/Auth_Shared.thy@e2249cd6df67 (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
61830 4f5ab843cf5b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	5	section \<open>Conventional protocols: rely on conventional Message, Event and Public -- Shared-key protocols\<close>
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
65538 a39ef48fbee0 tuned imports; wenzelm parents: 61830 diff changeset	9	NS_Shared
a39ef48fbee0 tuned imports; wenzelm parents: 61830 diff changeset	10	Kerberos_BAN
a39ef48fbee0 tuned imports; wenzelm parents: 61830 diff changeset	11	Kerberos_BAN_Gets
a39ef48fbee0 tuned imports; wenzelm parents: 61830 diff changeset	12	KerberosIV
a39ef48fbee0 tuned imports; wenzelm parents: 61830 diff changeset	13	KerberosIV_Gets
a39ef48fbee0 tuned imports; wenzelm parents: 61830 diff changeset	14	KerberosV
a39ef48fbee0 tuned imports; wenzelm parents: 61830 diff changeset	15	OtwayRees
a39ef48fbee0 tuned imports; wenzelm parents: 61830 diff changeset	16	OtwayRees_AN
a39ef48fbee0 tuned imports; wenzelm parents: 61830 diff changeset	17	OtwayRees_Bad
a39ef48fbee0 tuned imports; wenzelm parents: 61830 diff changeset	18	OtwayReesBella
a39ef48fbee0 tuned imports; wenzelm parents: 61830 diff changeset	19	WooLam
a39ef48fbee0 tuned imports; wenzelm parents: 61830 diff changeset	20	Recur
a39ef48fbee0 tuned imports; wenzelm parents: 61830 diff changeset	21	Yahalom
a39ef48fbee0 tuned imports; wenzelm parents: 61830 diff changeset	22	Yahalom2
a39ef48fbee0 tuned imports; wenzelm parents: 61830 diff changeset	23	Yahalom_Bad
a39ef48fbee0 tuned imports; wenzelm parents: 61830 diff changeset	24	ZhouGollmann
32632 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	paulson <lp15@cam.ac.uk>
	Mon, 28 Aug 2017 20:33:08 +0100
changeset 66537	e2249cd6df67
parent 65538	a39ef48fbee0
permissions	-rw-r--r--