# Theory Message

section‹Theory of Agents and Messages for Security Protocols against Dolev-Yao›
theory Message
imports Main
begin
lemma [simp] : "A ∪ (B ∪ A) = B ∪ A"
by blast
type_synonym
key = nat
consts
all_symmetric :: bool
invKey :: "key=>key"
specification (invKey)
invKey [simp]: "invKey (invKey K) = K"
invKey_symmetric: "all_symmetric --> invKey = id"
by (rule exI [of _ id], auto)
text‹The inverse of a symmetric key is itself; that of a public key
is the private key and vice versa›
definition symKeys :: "key set" where
"symKeys == {K. invKey K = K}"