# Theory Needham_Schroeder_No_Attacker_Example

theory Needham_Schroeder_No_Attacker_Example
imports Needham_Schroeder_Base
```theory Needham_Schroeder_No_Attacker_Example
imports Needham_Schroeder_Base
begin

inductive_set ns_public :: "event list set"
where
(*Initial trace is empty*)
Nil:  "[] ∈ ns_public"
(*Alice initiates a protocol run, sending a nonce to Bob*)
| NS1:  "⟦evs1 ∈ ns_public;  Nonce NA ∉ used evs1⟧
⟹ Says A B (Crypt (pubEK B) ⦃Nonce NA, Agent A⦄)
# evs1  ∈  ns_public"
(*Bob responds to Alice's message with a further nonce*)
| NS2:  "⟦evs2 ∈ ns_public;  Nonce NB ∉ used evs2;
Says A' B (Crypt (pubEK B) ⦃Nonce NA, Agent A⦄) ∈ set evs2⟧
⟹ Says B A (Crypt (pubEK A) ⦃Nonce NA, Nonce NB⦄)
# evs2  ∈  ns_public"

(*Alice proves her existence by sending NB back to Bob.*)
| NS3:  "⟦evs3 ∈ ns_public;
Says A  B (Crypt (pubEK B) ⦃Nonce NA, Agent A⦄) ∈ set evs3;
Says B' A (Crypt (pubEK A) ⦃Nonce NA, Nonce NB⦄) ∈ set evs3⟧
⟹ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 ∈ ns_public"

code_pred [skip_proof] ns_publicp .
thm ns_publicp.equation

code_pred [generator_cps] ns_publicp .
thm ns_publicp.generator_cps_equation

lemma "ns_publicp evs ==> ¬ (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs"
(*quickcheck[random, iterations = 1000000, size = 20, timeout = 3600, verbose]
quickcheck[exhaustive, size = 8, timeout = 3600, verbose]
quickcheck[narrowing, size = 7, timeout = 3600, verbose]*)
quickcheck[smart_exhaustive, depth = 5, timeout = 30, expect = counterexample]
oops

lemma
"⟦ns_publicp evs⟧
⟹ Says B A (Crypt (pubEK A) ⦃Nonce NA, Nonce NB⦄) : set evs
⟹ A ≠ Spy ⟹ B ≠ Spy ⟹ A ≠ B
⟹ Nonce NB ∉ analz (spies evs)"
quickcheck[smart_exhaustive, depth = 6, timeout = 30]
quickcheck[narrowing, size = 6, timeout = 30, verbose]
oops

end
```