src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy
author wenzelm
Wed Apr 10 21:20:35 2013 +0200 (2013-04-10)
changeset 51692 ecd34f863242
parent 48618 1f7e068b4613
child 61984 cdea44c775fa
permissions -rw-r--r--
tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side;
declare command "print_case_translations" where it is actually defined;
     1 theory Needham_Schroeder_Guided_Attacker_Example
     2 imports Needham_Schroeder_Base
     3 begin
     4 
     5 inductive_set ns_public :: "event list set"
     6   where
     7          (*Initial trace is empty*)
     8    Nil:  "[] \<in> ns_public"
     9 
    10  | Fake_NS1:  "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<in> analz (spies evs1) \<rbrakk>
    11           \<Longrightarrow> Says Spy B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
    12                 # evs1  \<in> ns_public"
    13  | Fake_NS2:  "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<in> analz (spies evs1); Nonce NB \<in> analz (spies evs1) \<rbrakk>
    14           \<Longrightarrow> Says Spy A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
    15                 # evs1  \<in> ns_public"
    16 
    17          (*Alice initiates a protocol run, sending a nonce to Bob*)
    18  | NS1:  "\<lbrakk>evs1 \<in> ns_public;  Nonce NA \<notin> used evs1\<rbrakk>
    19           \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
    20                 # evs1  \<in>  ns_public"
    21          (*Bob responds to Alice's message with a further nonce*)
    22  | NS2:  "\<lbrakk>evs2 \<in> ns_public;  Nonce NB \<notin> used evs2;
    23            Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
    24           \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
    25                 # evs2  \<in>  ns_public"
    26 
    27          (*Alice proves her existence by sending NB back to Bob.*)
    28  | NS3:  "\<lbrakk>evs3 \<in> ns_public;
    29            Says A  B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
    30            Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
    31           \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
    32 
    33 declare ListMem_iff[symmetric, code_pred_inline]
    34 
    35 lemmas [code_pred_intro] = ns_publicp.intros[folded synth'_def]
    36 
    37 code_pred [skip_proof] ns_publicp unfolding synth'_def by (rule ns_publicp.cases) fastforce+
    38 thm ns_publicp.equation
    39 
    40 code_pred [generator_cps] ns_publicp .
    41 thm ns_publicp.generator_cps_equation
    42 
    43 
    44 lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs"
    45 quickcheck[smart_exhaustive, depth = 5, timeout = 100, expect = counterexample]
    46 (*quickcheck[narrowing, size = 6, timeout = 200, verbose, expect = no_counterexample]*)
    47 oops
    48 
    49 lemma
    50   "\<lbrakk>ns_publicp evs\<rbrakk>            
    51        \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs
    52        \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B 
    53            \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
    54 (*quickcheck[smart_exhaustive, depth = 6, timeout = 100, expect = counterexample]
    55 quickcheck[narrowing, size = 7, timeout = 200, expect = no_counterexample]*)
    56 oops
    57 
    58 section {* Proving the counterexample trace for validation *}
    59 
    60 lemma
    61   assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1"
    62   assumes "evs = 
    63   [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)),
    64    Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}),
    65    Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}),
    66    Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|})]" (is "_ = [?e3, ?e2, ?e1, ?e0]")
    67   shows "A \<noteq> Spy" "B \<noteq> Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)"
    68 proof -
    69   from assms show "A \<noteq> Spy" by auto
    70   from assms show "B \<noteq> Spy" by auto
    71   have "[] : ns_public" by (rule Nil)
    72   then have first_step: "[?e0] : ns_public"
    73   proof (rule NS1)
    74     show "Nonce 0 ~: used []" by eval
    75   qed
    76   then have "[?e1, ?e0] : ns_public"
    77   proof (rule Fake_NS1)
    78     show "Nonce 0 : analz (knows Spy [?e0])" by eval
    79   qed
    80   then have "[?e2, ?e1, ?e0] : ns_public"
    81   proof (rule NS2)
    82     show "Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}) \<in> set [?e1, ?e0]" by simp
    83     show " Nonce 1 ~: used [?e1, ?e0]" by eval
    84   qed
    85   then show "evs : ns_public"
    86   unfolding assms
    87   proof (rule NS3)
    88     show "  Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|}) \<in> set [?e2, ?e1, ?e0]" by simp
    89     show "Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|})
    90     : set [?e2, ?e1, ?e0]" by simp
    91   qed
    92   from assms show "Nonce NB : analz (knows Spy evs)"
    93     apply simp
    94     apply (rule analz.intros(4))
    95     apply (rule analz.intros(1))
    96     apply (auto simp add: bad_def)
    97     done
    98 qed
    99 
   100 end