(* Title: HOL/Auth/OtwayRees.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
*)
section‹The Original Otway-Rees Protocol
›
theory OtwayRees
imports Public
begin
text‹From page 244 of
Burrows, Abadi
and Needham (1989). A Logic of Authentication.
Proc. Royal Soc. 426
This
is the original version, which encrypts Nonce NB.
›
inductive_set otway ::
"event list set"
where
Nil:
"[] \ otway"
🍋 ‹Initial trace
is empty
›
| Fake:
"\evsf \ otway; X \ synth (analz (knows Spy evsf)) \
==> Says Spy B X # evsf
∈ otway
"
🍋 ‹The spy can say almost anything.
›
| Reception:
"\evsr \ otway; Says A B X \set evsr\ \ Gets B X # evsr \ otway"
🍋 ‹A message that has been sent can be received
by the intended recipient.
›
| OR1:
"\evs1 \ otway; Nonce NA \ used evs1\
==> Says A B
{Nonce NA, Agent A, Agent B,
Crypt (shrK A)
{Nonce NA, Agent A, Agent B
} }
# evs1
∈ otway
"
🍋 ‹Alice initiates a protocol run
›
| OR2:
"\evs2 \ otway; Nonce NB \ used evs2;
Gets B
{Nonce NA, Agent A, Agent B, X
} ∈ set evs2
]
==> Says B Server
{Nonce NA, Agent A, Agent B, X,
Crypt (shrK B)
{Nonce NA, Nonce NB, Agent A, Agent B
}}
# evs2
∈ otway
"
🍋 ‹Bob
's response to Alice's message.
Note that NB
is encrypted.
›
| OR3:
"\evs3 \ otway; Key KAB \ used evs3;
Gets Server
{Nonce NA, Agent A, Agent B,
Crypt (shrK A)
{Nonce NA, Agent A, Agent B
},
Crypt (shrK B)
{Nonce NA, Nonce NB, Agent A, Agent B
}}
∈ set evs3
]
==> Says Server B
{Nonce NA,
Crypt (shrK A)
{Nonce NA, Key KAB
},
Crypt (shrK B)
{Nonce NB, Key KAB
}}
# evs3
∈ otway
"
🍋 ‹The Server receives Bob
's message and checks that the three NAs
match.
Then he sends a new session key
to Bob
with a packet
for forwarding
to Alice
›
| OR4:
"\evs4 \ otway; B \ Server;
Says B Server
{Nonce NA, Agent A, Agent B, X
',
Crypt (shrK B)
{Nonce NA, Nonce NB, Agent A, Agent B
}}
∈ set evs4;
Gets B
{Nonce NA, X, Crypt (shrK B)
{Nonce NB, Key K
}}
∈ set evs4
]
==> Says B A
{Nonce NA, X
} # evs4
∈ otway
"
🍋 ‹Bob receives the Server
's (?) message and compares the Nonces with
those
in the message he previously sent the Server.
Need @{
term"B \ Server"} because we allow messages
to self.
›
|
Oops:
"\evso \ otway;
Says Server B
{Nonce NA, X, Crypt (shrK B)
{Nonce NB, Key K
}}
∈ set evso
]
==> Notes Spy
{Nonce NA, Nonce NB, Key K
} # evso
∈ otway
"
🍋 ‹This message models possible leaks of session keys. The nonces identify the protocol run
›
declare Says_imp_analz_Spy [dest]
declare parts.Body [dest]
declare analz_into_parts [dest]
declare Fake_parts_insert_in_Un [dest]
text‹A
"possibility property": there are traces that reach the
end›
lemma "\B \ Server; Key K \ used []\
==> ∃evs
∈ otway.
Says B A
{Nonce NA, Crypt (shrK A)
{Nonce NA, Key K
}}
∈ set evs
"
apply (intro exI bexI)
apply (rule_tac [2] otway.Nil
[
THEN otway.OR1,
THEN otway.Reception,
THEN otway.OR2,
THEN otway.Reception,
THEN otway.OR3,
THEN otway.Reception,
THEN otway.OR4])
apply (possibility, simp add: used_Cons)
done
lemma Gets_imp_Says [dest!]:
"\Gets B X \ set evs; evs \ otway\ \ \A. Says A B X \ set evs"
apply (erule rev_mp)
apply (erule otway.induct, auto)
done
(** For reasoning about the encrypted portion of messages **)
lemma OR2_analz_knows_Spy:
"\Gets B \N, Agent A, Agent B, X\ \ set evs; evs \ otway\
==> X
∈ analz (knows Spy evs)
"
by blast
lemma OR4_analz_knows_Spy:
"\Gets B \N, X, Crypt (shrK B) X'\ \ set evs; evs \ otway\
==> X
∈ analz (knows Spy evs)
"
by blast
(*These lemmas assist simplification by removing forwarded X-variables.
We can replace them by rewriting with parts_insert2 and proving using
dest: parts_cut, but the proofs become more difficult.*)
lemmas OR2_parts_knows_Spy =
OR2_analz_knows_Spy [
THEN analz_into_parts]
(*There could be OR4_parts_knows_Spy and Oops_parts_knows_Spy, but for
some reason proofs work without them!*)
text‹Theorems of the form
🍋‹X
∉ parts (spies evs)
› imply that
NOBODY sends messages containing X!
›
text‹Spy never sees a good agent
's shared key!\
lemma Spy_see_shrK [simp]:
"evs \ otway \ (Key (shrK A) \ parts (knows Spy evs)) = (A \ bad)"
by (erule otway.induct, force,
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
lemma Spy_analz_shrK [simp]:
"evs \ otway \ (Key (shrK A) \ analz (knows Spy evs)) = (A \ bad)"
by auto
lemma Spy_see_shrK_D [dest!]:
"\Key (shrK A) \ parts (knows Spy evs); evs \ otway\ \ A \ bad"
by (blast dest: Spy_see_shrK)
subsection‹Towards Secrecy: Proofs Involving
🍋‹analz
››
text ‹Describes the form of K
and NA when the Server sends this message.
Also
for Oops case.
›
lemma Says_Server_message_form:
"\Says Server B \NA, X, Crypt (shrK B) \NB, Key K\\ \ set evs;
evs
∈ otway
]
==> K
∉ range shrK
∧ (
∃i. NA = Nonce i)
∧ (
∃j. NB = Nonce j)
"
by (erule rev_mp, erule otway.induct, simp_all)
(****
The following is to prove theorems of the form
Key K \<in> analz (insert (Key KAB) (knows Spy evs)) \<Longrightarrow>
Key K \<in> analz (knows Spy evs)
A more general formula must be proved inductively.
****)
text‹Session keys are not used
to encrypt other session keys
›
text‹The equality makes the
induction hypothesis easier
to apply›
lemma analz_image_freshK [rule_format]:
"evs \ otway \
∀K KK. KK
⊆ -(range shrK)
⟶
(Key K
∈ analz (Key`KK
∪ (knows Spy evs))) =
(K
∈ KK | Key K
∈ analz (knows Spy evs))
"
apply (erule otway.induct)
apply (frule_tac [8] Says_Server_message_form)
apply (drule_tac [7] OR4_analz_knows_Spy)
apply (drule_tac [5] OR2_analz_knows_Spy, analz_freshK, spy_analz, auto)
done
lemma analz_insert_freshK:
"\evs \ otway; KAB \ range shrK\ \
(Key K
∈ analz (insert (Key KAB) (knows Spy evs))) =
(K = KAB | Key K
∈ analz (knows Spy evs))
"
by (simp only: analz_image_freshK analz_image_freshK_simps)
text‹The Key K uniquely identifies the Server
's message.\
lemma unique_session_keys:
"\Says Server B \NA, X, Crypt (shrK B) \NB, K\\ \ set evs;
Says Server B
' \NA',X
',Crypt (shrK B')
{NB
',K\\ \ set evs;
evs
∈ otway
] ==> X=X
' \ B=B' ∧ NA=NA
' \ NB=NB'"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule otway.induct, simp_all)
apply blast+
🍋 ‹OR3
and OR4
›
done
subsection‹Authenticity properties relating
to NA
›
text‹Only OR1 can
have caused such a part of a message
to appear.
›
lemma Crypt_imp_OR1 [rule_format]:
"\A \ bad; evs \ otway\
==> Crypt (shrK A)
{NA, Agent A, Agent B
} ∈ parts (knows Spy evs)
⟶
Says A B
{NA, Agent A, Agent B,
Crypt (shrK A)
{NA, Agent A, Agent B
}}
∈ set evs
"
by (erule otway.induct, force,
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
lemma Crypt_imp_OR1_Gets:
"\Gets B \NA, Agent A, Agent B,
Crypt (shrK A)
{NA, Agent A, Agent B
}} ∈ set evs;
A
∉ bad; evs
∈ otway
]
==> Says A B
{NA, Agent A, Agent B,
Crypt (shrK A)
{NA, Agent A, Agent B
}}
∈ set evs
"
by (blast dest: Crypt_imp_OR1)
text‹The Nonce NA uniquely identifies A
's message\
lemma unique_NA:
"\Crypt (shrK A) \NA, Agent A, Agent B\ \ parts (knows Spy evs);
Crypt (shrK A)
{NA, Agent A, Agent C
} ∈ parts (knows Spy evs);
evs
∈ otway; A
∉ bad
]
==> B = C
"
apply (erule rev_mp, erule rev_mp)
apply (erule otway.induct, force,
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
done
text‹It
is impossible
to re-use a nonce
in both OR1
and OR2. This holds because
OR2 encrypts Nonce NB. It prevents the attack that can occur
in the
over-simplified version of this protocol: see
‹OtwayRees_Bad
›.
›
lemma no_nonce_OR1_OR2:
"\Crypt (shrK A) \NA, Agent A, Agent B\ \ parts (knows Spy evs);
A
∉ bad; evs
∈ otway
]
==> Crypt (shrK A)
{NA
', NA, Agent A', Agent A
} ∉ parts (knows Spy evs)
"
apply (erule rev_mp)
apply (erule otway.induct, force,
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
done
text‹Crucial property:
If the encrypted message appears,
and A has used NA
to start a run,
then it originated
with the Server!
›
lemma NA_Crypt_imp_Server_msg [rule_format]:
"\A \ bad; evs \ otway\
==> Says A B
{NA, Agent A, Agent B,
Crypt (shrK A)
{NA, Agent A, Agent B
}} ∈ set evs
⟶
Crypt (shrK A)
{NA, Key K
} ∈ parts (knows Spy evs)
⟶ (
∃NB. Says Server B
{NA,
Crypt (shrK A)
{NA, Key K
},
Crypt (shrK B)
{NB, Key K
}} ∈ set evs)
"
apply (erule otway.induct, force,
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast)
subgoal
🍋 ‹OR1:
by freshness
›
by blast
subgoal
🍋 ‹OR3
›
by (blast dest!: no_nonce_OR1_OR2 intro: unique_NA)
subgoal
🍋 ‹OR4
›
by (blast intro!: Crypt_imp_OR1)
done
text‹Corollary:
if A receives B
's OR4 message and the nonce NA agrees
then the key really did come
from the Server! CANNOT prove this of the
bad form of this protocol, even though we can prove
‹Spy_not_see_encrypted_key
››
lemma A_trusts_OR4:
"\Says A B \NA, Agent A, Agent B,
Crypt (shrK A)
{NA, Agent A, Agent B
}} ∈ set evs;
Says B
' A \NA, Crypt (shrK A) \NA, Key K\\ \ set evs;
A
∉ bad; evs
∈ otway
]
==> ∃NB. Says Server B
{NA,
Crypt (shrK A)
{NA, Key K
},
Crypt (shrK B)
{NB, Key K
}}
∈ set evs
"
by (blast intro!: NA_Crypt_imp_Server_msg)
text‹Crucial secrecy property: Spy does not see the keys sent
in msg OR3
Does not
in itself guarantee security: an attack could violate
the premises, e.g.
by having
🍋‹A=Spy
››
lemma secrecy_lemma:
"\A \ bad; B \ bad; evs \ otway\
==> Says Server B
{NA, Crypt (shrK A)
{NA, Key K
},
Crypt (shrK B)
{NB, Key K
}} ∈ set evs
⟶
Notes Spy
{NA, NB, Key K
} ∉ set evs
⟶
Key K
∉ analz (knows Spy evs)
"
apply (erule otway.induct, force, simp_all)
subgoal
🍋 ‹Fake
›
by spy_analz
subgoal
🍋 ‹OR2
›
by (drule OR2_analz_knows_Spy) (auto simp: analz_insert_eq)
subgoal
🍋 ‹OR3
›
by (auto simp add: analz_insert_freshK pushes)
subgoal
🍋 ‹OR4
›
by (drule OR4_analz_knows_Spy) (auto simp: analz_insert_eq)
subgoal
🍋 ‹Oops›
by (auto simp add: Says_Server_message_form analz_insert_freshK unique_session_keys)
done
theorem Spy_not_see_encrypted_key:
"\Says Server B
{NA, Crypt (shrK A)
{NA, Key K
},
Crypt (shrK B)
{NB, Key K
}} ∈ set evs;
Notes Spy
{NA, NB, Key K
} ∉ set evs;
A
∉ bad; B
∉ bad; evs
∈ otway
]
==> Key K
∉ analz (knows Spy evs)
"
by (blast dest: Says_Server_message_form secrecy_lemma)
text‹This form
is an immediate consequence of the previous result. It
is
similar
to the assertions established
by other methods. It
is equivalent
to the previous result
in that the Spy already has
🍋‹analz
› and
🍋‹synth
› at his disposal. However, the conclusion
🍋‹Key K
∉ knows Spy evs
› appears not
to be
inductive: all the cases
other than Fake are trivial, while Fake requires
🍋‹Key K
∉ analz (knows Spy evs)
›.
›
lemma Spy_not_know_encrypted_key:
"\Says Server B
{NA, Crypt (shrK A)
{NA, Key K
},
Crypt (shrK B)
{NB, Key K
}} ∈ set evs;
Notes Spy
{NA, NB, Key K
} ∉ set evs;
A
∉ bad; B
∉ bad; evs
∈ otway
]
==> Key K
∉ knows Spy evs
"
by (blast dest: Spy_not_see_encrypted_key)
text‹A
's guarantee. The Oops premise quantifies over NB because A cannot know
what it
is.
›
lemma A_gets_good_key:
"\Says A B \NA, Agent A, Agent B,
Crypt (shrK A)
{NA, Agent A, Agent B
}} ∈ set evs;
Says B
' A \NA, Crypt (shrK A) \NA, Key K\\ \ set evs;
∀NB.
Notes Spy
{NA, NB, Key K
} ∉ set evs;
A
∉ bad; B
∉ bad; evs
∈ otway
]
==> Key K
∉ analz (knows Spy evs)
"
by (blast dest!: A_trusts_OR4 Spy_not_see_encrypted_key)
subsection‹Authenticity properties relating
to NB
›
text‹Only OR2 can
have caused such a part of a message
to appear. We do not
know anything about X: it does NOT
have to have the right form.
›
lemma Crypt_imp_OR2:
"\Crypt (shrK B) \NA, NB, Agent A, Agent B\ \ parts (knows Spy evs);
B
∉ bad; evs
∈ otway
]
==> ∃X. Says B Server
{NA, Agent A, Agent B, X,
Crypt (shrK B)
{NA, NB, Agent A, Agent B
}}
∈ set evs
"
apply (erule rev_mp)
apply (erule otway.induct, force,
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
done
text‹The Nonce NB uniquely identifies B
's message\
lemma unique_NB:
"\Crypt (shrK B) \NA, NB, Agent A, Agent B\ \ parts(knows Spy evs);
Crypt (shrK B)
{NC, NB, Agent C, Agent B
} ∈ parts(knows Spy evs);
evs
∈ otway; B
∉ bad
]
==> NC = NA
∧ C = A
"
apply (erule rev_mp, erule rev_mp)
apply (erule otway.induct, force,
drule_tac [4] OR2_parts_knows_Spy, simp_all)
apply blast+
🍋 ‹Fake, OR2
›
done
text‹If the encrypted message appears,
and B has used Nonce NB,
then it originated
with the Server! Quite messy
proof.
›
lemma NB_Crypt_imp_Server_msg [rule_format]:
"\B \ bad; evs \ otway\
==> Crypt (shrK B)
{NB, Key K
} ∈ parts (knows Spy evs)
⟶ (
∀X
'. Says B Server
{NA, Agent A, Agent B, X
',
Crypt (shrK B)
{NA, NB, Agent A, Agent B
}}
∈ set evs
⟶ Says Server B
{NA, Crypt (shrK A)
{NA, Key K
},
Crypt (shrK B)
{NB, Key K
}}
∈ set evs)
"
apply simp
apply (erule otway.induct, force, simp_all)
subgoal
🍋 ‹Fake
›
by blast
subgoal
🍋 ‹OR2
›
by (force dest!: OR2_parts_knows_Spy)
subgoal
🍋 ‹OR3
›
by (blast dest: unique_NB dest!: no_nonce_OR1_OR2)
🍋 ‹OR3
›
subgoal
🍋 ‹OR4
›
by (blast dest!: Crypt_imp_OR2)
done
text‹Guarantee
for B:
if it gets a message
with matching NB
then the Server
has sent the correct message.
›
theorem B_trusts_OR3:
"\Says B Server \NA, Agent A, Agent B, X',
Crypt (shrK B)
{NA, NB, Agent A, Agent B
}}
∈ set evs;
Gets B
{NA, X, Crypt (shrK B)
{NB, Key K
}} ∈ set evs;
B
∉ bad; evs
∈ otway
]
==> Says Server B
{NA,
Crypt (shrK A)
{NA, Key K
},
Crypt (shrK B)
{NB, Key K
}}
∈ set evs
"
by (blast intro!: NB_Crypt_imp_Server_msg)
text‹The obvious combination of
‹B_trusts_OR3
› with
‹Spy_not_see_encrypted_key
››
lemma B_gets_good_key:
"\Says B Server \NA, Agent A, Agent B, X',
Crypt (shrK B)
{NA, NB, Agent A, Agent B
}}
∈ set evs;
Gets B
{NA, X, Crypt (shrK B)
{NB, Key K
}} ∈ set evs;
Notes Spy
{NA, NB, Key K
} ∉ set evs;
A
∉ bad; B
∉ bad; evs
∈ otway
]
==> Key K
∉ analz (knows Spy evs)
"
by (blast dest!: B_trusts_OR3 Spy_not_see_encrypted_key)
lemma OR3_imp_OR2:
"\Says Server B
{NA, Crypt (shrK A)
{NA, Key K
},
Crypt (shrK B)
{NB, Key K
}} ∈ set evs;
B
∉ bad; evs
∈ otway
]
==> ∃X. Says B Server
{NA, Agent A, Agent B, X,
Crypt (shrK B)
{NA, NB, Agent A, Agent B
}}
∈ set evs
"
apply (erule rev_mp)
apply (erule otway.induct, simp_all)
apply (blast dest!: Crypt_imp_OR2)+
done
text‹After getting
and checking OR4, agent A can trust that B has been active.
We could probably prove that X has the expected form, but that
is not
strictly necessary
for authentication.
›
theorem A_auths_B:
"\Says B' A \NA, Crypt (shrK A) \NA, Key K\\ \ set evs;
Says A B
{NA, Agent A, Agent B,
Crypt (shrK A)
{NA, Agent A, Agent B
}} ∈ set evs;
A
∉ bad; B
∉ bad; evs
∈ otway
]
==> ∃NB X. Says B Server
{NA, Agent A, Agent B, X,
Crypt (shrK B)
{NA, NB, Agent A, Agent B
}}
∈ set evs
"
by (blast dest!: A_trusts_OR4 OR3_imp_OR2)
end
