# Theory MessageGA

section‹Theory of Agents and Messages for Security Protocols against the General Attacker›
theory MessageGA 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}"
datatype
agent = Friend nat