Theory sklvl1
section ‹SKEME Protocol (L1)›
theory sklvl1
imports dhlvl1
begin
declare option.split_asm [split]
subsection ‹State and Events›
abbreviation ni :: nat where "ni ≡ 4"
abbreviation nr :: nat where "nr ≡ 5"
text ‹Proofs break if @{term "1"} is used, because @{method "simp"} replaces it with
@{term "Suc 0"}\dots.›
abbreviation
"xni ≡ Var 7"
abbreviation
"xnr ≡ Var 8"
text ‹Domain of each role (protocol-dependent).›
fun domain :: "role_t ⇒ var set" where
"domain Init = {xnx, xni, xnr, xgnx, xgny, xsk, xEnd}"
| "domain Resp = {xny, xni, xnr, xgnx, xgny, xsk, xEnd}"
consts
guessed_frame :: "rid_t ⇒ frame"
text ‹Specification of the guessed frame:
\begin{enumerate}
\item Domain.
\item Well-typedness.
The messages in the frame of a run never contain implementation material
even if the agents of the run are dishonest.
Therefore we consider only well-typed frames.
This is notably required for the session key compromise; it also helps proving
the partitionning of ik,
since we know that the messages added by the protocol do not contain ltkeys in their
payload and are therefore valid implementations.
\item We also ensure that the values generated by the frame owner are correctly guessed.
\item The new frame extends the previous one (from @{theory Key_Agreement_Strong_Adversaries.dhlvl1})
\end{enumerate}
›
specification (guessed_frame)
guessed_frame_dom_spec [simp]:
"dom (guessed_frame R) = domain (role (guessed_runs R))"
guessed_frame_payload_spec [simp, elim]:
"guessed_frame R x = Some y ⟹ y ∈ payload"
guessed_frame_Init_xnx [simp]:
"role (guessed_runs R) = Init ⟹ guessed_frame R xnx = Some (NonceF (R$nx))"
guessed_frame_Init_xgnx [simp]:
"role (guessed_runs R) = Init ⟹ guessed_frame R xgnx = Some (Exp Gen (NonceF (R$nx)))"
guessed_frame_Init_xni [simp]:
"role (guessed_runs R) = Init ⟹ guessed_frame R xni = Some (NonceF (R$ni))"
guessed_frame_Resp_xny [simp]:
"role (guessed_runs R) = Resp ⟹ guessed_frame R xny = Some (NonceF (R$ny))"
guessed_frame_Resp_xgny [simp]:
"role (guessed_runs R) = Resp ⟹ guessed_frame R xgny = Some (Exp Gen (NonceF (R$ny)))"
guessed_frame_Resp_xnr [simp]:
"role (guessed_runs R) = Resp ⟹ guessed_frame R xnr = Some (NonceF (R$nr))"
guessed_frame_xEnd [simp]:
"guessed_frame R xEnd = Some End"
guessed_frame_eq [simp]:
"x ∈ {xnx, xny, xgnx, xgny, xsk, xEnd} ⟹ dhlvl1.guessed_frame R x = guessed_frame R x"
apply (rule exI [of _
"λR.
if role (guessed_runs R) = Init then
(dhlvl1.guessed_frame R) (xni ↦ NonceF (R$ni), xnr ↦ End)
else
(dhlvl1.guessed_frame R) (xnr ↦ NonceF (R$nr), xni ↦ End)"],
auto simp add: domIff intro: role_t.exhaust)
done
record skl1_state =
l1_state +
signalsInit2 :: "signal ⇒ nat"
signalsResp2 :: "signal ⇒ nat"
type_synonym skl1_obs = "skl1_state"
text ‹Protocol events:
\begin{itemize}
\item step 1: create @{term "Ra"}, @{term "A"} generates @{term "nx"} and @{term "ni"},
computes $@{term "g"}^@{term "nx"}$
\item step 2: create @{term "Rb"}, @{term "B"} reads @{term "ni"} and $@{term "g"}^@{term "nx"}$
insecurely,
generates @{term "ny"} and @{term "nr"}, computes $@{term "g"}^@{term "ny"}$,
computes $@{term "g"}^@{term "nx*ny"}$,
emits a running signal for @{term "Init"}, @{term "ni"}, @{term "nr"}, $@{term "g"}^@{term "nx*ny"}$
\item step 3: @{term "A"} reads $@{term "g"}^@{term "ny"}$ and $@{term "g"}^@{term "nx"}$
authentically,
computes $@{term "g"}^@{term "ny*nx"}$, emits a commit signal for @{term "Init"}, @{term "ni"},
@{term "nr"}, $@{term "g"}^@{term "ny*nx"}$,
a running signal for @{term "Resp"}, @{term "ni"}, @{term "nr"}, $@{term "g"}^@{term "ny*nx"}$,
declares the secret $@{term "g"}^@{term "ny*nx"}$
\item step 4: @{term "B"} reads @{term "nr"}, @{term "ni"}, $@{term "g"}^@{term "nx"}$
and $@{term "g"}^@{term "ny"}$ authentically,
emits a commit signal for @{term "Resp"}, @{term "ni"}, @{term "nr"},
$@{term "g"}^@{term "nx*ny"}$,
declares the secret $@{term "g"}^@{term "nx*ny"}$
\end{itemize}
›
definition
skl1_step1 :: "rid_t ⇒ agent ⇒ agent ⇒ ('a skl1_state_scheme * 'a skl1_state_scheme) set"
where
"skl1_step1 Ra A B ≡ {(s, s').
Ra ∉ dom (progress s) ∧
guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ∧
s' = s⦇
progress := (progress s)(Ra ↦ {xnx, xni, xgnx})
⦈
}"
definition
skl1_step2 ::
"rid_t ⇒ agent ⇒ agent ⇒ msg ⇒ msg ⇒ ('a skl1_state_scheme * 'a skl1_state_scheme) set"
where
"skl1_step2 Rb A B Ni gnx ≡ {(s, s').
guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ∧
Rb ∉ dom (progress s) ∧
guessed_frame Rb xgnx = Some gnx ∧
guessed_frame Rb xni = Some Ni ∧
guessed_frame Rb xsk = Some (Exp gnx (NonceF (Rb$ny))) ∧
s' = s⦇ progress := (progress s)(Rb ↦ {xny, xni, xnr, xgny, xgnx, xsk}),
signalsInit :=
if can_signal s A B then
addSignal (signalsInit s)
(Running A B ⟨Ni, NonceF (Rb$nr), Exp gnx (NonceF (Rb$ny))⟩)
else
signalsInit s,
signalsInit2 :=
if can_signal s A B then
addSignal (signalsInit2 s) (Running A B (Exp gnx (NonceF (Rb$ny))))
else
signalsInit2 s
⦈
}"
definition
skl1_step3 ::
"rid_t ⇒ agent ⇒ agent ⇒ msg ⇒ msg ⇒ ('a skl1_state_scheme * 'a skl1_state_scheme) set"
where
"skl1_step3 Ra A B Nr gny ≡ {(s, s').
guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ∧
progress s Ra = Some {xnx, xni, xgnx} ∧
guessed_frame Ra xgny = Some gny ∧
guessed_frame Ra xnr = Some Nr ∧
guessed_frame Ra xsk = Some (Exp gny (NonceF (Ra$nx))) ∧
(can_signal s A B ⟶
(∃ Rb. guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ∧
in_progressS (progress s Rb) {xny, xni, xnr, xgnx, xgny, xsk} ∧
guessed_frame Rb xgny = Some gny ∧
guessed_frame Rb xnr = Some Nr ∧
guessed_frame Rb xni = Some (NonceF (Ra$ni)) ∧
guessed_frame Rb xgnx = Some (Exp Gen (NonceF (Ra$nx))))) ∧
(Ra = test ⟶ Exp gny (NonceF (Ra$nx)) ∉ synth (analz (ik s))) ∧
s' = s⦇ progress := (progress s)(Ra ↦ {xnx, xni, xnr, xgnx, xgny, xsk, xEnd}),
secret := {x. x = Exp gny (NonceF (Ra$nx)) ∧ Ra = test} ∪ secret s,
signalsInit :=
if can_signal s A B then
addSignal (signalsInit s)
(Commit A B ⟨NonceF (Ra$ni), Nr, Exp gny (NonceF (Ra$nx))⟩)
else
signalsInit s,
signalsInit2 :=
if can_signal s A B then
addSignal (signalsInit2 s) (Commit A B (Exp gny (NonceF (Ra$nx))))
else
signalsInit2 s,
signalsResp :=
if can_signal s A B then
addSignal (signalsResp s)
(Running A B ⟨NonceF (Ra$ni), Nr, Exp gny (NonceF (Ra$nx))⟩)
else
signalsResp s,
signalsResp2 :=
if can_signal s A B then
addSignal (signalsResp2 s) (Running A B (Exp gny (NonceF (Ra$nx))))
else
signalsResp2 s
⦈
}"
definition
skl1_step4 ::
"rid_t ⇒ agent ⇒ agent ⇒ msg ⇒ msg ⇒ ('a skl1_state_scheme * 'a skl1_state_scheme) set"
where
"skl1_step4 Rb A B Ni gnx ≡ {(s, s').
guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ∧
progress s Rb = Some {xny, xni, xnr, xgnx, xgny, xsk} ∧
guessed_frame Rb xgnx = Some gnx ∧
guessed_frame Rb xni = Some Ni ∧
(can_signal s A B ⟶
(∃ Ra. guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ∧
in_progressS (progress s Ra) {xnx, xni, xnr, xgnx, xgny, xsk, xEnd} ∧
guessed_frame Ra xgnx = Some gnx ∧
guessed_frame Ra xni = Some Ni ∧
guessed_frame Ra xnr = Some (NonceF (Rb$nr)) ∧
guessed_frame Ra xgny = Some (Exp Gen (NonceF (Rb$ny))))) ∧
(Rb = test ⟶ Exp gnx (NonceF (Rb$ny)) ∉ synth (analz (ik s))) ∧
s' = s⦇ progress := (progress s)(Rb ↦ {xny, xni, xnr, xgnx, xgny, xsk, xEnd}),
secret := {x. x = Exp gnx (NonceF (Rb$ny)) ∧ Rb = test} ∪ secret s,
signalsResp :=
if can_signal s A B then
addSignal (signalsResp s)
(Commit A B ⟨Ni, NonceF (Rb$nr), Exp gnx (NonceF (Rb$ny))⟩)
else
signalsResp s,
signalsResp2 :=
if can_signal s A B then
addSignal (signalsResp2 s) (Commit A B (Exp gnx (NonceF (Rb$ny))))
else
signalsResp2 s
⦈
}"
text ‹Specification.›
definition
skl1_trans :: "('a skl1_state_scheme * 'a skl1_state_scheme) set" where
"skl1_trans ≡ (⋃m Ra Rb A B x y.
skl1_step1 Ra A B ∪
skl1_step2 Rb A B x y ∪
skl1_step3 Ra A B x y ∪
skl1_step4 Rb A B x y ∪
l1_learn m ∪
Id
)"
definition
skl1_init :: "skl1_state set"
where
"skl1_init ≡ { ⦇
ik = {},
secret = {},
progress = Map.empty,
signalsInit = λx. 0,
signalsResp = λx. 0,
signalsInit2 = λx. 0,
signalsResp2 = λx. 0
⦈ }"
definition
skl1 :: "(skl1_state, skl1_obs) spec" where
"skl1 ≡ ⦇
init = skl1_init,
trans = skl1_trans,
obs = id
⦈"
lemmas skl1_defs =
skl1_def skl1_init_def skl1_trans_def
l1_learn_def
skl1_step1_def skl1_step2_def skl1_step3_def skl1_step4_def
lemmas skl1_nostep_defs =
skl1_def skl1_init_def skl1_trans_def
lemma skl1_obs_id [simp]: "obs skl1 = id"
by (simp add: skl1_def)
lemma run_ended_trans:
"run_ended (progress s R) ⟹
(s, s') ∈ trans skl1 ⟹
run_ended (progress s' R)"
by (auto simp add: skl1_nostep_defs)
(auto simp add: skl1_defs ik_dy_def domIff)
lemma can_signal_trans:
"can_signal s' A B ⟹
(s, s') ∈ trans skl1 ⟹
can_signal s A B"
by (auto simp add: can_signal_def run_ended_trans)
subsection ‹Refinement: secrecy›
fun option_inter :: "var set ⇒ var set option ⇒ var set option"
where
"option_inter S (Some x) = Some (x ∩ S)"
|"option_inter S None = None"
definition med_progress :: "progress_t ⇒ progress_t"
where
"med_progress r ≡ λ R. option_inter {xnx, xny, xgnx, xgny, xsk, xEnd} (r R)"
lemma med_progress_upd [simp]:
"med_progress (r(R ↦ S)) = (med_progress r) (R ↦ S ∩ {xnx, xny, xgnx, xgny, xsk, xEnd})"
by (auto simp add: med_progress_def)
lemma med_progress_Some:
"r x = Some s ⟹ med_progress r x = Some (s ∩ {xnx, xny, xgnx, xgny, xsk, xEnd})"
by (auto simp add: med_progress_def)
lemma med_progress_None [simp]: "med_progress r x = None ⟷ r x = None"
by (cases "r x", auto simp add: med_progress_def)
lemma med_progress_Some2 [dest]:
"med_progress r x = Some y ⟹ ∃ z. r x = Some z ∧ y = z ∩ {xnx, xny, xgnx, xgny, xsk, xEnd}"
by (cases "r x", auto simp add: med_progress_def)
lemma med_progress_dom [simp]: "dom (med_progress r) = dom r"
apply (auto simp add: domIff med_progress_def)
apply (rename_tac x y, case_tac "r x", auto)
done
lemma med_progress_empty [simp]: "med_progress Map.empty = Map.empty"
by (rule ext, auto)
text ‹Mediator function.›
definition
med11 :: "skl1_obs ⇒ l1_obs"
where
"med11 t ≡ ⦇ik = ik t,
secret=secret t,
progress = med_progress (progress t),
signalsInit = signalsInit2 t,
signalsResp = signalsResp2 t⦈"
text ‹relation between states›
definition
R11 :: "(l1_state * skl1_state) set"
where
"R11 ≡ {(s,s').
s = med11 s'
}"
lemmas R11_defs = R11_def med11_def
lemma in_progress_med_progress:
"x ∈ {xnx, xny, xgnx, xgny, xsk, xEnd}
⟹ in_progress (med_progress r R) x ⟷ in_progress (r R) x"
by (cases "r R", auto)
(cases "med_progress r R", auto)+
lemma in_progressS_eq: "in_progressS S S' ⟷ (S ≠ None ∧ (∀ x ∈ S'. in_progress S x))"
by (cases S, auto)
lemma in_progressS_med_progress:
"in_progressS (r R) S
⟹ in_progressS (med_progress r R) (S ∩ {xnx, xny, xgnx, xgny, xsk, xEnd})"
by (auto simp add: in_progressS_eq in_progress_med_progress)
lemma can_signal_R11 [simp]:
"(s1, s2) ∈ R11 ⟹
can_signal s1 A B ⟷ can_signal s2 A B"
by (auto simp add: can_signal_def R11_defs in_progress_med_progress)
text ‹Protocol-independent events.›
lemma skl1_learn_refines_learn:
"{R11} l1_learn m, l1_learn m {>R11}"
by (auto simp add: PO_rhoare_defs R11_defs)
(simp add: l1_defs)
text ‹Protocol events.›
lemma skl1_step1_refines_step1:
"{R11} l1_step1 Ra A B, skl1_step1 Ra A B {>R11}"
by (auto simp add: PO_rhoare_defs R11_defs l1_step1_def skl1_step1_def)
lemma skl1_step2_refines_step2:
"{R11} l1_step2 Rb A B gnx, skl1_step2 Rb A B Ni gnx {>R11}"
by (auto simp add: PO_rhoare_defs R11_defs l1_step2_def)
(auto simp add: skl1_step2_def)
lemma skl1_step3_refines_step3:
"{R11} l1_step3 Ra A B gny, skl1_step3 Ra A B Nr gny {>R11}"
apply (auto simp add: PO_rhoare_defs R11_defs l1_step3_def)
apply (auto simp add: skl1_step3_def, auto dest: med_progress_Some)
apply (drule in_progressS_med_progress, auto)+
done
lemma skl1_step4_refines_step4:
"{R11} l1_step4 Rb A B gnx, skl1_step4 Rb A B Ni gnx {>R11}"
apply (auto simp add: PO_rhoare_defs R11_defs l1_step4_def)
apply (auto simp add: skl1_step4_def, auto dest: med_progress_Some)
apply (drule in_progressS_med_progress, auto)+
done
text ‹Refinement proof.›
lemmas skl1_trans_refines_l1_trans =
skl1_learn_refines_learn
skl1_step1_refines_step1 skl1_step2_refines_step2
skl1_step3_refines_step3 skl1_step4_refines_step4
lemma skl1_refines_init_l1 [iff]:
"init skl1 ⊆ R11 `` (init l1)"
by (auto simp add: R11_defs l1_defs skl1_defs)
lemma skl1_refines_trans_l1 [iff]:
"{R11} trans l1, trans skl1 {> R11}"
by (auto 0 3 simp add: l1_def skl1_def l1_trans_def skl1_trans_def
intro: skl1_trans_refines_l1_trans)
lemma obs_consistent_med11 [iff]:
"obs_consistent R11 med11 l1 skl1"
by (auto simp add: obs_consistent_def R11_defs)
text ‹Refinement result.›
lemma skl1_refines_l1 [iff]:
"refines
R11
med11 l1 skl1"
by (auto simp add:refines_def PO_refines_def)
lemma skl1_implements_l1 [iff]: "implements med11 l1 skl1"
by (rule refinement_soundness) (fast)
subsection ‹Derived invariants: secrecy›
lemma skl1_obs_secrecy [iff]: "oreach skl1 ⊆ s0_secrecy"
apply (rule external_invariant_translation [OF l1_obs_secrecy _ skl1_implements_l1])
apply (auto simp add: med11_def s0_secrecy_def)
done
lemma skl1_secrecy [iff]: "reach skl1 ⊆ s0_secrecy"
by (rule external_to_internal_invariant [OF skl1_obs_secrecy], auto)
subsection ‹Invariants: @{term "Init"} authenticates @{term "Resp"}›
subsubsection ‹inv1›
text ‹If an initiator commit signal exists for @{term "Ra$ni"}, @{term "Nr"},
$(@{term "g"}^@{term "ny"})^@{term "Ra$nx"}$, then @{term "Ra"} is
@{term "Init"}, has passed step 3, and has the nonce @{term "Nr"}, and
‹(g^ny)^(Ra$nx)› as the key in its frame.
›
definition
skl1_inv1 :: "skl1_state set"
where
"skl1_inv1 ≡ {s. ∀ Ra A B gny Nr.
signalsInit s (Commit A B ⟨NonceF (Ra$ni), Nr, Exp gny (NonceF (Ra$nx))⟩) > 0 ⟶
guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ∧
progress s Ra = Some {xnx, xni, xnr, xgnx, xgny, xsk, xEnd} ∧
guessed_frame Ra xnr = Some Nr ∧
guessed_frame Ra xsk = Some (Exp gny (NonceF (Ra$nx)))
}"
lemmas skl1_inv1I = skl1_inv1_def [THEN setc_def_to_intro, rule_format]
lemmas skl1_inv1E [elim] = skl1_inv1_def [THEN setc_def_to_elim, rule_format]
lemmas skl1_inv1D = skl1_inv1_def [THEN setc_def_to_dest, rule_format, rotated 1, simplified]
lemma skl1_inv1_init [iff]:
"init skl1 ⊆ skl1_inv1"
by (auto simp add: skl1_def skl1_init_def skl1_inv1_def)
lemma skl1_inv1_trans [iff]:
"{skl1_inv1} trans skl1 {> skl1_inv1}"
apply (auto simp add: PO_hoare_defs skl1_nostep_defs intro!: skl1_inv1I)
apply (auto simp add: skl1_defs ik_dy_def skl1_inv1_def domIff dest: Exp_Exp_Gen_inj2 [OF sym])
done
lemma PO_skl1_inv1 [iff]: "reach skl1 ⊆ skl1_inv1"
by (rule inv_rule_basic) (auto)
subsubsection ‹inv2›
text ‹If a @{term "Resp"} run @{term "Rb"} has passed step 2 then (if possible)
an initiator running signal has been emitted.›
definition
skl1_inv2 :: "skl1_state set"
where
"skl1_inv2 ≡ {s. ∀ gnx A B Rb Ni.
guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ⟶
in_progressS (progress s Rb) {xny, xni, xnr, xgnx, xgny, xsk} ⟶
guessed_frame Rb xgnx = Some gnx ⟶
guessed_frame Rb xni = Some Ni ⟶
can_signal s A B ⟶
signalsInit s (Running A B ⟨Ni, NonceF (Rb$nr), Exp gnx (NonceF (Rb$ny))⟩) > 0
}"
lemmas skl1_inv2I = skl1_inv2_def [THEN setc_def_to_intro, rule_format]
lemmas skl1_inv2E [elim] = skl1_inv2_def [THEN setc_def_to_elim, rule_format]
lemmas skl1_inv2D = skl1_inv2_def [THEN setc_def_to_dest, rule_format, rotated 1, simplified]
lemma skl1_inv2_init [iff]:
"init skl1 ⊆ skl1_inv2"
by (auto simp add: skl1_def skl1_init_def skl1_inv2_def)
lemma skl1_inv2_trans [iff]:
"{skl1_inv2} trans skl1 {> skl1_inv2}"
apply (auto simp add: PO_hoare_defs intro!: skl1_inv2I)
apply (drule can_signal_trans, assumption)
apply (auto simp add: skl1_nostep_defs)
apply (auto simp add: skl1_defs ik_dy_def skl1_inv2_def)
done
lemma PO_skl1_inv2 [iff]: "reach skl1 ⊆ skl1_inv2"
by (rule inv_rule_basic) (auto)
subsubsection ‹inv3 (derived)›
text ‹If an @{term "Init"} run before step 3 and a @{term "Resp"} run after step 2 both know
the same half-keys and nonces (more or less), then the number of @{term "Init"} running signals
for the key is strictly greater than the number of @{term "Init"} commit signals.
(actually, there are 0 commit and 1 running).
›
definition
skl1_inv3 :: "skl1_state set"
where
"skl1_inv3 ≡ {s. ∀ A B Rb Ra gny Nr.
guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ⟶
in_progressS (progress s Rb) {xny, xni, xnr, xgnx, xgny, xsk} ⟶
guessed_frame Rb xgny = Some gny ⟶
guessed_frame Rb xnr = Some Nr ⟶
guessed_frame Rb xni = Some (NonceF (Ra$ni)) ⟶
guessed_frame Rb xgnx = Some (Exp Gen (NonceF (Ra$nx))) ⟶
guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ⟶
progress s Ra = Some {xnx, xgnx, xni} ⟶
can_signal s A B ⟶
signalsInit s (Commit A B ⟨NonceF (Ra$ni), Nr, Exp gny (NonceF (Ra$nx))⟩)
< signalsInit s (Running A B ⟨NonceF (Ra$ni), Nr, Exp gny (NonceF (Ra$nx))⟩)
}"
lemmas skl1_inv3I = skl1_inv3_def [THEN setc_def_to_intro, rule_format]
lemmas skl1_inv3E [elim] = skl1_inv3_def [THEN setc_def_to_elim, rule_format]
lemmas skl1_inv3D = skl1_inv3_def [THEN setc_def_to_dest, rule_format, rotated 1, simplified]
lemma skl1_inv3_derived: "skl1_inv1 ∩ skl1_inv2 ⊆ skl1_inv3"
apply (auto intro!:skl1_inv3I)
apply (auto dest!: skl1_inv2D)
apply (rename_tac x A B Rb Ra)
apply (case_tac
"signalsInit x (Commit A B
⟨NonceF (Ra $ ni), NonceF (Rb $ nr),
Exp (Exp Gen (NonceF (Rb $ ny))) (NonceF (Ra $ nx))⟩) > 0", auto)
apply (fastforce dest: skl1_inv1D elim: equalityE)
done
subsection ‹Invariants: Resp authenticates Init›
subsubsection ‹inv4›
text ‹If a @{term "Resp"} commit signal exists for @{term "Ni"}, @{term "Rb$nr"},
$(@{term "g"}^@{term "nx"})^@{term "Rb$ny"}$
then @{term "Rb"} is @{term "Resp"}, has finished its run, and has the nonce @{term "Ni"} and
$(@{term "g"}^@{term "nx"})^@{term "Rb$ny"}$ as the key in its frame.
›
definition
skl1_inv4 :: "skl1_state set"
where
"skl1_inv4 ≡ {s. ∀ Rb A B gnx Ni.
signalsResp s (Commit A B ⟨Ni, NonceF (Rb$nr), Exp gnx (NonceF (Rb$ny))⟩) > 0 ⟶
guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ∧
progress s Rb = Some {xny, xni, xnr, xgnx, xgny, xsk, xEnd} ∧
guessed_frame Rb xgnx = Some gnx ∧
guessed_frame Rb xni = Some Ni
}"
lemmas skl1_inv4I = skl1_inv4_def [THEN setc_def_to_intro, rule_format]
lemmas skl1_inv4E [elim] = skl1_inv4_def [THEN setc_def_to_elim, rule_format]
lemmas skl1_inv4D = skl1_inv4_def [THEN setc_def_to_dest, rule_format, rotated 1, simplified]
lemma skl1_inv4_init [iff]:
"init skl1 ⊆ skl1_inv4"
by (auto simp add: skl1_def skl1_init_def skl1_inv4_def)
lemma skl1_inv4_trans [iff]:
"{skl1_inv4} trans skl1 {> skl1_inv4}"
apply (auto simp add: PO_hoare_defs skl1_nostep_defs intro!: skl1_inv4I)
apply (auto simp add: skl1_inv4_def skl1_defs ik_dy_def domIff dest: Exp_Exp_Gen_inj2 [OF sym])
done
lemma PO_skl1_inv4 [iff]: "reach skl1 ⊆ skl1_inv4"
by (rule inv_rule_basic) (auto)
subsubsection ‹inv5›
text ‹If an @{term "Init"} run @{term "Ra"} has passed step3 then (if possible) a
@{term "Resp"} running signal has been emitted.›
definition
skl1_inv5 :: "skl1_state set"
where
"skl1_inv5 ≡ {s. ∀ gny A B Ra Nr.
guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ⟶
in_progressS (progress s Ra) {xnx, xni, xnr, xgnx, xgny, xsk, xEnd} ⟶
guessed_frame Ra xgny = Some gny ⟶
guessed_frame Ra xnr = Some Nr ⟶
can_signal s A B ⟶
signalsResp s (Running A B ⟨NonceF (Ra$ni), Nr, Exp gny (NonceF (Ra$nx))⟩) > 0
}"
lemmas skl1_inv5I = skl1_inv5_def [THEN setc_def_to_intro, rule_format]
lemmas skl1_inv5E [elim] = skl1_inv5_def [THEN setc_def_to_elim, rule_format]
lemmas skl1_inv5D = skl1_inv5_def [THEN setc_def_to_dest, rule_format, rotated 1, simplified]
lemma skl1_inv5_init [iff]:
"init skl1 ⊆ skl1_inv5"
by (auto simp add: skl1_def skl1_init_def skl1_inv5_def)
lemma skl1_inv5_trans [iff]:
"{skl1_inv5} trans skl1 {> skl1_inv5}"
apply (auto simp add: PO_hoare_defs intro!: skl1_inv5I)
apply (drule can_signal_trans, assumption)
apply (auto simp add: skl1_nostep_defs)
apply (auto simp add: skl1_defs ik_dy_def dest: skl1_inv5D)
done
lemma PO_skl1_inv5 [iff]: "reach skl1 ⊆ skl1_inv5"
by (rule inv_rule_basic) (auto)
subsubsection ‹inv6 (derived)›
text ‹If a @{term "Resp"} run before step 4 and an @{term "Init"} run after step 3 both know
the same half-keys (more or less), then the number of @{term "Resp"} running signals
for the key is strictly greater than the number of @{term "Resp"} commit signals.
(actually, there are 0 commit and 1 running).
›
definition
skl1_inv6 :: "skl1_state set"
where
"skl1_inv6 ≡ {s. ∀ A B Rb Ra gnx Ni.
guessed_runs Ra = ⦇role=Init, owner=A, partner=B⦈ ⟶
in_progressS (progress s Ra) {xnx, xni, xnr, xgnx, xgny, xsk, xEnd} ⟶
guessed_frame Ra xgnx = Some gnx ⟶
guessed_frame Ra xni = Some Ni ⟶
guessed_frame Ra xgny = Some (Exp Gen (NonceF (Rb$ny))) ⟶
guessed_frame Ra xnr = Some (NonceF (Rb$nr)) ⟶
guessed_runs Rb = ⦇role=Resp, owner=B, partner=A⦈ ⟶
progress s Rb = Some {xny, xni, xnr, xgnx, xgny, xsk} ⟶
can_signal s A B ⟶
signalsResp s (Commit A B ⟨Ni, NonceF (Rb$nr), Exp gnx (NonceF (Rb$ny))⟩)
< signalsResp s (Running A B ⟨Ni, NonceF (Rb$nr), Exp gnx (NonceF (Rb$ny))⟩)
}"
lemmas skl1_inv6I = skl1_inv6_def [THEN setc_def_to_intro, rule_format]
lemmas skl1_inv6E [elim] = skl1_inv6_def [THEN setc_def_to_elim, rule_format]
lemmas skl1_inv6D = skl1_inv6_def [THEN setc_def_to_dest, rule_format, rotated 1, simplified]
lemma skl1_inv6_derived:
"skl1_inv4 ∩ skl1_inv5 ⊆ skl1_inv6"
proof (auto intro!: skl1_inv6I)
fix s::skl1_state fix A B Rb Ra
assume HRun:"guessed_runs Ra = ⦇role = Init, owner = A, partner = B⦈"
"in_progressS (progress s Ra) {xnx, xni, xnr, xgnx, xgny, xsk, xEnd}"
"guessed_frame Ra xgny = Some (Exp Gen (NonceF (Rb $ ny)))"
"guessed_frame Ra xnr = Some (NonceF (Rb $ nr))"
"can_signal s A B"
assume HRb: "progress s Rb = Some {xny, xni, xnr, xgnx, xgny, xsk}"
assume I4:"s ∈ skl1_inv4"
assume I5:"s ∈ skl1_inv5"
from I4 HRb have "signalsResp s (Commit A B ⟨NonceF (Ra$ni), NonceF (Rb$nr),
Exp (Exp Gen (NonceF (Rb $ ny))) (NonceF (Ra $ nx))⟩) > 0 ⟹ False"
proof (auto dest!: skl1_inv4D)
assume "{xny, xni, xnr, xgnx, xgny, xsk, xEnd} = {xny, xni, xnr, xgnx, xgny, xsk}"
thus ?thesis by force
qed
then have HC:"signalsResp s (Commit A B ⟨NonceF (Ra$ni), NonceF (Rb$nr),
Exp (Exp Gen (NonceF (Rb $ ny))) (NonceF (Ra $ nx))⟩) = 0"
by auto
from I5 HRun have "signalsResp s (Running A B ⟨NonceF (Ra$ni), NonceF (Rb$nr),
Exp (Exp Gen (NonceF (Rb $ ny))) (NonceF (Ra $ nx))⟩) > 0"
by (auto dest!: skl1_inv5D)
with HC show "signalsResp s (Commit A B ⟨NonceF (Ra$ni), NonceF (Rb$nr),
Exp (Exp Gen (NonceF (Rb $ ny))) (NonceF (Ra $ nx))⟩)
< signalsResp s (Running A B ⟨NonceF (Ra$ni), NonceF (Rb$nr),
Exp (Exp Gen (NonceF (Rb $ ny))) (NonceF (Ra $ nx))⟩)"
by auto
qed
subsection ‹Refinement: injective agreement (Init authenticates Resp)›
text ‹Mediator function.›
definition
med0sk1iai :: "skl1_obs ⇒ a0i_obs"
where
"med0sk1iai t ≡ ⦇a0n_state.signals = signalsInit t⦈"
text ‹Relation between states.›
definition
R0sk1iai :: "(a0i_state * skl1_state) set"
where
"R0sk1iai ≡ {(s,s').
a0n_state.signals s = signalsInit s'
}"
text ‹Protocol-independent events.›
lemma skl1_learn_refines_a0_ia_skip_i:
"{R0sk1iai} Id, l1_learn m {>R0sk1iai}"
apply (auto simp add: PO_rhoare_defs R0sk1iai_def)
apply (simp add: l1_learn_def)
done
text ‹Protocol events.›
lemma skl1_step1_refines_a0i_skip_i:
"{R0sk1iai} Id, skl1_step1 Ra A B {>R0sk1iai}"
by (auto simp add: PO_rhoare_defs R0sk1iai_def skl1_step1_def)
lemma skl1_step2_refines_a0i_running_skip_i:
"{R0sk1iai} a0i_running A B ⟨Ni, NonceF (Rb$nr),Exp gnx (NonceF (Rb$ny))⟩ ∪ Id,
skl1_step2 Rb A B Ni gnx {>R0sk1iai}"
by (auto simp add: PO_rhoare_defs R0sk1iai_def,
simp_all add: skl1_step2_def a0i_running_def, auto)
lemma skl1_step3_refines_a0i_commit_skip_i:
"{R0sk1iai ∩ (UNIV × skl1_inv3)}
a0i_commit A B ⟨NonceF (Ra$ni), Nr, Exp gny (NonceF (Ra$nx))⟩ ∪ Id,
skl1_step3 Ra A B Nr gny
{>R0sk1iai}"
apply (auto simp add: PO_rhoare_defs R0sk1iai_def)
apply (auto simp add: skl1_step3_def a0i_commit_def)
apply (frule skl1_inv3D, auto)+
done
lemma skl1_step4_refines_a0i_skip_i:
"{R0sk1iai} Id, skl1_step4 Rb A B Ni gnx {>R0sk1iai}"
by (auto simp add: PO_rhoare_defs R0sk1iai_def, auto simp add: skl1_step4_def)
text ‹refinement proof›
lemmas skl1_trans_refines_a0i_trans_i =
skl1_learn_refines_a0_ia_skip_i
skl1_step1_refines_a0i_skip_i skl1_step2_refines_a0i_running_skip_i
skl1_step3_refines_a0i_commit_skip_i skl1_step4_refines_a0i_skip_i
lemma skl1_refines_init_a0i_i [iff]:
"init skl1 ⊆ R0sk1iai `` (init a0i)"
by (auto simp add: R0sk1iai_def a0i_defs skl1_defs)
lemma skl1_refines_trans_a0i_i [iff]:
"{R0sk1iai ∩ (UNIV × (skl1_inv1 ∩ skl1_inv2))} trans a0i, trans skl1 {> R0sk1iai}"
proof -
let ?pre' = "R0sk1iai ∩ (UNIV × skl1_inv3)"
show ?thesis (is "{?pre} ?t1, ?t2 {>?post}")
proof (rule relhoare_conseq_left)
show "?pre ⊆ ?pre'"
using skl1_inv3_derived by blast
next
show "{?pre'} ?t1, ?t2 {> ?post}"
apply (auto simp add: a0i_def skl1_def a0i_trans_def skl1_trans_def)
prefer 2 using skl1_step2_refines_a0i_running_skip_i apply (simp add: PO_rhoare_defs, blast)
prefer 2 using skl1_step3_refines_a0i_commit_skip_i apply (simp add: PO_rhoare_defs, blast)
apply (blast intro!:skl1_trans_refines_a0i_trans_i)+
done
qed
qed
lemma obs_consistent_med01iai [iff]:
"obs_consistent R0sk1iai med0sk1iai a0i skl1"
by (auto simp add: obs_consistent_def R0sk1iai_def med0sk1iai_def)
text ‹refinement result›
lemma skl1_refines_a0i_i [iff]:
"refines
(R0sk1iai ∩ (reach a0i × (skl1_inv1 ∩ skl1_inv2)))
med0sk1iai a0i skl1"
by (rule Refinement_using_invariants, auto)
lemma skl1_implements_a0i_i [iff]: "implements med0sk1iai a0i skl1"
by (rule refinement_soundness) (fast)
subsection ‹Derived invariants: injective agreement (@{term "Init"} authenticates @{term "Resp"})›
lemma skl1_obs_iagreement_Init [iff]: "oreach skl1 ⊆ l1_iagreement_Init"
apply (rule external_invariant_translation
[OF PO_a0i_obs_agreement _ skl1_implements_a0i_i])
apply (auto simp add: med0sk1iai_def l1_iagreement_Init_def a0i_agreement_def)
done
lemma skl1_iagreement_Init [iff]: "reach skl1 ⊆ l1_iagreement_Init"
by (rule external_to_internal_invariant [OF skl1_obs_iagreement_Init], auto)
subsection ‹Refinement: injective agreement (@{term "Resp"} authenticates @{term "Init"})›
text ‹Mediator function.›
definition
med0sk1iar :: "skl1_obs ⇒ a0i_obs"
where
"med0sk1iar t ≡ ⦇a0n_state.signals = signalsResp t⦈"
text ‹Relation between states.›
definition
R0sk1iar :: "(a0i_state * skl1_state) set"
where
"R0sk1iar ≡ {(s,s').
a0n_state.signals s = signalsResp s'
}"
text ‹Protocol independent events.›
lemma skl1_learn_refines_a0_ia_skip_r:
"{R0sk1iar} Id, l1_learn m {>R0sk1iar}"
apply (auto simp add: PO_rhoare_defs R0sk1iar_def)
apply (simp add: l1_learn_def)
done
text ‹Protocol events.›
lemma skl1_step1_refines_a0i_skip_r:
"{R0sk1iar} Id, skl1_step1 Ra A B {>R0sk1iar}"
by (auto simp add: PO_rhoare_defs R0sk1iar_def skl1_step1_def)
lemma skl1_step2_refines_a0i_skip_r:
"{R0sk1iar} Id, skl1_step2 Rb A B Ni gnx {>R0sk1iar}"
by (auto simp add: PO_rhoare_defs R0sk1iar_def, auto simp add:skl1_step2_def)
lemma skl1_step3_refines_a0i_running_skip_r:
"{R0sk1iar}
a0i_running A B ⟨NonceF (Ra$ni), Nr, Exp gny (NonceF (Ra$nx))⟩ ∪ Id,
skl1_step3 Ra A B Nr gny
{>R0sk1iar}"
by (auto simp add: PO_rhoare_defs R0sk1iar_def,
simp_all add: skl1_step3_def a0i_running_def, auto)
lemma skl1_step4_refines_a0i_commit_skip_r:
"{R0sk1iar ∩ UNIV×skl1_inv6}
a0i_commit A B ⟨Ni, NonceF (Rb$nr), Exp gnx (NonceF (Rb$ny))⟩ ∪ Id,
skl1_step4 Rb A B Ni gnx
{>R0sk1iar}"
apply (auto simp add: PO_rhoare_defs R0sk1iar_def)
apply (auto simp add: skl1_step4_def a0i_commit_def)
apply (auto dest!: skl1_inv6D [rotated 1])
done
text ‹Refinement proof.›
lemmas skl1_trans_refines_a0i_trans_r =
skl1_learn_refines_a0_ia_skip_r
skl1_step1_refines_a0i_skip_r skl1_step2_refines_a0i_skip_r
skl1_step3_refines_a0i_running_skip_r skl1_step4_refines_a0i_commit_skip_r
lemma skl1_refines_init_a0i_r [iff]:
"init skl1 ⊆ R0sk1iar `` (init a0i)"
by (auto simp add: R0sk1iar_def a0i_defs skl1_defs)
lemma skl1_refines_trans_a0i_r [iff]:
"{R0sk1iar ∩ (UNIV × (skl1_inv4 ∩ skl1_inv5))} trans a0i, trans skl1 {> R0sk1iar}"
proof -
let ?pre' = "R0sk1iar ∩ (UNIV × skl1_inv6)"
show ?thesis (is "{?pre} ?t1, ?t2 {>?post}")
proof (rule relhoare_conseq_left)
show "?pre ⊆ ?pre'"
using skl1_inv6_derived by blast
next
show "{?pre'} ?t1, ?t2 {> ?post}"
apply (auto simp add: a0i_def skl1_def a0i_trans_def skl1_trans_def)
prefer 3 using skl1_step3_refines_a0i_running_skip_r apply (simp add: PO_rhoare_defs, blast)
prefer 3 using skl1_step4_refines_a0i_commit_skip_r apply (simp add: PO_rhoare_defs, blast)
apply (blast intro!:skl1_trans_refines_a0i_trans_r)+
done
qed
qed
lemma obs_consistent_med0sk1iar [iff]:
"obs_consistent R0sk1iar med0sk1iar a0i skl1"
by (auto simp add: obs_consistent_def R0sk1iar_def med0sk1iar_def)
text ‹Refinement result.›
lemma skl1_refines_a0i_r [iff]:
"refines
(R0sk1iar ∩ (reach a0i × (skl1_inv4 ∩ skl1_inv5)))
med0sk1iar a0i skl1"
by (rule Refinement_using_invariants, auto)
lemma skl1_implements_a0i_r [iff]: "implements med0sk1iar a0i skl1"
by (rule refinement_soundness) (fast)
subsection ‹Derived invariants: injective agreement (@{term "Resp"} authenticates @{term "Init"})›
lemma skl1_obs_iagreement_Resp [iff]: "oreach skl1 ⊆ l1_iagreement_Resp"
apply (rule external_invariant_translation
[OF PO_a0i_obs_agreement _ skl1_implements_a0i_r])
apply (auto simp add: med0sk1iar_def l1_iagreement_Resp_def a0i_agreement_def)
done
lemma skl1_iagreement_Resp [iff]: "reach skl1 ⊆ l1_iagreement_Resp"
by (rule external_to_internal_invariant [OF skl1_obs_iagreement_Resp], auto)
end