src/HOL/Auth/Public.thy

    apply presburger
    apply presburger
    done                       
 
 
-axioms
+axiomatization where
   (*No private key equals any public key (essential to ensure that private
     keys are private!) *)
   privateKey_neq_publicKey [iff]: "privateKey b A \<noteq> publicKey c A'"
 
 lemmas publicKey_neq_privateKey = privateKey_neq_publicKey [THEN not_sym]

   --{*No two agents have the same long-term key*}
    apply (rule exI [of _ "agent_case 0 (\<lambda>n. n + 2) 1"]) 
    apply (simp add: inj_on_def split: agent.split) 
    done
 
-axioms
+axiomatization where
   sym_shrK [iff]: "shrK X \<in> symKeys" --{*All shared keys are symmetric*}
 
 text{*Injectiveness: Agents' long-term keys are distinct.*}
 lemmas shrK_injective = inj_shrK [THEN inj_eq]
 declare shrK_injective [iff]