isabelle: src/HOL/Auth/Guard/Auth_Guard_Public.thy@e6b51fab96f7 (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
32632 8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	5	header {* Blanqui's "guard" concept: protocol-independent secrecy *}
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_Guard_Public
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	"P1"
8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	10	"P2"
8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	11	"Guard_NS_Public"
8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	12	"Proto"
8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	13	begin
14145 2e31b8cc8788 ZhouGollmann: new example (fair non-repudiation protocol) paulson parents: 13922 diff changeset	14
32632 8ae912371831 added session entry point theories haftmann parents: 28098 diff changeset	15	end

author	blanchet
	Mon, 21 May 2012 10:39:31 +0200
changeset 47944	e6b51fab96f7
parent 32632	8ae912371831
child 58889	5b7a9633cfa8
permissions	-rw-r--r--