src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy
author traytel
Mon, 24 Oct 2016 16:53:32 +0200
changeset 64379 71f42dcaa1df
parent 62290 658276428cfc
child 67399 eab6ce8368fa
permissions -rw-r--r--
additional user-specified simp (naturality) rules used in friend_of_corec
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48243
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
     1
theory Needham_Schroeder_Guided_Attacker_Example
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
     2
imports Needham_Schroeder_Base
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
     3
begin
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
     4
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
     5
inductive_set ns_public :: "event list set"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
     6
  where
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
     7
         (*Initial trace is empty*)
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
     8
   Nil:  "[] \<in> ns_public"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
     9
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    10
 | Fake_NS1:  "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<in> analz (spies evs1) \<rbrakk>
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    11
          \<Longrightarrow> Says Spy B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    12
                # evs1  \<in> ns_public"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    13
 | Fake_NS2:  "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<in> analz (spies evs1); Nonce NB \<in> analz (spies evs1) \<rbrakk>
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    14
          \<Longrightarrow> Says Spy A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    15
                # evs1  \<in> ns_public"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    16
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    17
         (*Alice initiates a protocol run, sending a nonce to Bob*)
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    18
 | NS1:  "\<lbrakk>evs1 \<in> ns_public;  Nonce NA \<notin> used evs1\<rbrakk>
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    19
          \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    20
                # evs1  \<in>  ns_public"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    21
         (*Bob responds to Alice's message with a further nonce*)
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    22
 | NS2:  "\<lbrakk>evs2 \<in> ns_public;  Nonce NB \<notin> used evs2;
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    23
           Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    24
          \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    25
                # evs2  \<in>  ns_public"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    26
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    27
         (*Alice proves her existence by sending NB back to Bob.*)
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    28
 | NS3:  "\<lbrakk>evs3 \<in> ns_public;
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    29
           Says A  B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    30
           Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    31
          \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    32
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    33
declare ListMem_iff[symmetric, code_pred_inline]
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    34
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    35
lemmas [code_pred_intro] = ns_publicp.intros[folded synth'_def]
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    36
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    37
code_pred [skip_proof] ns_publicp unfolding synth'_def by (rule ns_publicp.cases) fastforce+
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    38
thm ns_publicp.equation
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    39
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    40
code_pred [generator_cps] ns_publicp .
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    41
thm ns_publicp.generator_cps_equation
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    42
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    43
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    44
lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    45
quickcheck[smart_exhaustive, depth = 5, timeout = 100, expect = counterexample]
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    46
(*quickcheck[narrowing, size = 6, timeout = 200, verbose, expect = no_counterexample]*)
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    47
oops
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    48
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    49
lemma
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    50
  "\<lbrakk>ns_publicp evs\<rbrakk>            
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    51
       \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    52
       \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B 
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    53
           \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    54
(*quickcheck[smart_exhaustive, depth = 6, timeout = 100, expect = counterexample]
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    55
quickcheck[narrowing, size = 7, timeout = 200, expect = no_counterexample]*)
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    56
oops
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    57
62290
658276428cfc isabelle update_cartouches -c -t;
wenzelm
parents: 62286
diff changeset
    58
section \<open>Proving the counterexample trace for validation\<close>
48243
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    59
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    60
lemma
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    61
  assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    62
  assumes "evs = 
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    63
  [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)),
61984
cdea44c775fa more symbols;
wenzelm
parents: 48618
diff changeset
    64
   Says Bob Alice (Crypt (pubEK Alice) \<lbrace>Nonce 0, Nonce 1\<rbrace>),
cdea44c775fa more symbols;
wenzelm
parents: 48618
diff changeset
    65
   Says Spy Bob (Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace>),
cdea44c775fa more symbols;
wenzelm
parents: 48618
diff changeset
    66
   Says Alice Spy (Crypt (pubEK Spy) \<lbrace>Nonce 0, Agent Alice\<rbrace>)]" (is "_ = [?e3, ?e2, ?e1, ?e0]")
48243
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    67
  shows "A \<noteq> Spy" "B \<noteq> Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    68
proof -
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    69
  from assms show "A \<noteq> Spy" by auto
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    70
  from assms show "B \<noteq> Spy" by auto
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    71
  have "[] : ns_public" by (rule Nil)
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    72
  then have first_step: "[?e0] : ns_public"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    73
  proof (rule NS1)
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    74
    show "Nonce 0 ~: used []" by eval
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    75
  qed
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    76
  then have "[?e1, ?e0] : ns_public"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    77
  proof (rule Fake_NS1)
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    78
    show "Nonce 0 : analz (knows Spy [?e0])" by eval
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    79
  qed
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    80
  then have "[?e2, ?e1, ?e0] : ns_public"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    81
  proof (rule NS2)
61984
cdea44c775fa more symbols;
wenzelm
parents: 48618
diff changeset
    82
    show "Says Spy Bob (Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace>) \<in> set [?e1, ?e0]" by simp
48243
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    83
    show " Nonce 1 ~: used [?e1, ?e0]" by eval
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    84
  qed
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    85
  then show "evs : ns_public"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    86
  unfolding assms
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    87
  proof (rule NS3)
61984
cdea44c775fa more symbols;
wenzelm
parents: 48618
diff changeset
    88
    show "  Says Alice Spy (Crypt (pubEK Spy) \<lbrace>Nonce 0, Agent Alice\<rbrace>) \<in> set [?e2, ?e1, ?e0]" by simp
cdea44c775fa more symbols;
wenzelm
parents: 48618
diff changeset
    89
    show "Says Bob Alice (Crypt (pubEK Alice) \<lbrace>Nonce 0, Nonce 1\<rbrace>)
48243
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    90
    : set [?e2, ?e1, ?e0]" by simp
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    91
  qed
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    92
  from assms show "Nonce NB : analz (knows Spy evs)"
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    93
    apply simp
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    94
    apply (rule analz.intros(4))
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    95
    apply (rule analz.intros(1))
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    96
    apply (auto simp add: bad_def)
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    97
    done
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    98
qed
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
    99
b149de01d669 adding three variants of the Needham-Schroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff changeset
   100
end