# HG changeset patch # User paulson # Date 1066293156 -7200 # Node ID 59b02c1efd010ce0582dbfd01820eb8784d259e6 # Parent a486123e24a5edb8e14de5d2d7c0ed6680445793 improved presentation diff -r a486123e24a5 -r 59b02c1efd01 src/HOL/Auth/OtwayRees.thy --- a/src/HOL/Auth/OtwayRees.thy Thu Oct 16 10:32:06 2003 +0200 +++ b/src/HOL/Auth/OtwayRees.thy Thu Oct 16 10:32:36 2003 +0200 @@ -341,7 +341,6 @@ 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 diff -r a486123e24a5 -r 59b02c1efd01 src/HOL/Auth/OtwayRees_AN.thy --- a/src/HOL/Auth/OtwayRees_AN.thy Thu Oct 16 10:32:06 2003 +0200 +++ b/src/HOL/Auth/OtwayRees_AN.thy Thu Oct 16 10:32:36 2003 +0200 @@ -25,33 +25,33 @@ consts otway :: "event list set" inductive "otway" intros - (*Initial trace is empty*) - Nil: "[] \ otway" + Nil: --{*The empty trace*} + "[] \ otway" - (*The spy MAY say anything he CAN say. We do not expect him to - invent new nonces here, but he can also use NS1. Common to - all similar protocols.*) - Fake: "[| evsf \ otway; X \ synth (analz (knows Spy evsf)) |] + Fake: --{*The Spy may say anything he can say. The sender field is correct, + but agents don't use that information.*} + "[| evsf \ otway; X \ synth (analz (knows Spy evsf)) |] ==> Says Spy B X # evsf \ otway" - (*A message that has been sent can be received by the - intended recipient.*) - Reception: "[| evsr \ otway; Says A B X \set evsr |] + + Reception: --{*A message that has been sent can be received by the + intended recipient.*} + "[| evsr \ otway; Says A B X \set evsr |] ==> Gets B X # evsr \ otway" - (*Alice initiates a protocol run*) - OR1: "evs1 \ otway + OR1: --{*Alice initiates a protocol run*} + "evs1 \ otway ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs1 \ otway" - (*Bob's response to Alice's message.*) - OR2: "[| evs2 \ otway; + OR2: --{*Bob's response to Alice's message.*} + "[| evs2 \ otway; Gets B {|Agent A, Agent B, Nonce NA|} \set evs2 |] ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} # evs2 \ otway" - (*The Server receives Bob's message. Then he sends a new - session key to Bob with a packet for forwarding to Alice.*) - OR3: "[| evs3 \ otway; Key KAB \ used evs3; + OR3: --{*The Server receives Bob's message. Then he sends a new + session key to Bob with a packet for forwarding to Alice.*} + "[| evs3 \ otway; Key KAB \ used evs3; Gets Server {|Agent A, Agent B, Nonce NA, Nonce NB|} \set evs3 |] ==> Says Server B @@ -59,18 +59,18 @@ Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key KAB|}|} # evs3 \ otway" - (*Bob receives the Server's (?) message and compares the Nonces with - those in the message he previously sent the Server. - Need B \ Server because we allow messages to self.*) - OR4: "[| evs4 \ otway; B \ Server; + OR4: --{*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.*} + "[| evs4 \ otway; B \ Server; Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} \set evs4; Gets B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|} \set evs4 |] ==> Says B A X # evs4 \ otway" - (*This message models possible leaks of session keys. The nonces - identify the protocol run. B is not assumed to know shrK A.*) - Oops: "[| evso \ otway; + Oops: --{*This message models possible leaks of session keys. The nonces + identify the protocol run.*} + "[| evso \ otway; Says Server B {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}, Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|} @@ -84,7 +84,7 @@ declare Fake_parts_insert_in_Un [dest] -(*A "possibility property": there are traces that reach the end*) +text{*A "possibility property": there are traces that reach the end*} lemma "[| B \ Server; Key K \ used [] |] ==> \evs \ otway. Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) @@ -102,9 +102,8 @@ by (erule rev_mp, erule otway.induct, auto) -(**** Inductive proofs about otway ****) -(** For reasoning about the encrypted portion of messages **) +text{* For reasoning about the encrypted portion of messages *} lemma OR4_analz_knows_Spy: "[| Gets B {|X, Crypt(shrK B) X'|} \ set evs; evs \ otway |] @@ -112,14 +111,13 @@ by blast -(** Theorems of the form X \ parts (knows Spy evs) imply that NOBODY - sends messages containing X! **) +text{*Theorems of the form @{term "X \ parts (spies evs)"} imply that +NOBODY sends messages containing X! *} -(*Spy never sees a good agent's shared key!*) +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)" -apply (erule otway.induct, simp_all, blast+) -done +by (erule otway.induct, simp_all, blast+) lemma Spy_analz_shrK [simp]: "evs \ otway ==> (Key (shrK A) \ analz (knows Spy evs)) = (A \ bad)" @@ -130,9 +128,9 @@ by (blast dest: Spy_see_shrK) -(*** Proofs involving analz ***) +subsection{*Proofs involving analz *} -(*Describes the form of K and NA when the Server sends this message.*) +text{*Describes the form of K and NA when the Server sends this message.*} lemma Says_Server_message_form: "[| Says Server B {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, @@ -156,9 +154,9 @@ ****) -(** Session keys are not used to encrypt other session keys **) +text{* Session keys are not used to encrypt other session keys *} -(*The equality makes the induction hypothesis easier to apply*) +text{*The equality makes the induction hypothesis easier to apply*} lemma analz_image_freshK [rule_format]: "evs \ otway ==> \K KK. KK <= -(range shrK) --> @@ -176,8 +174,7 @@ by (simp only: analz_image_freshK analz_image_freshK_simps) -(*** The Key K uniquely identifies the Server's message. **) - +text{*The Key K uniquely identifies the Server's message.*} lemma unique_session_keys: "[| Says Server B {|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, @@ -190,14 +187,13 @@ evs \ otway |] ==> A=A' & B=B' & NA=NA' & NB=NB'" apply (erule rev_mp, erule rev_mp, erule otway.induct, simp_all) -(*Remaining cases: OR3 and OR4*) -apply blast+ +apply blast+ --{*OR3 and OR4*} done -(**** Authenticity properties relating to NA ****) +subsection{*Authenticity properties relating to NA*} -(*If the encrypted message appears then it originated with the Server!*) +text{*If the encrypted message appears then it originated with the Server!*} lemma NA_Crypt_imp_Server_msg [rule_format]: "[| A \ bad; A \ B; evs \ otway |] ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} \ parts (knows Spy evs) @@ -207,13 +203,12 @@ \ set evs)" apply (erule otway.induct, force) apply (simp_all add: ex_disj_distrib) -(*Fake, OR3*) -apply blast+ +apply blast+ --{*Fake, OR3*} done -(*Corollary: if A receives B's OR4 message then it originated with the Server. - Freshness may be inferred from nonce NA.*) +text{*Corollary: if A receives B's OR4 message then it originated with the + Server. Freshness may be inferred from nonce NA.*} lemma A_trusts_OR4: "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \ set evs; A \ bad; A \ B; evs \ otway |] @@ -224,10 +219,9 @@ by (blast intro!: NA_Crypt_imp_Server_msg) -(** Crucial secrecy property: Spy does not see the keys sent in msg OR3 +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 **) - + the premises, e.g. by having @{term "A=Spy"}*} lemma secrecy_lemma: "[| A \ bad; B \ bad; evs \ otway |] ==> Says Server B @@ -239,9 +233,9 @@ apply (erule otway.induct, force) apply (frule_tac [7] Says_Server_message_form) apply (drule_tac [6] OR4_analz_knows_Spy) -apply (simp_all add: analz_insert_eq analz_insert_freshK pushes, spy_analz) (*Fake*) -(*OR3, OR4, Oops*) -apply (blast dest: unique_session_keys)+ +apply (simp_all add: analz_insert_eq analz_insert_freshK pushes) +apply spy_analz --{*Fake*} +apply (blast dest: unique_session_keys)+ --{*OR3, OR4, Oops*} done @@ -256,8 +250,8 @@ by (blast dest: Says_Server_message_form secrecy_lemma) -(*A's guarantee. The Oops premise quantifies over NB because A cannot know - what it is.*) +text{*A's guarantee. The Oops premise quantifies over NB because A cannot know + what it is.*} lemma A_gets_good_key: "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \ set evs; \NB. Notes Spy {|NA, NB, Key K|} \ set evs; @@ -267,10 +261,9 @@ -(**** Authenticity properties relating to NB ****) +subsection{*Authenticity properties relating to NB*} -(*If the encrypted message appears then it originated with the Server!*) - +text{*If the encrypted message appears then it originated with the Server!*} lemma NB_Crypt_imp_Server_msg [rule_format]: "[| B \ bad; A \ B; evs \ otway |] ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} \ parts (knows Spy evs) @@ -279,14 +272,13 @@ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ set evs)" apply (erule otway.induct, force, simp_all add: ex_disj_distrib) -(*Fake, OR3*) -apply blast+ +apply blast+ --{*Fake, OR3*} done -(*Guarantee for B: if it gets a well-formed certificate then the Server - has sent the correct message in round 3.*) +text{*Guarantee for B: if it gets a well-formed certificate then the Server + has sent the correct message in round 3.*} lemma B_trusts_OR3: "[| Says S B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ set evs; @@ -298,7 +290,8 @@ by (blast intro!: NB_Crypt_imp_Server_msg) -(*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*) +text{*The obvious combination of @{text B_trusts_OR3} with + @{text Spy_not_see_encrypted_key}*} lemma B_gets_good_key: "[| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ set evs; diff -r a486123e24a5 -r 59b02c1efd01 src/HOL/Auth/OtwayRees_Bad.thy --- a/src/HOL/Auth/OtwayRees_Bad.thy Thu Oct 16 10:32:06 2003 +0200 +++ b/src/HOL/Auth/OtwayRees_Bad.thy Thu Oct 16 10:32:36 2003 +0200 @@ -208,10 +208,9 @@ done -subsection{*Crucial secrecy property: Spy does not see the keys sent in msg OR3 +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 @{term "A=Spy"} *} - lemma secrecy_lemma: "[| A \ bad; B \ bad; evs \ otway |] ==> Says Server B