isabelle: src/HOL/Auth/All_Symmetric.thy@df65f5c27c15 (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
32631 2489e3c3562b common base for protocols with symmetric keys haftmann parents: 28098 diff changeset	7	defs all_symmetric_def: "all_symmetric \<equiv> True"
14145 2e31b8cc8788 ZhouGollmann: new example (fair non-repudiation protocol) paulson parents: 13922 diff changeset	8
32631 2489e3c3562b common base for protocols with symmetric keys haftmann parents: 28098 diff changeset	9	lemma isSym_keys: "K \<in> symKeys"
2489e3c3562b common base for protocols with symmetric keys haftmann parents: 28098 diff changeset	10	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	11
32631 2489e3c3562b common base for protocols with symmetric keys haftmann parents: 28098 diff changeset	12	end