Theory All_Symmetric

theory All_Symmetric
imports Message
begin

text ‹All keys are symmetric›

overloading all_symmetric ≡ all_symmetric
begin
  definition "all_symmetric ≡ True"
end

lemma isSym_keys: "K ∈ symKeys"
  by (simp add: symKeys_def all_symmetric_def invKey_symmetric) 

end