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