Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/Doc/Tutorial/Protocol/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 5 kB

Quelle Public.thy Sprache: Isabelle

(*  Title:      Doc/Tutorial/Protocol/Public.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1996  University of Cambridge

Theory of Public Keys (common to all public-key protocols)

Private and public keys; initial states of agents
*)
theory Public imports Event
begin
(*>*)

text \<open>
The function
\<open>pubK\<close> maps agents to their public keys.  The function
\<open>priK\<close> maps agents to their private keys.  It is merely
an abbreviation (cf.\ \S\ref{sec:abbreviations}) defined in terms of
\<open>invKey\<close> and \<open>pubK\<close>.
\<close>

consts pubK :: "agent \ key"
abbreviation priK :: "agent \ key"
where "priK x \ invKey(pubK x)"
(*<*)
overloading initState \<equiv> initState
begin

primrec initState where
        (*Agents know their private key and all public keys*)
  initState_Server:  "initState Server =
                         insert (Key (priK Server)) (Key ` range pubK)"
| initState_Friend:  "initState (Friend i) =
                         insert (Key (priK (Friend i))) (Key ` range pubK)"
| initState_Spy:     "initState Spy =
                         (Key`invKey`pubK`bad) \<union> (Key ` range pubK)"

end
(*>*)

text \<open>
\noindent
The set \<open>bad\<close> consists of those agents whose private keys are known to
the spy.

Two axioms are asserted about the public-key cryptosystem.
No two agents have the same public key, and no private key equals
any public key.
\<close>

axiomatization where
  inj_pubK:        "inj pubK" and
  priK_neq_pubK:   "priK A \ pubK B"
(*<*)
lemmas [iff] = inj_pubK [THEN inj_eq]

lemma priK_inj_eq[iff]: "(priK A = priK B) = (A=B)"
  apply safe
  apply (drule_tac f=invKey in arg_cong)
  apply simp
  done

lemmas [iff] = priK_neq_pubK priK_neq_pubK [THEN not_sym]

lemma not_symKeys_pubK[iff]: "pubK A \ symKeys"
  by (simp add: symKeys_def)

lemma not_symKeys_priK[iff]: "priK A \ symKeys"
  by (simp add: symKeys_def)

lemma symKeys_neq_imp_neq: "(K \ symKeys) \ (K' \ symKeys) \ K \ K'"
  by blast

lemma analz_symKeys_Decrypt: "[| Crypt K X \ analz H; K \ symKeys; Key K \ analz H |]
     ==> X \<in> analz H"
  by (auto simp add: symKeys_def)

(** "Image" equations that hold for injective functions **)

lemma invKey_image_eq[simp]: "(invKey x \ invKey`A) = (x\A)"
  by auto

(*holds because invKey is injective*)
lemma pubK_image_eq[simp]: "(pubK x \ pubK`A) = (x\A)"
  by auto

lemma priK_pubK_image_eq[simp]: "(priK x \ pubK`A)"
  by auto

(** Rewrites should not refer to  initState(Friend i)
    -- not in normal form! **)

lemma keysFor_parts_initState[simp]: "keysFor (parts (initState C)) = {}"
  apply (unfold keysFor_def)
  apply (induct C)
  apply (auto intro: range_eqI)
  done

(*** Function "spies" ***)

(*Agents see their own private keys!*)
lemma priK_in_initState[iff]: "Key (priK A) \ initState A"
  by (induct A) auto

(*All public keys are visible*)
lemma spies_pubK[iff]: "Key (pubK A) \ spies evs"
  by (induct evs) (simp_all add: imageI knows_Cons split: event.split)

(*Spy sees private keys of bad agents!*)
lemma Spy_spies_bad[intro!]: "A \ bad \ Key (priK A) \ spies evs"
  by (induct evs) (simp_all add: imageI knows_Cons split: event.split)

lemmas [iff] = spies_pubK [THEN analz.Inj]

(*** Fresh nonces ***)

lemma Nonce_notin_initState[iff]: "Nonce N \ parts (initState B)"
  by (induct B) auto

lemma Nonce_notin_used_empty[simp]: "Nonce N \ used []"
  by (simp add: used_Nil)

(*** Supply fresh nonces for possibility theorems. ***)

(*In any trace, there is an upper bound N on the greatest nonce in use.*)
lemma Nonce_supply_lemma: "\N. \n. N\n \ Nonce n \ used evs"
apply (induct_tac "evs")
apply (rule_tac x = 0 in exI)
apply (simp_all (no_asm_simp) add: used_Cons split: event.split)
apply safe
apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
done

lemma Nonce_supply1: "\N. Nonce N \ used evs"
by (rule Nonce_supply_lemma [THEN exE], blast)

lemma Nonce_supply: "Nonce (SOME N. Nonce N \ used evs) \ used evs"
apply (rule Nonce_supply_lemma [THEN exE])
apply (rule someI, fast)
done

(*** Specialized rewriting for the analz_image_... theorems ***)

lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} \ H"
  by blast

lemma insert_Key_image: "insert (Key K) (Key`KK \ C) = Key ` (insert K KK) \ C"
  by blast

(*Specialized methods*)

(*Tactic for possibility theorems*)
ML \<open>
fun possibility_tac ctxt =
    REPEAT (*omit used_Says so that Nonces start from different traces!*)
    (ALLGOALS (simp_tac (ctxt delsimps [used_Says]))
     THEN
     REPEAT_FIRST (eq_assume_tac ORELSE'
                   resolve_tac ctxt [refl, conjI, @{thm Nonce_supply}]));
\<close>

method_setup possibility = \<open>Scan.succeed (SIMPLE_METHOD o possibility_tac)\<close>
    "for proving possibility theorems"

end
(*>*)

quality100%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.