src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_No_Attacker_Example.thy
author wenzelm
Tue, 16 Jan 2018 09:58:17 +0100
changeset 67445 4311845b0412
parent 62286 705d4c4003ea
permissions -rw-r--r--
tuned document;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48224
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
     1
theory Needham_Schroeder_No_Attacker_Example
48618
1f7e068b4613 moved another larger quickcheck example to Quickcheck_Benchmark
bulwahn
parents: 48243
diff changeset
     2
imports Needham_Schroeder_Base
48224
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
     3
begin
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
     4
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
     5
inductive_set ns_public :: "event list set"
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
     6
  where
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
     7
         (*Initial trace is empty*)
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
     8
   Nil:  "[] \<in> ns_public"
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
     9
         (*Alice initiates a protocol run, sending a nonce to Bob*)
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    10
 | NS1:  "\<lbrakk>evs1 \<in> ns_public;  Nonce NA \<notin> used evs1\<rbrakk>
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    11
          \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    12
                # evs1  \<in>  ns_public"
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    13
         (*Bob responds to Alice's message with a further nonce*)
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    14
 | NS2:  "\<lbrakk>evs2 \<in> ns_public;  Nonce NB \<notin> used evs2;
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    15
           Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    16
          \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    17
                # evs2  \<in>  ns_public"
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    18
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    19
         (*Alice proves her existence by sending NB back to Bob.*)
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    20
 | NS3:  "\<lbrakk>evs3 \<in> ns_public;
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    21
           Says A  B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    22
           Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    23
          \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    24
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    25
code_pred [skip_proof] ns_publicp .
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    26
thm ns_publicp.equation
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    27
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    28
code_pred [generator_cps] ns_publicp .
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    29
thm ns_publicp.generator_cps_equation
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    30
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    31
lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs"
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    32
(*quickcheck[random, iterations = 1000000, size = 20, timeout = 3600, verbose]
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    33
quickcheck[exhaustive, size = 8, timeout = 3600, verbose]
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    34
quickcheck[narrowing, size = 7, timeout = 3600, verbose]*)
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    35
quickcheck[smart_exhaustive, depth = 5, timeout = 30, expect = counterexample]
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    36
oops
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    37
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    38
lemma
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    39
  "\<lbrakk>ns_publicp evs\<rbrakk>            
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    40
       \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    41
       \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B 
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    42
           \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    43
quickcheck[smart_exhaustive, depth = 6, timeout = 30]
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    44
quickcheck[narrowing, size = 6, timeout = 30, verbose]
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    45
oops
f2dd90cc724b adding an example using Quickcheck to find a valid trace for the needham-schroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff changeset
    46
48618
1f7e068b4613 moved another larger quickcheck example to Quickcheck_Benchmark
bulwahn
parents: 48243
diff changeset
    47
end