src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Unguided_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_Unguided_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:  "\<lbrakk>evs1 \<in> ns_public; X \<in> synth (analz (spies evs1)) \<rbrakk>
    11           \<Longrightarrow> Says Spy A X # evs1  \<in> ns_public"
    12 
    13          (*Alice initiates a protocol run, sending a nonce to Bob*)
    14  | NS1:  "\<lbrakk>evs1 \<in> ns_public;  Nonce NA \<notin> used evs1\<rbrakk>
    15           \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
    16                 # evs1  \<in>  ns_public"
    17          (*Bob responds to Alice's message with a further nonce*)
    18  | NS2:  "\<lbrakk>evs2 \<in> ns_public;  Nonce NB \<notin> used evs2;
    19            Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
    20           \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
    21                 # evs2  \<in>  ns_public"
    22 
    23          (*Alice proves her existence by sending NB back to Bob.*)
    24  | NS3:  "\<lbrakk>evs3 \<in> ns_public;
    25            Says A  B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
    26            Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
    27           \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
    28 
    29 declare ListMem_iff[symmetric, code_pred_inline]
    30 
    31 lemmas [code_pred_intro] = ns_publicp.intros[folded synth'_def]
    32 
    33 code_pred [skip_proof] ns_publicp unfolding synth'_def by (rule ns_publicp.cases) fastforce+
    34 thm ns_publicp.equation
    35 
    36 code_pred [generator_cps] ns_publicp .
    37 thm ns_publicp.generator_cps_equation
    38 
    39 
    40 lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs"
    41 quickcheck[smart_exhaustive, depth = 5, timeout = 200, expect = counterexample]
    42 (*quickcheck[narrowing, size = 6, timeout = 200, verbose, expect = no_counterexample]*)
    43 oops
    44 
    45 lemma
    46   "\<lbrakk>ns_publicp evs\<rbrakk>            
    47        \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs
    48        \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B 
    49            \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
    50 quickcheck[smart_exhaustive, depth = 6, timeout = 100, expect = no_counterexample]
    51 (*quickcheck[narrowing, size = 7, timeout = 200, expect = no_counterexample]*)
    52 oops
    53 
    54 section {* Proving the counterexample trace for validation *}
    55 
    56 lemma
    57   assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1"
    58   assumes "evs = 
    59   [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)),
    60    Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}),
    61    Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}),
    62    Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|})]" (is "_ = [?e3, ?e2, ?e1, ?e0]")
    63   shows "A \<noteq> Spy" "B \<noteq> Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)"
    64 proof -
    65   from assms show "A \<noteq> Spy" by auto
    66   from assms show "B \<noteq> Spy" by auto
    67   have "[] : ns_public" by (rule Nil)
    68   then have first_step: "[?e0] : ns_public"
    69   proof (rule NS1)
    70     show "Nonce 0 ~: used []" by eval
    71   qed
    72   then have "[?e1, ?e0] : ns_public"
    73   proof (rule Fake)
    74     show "Crypt (pubEK Bob) {|Nonce 0, Agent Alice|} : synth (analz (knows Spy [?e0]))"
    75       by (intro synth.intros(2,3,4,1)) eval+
    76   qed
    77   then have "[?e2, ?e1, ?e0] : ns_public"
    78   proof (rule NS2)
    79     show "Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}) \<in> set [?e1, ?e0]" by simp
    80     show " Nonce 1 ~: used [?e1, ?e0]" by eval
    81   qed
    82   then show "evs : ns_public"
    83   unfolding assms
    84   proof (rule NS3)
    85     show "  Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|}) \<in> set [?e2, ?e1, ?e0]" by simp
    86     show "Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}) : set [?e2, ?e1, ?e0]" by simp
    87   qed
    88   from assms show "Nonce NB : analz (knows Spy evs)"
    89     apply simp
    90     apply (rule analz.intros(4))
    91     apply (rule analz.intros(1))
    92     apply (auto simp add: bad_def)
    93     done
    94 qed
    95 
    96 end