src/HOL/Quickcheck_Benchmark/Needham_Schroeder_No_Attacker_Example.thy
author wenzelm
Wed Apr 10 21:20:35 2013 +0200 (2013-04-10)
changeset 51692 ecd34f863242
parent 48618 1f7e068b4613
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_No_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          (*Alice initiates a protocol run, sending a nonce to Bob*)
    10  | NS1:  "\<lbrakk>evs1 \<in> ns_public;  Nonce NA \<notin> used evs1\<rbrakk>
    11           \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
    12                 # evs1  \<in>  ns_public"
    13          (*Bob responds to Alice's message with a further nonce*)
    14  | NS2:  "\<lbrakk>evs2 \<in> ns_public;  Nonce NB \<notin> used evs2;
    15            Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
    16           \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
    17                 # evs2  \<in>  ns_public"
    18 
    19          (*Alice proves her existence by sending NB back to Bob.*)
    20  | NS3:  "\<lbrakk>evs3 \<in> ns_public;
    21            Says A  B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
    22            Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
    23           \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"
    24 
    25 code_pred [skip_proof] ns_publicp .
    26 thm ns_publicp.equation
    27 
    28 code_pred [generator_cps] ns_publicp .
    29 thm ns_publicp.generator_cps_equation
    30 
    31 lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs"
    32 (*quickcheck[random, iterations = 1000000, size = 20, timeout = 3600, verbose]
    33 quickcheck[exhaustive, size = 8, timeout = 3600, verbose]
    34 quickcheck[narrowing, size = 7, timeout = 3600, verbose]*)
    35 quickcheck[smart_exhaustive, depth = 5, timeout = 30, expect = counterexample]
    36 oops
    37 
    38 lemma
    39   "\<lbrakk>ns_publicp evs\<rbrakk>            
    40        \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs
    41        \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B 
    42            \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
    43 quickcheck[smart_exhaustive, depth = 6, timeout = 30]
    44 quickcheck[narrowing, size = 6, timeout = 30, verbose]
    45 oops
    46 
    47 end