isabelle: src/HOL/Auth/All_Symmetric.thy@ff813e8a3271 (annotated)

32631 2489e3c3562b common base for protocols with symmetric keys haftmann parents: 28098 diff changeset	1	theory All_Symmetric
2489e3c3562b common base for protocols with symmetric keys haftmann parents: 28098 diff changeset	2	imports Message
2489e3c3562b common base for protocols with symmetric keys haftmann parents: 28098 diff changeset	3	begin
1944 ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	4
61830 4f5ab843cf5b isabelle update_cartouches -c -t; wenzelm parents: 32631 diff changeset	5	text \<open>All keys are symmetric\<close>
1944 ea0f573b222b ROOT file for Auth directory paulson parents: diff changeset	6
62145 5b946c81dfbf eliminated old defs; wenzelm parents: 61830 diff changeset	7	overloading all_symmetric \<equiv> all_symmetric
5b946c81dfbf eliminated old defs; wenzelm parents: 61830 diff changeset	8	begin
5b946c81dfbf eliminated old defs; wenzelm parents: 61830 diff changeset	9	definition "all_symmetric \<equiv> True"
5b946c81dfbf eliminated old defs; wenzelm parents: 61830 diff changeset	10	end
14145 2e31b8cc8788 ZhouGollmann: new example (fair non-repudiation protocol) paulson parents: 13922 diff changeset	11
32631 2489e3c3562b common base for protocols with symmetric keys haftmann parents: 28098 diff changeset	12	lemma isSym_keys: "K \<in> symKeys"
2489e3c3562b common base for protocols with symmetric keys haftmann parents: 28098 diff changeset	13	by (simp add: symKeys_def all_symmetric_def invKey_symmetric)
18886 9f27383426db new and updated protocol proofs by Giamp Bella paulson parents: 17394 diff changeset	14
32631 2489e3c3562b common base for protocols with symmetric keys haftmann parents: 28098 diff changeset	15	end

author	Thomas Lindae <thomas.lindae@in.tum.de>
	Thu, 18 Jul 2024 22:08:46 +0200
changeset 81079	ff813e8a3271
parent 62145	5b946c81dfbf
permissions	-rw-r--r--