%Patch files loaded: patch2 version 1.2.2.133 $$$pvs-strategies ;; ;; Proof Strategies for the Enclaves Verification Diagram ;; ;; install rewrite rules for a user step (defstep user-rewrites () (then (auto-rewrite-theory "user_transitions") (auto-rewrite "Ta" "T1" "T3" "T6" "T8")) "Install rewrite rules for User model" "User rewrites installed") ;; install rewrite rules for a leader step (defstep leader-rewrites () (then (auto-rewrite-theory "leader_transitions") (auto-rewrite "Tl" "T2" "T4" "T5" "T7" "T9")) "Install rewrite rules for Leader model" "Leader rewrites installed") ;; install rewrite rules for expanding messages, ;; showing equality of messages and fields, and for simplifying ;; set membership expressions (defstep message-rewrites () (then (auto-rewrite-theories "enclaves_messages" "sets[field]") (auto-rewrite "Parts" "equal_encr" "equal_conc" "equal_key" "equal_stkey" "equal_ltkey" "equal_agent" "equal_data" "equal_nonce" "fresh_nonce1" "fresh_nonce2" "fresh_nonce3" "fresh_key1") (assert)) "Install rewrite rules for checking message equalities" "Message rewrites installed") ;; common steps for all proof obligations ;; Q is the name of the source state predicate ;; - expands the transition relation ;; - does the following case split: ;; 1) transition from A0 ;; 2) transition from the leader on a message from A0 ;; 3) transition from the leader on a message other than from A0 ;; 4) transition from a faked message ;; - simplifies by rewriting and by forward chaining ;; all the subgoals (defstep origin (Q) (then (skosimp) (auto-rewrite ("T")) (spread (smash) ((then (user-rewrites)(reduce)(expand Q -)(skosimp)) (then (skolem!) (spread (case-replace "A!1=A0") ((then (leader-rewrites)(reduce)(expand Q -)(skosimp)) (then (expand Q)(skosimp) (forward-chain "unchanged_leader3") (forward-chain "unchanged_user1") (ground))))) (then (expand Q)(skosimp) (forward-chain "unchanged_user2") (forward-chain "unchanged_leader2") (ground))))) "Expand and case split from state Q" "Expand and case split from state Q") ;; to be used after message-rewrites (defstep replace-ground () (then (replace*)(assert)(ground)(replace*)) "Replace and ground" "Simplifying") ;; instantiates a consequent formula then ;; tries one of the lemmas other_user1, ..., other_user4 (defstep other-user () (then (repeat* (inst? +)) (ground) (skosimp) (try (forward-chain "other_user1") (then (repeat* (inst? -))(ground)) (try (forward-chain "other_user2") (then (repeat* (inst? -))(ground)) (try (forward-chain "other_user3") (then (repeat* (inst? -))(ground)) (try (forward-chain "other_user4") (then (repeat* (inst?))(ground)) (skip)))))) "Instantiates and applies the `other-user' lemmas (forward chaining)" "Applying the `other-user' lemmas") ;; instantiates a consequent formula then ;; tries one of lemmas replay1 and replay2 (defstep replay () (then (repeat* (inst? +)) (auto-rewrite "Ag" "InUse") (ground) (skosimp) (else (then (lemma "replay2") (repeat* (try (inst? :where - :polarity? t) (ground) (skip))) (fail)) (then (lemma "replay1") (repeat* (try (inst? :where - :polarity? t) (ground) (skip))) (fail)))) "Instantiates and applies the `replay' lemmas" "Applying the `replay' lemmas") ;; instantiates a consequent formula then ;; tries lemma `new_message' (defstep new-message () (then (repeat* (inst? +)) (ground) (skosimp) (use "new_message") (ground) (repeat* (try (inst?)(assert)(skip)))) "Instantiates and applies the `new_message' lemma" "By lemma new_message") ;; instantiates a consequent formula then ;; tries lemma `no_message' (defstep no-message () (then (repeat* (inst? +)) (ground) (skosimp) (lemma "no_message") (if *new-fmla-nums* (let ((fnum (car *new-fmla-nums*))) (then (inst? fnum :polarity? t) (assert) (repeat* (inst? fnum)) (assert) (repeat* (inst?)))) (skip))) "Instantiates and applies the `no_message' lemma" "By lemma no_message") ;; instantiates a consequent formula then ;; tries lemma `oops_event' (defstep oops-event () (then (repeat* (inst? +)) (ground) (skosimp) (lemma "oops_event") (if *new-fmla-nums* (let ((fnum (car *new-fmla-nums*))) (then (inst? fnum :polarity? t) (assert) (repeat* (inst? fnum)) (assert) (repeat* (inst?)))) (skip))) "Instantiates and applies the `oops_event' lemma" "By lemma oops_event") $$$enclaves_abstraction.pvs enclaves_abstraction : THEORY BEGIN IMPORTING enclaves A: VAR user X: VAR field B, C, G: VAR agent S: VAR set[field] N, Nl, Nl1, Nl2, Na, Na1, Na2 : VAR nonce K, Ka, Kg, Kb: VAR (Ssk?) q, q1, q2, q3: VAR global e, e1, e2: VAR event n, n1, n2: VAR nat %---------------------- % State abstractions %---------------------- Q1(q): bool = q`users(A0) = NotConnected and q`leader(A0) = NotConnected Q2(q): bool = EXISTS Na: q`users(A0) = WaitingForKey(Na) & q`leader(A0) = NotConnected & (FORALL K, N: not PartsTrace(q)(Encr(Shr(A0), Leader ++ A0 ++ Na ++ N ++ K))) Q3(q): bool = EXISTS Na, Nl, Ka: q`users(A0) = WaitingForKey(Na) & q`leader(A0) = WaitingForKeyAck(Nl, Ka) & (FORALL K, N: PartsTrace(q)(Encr(Shr(A0), Leader ++ A0 ++ Na ++ N ++ K)) => N=Nl & K=Ka) & (FORALL N: not PartsTrace(q)(Encr(Ka, A0 ++ Leader ++ Nl ++ N))) & not PartsTrace(q)(Encr(Ka, A0 ++ Leader)) Q4(q): bool = EXISTS Na, Nl, Ka: q`users(A0) = Connected(Na, Ka) & q`leader(A0) = WaitingForKeyAck(Nl, Ka) & (FORALL N: PartsTrace(q)(Encr(Ka, A0 ++ Leader ++ Nl ++ N)) => N=Na) & (FORALL N: not PartsTrace(q)(Encr(Ka, Leader ++ A0 ++ Na ++ N))) & not PartsTrace(q)(Encr(Ka, A0 ++ Leader)) Q5(q): bool = EXISTS Na, Ka: q`users(A0) = Connected(Na, Ka) & q`leader(A0) = Connected(Na, Ka) & (FORALL N: not PartsTrace(q)(Encr(Ka, Leader ++ A0 ++ Na ++ N))) & not PartsTrace(q)(Encr(Ka, A0 ++ Leader)) Q6(q): bool = EXISTS Na, Nl, Ka: q`users(A0) = Connected(Na, Ka) & q`leader(A0) = WaitingForAck(Nl, Ka) & (FORALL N: PartsTrace(q)(Encr(Ka, Leader ++ A0 ++ Na ++ N)) => N=Nl) & (FORALL N: not PartsTrace(q)(Encr(Ka, A0 ++ Leader ++ Nl ++ N))) & not PartsTrace(q)(Encr(Ka, A0 ++ Leader)) Q7(q): bool = EXISTS Na, Nl, Ka: q`users(A0) = Connected(Na, Ka) & q`leader(A0) = WaitingForAck(Nl, Ka) & (FORALL N: PartsTrace(q)(Encr(Ka, A0 ++ Leader ++ Nl ++ N)) => N=Na) & (FORALL N: not PartsTrace(q)(Encr(Ka, Leader ++ A0 ++ Na ++ N))) & not PartsTrace(q)(Encr(Ka, A0 ++ Leader)) Q8(q): bool = EXISTS Nl, Ka: q`users(A0) = NotConnected & q`leader(A0) = WaitingForAck(Nl, Ka) Q9(q): bool = EXISTS Nl, Ka: q`users(A0) = NotConnected & q`leader(A0) = WaitingForKeyAck(Nl, Ka) Q10(q): bool = EXISTS Na, Ka: q`users(A0) = NotConnected & q`leader(A0) = Connected(Na, Ka) Q11(q): bool = EXISTS Nl, Ka: q`users(A0) = NotConnected & q`leader(A0) = WaitingForAck(Nl, Ka) & (FORALL N: not PartsTrace(q)(Encr(Ka, A0 ++ Leader ++ Nl ++ N))) Q12(q): bool = EXISTS Nl, Ka: q`users(A0) = NotConnected & q`leader(A0) = WaitingForKeyAck(Nl, Ka) & (FORALL N: not PartsTrace(q)(Encr(Ka, A0 ++ Leader ++ Nl ++ N))) Q13(q): bool = EXISTS Na, Nl, Ka: q`users(A0) = WaitingForKey(Na) & q`leader(A0) = WaitingForKeyAck(Nl, Ka) & (FORALL N: not PartsTrace(q)(Encr(Ka, A0 ++ Leader ++ Nl ++ N))) & (FORALL N, K: not PartsTrace(q)(Encr(Shr(A0), Leader ++ A0 ++ Na ++ N ++ K))) Q14(q): bool = EXISTS Na, Nl, Ka: q`users(A0) = WaitingForKey(Na) & q`leader(A0) = WaitingForAck(Nl, Ka) & (FORALL N, K: not PartsTrace(q)(Encr(Shr(A0), Leader ++ A0 ++ Na ++ N ++ K))) Q15(q): bool = EXISTS Na, Nl, Ka: q`users(A0) = WaitingForKey(Na) & q`leader(A0) = WaitingForKeyAck(Nl, Ka) & (FORALL N, K: not PartsTrace(q)(Encr(Shr(A0), Leader ++ A0 ++ Na ++ N ++ K))) Q16(q): bool = EXISTS Na, Na2, Ka: q`users(A0) = WaitingForKey(Na) & q`leader(A0) = Connected(Na2, Ka) & (FORALL N, K: not PartsTrace(q)(Encr(Shr(A0), Leader ++ A0 ++ Na ++ N ++ K))) Q17(q): bool = EXISTS Na, Nl, Ka: q`users(A0) = WaitingForKey(Na) & q`leader(A0) = WaitingForAck(Nl, Ka) & (FORALL N: not PartsTrace(q)(Encr(Ka, A0 ++ Leader ++ Nl ++ N))) & (FORALL N, K: not PartsTrace(q)(Encr(Shr(A0), Leader ++ A0 ++ Na ++ N ++ K))) %--------------- % Transitions %---------------- tran_Q1: LEMMA Reachable(Q0, T)(q1) AND Q1(q1) AND T(G)(q1, e, q2) IMPLIES Q1(q2) OR Q2(q2) OR Q12(q2) tran_Q2: LEMMA Reachable(Q0, T)(q1) AND Q2(q1) AND T(G)(q1, e, q2) IMPLIES Q2(q2) OR Q3(q2) OR Q13(q2) tran_Q3: LEMMA Reachable(Q0, T)(q1) AND Q3(q1) AND T(G)(q1, e, q2) IMPLIES Q3(q2) OR Q4(q2) tran_Q4: LEMMA Reachable(Q0, T)(q1) AND Q4(q1) AND T(G)(q1, e, q2) IMPLIES Q4(q2) OR Q5(q2) OR Q9(q2) tran_Q5: LEMMA Reachable(Q0, T)(q1) AND Q5(q1) AND T(G)(q1, e, q2) IMPLIES Q5(q2) OR Q6(q2) OR Q10(q2) tran_Q6: LEMMA Reachable(Q0, T)(q1) AND Q6(q1) AND T(G)(q1, e, q2) IMPLIES Q6(q2) OR Q7(q2) OR Q11(q2) tran_Q7: LEMMA Reachable(Q0, T)(q1) AND Q7(q1) AND T(G)(q1, e, q2) IMPLIES Q7(q2) OR Q8(q2) OR Q5(q2) tran_Q8: LEMMA Reachable(Q0, T)(q1) AND Q8(q1) AND T(G)(q1, e, q2) IMPLIES Q8(q2) OR Q10(q2) OR Q14(q2) OR Q1(q2) tran_Q9: LEMMA Reachable(Q0, T)(q1) AND Q9(q1) AND T(G)(q1, e, q2) IMPLIES Q9(q2) OR Q10(q2) OR Q15(q2) tran_Q10: LEMMA Reachable(Q0, T)(q1) AND Q10(q1) AND T(G)(q1, e, q2) IMPLIES Q10(q2) OR Q11(q2) OR Q16(q2) OR Q1(q2) tran_Q11: LEMMA Reachable(Q0, T)(q1) AND Q11(q1) AND T(G)(q1, e, q2) IMPLIES Q11(q2) OR Q17(q2) OR Q1(q2) tran_Q12: LEMMA Reachable(Q0, T)(q1) AND Q12(q1) AND T(G)(q1, e, q2) IMPLIES Q12(q2) OR Q13(q2) tran_Q13: LEMMA Reachable(Q0, T)(q1) AND Q13(q1) AND T(G)(q1, e, q2) IMPLIES Q13(q2) tran_Q14: LEMMA Reachable(Q0, T)(q1) AND Q14(q1) AND T(G)(q1, e, q2) IMPLIES Q14(q2) OR Q16(q2) OR Q2(q2) tran_Q15: LEMMA Reachable(Q0, T)(q1) AND Q15(q1) AND T(G)(q1, e, q2) IMPLIES Q15(q2) OR Q16(q2) tran_Q16: LEMMA Reachable(Q0, T)(q1) AND Q16(q1) AND T(G)(q1, e, q2) IMPLIES Q16(q2) OR Q17(q2) OR Q2(q2) tran_Q17: LEMMA Reachable(Q0, T)(q1) AND Q17(q1) AND T(G)(q1, e, q2) IMPLIES Q17(q2) OR Q2(q2) %-------------- % Invariants %-------------- state_space: PROPOSITION Reachable(Q0, T)(q) IMPLIES Q1(q) OR Q2(q) OR Q3(q) OR Q4(q) OR Q5(q) OR Q6(q) OR Q7(q) OR Q8(q) OR Q9(q) OR Q10(q) OR Q11(q) OR Q12(q) OR Q13(q) OR Q14(q) OR Q15(q) OR Q16(q) OR Q17(q) session_key_prop: PROPOSITION Reachable(Q0, T)(q) AND q`users(A0) = Connected(N, Ka) => InUse(Ka, q) connected_states: PROPOSITION Reachable(Q0, T)(q) AND Connected?(q`users(A0)) AND Connected?(q`leader(A0)) => EXISTS Ka, Na: q`users(A0) = Connected(Na, Ka) AND q`leader(A0) = Connected(Na, Ka) END enclaves_abstraction $$$enclaves_abstraction.prf (|enclaves_abstraction| (|tran_Q1| "" (ORIGIN "Q1") (("1" (MESSAGE-REWRITES) (("1" (EXPAND "Q2") (("1" (NEW-MESSAGE) NIL NIL)) NIL)) NIL) ("2" (MESSAGE-REWRITES) (("2" (EXPAND "Q12") (("2" (NEW-MESSAGE) NIL NIL)) NIL)) NIL)) NIL) (|tran_Q2| "" (ORIGIN "Q2") (("1" (REPLACE-GROUND) (("1" (FORWARD-CHAIN "auth_key_dist") (("1" (INST?) NIL NIL)) NIL)) NIL) ("2" (MESSAGE-REWRITES) (("2" (CASE-REPLACE "Na!2 = Na!1") (("1" (EXPAND "Q3") (("1" (NEW-MESSAGE) NIL NIL)) NIL) ("2" (EXPAND "Q13") (("2" (NEW-MESSAGE) NIL NIL)) NIL)) NIL)) NIL) ("3" (OTHER-USER) NIL NIL) ("4" (REPLAY) NIL NIL)) NIL) (|tran_Q3| "" (ORIGIN "Q3") (("1" (REPLACE-GROUND) (("1" (FORWARD-CHAIN "auth_key_dist") (("1" (INST?) (("1" (GROUND) (("1" (REPLACE*) (("1" (DELETE -1 -2 -3) (("1" (MESSAGE-REWRITES) (("1" (EXPAND "Q4") (("1" (NEW-MESSAGE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FORWARD-CHAIN "auth_ack_key") (("2" (REPLACE-GROUND) (("2" (INST? -8) NIL NIL)) NIL)) NIL) ("3" (OTHER-USER) NIL NIL) ("4" (REPLAY) NIL NIL)) NIL) (|tran_Q4| "" (ORIGIN "Q4") (("1" (REPLACE-GROUND) (("1" (FORWARD-CHAIN "admin_msg") (("1" (INST? -7) NIL NIL)) NIL)) NIL) ("2" (EXPAND "Q9") (("2" (INST + "Nl!1" "Ka!2") (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("3" (REPLACE-GROUND) (("3" (FORWARD-CHAIN "auth_ack_key") (("3" (INST?) (("3" (ASSERT) (("3" (DELETE -1) (("3" (REPLACE*) (("3" (EXPAND "Q5") (("3" (NO-MESSAGE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (OTHER-USER) NIL NIL) ("5" (REPLAY) NIL NIL)) NIL) (|tran_Q5| "" (ORIGIN "Q5") (("1" (REPLACE-GROUND) (("1" (FORWARD-CHAIN "admin_msg") (("1" (INST?) NIL NIL)) NIL)) NIL) ("2" (EXPAND "Q10") (("2" (INST + "Na!2" "Ka!2") (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("3" (REPLACE-GROUND) (("3" (MESSAGE-REWRITES) (("3" (EXPAND "Q6") (("3" (NEW-MESSAGE) NIL NIL)) NIL)) NIL)) NIL) ("4" (REPLACE-GROUND) (("4" (FORWARD-CHAIN "req_close") NIL NIL)) NIL) ("5" (OTHER-USER) NIL NIL) ("6" (REPLAY) NIL NIL)) NIL) (|tran_Q6| "" (ORIGIN "Q6") (("1" (REPLACE-GROUND) (("1" (FORWARD-CHAIN "admin_msg") (("1" (INST?) (("1" (ASSERT) (("1" (DELETE -1) (("1" (REPLACE*) (("1" (MESSAGE-REWRITES) (("1" (EXPAND "Q7") (("1" (INST + "Na2!1" "Nl!2" "Ka!1") (("1" (NEW-MESSAGE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE-GROUND) (("2" (MESSAGE-REWRITES) (("2" (EXPAND "Q11") (("2" (NEW-MESSAGE) NIL NIL)) NIL)) NIL)) NIL) ("3" (REPLACE-GROUND) (("3" (FORWARD-CHAIN "ack_admin") (("3" (INST? -8) NIL NIL)) NIL)) NIL) ("4" (REPLACE-GROUND) (("4" (FORWARD-CHAIN "req_close") NIL NIL)) NIL) ("5" (OTHER-USER) NIL NIL) ("6" (REPLAY) NIL NIL)) NIL) (|tran_Q7| "" (ORIGIN "Q7") (("1" (REPLACE-GROUND) (("1" (FORWARD-CHAIN "admin_msg") (("1" (INST? -7) NIL NIL)) NIL)) NIL) ("2" (EXPAND "Q8") (("2" (INST + "Nl!1" "Ka!2") (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("3" (REPLACE-GROUND) (("3" (FORWARD-CHAIN "ack_admin") (("3" (INST?) (("3" (ASSERT) (("3" (DELETE -1) (("3" (REPLACE*) (("3" (EXPAND "Q5") (("3" (NO-MESSAGE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (REPLACE-GROUND) (("4" (FORWARD-CHAIN "req_close") NIL NIL)) NIL) ("5" (OTHER-USER) NIL NIL) ("6" (REPLAY) NIL NIL)) NIL) (|tran_Q8| "" (ORIGIN "Q8") (("1" (MESSAGE-REWRITES) (("1" (EXPAND "Q14") (("1" (NEW-MESSAGE) NIL NIL)) NIL)) NIL) ("2" (EXPAND "Q10") (("2" (INST + "Na!1" "Ka!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("3" (EXPAND "Q1") (("3" (ASSERT) NIL NIL)) NIL) ("4" (INST?) (("4" (GROUND) NIL NIL)) NIL) ("5" (INST?) (("5" (GROUND) NIL NIL)) NIL)) NIL) (|tran_Q9| "" (ORIGIN "Q9") (("1" (MESSAGE-REWRITES) (("1" (EXPAND "Q15") (("1" (NEW-MESSAGE) NIL NIL)) NIL)) NIL) ("2" (EXPAND "Q10") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("3" (INST?) (("3" (ASSERT) NIL NIL)) NIL) ("4" (INST?) (("4" (ASSERT) NIL NIL)) NIL)) NIL) (|tran_Q10| "" (ORIGIN "Q10") (("1" (MESSAGE-REWRITES) (("1" (EXPAND "Q16") (("1" (NEW-MESSAGE) NIL NIL)) NIL)) NIL) ("2" (REPLACE-GROUND) (("2" (MESSAGE-REWRITES) (("2" (EXPAND "Q11") (("2" (NEW-MESSAGE) NIL NIL)) NIL)) NIL)) NIL) ("3" (EXPAND "Q1") (("3" (ASSERT) NIL NIL)) NIL) ("4" (INST?) (("4" (ASSERT) NIL NIL)) NIL) ("5" (INST?) (("5" (ASSERT) NIL NIL)) NIL)) NIL) (|tran_Q11| "" (ORIGIN "Q11") (("1" (MESSAGE-REWRITES) (("1" (EXPAND "Q17") (("1" (NEW-MESSAGE) NIL NIL)) NIL)) NIL) ("2" (REPLACE-GROUND) (("2" (FORWARD-CHAIN "ack_admin") (("2" (INST?) NIL NIL)) NIL)) NIL) ("3" (EXPAND "Q1") (("3" (ASSERT) NIL NIL)) NIL) ("4" (OTHER-USER) NIL NIL) ("5" (REPLAY) NIL NIL)) NIL) (|tran_Q12| "" (ORIGIN "Q12") (("1" (MESSAGE-REWRITES) (("1" (EXPAND "Q13") (("1" (NEW-MESSAGE) NIL NIL)) NIL)) NIL) ("2" (REPLACE-GROUND) (("2" (FORWARD-CHAIN "auth_ack_key") (("2" (INST?) NIL NIL)) NIL)) NIL) ("3" (OTHER-USER) NIL NIL) ("4" (REPLAY) NIL NIL)) NIL) (|tran_Q13| "" (ORIGIN "Q13") (("1" (FORWARD-CHAIN "auth_key_dist") (("1" (REPLACE-GROUND) (("1" (INST? -7) NIL NIL)) NIL)) NIL) ("2" (FORWARD-CHAIN "auth_ack_key") (("2" (REDUCE :IF-MATCH ALL) NIL NIL)) NIL) ("3" (OTHER-USER) NIL NIL) ("4" (REPLAY) NIL NIL)) NIL) (|tran_Q14| "" (ORIGIN "Q14") (("1" (REPLACE-GROUND) (("1" (FORWARD-CHAIN "auth_key_dist") (("1" (INST?) NIL NIL)) NIL)) NIL) ("2" (REPLACE-GROUND) (("2" (MESSAGE-REWRITES) (("2" (EXPAND "Q16") (("2" (NO-MESSAGE) NIL NIL)) NIL)) NIL)) NIL) ("3" (REPLACE-GROUND) (("3" (MESSAGE-REWRITES) (("3" (EXPAND "Q2") (("3" (OOPS-EVENT) NIL NIL)) NIL)) NIL)) NIL) ("4" (OTHER-USER) NIL NIL) ("5" (REPLAY) NIL NIL)) NIL) (|tran_Q15| "" (ORIGIN "Q15") (("1" (REPLACE-GROUND) (("1" (FORWARD-CHAIN "auth_key_dist") (("1" (INST?) NIL NIL)) NIL)) NIL) ("2" (REPLACE-GROUND) (("2" (MESSAGE-REWRITES) (("2" (EXPAND "Q16") (("2" (NO-MESSAGE) NIL NIL)) NIL)) NIL)) NIL) ("3" (OTHER-USER) NIL NIL) ("4" (REPLAY) NIL NIL)) NIL) (|tran_Q16| "" (ORIGIN "Q16") (("1" (REPLACE-GROUND) (("1" (FORWARD-CHAIN "auth_key_dist") (("1" (INST?) NIL NIL)) NIL)) NIL) ("2" (REPLACE-GROUND) (("2" (MESSAGE-REWRITES) (("2" (EXPAND "Q17") (("2" (NEW-MESSAGE) NIL NIL)) NIL)) NIL)) NIL) ("3" (REPLACE-GROUND) (("3" (MESSAGE-REWRITES) (("3" (EXPAND "Q2") (("3" (OOPS-EVENT) NIL NIL)) NIL)) NIL)) NIL) ("4" (OTHER-USER) NIL NIL) ("5" (REPLAY) NIL NIL)) NIL) (|tran_Q17| "" (ORIGIN "Q17") (("1" (REPLACE-GROUND) (("1" (FORWARD-CHAIN "auth_key_dist") (("1" (INST? -7) NIL NIL)) NIL)) NIL) ("2" (REPLACE-GROUND) (("2" (FORWARD-CHAIN "ack_admin") (("2" (INST?) NIL NIL)) NIL)) NIL) ("3" (REPLACE-GROUND) (("3" (MESSAGE-REWRITES) (("3" (EXPAND "Q2") (("3" (OOPS-EVENT) NIL NIL)) NIL)) NIL)) NIL) ("4" (OTHER-USER) NIL NIL) ("5" (REPLAY) NIL NIL)) NIL) (|state_space| "" (REWRITE "Reachable_induct3") (("1" (DELETE 2) (("1" (SKOSIMP) (("1" (DELETE 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (APPLY (THEN (SKOSIMP) (GROUND))) (("1" (FORWARD-CHAIN "tran_Q1") NIL NIL) ("2" (FORWARD-CHAIN "tran_Q2") NIL NIL) ("3" (FORWARD-CHAIN "tran_Q3") NIL NIL) ("4" (FORWARD-CHAIN "tran_Q4") NIL NIL) ("5" (FORWARD-CHAIN "tran_Q5") NIL NIL) ("6" (FORWARD-CHAIN "tran_Q6") NIL NIL) ("7" (FORWARD-CHAIN "tran_Q7") NIL NIL) ("8" (FORWARD-CHAIN "tran_Q8") NIL NIL) ("9" (FORWARD-CHAIN "tran_Q9") NIL NIL) ("10" (FORWARD-CHAIN "tran_Q10") NIL NIL) ("11" (FORWARD-CHAIN "tran_Q11") NIL NIL) ("12" (FORWARD-CHAIN "tran_Q12") NIL NIL) ("13" (FORWARD-CHAIN "tran_Q13") NIL NIL) ("14" (FORWARD-CHAIN "tran_Q14") NIL NIL) ("15" (FORWARD-CHAIN "tran_Q15") NIL NIL) ("16" (FORWARD-CHAIN "tran_Q16") NIL NIL) ("17" (FORWARD-CHAIN "tran_Q17") NIL NIL)) NIL)) NIL)) NIL) (|session_key_prop| "" (SKOSIMP) (("" (USE "state_space") (("" (AUTO-REWRITE-THEORIES "user_transitions" "leader_transitions" "enclaves_abstraction") (("" (AUTO-REWRITE "InUse") (("" (APPLY (THEN (REDUCE :IF-MATCH NIL) (INST? + :IF-MATCH ALL))) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|connected_states| "" (SKOSIMP) (("" (USE "state_space") (("" (AUTO-REWRITE-THEORIES "user_transitions" "leader_transitions" "enclaves_abstraction") (("" (AUTO-REWRITE "InUse") (("" (APPLY (THEN (REDUCE :IF-MATCH NIL) (REPEAT* (THEN (INST? + :IF-MATCH ALL) (ASSERT))))) NIL NIL)) NIL)) NIL)) NIL)) NIL)) $$$basics.pvs %--------------------------------- % Analz, Parts, Synth, and Fake %--------------------------------- basics: THEORY BEGIN IMPORTING fields X, Y, Z, W: VAR field X0: VAR (Atom?) K: VAR key S, S1, S2, P: VAR set[field] S0: VAR { S | subset?(S, Atom?) } % -- Parts Parts(S)(X): INDUCTIVE bool = S(X) OR (EXISTS Y: Parts(S)(X ++ Y)) OR (EXISTS Y: Parts(S)(Y ++ X)) OR (EXISTS K: Parts(S)(Encr(K, X))) Inj_parts : LEMMA Parts(S)(X) WHEN S(X) Fst_parts : LEMMA Parts(S)(X) WHEN Parts(S)(X ++ Y) Snd_parts : LEMMA Parts(S)(Y) WHEN Parts(S)(X ++ Y) Body_parts: LEMMA Parts(S)(X) WHEN Parts(S)(Encr(K, X)) Parts_induct: LEMMA subset?(S, P) AND (FORALL X, Y: P(X ++ Y) => P(X)) AND (FORALL X, Y: P(X ++ Y) => P(Y)) AND (FORALL X, K: P(Encr(K, X)) => P(X)) IMPLIES subset?(Parts(S), P) Parts_sub: LEMMA subset?(S, Parts(S)) Parts_emptyset: LEMMA Parts(emptyset) = emptyset Parts_subset: LEMMA subset?(S1, S2) IMPLIES subset?(Parts(S1), Parts(S2)) Parts_union: LEMMA Parts(union(S1, S2)) = union(Parts(S1), Parts(S2)) Parts_atom: LEMMA Parts(S0) = S0 Parts_member_aux: LEMMA Parts(S)(X) IMPLIES subset?(Parts(X), Parts(S)) Parts_member: LEMMA S(X) IMPLIES subset?(Parts(X), Parts(S)) Parts_equiv: LEMMA Parts(S) = { X | EXISTS Y: S(Y) AND Parts(Y)(X) } Parts_singleton: LEMMA Parts(singleton(X)) = Parts(X) Parts_add: LEMMA Parts(add(X, S)) = union(Parts(X), Parts(S)) % -- Visible parts of S Visible(S)(X): INDUCTIVE bool = S(X) OR (EXISTS Y: Visible(S)(X ++ Y)) OR (EXISTS Y: Visible(S)(Y ++ X)) Inj_Visible: LEMMA Visible(S)(X) WHEN S(X) Fst_Visible: LEMMA Visible(S)(X) WHEN Visible(S)(X ++ Y) Snd_Visible: LEMMA Visible(S)(X) WHEN Visible(S)(Y ++ X) Visible_induct: LEMMA subset?(S, P) AND (FORALL X, Y: P(X ++ Y) => P(X)) AND (FORALL X, Y: P(X ++ Y) => P(Y)) IMPLIES subset?(Visible(S), P) Visible_sub: LEMMA subset?(S, Visible(S)) Visible_emptyset: LEMMA Visible(emptyset) = emptyset Visible_subset: LEMMA subset?(S1, S2) IMPLIES subset?(Visible(S1), Visible(S2)) Visible_union: LEMMA Visible(union(S1, S2)) = union(Visible(S1), Visible(S2)) Visible_atom: LEMMA Visible(S0) = S0 Visible_member_aux: LEMMA Visible(S)(X) IMPLIES subset?(Visible(X), Visible(S)) Visible_member: LEMMA S(X) IMPLIES subset?(Visible(X), Visible(S)) Visible_equiv: LEMMA Visible(S) = { X | EXISTS Y: S(Y) AND Visible(Y)(X) } Visible_singleton: LEMMA Visible(singleton(X)) = Visible(X) Visible_add: LEMMA Visible(add(X, S)) = union(Visible(X), Visible(S)) % -- Analz Analz(S)(X): INDUCTIVE bool = S(X) OR (EXISTS Y: Analz(S)(X ++ Y)) OR (EXISTS Y: Analz(S)(Y ++ X)) OR (EXISTS K: Analz(S)(Encr(K, X)) AND Analz(S)(K)) Inj_Analz: LEMMA Analz(S)(X) WHEN S(X) Fst_Analz: LEMMA Analz(S)(X) WHEN Analz(S)(X ++ Y) Snd_Analz: LEMMA Analz(S)(X) WHEN Analz(S)(Y ++ X) Key_Analz: LEMMA Analz(S)(X) WHEN Analz(S)(Encr(K, X)) AND Analz(S)(K) Analz_induct: LEMMA subset?(S, P) AND (FORALL X, Y: P(X ++ Y) => P(X)) AND (FORALL X, Y: P(X ++ Y) => P(Y)) AND (FORALL X, K: P(Encr(K, X)) AND P(K) => P(X)) IMPLIES subset?(Analz(S), P) Analz_sub: LEMMA subset?(S, Analz(S)) Analz_emptyset: LEMMA Analz(emptyset) = emptyset Analz_subset: LEMMA subset?(S1, S2) IMPLIES subset?(Analz(S1), Analz(S2)) % -- Synth Synth(S)(X): INDUCTIVE bool = S(X) OR (EXISTS Y, Z: X = Y ++ Z AND Synth(S)(Y) AND Synth(S)(Z)) OR (EXISTS K, Y: X = Encr(K,Y) AND Synth(S)(K) AND Synth(S)(Y)) Inj_Synth : LEMMA Synth(S)(X) WHEN S(X) Comp_Synth: LEMMA Synth(S)(X ++ Y) WHEN Synth(S)(X) AND Synth(S)(Y) Key_Synth : LEMMA Synth(S)(Encr(K, X)) WHEN Synth(S)(X) AND Synth(S)(K) Synth_induct: LEMMA subset?(S, P) AND (FORALL X, Y: P(X) AND P(Y) => P(X ++ Y)) AND (FORALL X, K: P(X) AND P(K) => P(Encr(K, X))) IMPLIES subset?(Synth(S), P) Synth_sub: LEMMA subset?(S, Synth(S)) Synth_emptyset: LEMMA Synth(emptyset) = emptyset Synth_subset: LEMMA subset?(S1, S2) IMPLIES subset?(Synth(S1), Synth(S2)) Synth_Atom: LEMMA Synth(S)(X0) IFF S(X0) % -- Theorems Parts_idempotent: LEMMA Parts(Parts(S)) = Parts(S) Visible_idempotent: LEMMA Visible(Visible(S)) = Visible(S) Analz_idempotent: LEMMA Analz(Analz(S)) = Analz(S) Synth_idempotent: LEMMA Synth(Synth(S)) = Synth(S) Parts_Analz1 : LEMMA subset?(Analz(S), Parts(S)) Analz_Visible1: LEMMA subset?(Visible(S), Analz(S)) Parts_Visible1: LEMMA subset?(Visible(S), Parts(S)) Parts_Analz: LEMMA Parts(Analz(S)) = Parts(S) Analz_Parts: LEMMA Analz(Parts(S)) = Parts(S) Parts_Visible: LEMMA Parts(Visible(S)) = Parts(S) Visible_Parts: LEMMA Visible(Parts(S)) = Parts(S) Analz_Visible: LEMMA Analz(Visible(S)) = Analz(S) Visible_Analz: LEMMA Visible(Analz(S)) = Analz(S) Parts_Synth: LEMMA Parts(Synth(S)) = union(Parts(S), Synth(S)) Analz_Synth: LEMMA Analz(Synth(S)) = union(Analz(S), Synth(S)) Visible_Synth: LEMMA Visible(Synth(S)) = union(Visible(S), Synth(S)) Analz_union1: LEMMA (FORALL K: not Visible(S2)(K)) AND (FORALL K, X: Visible(S2)(Encr(K, X)) => not Analz(S1)(K)) IMPLIES Analz(union(S1, S2)) = union(Analz(S1), Visible(S2)) Analz_union2: LEMMA (FORALL K: not Parts(S2)(K)) IMPLIES subset?(Analz(union(S1, S2)), union(Analz(S1), Parts(S2))) % -- Fake Fake(S): set[field] = Synth(Analz(S)) Fake_Parts: LEMMA Parts(Fake(S)) = union(Parts(S), Fake(S)) Fake_mono: LEMMA subset?(S,S1) => subset?(Fake(S),Fake(S1)) END basics $$$basics.prf (|basics| (|Inj_parts| "" (GRIND) (("" (EXPAND "Parts") (("" (PROPAX) NIL NIL)) NIL)) NIL) (|Fst_parts| "" (SKOSIMP) (("" (EXPAND "Parts" +) (("" (REDUCE) NIL NIL)) NIL)) NIL) (|Snd_parts| "" (SKOSIMP) (("" (EXPAND "Parts" +) (("" (REDUCE) NIL NIL)) NIL)) NIL) (|Body_parts| "" (SKOSIMP) (("" (EXPAND "Parts" +) (("" (REDUCE) NIL NIL)) NIL)) NIL) (|Parts_induct| "" (SKOSIMP) (("" (EXPAND* "subset?" "member") (("" (REWRITE "Parts_induction") (("" (DELETE 2) (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Parts_sub| "" (SKOSIMP*) (("" (EXPAND "Parts") (("" (GRIND) NIL NIL)) NIL)) NIL) (|Parts_emptyset| "" (AUTO-REWRITE "subset_emptyset" "emptyset") (("" (REWRITE "subset_antisymmetric") (("" (REWRITE "Parts_induct") NIL NIL)) NIL)) NIL) (|Parts_subset| "" (AUTO-REWRITE "Inj_parts" "Fst_parts" "Snd_parts" "Body_parts") (("" (SKOSIMP) (("" (REWRITE "Parts_induct") (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Parts_union| "" (SKOLEM!) (("" (AUTO-REWRITE "Parts_sub" "Parts_subset" "union_upper_bound") (("" (CASE "subset?(S1!1, union(S1!1, S2!1)) AND subset?(S2!1, union(S1!1, S2!1))") (("1" (GROUND) (("1" (REWRITE "subset_antisymmetric") (("1" (DELETE -1 -2 2) (("1" (AUTO-REWRITE "Inj_parts" "union" "member" "subset?") (("1" (REWRITE "Parts_induct") (("1" (REDUCE) NIL NIL) ("2" (DELETE 2) (("2" (REDUCE) (("1" (FORWARD-CHAIN "Fst_parts") NIL NIL) ("2" (FORWARD-CHAIN "Fst_parts") NIL NIL)) NIL)) NIL) ("3" (DELETE 2) (("3" (REDUCE) (("1" (FORWARD-CHAIN "Snd_parts") NIL NIL) ("2" (FORWARD-CHAIN "Snd_parts") NIL NIL)) NIL)) NIL) ("4" (DELETE 2) (("4" (REDUCE) (("1" (FORWARD-CHAIN "Body_parts") NIL NIL) ("2" (FORWARD-CHAIN "Body_parts") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Parts_atom| "" (SKOLEM-TYPEPRED) (("" (AUTO-REWRITE "subset_reflexive" "Parts_sub") (("" (REWRITE "subset_antisymmetric") (("" (APPLY (THEN (REWRITE "Parts_induct") (DELETE 2 3) (GRIND))) NIL NIL)) NIL)) NIL)) NIL) (|Parts_member_aux| "" (SKOLEM + ("S!1" _)) (("" (INDUCT-AND-SIMPLIFY "X" :IF-MATCH NIL :REWRITES ("Inj_parts")) (("1" (INST? :POLARITY? T) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST? -2 :POLARITY? T) (("2" (ASSERT) NIL NIL)) NIL) ("3" (FORWARD-CHAIN "Snd_parts") NIL NIL) ("4" (FORWARD-CHAIN "Snd_parts") NIL NIL) ("5" (FORWARD-CHAIN "Fst_parts") NIL NIL) ("6" (FORWARD-CHAIN "Fst_parts") NIL NIL) ("7" (FORWARD-CHAIN "Fst_parts") NIL NIL) ("8" (FORWARD-CHAIN "Fst_parts") NIL NIL) ("9" (INST!) (("9" (ASSERT) NIL NIL)) NIL) ("10" (FORWARD-CHAIN "Body_parts") NIL NIL)) NIL)) NIL) (|Parts_member| "" (AUTO-REWRITE "Parts_member_aux" "Inj_parts") (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|Parts_equiv| "" (SKOLEM!) (("" (REWRITE "subset_antisymmetric") (("1" (DELETE 2) (("1" (REWRITE "Parts_induct") (("1" (DELETE 2) (("1" (GRIND :EXCLUDE ("Parts") :REWRITES ("Parts_self")) NIL NIL)) NIL) ("2" (REDUCE) (("2" (FORWARD-CHAIN "Parts_head") NIL NIL)) NIL) ("3" (REDUCE) (("3" (FORWARD-CHAIN "Parts_tail") NIL NIL)) NIL) ("4" (REDUCE) (("4" (FORWARD-CHAIN "Parts_text") NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND :EXCLUDE ("Parts")) (("2" (FORWARD-CHAIN "Parts_member") (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Parts_singleton| "" (SKOLEM!) (("" (EXPAND "singleton") (("" (REWRITE "Parts_equiv") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Parts_add| "" (SKOLEM!) (("" (CASE-REPLACE "add(X!1, S!1) = union(singleton(X!1), S!1)") (("1" (REWRITE "Parts_union") (("1" (REWRITE "Parts_singleton") NIL NIL)) NIL) ("2" (DELETE 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Inj_Visible| "" (SKOSIMP) (("" (EXPAND "Visible" +) (("" (REDUCE) NIL NIL)) NIL)) NIL) (|Fst_Visible| "" (SKOSIMP) (("" (EXPAND "Visible" +) (("" (REDUCE) NIL NIL)) NIL)) NIL) (|Snd_Visible| "" (SKOSIMP) (("" (EXPAND "Visible" +) (("" (REDUCE) NIL NIL)) NIL)) NIL) (|Visible_induct| "" (SKOSIMP) (("" (EXPAND* "subset?" "member") (("" (REWRITE "Visible_weak_induction") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL) (|Visible_sub| "" (GRIND :REWRITES ("Inj_Visible")) NIL NIL) (|Visible_emptyset| "" (USE "Visible_induct" ("P" "emptyset[field]")) (("" (AUTO-REWRITE "subset?" "member" "emptyset") (("" (REDUCE) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Visible_subset| "" (AUTO-REWRITE "Inj_Visible" "Fst_Visible" "Snd_Visible") (("" (SKOSIMP) (("" (REWRITE "Visible_induct") (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Visible_union| "" (SKOLEM!) (("" (AUTO-REWRITE "Visible_sub" "Visible_subset" "union_upper_bound") (("" (CASE "subset?(S1!1, union(S1!1, S2!1)) AND subset?(S2!1, union(S1!1, S2!1))") (("1" (GROUND) (("1" (REWRITE "subset_antisymmetric") (("1" (DELETE -1 -2 2) (("1" (AUTO-REWRITE "Inj_Visible" "union" "member" "subset?") (("1" (REWRITE "Visible_induct") (("1" (REDUCE) NIL NIL) ("2" (DELETE 2) (("2" (REDUCE) (("1" (FORWARD-CHAIN "Fst_Visible") NIL NIL) ("2" (FORWARD-CHAIN "Fst_Visible") NIL NIL)) NIL)) NIL) ("3" (DELETE 2) (("3" (REDUCE) (("1" (FORWARD-CHAIN "Snd_Visible") NIL NIL) ("2" (FORWARD-CHAIN "Snd_Visible") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Visible_atom| "" (SKOLEM-TYPEPRED) (("" (AUTO-REWRITE "subset_reflexive" "Visible_sub") (("" (REWRITE "subset_antisymmetric") (("" (APPLY (THEN (REWRITE "Visible_induct") (DELETE 2 3) (GRIND))) NIL NIL)) NIL)) NIL)) NIL) (|Visible_member_aux| "" (SKOLEM + ("S!1" _)) (("" (INDUCT-AND-SIMPLIFY "X" :IF-MATCH NIL :REWRITES ("Inj_Visible")) (("1" (INST? :POLARITY? T) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST? -2 :POLARITY? T) (("2" (ASSERT) NIL NIL)) NIL) ("3" (FORWARD-CHAIN "Snd_Visible") NIL NIL) ("4" (FORWARD-CHAIN "Snd_Visible") NIL NIL) ("5" (FORWARD-CHAIN "Fst_Visible") NIL NIL) ("6" (FORWARD-CHAIN "Fst_Visible") NIL NIL) ("7" (FORWARD-CHAIN "Fst_Visible") NIL NIL) ("8" (FORWARD-CHAIN "Fst_Visible") NIL NIL)) NIL)) NIL) (|Visible_member| "" (AUTO-REWRITE "Visible_member_aux" "Inj_Visible") (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|Visible_equiv| "" (SKOLEM!) (("" (REWRITE "subset_antisymmetric") (("1" (DELETE 2) (("1" (REWRITE "Visible_induct") (("1" (DELETE 2) (("1" (GRIND :EXCLUDE ("Visible") :REWRITES ("Visible_self")) NIL NIL)) NIL) ("2" (REDUCE) (("2" (FORWARD-CHAIN "Visible_head") NIL NIL)) NIL) ("3" (REDUCE) (("3" (FORWARD-CHAIN "Visible_tail") NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND :EXCLUDE ("Visible")) (("2" (FORWARD-CHAIN "Visible_member") (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Visible_singleton| "" (SKOLEM!) (("" (EXPAND "singleton") (("" (REWRITE "Visible_equiv") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Visible_add| "" (SKOLEM!) (("" (CASE-REPLACE "add(X!1, S!1) = union(singleton(X!1), S!1)") (("1" (REWRITE "Visible_union") (("1" (REWRITE "Visible_singleton") NIL NIL)) NIL) ("2" (DELETE 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Inj_Analz| "" (SKOSIMP) (("" (EXPAND "Analz" +) (("" (REDUCE) NIL NIL)) NIL)) NIL) (|Fst_Analz| "" (SKOSIMP) (("" (EXPAND "Analz" +) (("" (REDUCE) NIL NIL)) NIL)) NIL) (|Snd_Analz| "" (SKOSIMP) (("" (EXPAND "Analz" +) (("" (REDUCE) NIL NIL)) NIL)) NIL) (|Key_Analz| "" (SKOSIMP) (("" (EXPAND "Analz" +) (("" (REDUCE) NIL NIL)) NIL)) NIL) (|Analz_induct| "" (SKOSIMP) (("" (EXPAND* "subset?" "member") (("" (REWRITE "Analz_induction") (("" (DELETE 2) (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Analz_sub| "" (SKOSIMP*) (("" (EXPAND "Analz") (("" (GRIND) NIL NIL)) NIL)) NIL) (|Analz_emptyset| "" (USE "Analz_induct" ("P" "emptyset[field]")) (("" (AUTO-REWRITE "subset?" "member" "emptyset") (("" (REDUCE) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Analz_subset| "" (AUTO-REWRITE "Inj_Analz" "Fst_Analz" "Snd_Analz" "Key_Analz") (("" (SKOSIMP) (("" (REWRITE "Analz_induct") (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Inj_Synth| "" (SKOSIMP) (("" (EXPAND "Synth" +) (("" (REDUCE) NIL NIL)) NIL)) NIL) (|Comp_Synth| "" (SKOSIMP) (("" (EXPAND "Synth" +) (("" (REDUCE) NIL NIL)) NIL)) NIL) (|Key_Synth| "" (SKOSIMP) (("" (EXPAND "Synth" +) (("" (REDUCE) NIL NIL)) NIL)) NIL) (|Synth_induct| "" (SKOSIMP) (("" (EXPAND* "subset?" "member") (("" (REWRITE "Synth_induction") (("" (DELETE 2) (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Synth_sub| "" (EXPAND "Synth") (("" (GRIND) NIL NIL)) NIL) (|Synth_emptyset| "" (USE "Synth_induct" ("P" "emptyset[field]")) (("" (AUTO-REWRITE "subset?" "member" "emptyset") (("" (REDUCE) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Synth_subset| "" (SKOSIMP) (("" (AUTO-REWRITE "Inj_Synth" "Comp_Synth" "Key_Synth") (("" (REWRITE "Synth_induct") (("1" (DELETE 2) (("1" (GRIND) NIL NIL)) NIL) ("2" (REDUCE) NIL NIL) ("3" (REDUCE) NIL NIL)) NIL)) NIL)) NIL) (|Synth_Atom| "" (EXPAND "Synth") (("" (GRIND) NIL NIL)) NIL) (|Parts_idempotent| "" (AUTO-REWRITE "Inj_parts" "Fst_parts" "Snd_parts" "Body_parts" "Parts_subset" "Parts_sub" "subset_reflexive") (("" (SKOLEM!) (("" (REWRITE "subset_antisymmetric") (("" (DELETE 2) (("" (REWRITE "Parts_induct") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Visible_idempotent| "" (AUTO-REWRITE "Inj_Visible" "Fst_Visible" "Snd_Visible" "Body_Visible" "Visible_subset" "Visible_sub" "subset_reflexive") (("" (SKOLEM!) (("" (REWRITE "subset_antisymmetric") (("" (DELETE 2) (("" (REWRITE "Visible_induct") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Analz_idempotent| "" (AUTO-REWRITE "Inj_Analz" "Fst_Analz" "Snd_Analz" "Key_Analz" "Analz_subset" "Analz_sub" "subset_reflexive") (("" (SKOLEM!) (("" (REWRITE "subset_antisymmetric") (("" (DELETE 2) (("" (REWRITE "Analz_induct") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Synth_idempotent| "" (AUTO-REWRITE "Inj_Synth" "Comp_Synth" "Key_Synth" "Synth_subset" "Synth_sub" "subset_reflexive") (("" (SKOLEM!) (("" (REWRITE "subset_antisymmetric") (("" (DELETE 2) (("" (REWRITE "Synth_induct") (("1" (REDUCE) NIL NIL) ("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Parts_Analz1| "" (SKOLEM!) (("" (AUTO-REWRITE "Inj_parts" "Fst_parts" "Snd_parts" "Parts_sub") (("" (REWRITE "Analz_induct") (("" (SKOSIMP) (("" (FORWARD-CHAIN "Body_parts") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Analz_Visible1| "" (SKOLEM!) (("" (AUTO-REWRITE "Inj_Analz" "Fst_Analz" "Snd_Analz" "Analz_sub") (("" (REWRITE "Visible_induct") NIL NIL)) NIL)) NIL) (|Parts_Visible1| "" (SKOLEM!) (("" (USE* "Parts_Analz1" "Analz_Visible1") (("" (FORWARD-CHAIN "subset_transitive") NIL NIL)) NIL)) NIL) (|Parts_Analz| "" (AUTO-REWRITE "Inj_parts" "Fst_parts" "Snd_parts" "Body_parts" "Parts_subset" "Analz_sub" "Parts_Analz1") (("" (SKOLEM!) (("" (REWRITE "subset_antisymmetric") (("" (DELETE 2) (("" (REWRITE "Parts_induct") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Analz_Parts| "" (SKOLEM!) (("" (AUTO-REWRITE "Analz_sub" "subset_reflexive" "Fst_parts" "Snd_parts" "Body_parts") (("" (REWRITE "subset_antisymmetric") (("" (DELETE 2) (("" (REWRITE "Analz_induct") (("" (SKOSIMP) (("" (FORWARD-CHAIN "Body_parts") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Parts_Visible| "" (AUTO-REWRITE "Inj_parts" "Fst_parts" "Snd_parts" "Body_parts" "Parts_subset" "Visible_sub" "Parts_Visible1") (("" (SKOLEM!) (("" (REWRITE "subset_antisymmetric") (("" (DELETE 2) (("" (REWRITE "Parts_induct") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Visible_Parts| "" (SKOLEM!) (("" (AUTO-REWRITE "Visible_sub" "subset_reflexive" "Fst_parts" "Snd_parts" "Body_parts") (("" (REWRITE "subset_antisymmetric") (("" (DELETE 2) (("" (REWRITE "Visible_induct") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Analz_Visible| "" (AUTO-REWRITE "Inj_Analz" "Fst_Analz" "Snd_Analz" "Key_Analz" "Analz_subset" "Visible_sub" "Analz_Visible1") (("" (SKOLEM!) (("" (REWRITE "subset_antisymmetric") (("" (DELETE 2) (("" (REWRITE "Analz_induct") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Visible_Analz| "" (SKOLEM!) (("" (AUTO-REWRITE "Visible_sub" "subset_reflexive" "Fst_Analz" "Snd_Analz" "Key_Analz") (("" (REWRITE "subset_antisymmetric") (("" (DELETE 2) (("" (REWRITE "Visible_induct") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Parts_Synth| "" (SKOLEM!) (("" (AUTO-REWRITE "Parts_subset" "Synth_sub" "Parts_sub" "union_upper_bound" "equal_conc" "equal_encr") (("" (REWRITE "subset_antisymmetric") (("" (DELETE 2) (("" (AUTO-REWRITE "union" "member" "Inj_parts") (("" (REWRITE "Parts_induct") (("1" (DELETE 2) (("1" (GRIND) NIL NIL)) NIL) ("2" (SKOSIMP) (("2" (CASE "Parts(S!1)(X!1 ++ Y!1)") (("1" (FORWARD-CHAIN "Fst_parts") NIL NIL) ("2" (EXPAND "Synth" -) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP) (("3" (CASE "Parts(S!1)(X!1 ++ Y!1)") (("1" (FORWARD-CHAIN "Snd_parts") NIL NIL) ("2" (ASSERT) (("2" (EXPAND "Synth" -) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("4" (SKOSIMP) (("4" (CASE "Parts(S!1)(Encr(K!1, X!1))") (("1" (FORWARD-CHAIN "Body_parts") NIL NIL) ("2" (ASSERT) (("2" (EXPAND "Synth" -) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Analz_Synth| "" (SKOLEM!) (("" (AUTO-REWRITE "Analz_subset" "Synth_sub" "Analz_sub" "union_upper_bound" "equal_conc" "equal_encr") (("" (REWRITE "subset_antisymmetric") (("" (DELETE 2) (("" (AUTO-REWRITE "union" "member" "Inj_Analz") (("" (REWRITE "Analz_induct") (("1" (DELETE 2) (("1" (GRIND) NIL NIL)) NIL) ("2" (SKOSIMP) (("2" (CASE "Analz(S!1)(X!1 ++ Y!1)") (("1" (FORWARD-CHAIN "Fst_Analz") NIL NIL) ("2" (ASSERT) (("2" (EXPAND "Synth" -) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP) (("3" (CASE "Analz(S!1)(X!1 ++ Y!1)") (("1" (FORWARD-CHAIN "Snd_Analz") NIL NIL) ("2" (ASSERT) (("2" (EXPAND "Synth" -) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("4" (SKOSIMP) (("4" (CASE "Analz(S!1)(Key(K!1))") (("1" (DELETE -3) (("1" (CASE "Analz(S!1)(Encr(K!1, X!1))") (("1" (FORWARD-CHAIN "Key_Analz") NIL NIL) ("2" (ASSERT) (("2" (EXPAND "Synth" -) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 2 3 4) (("2" (EXPAND "Synth") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Visible_Synth| "" (SKOLEM!) (("" (AUTO-REWRITE "Visible_subset" "Synth_sub" "Visible_sub" "union_upper_bound" "equal_conc" "equal_encr") (("" (REWRITE "subset_antisymmetric") (("" (DELETE 2) (("" (AUTO-REWRITE "union" "member" "Inj_Visible") (("" (REWRITE "Visible_induct") (("1" (DELETE 2) (("1" (GRIND) NIL NIL)) NIL) ("2" (SKOSIMP) (("2" (CASE "Visible(S!1)(X!1 ++ Y!1)") (("1" (FORWARD-CHAIN "Fst_Visible") NIL NIL) ("2" (ASSERT) (("2" (EXPAND "Synth" -) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP) (("3" (CASE "Visible(S!1)(X!1 ++ Y!1)") (("1" (FORWARD-CHAIN "Snd_Visible") NIL NIL) ("2" (ASSERT) (("2" (EXPAND "Synth" -) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Analz_union1| "" (SKOSIMP) (("" (AUTO-REWRITE "union" "member" "Inj_Analz" "Inj_Visible") (("" (REWRITE "subset_antisymmetric") (("1" (DELETE 2) (("1" (REWRITE "Analz_induct") (("1" (DELETE -1 -2 2) (("1" (REWRITE "union_upper_bound") (("1" (DELETE 2) (("1" (GRIND) NIL NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (SPLIT) (("1" (FORWARD-CHAIN "Fst_Analz") NIL NIL) ("2" (FORWARD-CHAIN "Fst_Visible") NIL NIL)) NIL)) NIL) ("3" (SKOSIMP) (("3" (SPLIT) (("1" (FORWARD-CHAIN "Snd_Analz") NIL NIL) ("2" (FORWARD-CHAIN "Snd_Visible") NIL NIL)) NIL)) NIL) ("4" (REDUCE) (("4" (FORWARD-CHAIN "Key_Analz") NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 -2 2) (("2" (CASE "subset?(S1!1, union(S1!1, S2!1)) AND subset?(S2!1, union(S1!1, S2!1))") (("1" (AUTO-REWRITE "Analz_subset") (("1" (GROUND) (("1" (REWRITE "union_upper_bound") (("1" (USE "Analz_Visible1" ("S" "S2!1")) (("1" (USE "subset_transitive" ("a" "Visible(S2!1)" "b" "Analz(S2!1)" "c" "Analz(union(S1!1, S2!1))")) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Analz_union2| "" (SKOSIMP) (("" (REWRITE "Analz_induct") (("1" (DELETE -1 2) (("1" (REWRITE "union_upper_bound") (("1" (DELETE 2) (("1" (GRIND :REWRITES ("Inj_Analz")) NIL NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND :REWRITES ("Inj_parts")) NIL NIL)) NIL)) NIL)) NIL) ("2" (AUTO-REWRITE "union" "member") (("2" (DELETE 2) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (GROUND) (("1" (FORWARD-CHAIN "Fst_Analz") NIL NIL) ("2" (FORWARD-CHAIN "Fst_parts") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (AUTO-REWRITE "union" "member") (("3" (ASSERT) (("3" (SKOSIMP) (("3" (GROUND) (("1" (FORWARD-CHAIN "Snd_Analz") NIL NIL) ("2" (FORWARD-CHAIN "Snd_parts") NIL NIL)) NIL)) NIL)) NIL)) NIL) ("4" (AUTO-REWRITE "union" "member") (("4" (ASSERT) (("4" (SKOSIMP) (("4" (INST?) (("4" (GROUND) (("1" (FORWARD-CHAIN "Key_Analz") NIL NIL) ("2" (FORWARD-CHAIN "Body_parts") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Fake_Parts| "" (SKOLEM!) (("" (EXPAND "Fake") (("" (REWRITE "Parts_Synth") (("" (REWRITE "Parts_Analz") NIL NIL)) NIL)) NIL)) NIL) (|Fake_mono| "" (AUTO-REWRITE "Fake" "Synth_subset" "Analz_subset") (("" (REDUCE) NIL NIL)) NIL)) $$$ideals.pvs ideals : THEORY BEGIN IMPORTING basics X, Y, Z: VAR field K: VAR key S, S1, S2: VAR set[field] P: VAR pred[field] X0: VAR (Atom?) S0: VAR { S | subset?(S, Atom?) } %----------------------- % Ideal generated by S %----------------------- Ideal(S)(X): INDUCTIVE bool = S(X) OR (EXISTS Y, Z: X = Y ++ Z AND (Ideal(S)(Y) OR Ideal(S)(Z))) OR (EXISTS Y, K: X = Encr(K, Y) AND Ideal(S)(Y) AND NOT S(K)) Inj_Ideal: LEMMA Ideal(S)(X) WHEN S(X) Fst_Ideal: LEMMA Ideal(S)(X ++ Y) WHEN Ideal(S)(X) Snd_Ideal: LEMMA Ideal(S)(X ++ Y) WHEN Ideal(S)(Y) Conc_Ideal: LEMMA Ideal(S)(X ++ Y) WHEN Ideal(S)(X) OR Ideal(S)(Y) Key_Ideal: LEMMA Ideal(S)(Encr(K, X)) WHEN Ideal(S)(X) AND NOT S(K) Ideal_induct: LEMMA subset?(S, P) AND (FORALL X, Y: P(X) OR P(Y) => P(X ++ Y)) AND (FORALL X, K: P(X) AND NOT S(K) => P(Encr(K, X))) IMPLIES subset?(Ideal(S), P) Ideal_emptyset: LEMMA Ideal(emptyset) = emptyset Ideal_sub: LEMMA subset?(S, Ideal(S)) %--------------------- % Basic properties %--------------------- Ideal_Atom: LEMMA Ideal(S)(X0) IFF S(X0) Ideal_Conc: LEMMA Ideal(S0)(X ++ Y) IFF Ideal(S0)(X) OR Ideal(S0)(Y) Ideal_Encr: LEMMA Ideal(S0)(Encr(K, X)) IFF Ideal(S0)(X) AND NOT S0(K) %----------------------- % Closures of Coideal %----------------------- Coideal(S)(X): bool = NOT Ideal(S)(X) Analz_Closure: LEMMA Analz(Coideal(S)) = Coideal(S) Visible_Closure: LEMMA Visible(Coideal(S)) = Coideal(S) Synth_Closure: LEMMA Synth(Coideal(S0)) = Coideal(S0) Fake_Closure: LEMMA Fake(Coideal(S0)) = Coideal(S0) Analz_Closure_Subset: LEMMA subset?(S1, Coideal(S)) IMPLIES subset?(Analz(S1), Coideal(S)) Visible_Closure_Subset: LEMMA subset?(S1, Coideal(S)) IMPLIES subset?(Visible(S1), Coideal(S)) Synth_Closure_Subset: LEMMA subset?(S1, Coideal(S0)) IMPLIES subset?(Synth(S1), Coideal(S0)) Fake_Closure_Subset: LEMMA subset?(S1, Coideal(S0)) IMPLIES subset?(Fake(S1), Coideal(S0)) %--------------------------- % Ideal-Parts and variant %--------------------------- Ideal_Parts: LEMMA Ideal(S)(X) IMPLIES (EXISTS Z: S(Z) AND Parts(X)(Z)) Subset_Coideal: LEMMA disjoint?(Parts(S1), S) IMPLIES subset?(S1, Coideal(S)) Parts_Coideal: LEMMA disjoint?(Parts(S1), S) IMPLIES subset?(Parts(S1), Coideal(S)) %---------------------------------------------------- % More lemmas to show that X belongs to Coideal(S) %---------------------------------------------------- Coideal_Encr: LEMMA Coideal(S0)(Encr(K, X)) IFF S0(K) OR Coideal(S0)(X) Coideal_Conc: LEMMA Coideal(S0)(X ++ Y) IFF Coideal(S0)(X) AND Coideal(S0)(Y) Coideal_Atom: LEMMA Coideal(S)(X0) IFF NOT S(X0) %------------------------------------------------------ % Variants of Ideal and Coideal to avoid conversions %------------------------------------------------------ Ideal(X): set[field] = Ideal(singleton(X)) Coideal(X): set[field] = Coideal(singleton(X)) END ideals $$$ideals.prf (|ideals| (|Inj_Ideal| "" (SKOSIMP) (("" (EXPAND "Ideal" +) (("" (REDUCE) NIL NIL)) NIL)) NIL) (|Fst_Ideal| "" (SKOSIMP) (("" (EXPAND "Ideal" +) (("" (REDUCE) NIL NIL)) NIL)) NIL) (|Snd_Ideal| "" (SKOSIMP) (("" (EXPAND "Ideal" +) (("" (REDUCE) NIL NIL)) NIL)) NIL) (|Conc_Ideal| "" (SKOSIMP) (("" (EXPAND "Ideal" +) (("" (REDUCE) NIL NIL)) NIL)) NIL) (|Key_Ideal| "" (SKOSIMP) (("" (EXPAND "Ideal" +) (("" (REDUCE) NIL NIL)) NIL)) NIL) (|Ideal_induct| "" (EXPAND* "subset?" "member") (("" (SKOSIMP) (("" (REWRITE "Ideal_induction") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL) (|Ideal_emptyset| "" (USE "emptyset_min[field]" ("a" "Ideal(emptyset)")) (("" (AUTO-REWRITE "emptyset" "subset_reflexive" "Ideal_induct") (("" (GROUND) NIL NIL)) NIL)) NIL) (|Ideal_sub| "" (GRIND :REWRITES ("Inj_Ideal")) NIL NIL) (|Ideal_Atom| "" (EXPAND "Ideal") (("" (GRIND) NIL NIL)) NIL) (|Ideal_Conc| "" (SKOLEM!) (("" (AUTO-REWRITE "Conc_Ideal" "equal_conc") (("" (REDUCE) (("" (EXPAND "Ideal" -) (("" (GROUND) (("1" (TYPEPRED "S0!1") (("1" (DELETE +) (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Ideal_Encr| "" (AUTO-REWRITE "Key_Ideal" "equal_encr" "subset?" "Atom?" "member") (("" (SKOLEM-TYPEPRED) (("" (GROUND) (("1" (EXPAND "Ideal" -) (("1" (REDUCE :IF-MATCH ALL) NIL NIL)) NIL) ("2" (EXPAND "Ideal" -) (("2" (REDUCE :IF-MATCH ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Analz_Closure| "" (SKOLEM!) (("" (AUTO-REWRITE "Analz_sub" "subset_reflexive" "Coideal" "Conc_Ideal" "Inj_Ideal") (("" (REWRITE "subset_antisymmetric") (("" (DELETE 2) (("" (REWRITE "Analz_induct") (("1" (REDUCE) NIL NIL) ("2" (REDUCE) NIL NIL) ("3" (REDUCE) (("3" (REWRITE "Key_Ideal") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Visible_Closure| "" (SKOLEM!) (("" (AUTO-REWRITE "Visible_sub" "subset_reflexive" "Coideal" "Conc_Ideal" "Inj_Ideal") (("" (REWRITE "subset_antisymmetric") (("" (DELETE 2) (("" (REWRITE "Visible_induct") (("1" (REDUCE) NIL NIL) ("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Synth_Closure| "" (SKOLEM!) (("" (AUTO-REWRITE "Synth_sub" "subset_reflexive" "Coideal" "Ideal_Conc" "Ideal_Encr") (("" (REWRITE "subset_antisymmetric") (("" (DELETE 2) (("" (REWRITE "Synth_induct") (("1" (REDUCE) NIL NIL) ("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Fake_Closure| "" (AUTO-REWRITE "Fake" "Synth_Closure" "Analz_Closure") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|Analz_Closure_Subset| "" (AUTO-REWRITE "Analz_Closure") (("" (SKOSIMP) (("" (FORWARD-CHAIN "Analz_subset") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|Visible_Closure_Subset| "" (AUTO-REWRITE "Visible_Closure") (("" (SKOSIMP) (("" (FORWARD-CHAIN "Visible_subset") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|Synth_Closure_Subset| "" (AUTO-REWRITE "Synth_Closure") (("" (SKOSIMP) (("" (FORWARD-CHAIN "Synth_subset") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|Fake_Closure_Subset| "" (AUTO-REWRITE "Fake" "Analz_Closure_Subset" "Synth_Closure_Subset") (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|Ideal_Parts| "" (SKOSIMP) (("" (CASE "subset?(Ideal(S!1), { X | EXISTS Z: S!1(Z) AND Parts(X)(Z) })") (("1" (GRIND :EXCLUDE "Parts") NIL NIL) ("2" (DELETE -1 2) (("2" (REWRITE "Ideal_induct") (("1" (DELETE 2) (("1" (GRIND :EXCLUDE ("Parts") :REWRITES ("Parts_self")) NIL NIL)) NIL) ("2" (APPLY (THEN (GRIND :IF-MATCH NIL) (INST?) (ASSERT))) NIL NIL) ("3" (APPLY (THEN (GRIND :IF-MATCH NIL) (INST?) (ASSERT))) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Subset_Coideal| "" (SKOSIMP) (("" (GRIND :IF-MATCH NIL) (("" (FORWARD-CHAIN "Ideal_Parts") (("" (AUTO-REWRITE "Parts_equiv") (("" (REDUCE :IF-MATCH NIL) (("" (INST - "Z!1") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Parts_Coideal| "" (AUTO-REWRITE "Parts_idempotent" "Subset_Coideal") (("" (REDUCE) NIL NIL)) NIL) (|Coideal_Encr| "" (AUTO-REWRITE "Coideal" "Ideal_Encr") (("" (REDUCE) NIL NIL)) NIL) (|Coideal_Conc| "" (AUTO-REWRITE "Coideal" "Ideal_Conc") (("" (REDUCE) NIL NIL)) NIL) (|Coideal_Atom| "" (AUTO-REWRITE "Coideal" "Ideal_Atom") (("" (REDUCE) NIL NIL)) NIL)) $$$protocols.pvs protocols [ (IMPORTING fields) event: TYPE, state: TYPE, content: [event -> set[field]], trace : [state -> set[event]] ] : THEORY BEGIN IMPORTING ideals X, Y, Z: VAR field e, f, g: VAR event q, q1, q2: VAR state A, B, C: VAR agent S, S1, S2: VAR set[field] %--------------- % Basic stuff %--------------- %--- Fields occurring in trace(q) ---- FieldsTrace(q): set[field] = { X | EXISTS e: trace(q)(e) AND content(e)(X) } %--- Parts of these fields --- PartsTrace(q): set[field] = Parts(FieldsTrace(q)) %--- Visible parts of these fields --- VisibleTrace(q): set[field] = Visible(FieldsTrace(q)) Visible_PartsTrace: LEMMA VisibleTrace(q)(X) => PartsTrace(q)(X) %--- Fresh nonces and keys --- FreshNonces(q): { S | subset?(S, Atom?) } = { X | Nonce?(X) AND NOT PartsTrace(q)(X) } UsedKeys(q): { S | subset?(S, Atom?) } = { X | SessionKey?(X) AND EXISTS Y: PartsTrace(q)(Encr(Val(X), Y)) } FreshKeys(q): { S | subset?(S, Atom?) } = { X | SessionKey?(X) AND NOT PartsTrace(q)(X) AND NOT UsedKeys(q)(X) } FreshFields(q): { S | subset?(S, Atom?) } = union(FreshNonces(q), FreshKeys(q)) Parts_FreshNonces: LEMMA Parts(FreshNonces(q)) = FreshNonces(q) Parts_FreshKeys: LEMMA Parts(FreshKeys(q)) = FreshKeys(q) Parts_FreshFields: LEMMA Parts(FreshFields(q)) = FreshFields(q) %------------------------------------------- % Initial knowledge: % only atoms, no nonces, no session keys %-------------------------------------------- init_set: TYPE = { S | subset?(S, Atom?) AND disjoint?(S, SessionKey?) AND disjoint?(S, Nonce?) } init_set_atoms: JUDGEMENT init_set SUBTYPE_OF { S | subset?(S, Atom?) } I: VAR [agent -> init_set] Parts_I: LEMMA Parts(I(A)) = I(A) Initial_NotFresh: LEMMA I(A)(X) IMPLIES NOT SessionKey?(X) AND NOT Nonce?(X) %----------------------------------------- % Fields that agent A know in state q %----------------------------------------- Know(I)(A, q): set[field] = Analz(union(I(A), FieldsTrace(q))) %------------------------------------------------------ % Fields that agent A can generate/fake in state q %------------------------------------------------------ Gen(I)(A, q): set[field] = Synth(union(Know(I)(A, q), FreshFields(q))) %--------------------------- % Rules for Know(I)(A, q) %--------------------------- X0: VAR (Atom?) Kl: VAR (LongTermKey?) Ks: VAR (SessionKey?) N : VAR (Nonce?) K : VAR key D : VAR data Know_Conc1: LEMMA Know(I)(A, q)(X ++ Y) IMPLIES Know(I)(A, q)(X) Know_Conc2: LEMMA Know(I)(A, q)(X ++ Y) IMPLIES Know(I)(A, q)(Y) Know_Encr: LEMMA Know(I)(A, q)(Encr(K, X)) AND Know(I)(A, q)(K) IMPLIES Know(I)(A, q)(X) Know_Init: LEMMA I(A)(X) IMPLIES Know(I)(A, q)(X) Know_Visible: LEMMA VisibleTrace(q)(X) IMPLIES Know(I)(A, q)(X) Know_Field2: LEMMA FieldsTrace(q)(X) IMPLIES Know(I)(A, q)(X) Know_Field: LEMMA trace(q)(e) IMPLIES subset?(content(e), Know(I)(A, q)) %----------------------------- % General properties of Gen %----------------------------- Gen_Conc: LEMMA Gen(I)(A, q)(X ++ Y) IFF Gen(I)(A, q)(X) AND Gen(I)(A, q)(Y) Gen_Encr: LEMMA Gen(I)(A, q)(Encr(K, X)) IFF Know(I)(A, q)(Encr(K, X)) OR Gen(I)(A, q)(K) AND Gen(I)(A, q)(X) Gen_Atom: LEMMA Gen(I)(A, q)(X0) IFF Know(I)(A, q)(X0) OR FreshNonces(q)(X0) OR FreshKeys(q)(X0) Gen_Data: LEMMA Gen(I)(A, q)(D) IFF Know(I)(A, q)(D) Gen_Agent: LEMMA Gen(I)(A, q)(B) IFF Know(I)(A, q)(B) Gen_Nonce: LEMMA Gen(I)(A, q)(N) IFF Know(I)(A, q)(N) OR FreshNonces(q)(N) Gen_LongTermKey: LEMMA Gen(I)(A, q)(Kl) IFF Know(I)(A, q)(Kl) Gen_SessionKey: LEMMA Gen(I)(A, q)(Ks) IFF Know(I)(A, q)(Ks) OR FreshKeys(q)(Ks) Gen_Visible: LEMMA Gen(I)(A, q)(X) AND Visible(X)(Y) IMPLIES Gen(I)(A, q)(Y) %----------------------------------------- % Relations between Know/Gen and Parts %----------------------------------------- Know_Parts: LEMMA Know(I)(A, q)(X) IMPLIES I(A)(X) OR PartsTrace(q)(X) Parts_Know: LEMMA Parts(Know(I)(A, q))(X) IFF I(A)(X) OR PartsTrace(q)(X) Parts_Gen_Atom: LEMMA Parts(Gen(I)(A, q))(X0) IMPLIES I(A)(X0) OR PartsTrace(q)(X0) OR FreshNonces(q)(X0) OR FreshKeys(q)(X0) Parts_Gen_LongTermKey: LEMMA Parts(Gen(I)(A, q))(Kl) IMPLIES I(A)(Kl) OR PartsTrace(q)(Kl) Parts_Gen_SessionKey: LEMMA Parts(Gen(I)(A, q))(Ks) IMPLIES FreshKeys(q)(Ks) OR PartsTrace(q)(Ks) Parts_Gen_Nonce: LEMMA Parts(Gen(I)(A, q))(N) IMPLIES FreshNonces(q)(N) OR PartsTrace(q)(N) %-------------------------------------------- % Transition relation and reachable states %-------------------------------------------- T: VAR [agent -> [state, event, state -> bool]] Q, P: VAR set[state] Reachable(Q, T)(q): INDUCTIVE bool = Q(q) OR EXISTS A, q1, e: Reachable(Q, T)(q1) AND T(A)(q1, e, q) Reachable_induct: LEMMA subset?(Q, P) AND (FORALL q1, q2, A, e: P(q1) & T(A)(q1, e, q2) => P(q2)) IMPLIES subset?(Reachable(Q, T), P) Reachable_induct2: LEMMA (FORALL q: Q(q) => P(q)) AND (FORALL q1, q2, A, e: P(q1) & T(A)(q1, e, q2) => P(q2)) IMPLIES (FORALL q: Reachable(Q, T)(q) => P(q)) Reachable_induct3: LEMMA (FORALL q: Q(q) => P(q)) AND (FORALL q1, q2, A, e: Reachable(Q, T)(q1) & P(q1) & T(A)(q1, e, q2) => P(q2)) IMPLIES (FORALL q: Reachable(Q, T)(q) => P(q)) %-------------------------------- % Protocol: (I, Q, T) % - I = initial knowledge % - Q = initial states % - T = transition relation %-------------------------------- Protocol?(I, Q, T): bool = (FORALL q: Q(q) => trace(q) = emptyset) AND (FORALL q1, q2, A, e: T(A)(q1, e, q2) => trace(q2) = add(e, trace(q1))) FieldsTrace_init: LEMMA Protocol?(I, Q, T) AND Q(q) IMPLIES FieldsTrace(q) = emptyset PartsTrace_init: LEMMA Protocol?(I, Q, T) AND Q(q) IMPLIES PartsTrace(q) = emptyset VisibleTrace_init: LEMMA Protocol?(I, Q, T) AND Q(q) IMPLIES VisibleTrace(q) = emptyset FieldsTrace_step: LEMMA Protocol?(I, Q, T) AND T(A)(q1, e, q2) IMPLIES FieldsTrace(q2) = union(content(e), FieldsTrace(q1)) PartsTrace_step: LEMMA Protocol?(I, Q, T) AND T(A)(q1, e, q2) IMPLIES PartsTrace(q2) = union(Parts(content(e)), PartsTrace(q1)) VisibleTrace_step: LEMMA Protocol?(I, Q, T) AND T(A)(q1, e, q2) IMPLIES VisibleTrace(q2) = union(Visible(content(e)), VisibleTrace(q1)) %---------------------- % Secrecy properties %---------------------- Ag: VAR set[agent] %--- Only agents in Ag know secret X ---% Secret(I)(X, Ag, q): bool = FORALL A: Know(I)(A, q)(X) IMPLIES Ag(A) %--- Only agents in Ag know secrets from S ---% Secret(I)(S, Ag, q): bool = FORALL A: disjoint?(S, Know(I)(A, q)) OR Ag(A) Secret_equiv: LEMMA Secret(I)(S, Ag, q) IFF (FORALL (X: (S)): Secret(I)(X, Ag, q)) %----------------- % Good protocol %----------------- GoodProtocol?(I, Q, T): bool = Protocol?(I, Q, T) AND (FORALL q1, q2, A, e: Reachable(Q, T)(q1) AND T(A)(q1, e, q2) => subset?(content(e), Gen(I)(A, q1))) %--------------------- % Regularity Lemmas %--------------------- Regular?(Ag, Kl)(I, Q, T): bool = (FORALL A: I(A)(Kl) => Ag(A)) AND (FORALL q1, q2, A, e: Reachable(Q, T)(q1) AND Ag(A) AND T(A)(q1, e, q2) => not Parts(content(e))(Kl)) Regularity: LEMMA GoodProtocol?(I, Q, T) AND Regular?(Ag, Kl)(I, Q, T) IMPLIES (FORALL q: Reachable(Q, T)(q) => not PartsTrace(q)(Kl)) Secrecy_of_long_term_keys: LEMMA GoodProtocol?(I, Q, T) AND Regular?(Ag, Kl)(I, Q, T) IMPLIES (FORALL q: Reachable(Q, T)(q) => Secret(I)(Kl, Ag, q)) StrongSecrecy_of_long_term_keys: LEMMA GoodProtocol?(I, Q, T) AND Regular?(Ag, Kl)(I, Q, T) IMPLIES (FORALL q: Reachable(Q, T)(q) => subset?(FieldsTrace(q), Coideal(Kl))) SK: VAR { S | subset?(S, LongTermKey?) } Regular?(Ag, SK)(I, Q, T): bool = (FORALL A: Ag(A) OR disjoint?(I(A), SK)) AND (FORALL q1, q2, A, e: Reachable(Q, T)(q1) AND Ag(A) AND T(A)(q1, e, q2) => disjoint?(Parts(content(e)), SK)) Regularity2: LEMMA GoodProtocol?(I, Q, T) AND Regular?(Ag, SK)(I, Q, T) IMPLIES (FORALL q: Reachable(Q, T)(q) => disjoint?(PartsTrace(q), SK)) Secrecy_of_long_term_keys2: LEMMA GoodProtocol?(I, Q, T) AND Regular?(Ag, SK)(I, Q, T) IMPLIES (FORALL q: Reachable(Q, T)(q) => Secret(I)(SK, Ag, q)) StrongSecrecy_of_long_term_keys2: LEMMA GoodProtocol?(I, Q, T) AND Regular?(Ag, SK)(I, Q, T) IMPLIES (FORALL q: Reachable(Q, T)(q) => subset?(FieldsTrace(q), Coideal(SK))) %--------------------------------- % New knowledge after each step %--------------------------------- Initial_Knowledge: LEMMA Protocol?(I, Q, T) AND Q(q) IMPLIES Know(I)(A, q) = I(A) Monotonic_Knowledge: LEMMA Protocol?(I, Q, T) AND T(A)(q1, e, q2) IMPLIES subset?(Know(I)(B, q1), Know(I)(B, q2)) Knowledge_step1: LEMMA trace(q2) = add(e, trace(q1)) AND (FORALL K: not Visible(content(e))(K)) AND (FORALL K, X: Visible(content(e))(Encr(K, X)) => not Know(I)(B, q1)(K)) IMPLIES Know(I)(B, q2) = union(Know(I)(B, q1), Visible(content(e))) Knowledge_step2: LEMMA trace(q2) = add(e, trace(q1)) AND (FORALL K: not Parts(content(e))(K)) AND Know(I)(B, q2)(X) IMPLIES Know(I)(B, q1)(X) OR Parts(content(e))(X) Knowledge_step3: LEMMA subset?(content(e), Gen(I)(A, q)) AND not Know(I)(A, q)(K) AND not FreshKeys(q)(K) AND Parts(content(e))(Encr(K, X)) IMPLIES PartsTrace(q)(Encr(K, X)) %--- Once a secret is compromized, it cannot become secret again ---% Secret_past1: LEMMA Protocol?(I, Q, T) AND T(A)(q1, e, q2) AND NOT Secret(I)(X, Ag, q1) IMPLIES NOT Secret(I)(X, Ag, q2) Secret_past2: LEMMA Protocol?(I, Q, T) AND T(A)(q1, e, q2) AND NOT Secret(I)(S, Ag, q1) IMPLIES NOT Secret(I)(S, Ag, q2) END protocols $$$protocols.prf (|protocols| (|Visible_PartsTrace| "" (AUTO-REWRITE "subset?" "member" "VisibleTrace" "PartsTrace") (("" (SKOSIMP) (("" (ASSERT) (("" (USE "Parts_Visible1") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|FreshNonces_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|UsedKeys_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|UsedKeys_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|FreshKeys_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|FreshFields_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|Parts_FreshNonces| "" (SKOLEM!) (("" (REWRITE "Parts_atom") NIL NIL)) NIL) (|Parts_FreshKeys| "" (SKOLEM!) (("" (REWRITE "Parts_atom") NIL NIL)) NIL) (|Parts_FreshFields| "" (SKOLEM!) (("" (REWRITE "Parts_atom") NIL NIL)) NIL) (|init_set_atoms| "" (SUBTYPE-TCC) NIL NIL) (|Parts_I| "" (SKOLEM!) (("" (REWRITE "Parts_atom") NIL NIL)) NIL) (|Initial_NotFresh| "" (SKOSIMP) (("" (TYPEPRED "I!1(A!1)") (("" (DELETE -1) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL) (|Know_Conc1| "" (AUTO-REWRITE "Know" "Fst_Analz") (("" (ASSERT) NIL NIL)) NIL) (|Know_Conc2| "" (AUTO-REWRITE "Know" "Snd_Analz") (("" (ASSERT) NIL NIL)) NIL) (|Know_Encr| "" (AUTO-REWRITE "Know" "Key_Analz") (("" (REDUCE) NIL NIL)) NIL) (|Know_Init| "" (AUTO-REWRITE "Know" "union" "member" "Inj_Analz") (("" (REDUCE) NIL NIL)) NIL) (|Know_Visible| "" (SKOSIMP) (("" (EXPAND* "VisibleTrace" "Know") (("" (USE "Analz_subset" ("S1" "FieldsTrace(q!1)")) (("" (GROUND) (("1" (USE "Analz_Visible1") (("1" (AUTO-REWRITE "subset?" "member") (("1" (REDUCE) NIL NIL)) NIL)) NIL) ("2" (DELETE -1 2) (("2" (GRIND :EXCLUDE ("FieldsTrace")) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Know_Field2| "" (AUTO-REWRITE "Know_Visible" "VisibleTrace" "Inj_Visible") (("" (REDUCE) NIL NIL)) NIL) (|Know_Field| "" (AUTO-REWRITE "subset?" "member" "FieldsTrace") (("" (REDUCE) (("" (REWRITE "Know_Field2") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Gen_Conc| "" (EXPAND "Gen") (("" (AUTO-REWRITE "union" "member" "FreshFields" "FreshNonces" "FreshKeys" "SessionKey?" "equal_conc") (("" (REDUCE) (("1" (EXPAND "Synth" -) (("1" (REDUCE) (("1" (FORWARD-CHAIN "Know_Conc2") (("1" (REWRITE "Inj_Synth") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "Synth" -) (("2" (REDUCE) (("2" (FORWARD-CHAIN "Know_Conc1") (("2" (REWRITE "Inj_Synth") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (REWRITE "Comp_Synth") NIL NIL)) NIL)) NIL)) NIL) (|Gen_Encr| "" (EXPAND "Gen") (("" (AUTO-REWRITE "union" "member" "FreshFields" "FreshNonces" "FreshKeys" "SessionKey?" "equal_encr") (("" (REDUCE) (("1" (EXPAND "Synth" -) (("1" (REDUCE) NIL NIL)) NIL) ("2" (EXPAND "Synth" -) (("2" (REDUCE) NIL NIL)) NIL) ("3" (REWRITE "Inj_Synth") NIL NIL) ("4" (REWRITE "Key_Synth") NIL NIL)) NIL)) NIL)) NIL) (|Gen_Atom| "" (EXPAND "Gen") (("" (AUTO-REWRITE "union" "member" "FreshFields" "Synth_Atom") (("" (REDUCE) NIL NIL)) NIL)) NIL) (|Gen_Data| "" (AUTO-REWRITE "Atom?" "Gen_Atom" "FreshNonces" "FreshKeys" "SessionKey?") (("" (REDUCE) NIL NIL)) NIL) (|Gen_Agent| "" (AUTO-REWRITE "Atom?" "Gen_Atom" "FreshNonces" "FreshKeys" "SessionKey?") (("" (REDUCE) NIL NIL)) NIL) (|Gen_Nonce| "" (AUTO-REWRITE "FreshKeys" "SessionKey?" "Gen_Atom" "Nonce_Atom") (("" (REDUCE) NIL NIL)) NIL) (|Gen_LongTermKey| "" (AUTO-REWRITE "Atom?" "Gen_Atom" "FreshNonces" "FreshKeys" "SessionKey?" "LongTermKey?") (("" (REDUCE) NIL NIL)) NIL) (|Gen_SessionKey| "" (AUTO-REWRITE "Gen_Atom" "Atom?" "FreshNonces" "SessionKey?") (("" (REDUCE) NIL NIL)) NIL) (|Gen_Visible| "" (SKOLEM + ("A!1" "I!1" _ "Y!1" "q!1")) (("" (INDUCT-AND-REWRITE "X" 1 "Visible" "Gen_Conc" "add" "member" "union" "singleton") (("" (REPLACE -3 + RL) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|Know_Parts| "" (SKOSIMP) (("" (AUTO-REWRITE "subset?" "member" "union" "Parts_union" "PartsTrace" "Parts_I") (("" (EXPAND "Know") (("" (USE "Parts_Analz1") (("" (ASSERT) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Parts_Know| "" (SKOLEM!) (("" (AUTO-REWRITE "Know" "union" "member" "Parts_Analz" "Parts_union" "PartsTrace" "Parts_I") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|Parts_Gen_Atom| "" (AUTO-REWRITE "union" "member" "Parts_union" "Parts_Know" "Parts_FreshNonces" "Parts_FreshKeys" "Gen_Atom") (("" (SKOSIMP) (("" (EXPAND "Gen") (("" (REWRITE "Parts_Synth") (("" (ASSERT) (("" (GROUND) (("1" (EXPAND "FreshFields") (("1" (ASSERT) NIL NIL)) NIL) ("2" (REWRITE "Gen" :DIR RL) (("2" (ASSERT) (("2" (FORWARD-CHAIN "Know_Parts") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Parts_Gen_LongTermKey| "" (AUTO-REWRITE "FreshNonces" "FreshKeys" "LongTermKey?" "SessionKey?" "Atom?") (("" (SKOSIMP :PREDS? T) (("" (FORWARD-CHAIN "Parts_Gen_Atom") (("1" (SMASH) NIL NIL) ("2" (SMASH) NIL NIL) ("3" (SMASH) NIL NIL)) NIL)) NIL)) NIL) (|Parts_Gen_SessionKey| "" (AUTO-REWRITE "FreshNonces" "FreshKeys" "SessionKey?" "Atom?") (("" (SKOSIMP :PREDS? T) (("" (FORWARD-CHAIN "Parts_Gen_Atom") (("1" (FORWARD-CHAIN "Initial_NotFresh") NIL NIL) ("2" (SMASH) NIL NIL) ("3" (SMASH) NIL NIL)) NIL)) NIL)) NIL) (|Parts_Gen_Nonce| "" (AUTO-REWRITE "FreshNonces" "FreshKeys" "SessionKey?" "Atom?") (("" (SKOSIMP :PREDS? T) (("" (FORWARD-CHAIN "Parts_Gen_Atom") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|Reachable_induct| "" (SKOSIMP) (("" (EXPAND* "subset?" "member") (("" (REWRITE "Reachable_weak_induction") (("" (DELETE 2) (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Reachable_induct2| "" (LEMMA "Reachable_induct") (("" (EXPAND* "subset?" "member") NIL NIL)) NIL) (|Reachable_induct3| "" (SKOSIMP) (("" (REWRITE "Reachable_induction") (("" (REDUCE) NIL NIL)) NIL)) NIL) (|FieldsTrace_init| "" (EXPAND "Protocol?") (("" (SKOSIMP) (("" (INST?) (("" (ASSERT) (("" (DELETE -2 -3 -4) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|PartsTrace_init| "" (AUTO-REWRITE "PartsTrace" "Parts_emptyset") (("" (SKOSIMP) (("" (FORWARD-CHAIN "FieldsTrace_init") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL) (|VisibleTrace_init| "" (AUTO-REWRITE "VisibleTrace" "Visible_emptyset") (("" (SKOSIMP) (("" (FORWARD-CHAIN "FieldsTrace_init") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL) (|FieldsTrace_step| "" (EXPAND "Protocol?") (("" (SKOSIMP) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (INST? -2) (("" (ASSERT) (("" (DELETE -1 -3 -4) (("" (APPLY (THEN (GRIND :IF-MATCH NIL) (INST?) (ASSERT))) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|PartsTrace_step| "" (SKOSIMP) (("" (FORWARD-CHAIN "FieldsTrace_step") (("" (AUTO-REWRITE "PartsTrace" "Parts_union") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL) (|VisibleTrace_step| "" (SKOSIMP) (("" (FORWARD-CHAIN "FieldsTrace_step") (("" (AUTO-REWRITE "VisibleTrace" "Visible_union") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL) (|Secret_equiv| "" (GRIND :EXCLUDE ("Know")) NIL NIL) (|Regularity| "" (EXPAND "GoodProtocol?") (("" (SKOSIMP) (("" (AUTO-REWRITE "emptyset" "union" "member") (("" (REWRITE "Reachable_induct3") (("1" (SKOSIMP) (("1" (FORWARD-CHAIN "PartsTrace_init") (("1" (REPLACE*) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (SKOSIMP) (("2" (FORWARD-CHAIN "PartsTrace_step") (("2" (EXPAND "Regular?") (("2" (FLATTEN) (("2" (REPLACE*) (("2" (DELETE -1 -5) (("2" (REDUCE) (("2" (FORWARD-CHAIN "Parts_subset") (("2" (EXPAND "subset?" -1) (("2" (INST?) (("2" (ASSERT) (("2" (FORWARD-CHAIN "Parts_Gen_LongTermKey") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Secrecy_of_long_term_keys| "" (EXPAND "Secret") (("" (SKOSIMP*) (("" (FORWARD-CHAIN "Regularity") (("" (INST?) (("" (ASSERT) (("" (FORWARD-CHAIN "Know_Parts") (("" (EXPAND "Regular?") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|StrongSecrecy_of_long_term_keys| "" (SKOSIMP*) (("" (FORWARD-CHAIN "Regularity") (("" (INST?) (("" (ASSERT) (("" (EXPAND "Coideal") (("" (AUTO-REWRITE "singleton" "PartsTrace" "disjoint?" "empty?" "intersection" "member") (("" (REWRITE "Subset_Coideal") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Regularity2| "" (EXPAND "GoodProtocol?") (("" (SKOSIMP) (("" (AUTO-REWRITE "disjoint?" "intersection" "empty?" "member" "emptyset" "union") (("" (REWRITE "Reachable_induct3") (("1" (SKOSIMP) (("1" (FORWARD-CHAIN "PartsTrace_init") (("1" (REPLACE*) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (SKOSIMP) (("2" (FORWARD-CHAIN "PartsTrace_step") (("2" (EXPAND "Regular?") (("2" (FLATTEN) (("2" (REPLACE*) (("2" (DELETE -1 -5) (("2" (REDUCE) (("2" (FORWARD-CHAIN "Parts_subset") (("2" (EXPAND "subset?" -1) (("2" (INST?) (("2" (ASSERT) (("2" (FORWARD-CHAIN "Parts_Gen_LongTermKey") (("2" (TYPEPRED "SK!1") (("2" (EXPAND "subset?" -1) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Secrecy_of_long_term_keys2| "" (EXPAND "Secret") (("" (SKOSIMP*) (("" (FORWARD-CHAIN "Regularity2") (("" (INST?) (("" (ASSERT) (("" (EXPAND "Regular?") (("" (FLATTEN) (("" (INST?) (("" (DELETE -2 -4 -5) (("" (ASSERT) (("" (TYPEPRED "SK!1") (("" (GRIND :EXCLUDE ("PartsTrace" "Know")) (("" (FORWARD-CHAIN "Know_Parts") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|StrongSecrecy_of_long_term_keys2| "" (SKOSIMP*) (("" (FORWARD-CHAIN "Regularity2") (("" (INST?) (("" (ASSERT) (("" (AUTO-REWRITE "PartsTrace") (("" (REWRITE "Subset_Coideal") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Initial_Knowledge| "" (SKOSIMP) (("" (REWRITE "subset_antisymmetric") (("1" (DELETE 2) (("1" (EXPAND "Know") (("1" (FORWARD-CHAIN "FieldsTrace_init") (("1" (REPLACE*) (("1" (DELETE -) (("1" (REWRITE "Analz_induct") (("1" (DELETE 2) (("1" (GRIND) NIL NIL)) NIL) ("2" (SKOSIMP) (("2" (TYPEPRED "I!1(A!1)") (("2" (DELETE -2 -3 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP) (("3" (TYPEPRED "I!1(A!1)") (("3" (DELETE -2 -3 2) (("3" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("4" (SKOSIMP) (("4" (TYPEPRED "I!1(A!1)") (("4" (DELETE -2 -3 -5 1 2) (("4" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 -2 2) (("2" (GRIND :EXCLUDE ("Know") :REWRITES ("Know_Init")) NIL NIL)) NIL)) NIL)) NIL) (|Monotonic_Knowledge| "" (SKOSIMP) (("" (EXPAND "Know") (("" (FORWARD-CHAIN "FieldsTrace_step") (("" (REPLACE*) (("" (DELETE -1) (("" (REWRITE "Analz_subset") (("" (DELETE -1 -2 2) (("" (GRIND :EXCLUDE ("FieldsTrace")) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Knowledge_step1| "" (SKOSIMP) (("" (EXPAND "Know") (("" (CASE-REPLACE "union(I!1(B!1), FieldsTrace(q2!1)) = union(union(I!1(B!1), FieldsTrace(q1!1)), content(e!1))") (("1" (REWRITE "Analz_union1" +) NIL NIL) ("2" (DELETE -2 -3 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (APPLY (THEN (GRIND :IF-MATCH NIL) (INST?) (ASSERT))) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Knowledge_step2| "" (SKOSIMP) (("" (EXPAND "Know") (("" (CASE-REPLACE "union(I!1(B!1), FieldsTrace(q2!1)) = union(union(I!1(B!1), FieldsTrace(q1!1)), content(e!1))") (("1" (DELETE -1 -2) (("1" (USE "Analz_union2") (("1" (AUTO-REWRITE "subset?" "union" "member") (("1" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -2 -3 2 3) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (APPLY (THEN (GRIND :IF-MATCH NIL) (INST?) (ASSERT))) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Knowledge_step3| "" (SKOSIMP) (("" (EXPAND "Gen") (("" (FORWARD-CHAIN "Parts_subset") (("" (DELETE -2) (("" (AUTO-REWRITE "Parts_Synth" "Parts_Know" "union" "member" "Synth_Atom" "Atom?" "subset?" "Parts_union" "Parts_FreshFields" "equal_encr") (("" (ASSERT) (("" (INST?) (("" (ASSERT) (("" (EXPAND "Synth" -) (("" (ASSERT) (("" (CASE "I!1(A!1)(Encr(K!1, X!1)) OR FreshFields(q!1)(Encr(K!1, X!1))") (("1" (DELETE -2 -3 1 2 3) (("1" (SPLIT) (("1" (TYPEPRED "I!1(A!1)") (("1" (REDUCE) NIL NIL)) NIL) ("2" (TYPEPRED "FreshFields(q!1)") (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL) ("2" (GROUND) (("1" (FORWARD-CHAIN "Know_Parts") NIL NIL) ("2" (SKOSIMP) (("2" (AUTO-REWRITE "FreshFields" "FreshNonces") (("2" (DELETE -4 -5 1 2 5) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Secret_past1| "" (EXPAND "Secret") (("" (SKOSIMP*) (("" (INST?) (("" (ASSERT) (("" (USE "Monotonic_Knowledge") (("" (ASSERT) (("" (EXPAND* "subset?" "member") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Secret_past2| "" (AUTO-REWRITE "Secret_equiv") (("" (REDUCE) (("" (FORWARD-CHAIN "Secret_past1") NIL NIL)) NIL)) NIL)) $$$leader_state_adt.pvs %%% ADT file generated from leader_state leader_state_adt: THEORY BEGIN IMPORTING fields leader_state: TYPE NotConnected?, WaitingForKeyAck?, Connected?, WaitingForAck?: [leader_state -> boolean] NotConnected: (NotConnected?) WaitingForKeyAck: [[nonce, key] -> (WaitingForKeyAck?)] ExpectedNonce: [(WaitingForKeyAck?) -> nonce] SessionKey: [(WaitingForKeyAck?) -> key] Connected: [[nonce, key] -> (Connected?)] ExpectedNonce: [(Connected?) -> nonce] SessionKey: [(Connected?) -> key] WaitingForAck: [[nonce, key] -> (WaitingForAck?)] ExpectedNonce: [(WaitingForAck?) -> nonce] SessionKey: [(WaitingForAck?) -> key] ord(x: leader_state): upto(3) = CASES x OF NotConnected: 0, WaitingForKeyAck(WaitingForKeyAck1_var, WaitingForKeyAck2_var): 1, Connected(Connected1_var, Connected2_var): 2, WaitingForAck(WaitingForAck1_var, WaitingForAck2_var): 3 ENDCASES leader_state_NotConnected_extensionality: AXIOM FORALL (NotConnected?_var: (NotConnected?), NotConnected?_var2: (NotConnected?)): NotConnected?_var = NotConnected?_var2; leader_state_WaitingForKeyAck_extensionality: AXIOM FORALL (WaitingForKeyAck?_var: (WaitingForKeyAck?), WaitingForKeyAck?_var2: (WaitingForKeyAck?)): ExpectedNonce(WaitingForKeyAck?_var) = ExpectedNonce(WaitingForKeyAck?_var2) AND SessionKey(WaitingForKeyAck?_var) = SessionKey(WaitingForKeyAck?_var2) IMPLIES WaitingForKeyAck?_var = WaitingForKeyAck?_var2; leader_state_WaitingForKeyAck_eta: AXIOM FORALL (WaitingForKeyAck?_var: (WaitingForKeyAck?)): WaitingForKeyAck(ExpectedNonce(WaitingForKeyAck?_var), SessionKey(WaitingForKeyAck?_var)) = WaitingForKeyAck?_var; leader_state_Connected_extensionality: AXIOM FORALL (Connected?_var: (Connected?), Connected?_var2: (Connected?)): ExpectedNonce(Connected?_var) = ExpectedNonce(Connected?_var2) AND SessionKey(Connected?_var) = SessionKey(Connected?_var2) IMPLIES Connected?_var = Connected?_var2; leader_state_Connected_eta: AXIOM FORALL (Connected?_var: (Connected?)): Connected(ExpectedNonce(Connected?_var), SessionKey(Connected?_var)) = Connected?_var; leader_state_WaitingForAck_extensionality: AXIOM FORALL (WaitingForAck?_var: (WaitingForAck?), WaitingForAck?_var2: (WaitingForAck?)): ExpectedNonce(WaitingForAck?_var) = ExpectedNonce(WaitingForAck?_var2) AND SessionKey(WaitingForAck?_var) = SessionKey(WaitingForAck?_var2) IMPLIES WaitingForAck?_var = WaitingForAck?_var2; leader_state_WaitingForAck_eta: AXIOM FORALL (WaitingForAck?_var: (WaitingForAck?)): WaitingForAck(ExpectedNonce(WaitingForAck?_var), SessionKey(WaitingForAck?_var)) = WaitingForAck?_var; leader_state_ExpectedNonce_WaitingForKeyAck: AXIOM FORALL (WaitingForKeyAck1_var: nonce, WaitingForKeyAck2_var: key): ExpectedNonce(WaitingForKeyAck(WaitingForKeyAck1_var, WaitingForKeyAck2_var)) = WaitingForKeyAck1_var; leader_state_SessionKey_WaitingForKeyAck: AXIOM FORALL (WaitingForKeyAck1_var: nonce, WaitingForKeyAck2_var: key): SessionKey(WaitingForKeyAck(WaitingForKeyAck1_var, WaitingForKeyAck2_var)) = WaitingForKeyAck2_var; leader_state_ExpectedNonce_Connected: AXIOM FORALL (Connected1_var: nonce, Connected2_var: key): ExpectedNonce(Connected(Connected1_var, Connected2_var)) = Connected1_var; leader_state_SessionKey_Connected: AXIOM FORALL (Connected1_var: nonce, Connected2_var: key): SessionKey(Connected(Connected1_var, Connected2_var)) = Connected2_var; leader_state_ExpectedNonce_WaitingForAck: AXIOM FORALL (WaitingForAck1_var: nonce, WaitingForAck2_var: key): ExpectedNonce(WaitingForAck(WaitingForAck1_var, WaitingForAck2_var)) = WaitingForAck1_var; leader_state_SessionKey_WaitingForAck: AXIOM FORALL (WaitingForAck1_var: nonce, WaitingForAck2_var: key): SessionKey(WaitingForAck(WaitingForAck1_var, WaitingForAck2_var)) = WaitingForAck2_var; leader_state_inclusive: AXIOM FORALL (leader_state_var: leader_state): NotConnected?(leader_state_var) OR WaitingForKeyAck?(leader_state_var) OR Connected?(leader_state_var) OR WaitingForAck?(leader_state_var); leader_state_induction: AXIOM FORALL (p: [leader_state -> boolean]): (p(NotConnected) AND (FORALL (WaitingForKeyAck1_var: nonce, WaitingForKeyAck2_var: key): p(WaitingForKeyAck(WaitingForKeyAck1_var, WaitingForKeyAck2_var))) AND (FORALL (Connected1_var: nonce, Connected2_var: key): p(Connected(Connected1_var, Connected2_var))) AND (FORALL (WaitingForAck1_var: nonce, WaitingForAck2_var: key): p(WaitingForAck(WaitingForAck1_var, WaitingForAck2_var)))) IMPLIES (FORALL (leader_state_var: leader_state): p(leader_state_var)); subterm(x, y: leader_state): boolean = x = y; <<(x, y: leader_state): boolean = FALSE; leader_state_well_founded: AXIOM well_founded?[leader_state](<<); reduce_nat(NotConnected?_fun: nat, WaitingForKeyAck?_fun, Connected?_fun, WaitingForAck?_fun: [[nonce, key] -> nat]): [leader_state -> nat] = LAMBDA (leader_state_adtvar: leader_state): LET red: [leader_state -> nat] = reduce_nat(NotConnected?_fun, WaitingForKeyAck?_fun, Connected?_fun, WaitingForAck?_fun) IN CASES leader_state_adtvar OF NotConnected: NotConnected?_fun, WaitingForKeyAck(WaitingForKeyAck1_var, WaitingForKeyAck2_var): WaitingForKeyAck?_fun(WaitingForKeyAck1_var, WaitingForKeyAck2_var), Connected(Connected1_var, Connected2_var): Connected?_fun(Connected1_var, Connected2_var), WaitingForAck(WaitingForAck1_var, WaitingForAck2_var): WaitingForAck?_fun(WaitingForAck1_var, WaitingForAck2_var) ENDCASES; REDUCE_nat(NotConnected?_fun: [leader_state -> nat], WaitingForKeyAck?_fun, Connected?_fun, WaitingForAck?_fun: [[nonce, key, leader_state] -> nat]): [leader_state -> nat] = LAMBDA (leader_state_adtvar: leader_state): LET red: [leader_state -> nat] = REDUCE_nat(NotConnected?_fun, WaitingForKeyAck?_fun, Connected?_fun, WaitingForAck?_fun) IN CASES leader_state_adtvar OF NotConnected: NotConnected?_fun(leader_state_adtvar), WaitingForKeyAck(WaitingForKeyAck1_var, WaitingForKeyAck2_var): WaitingForKeyAck?_fun(WaitingForKeyAck1_var, WaitingForKeyAck2_var, leader_state_adtvar), Connected(Connected1_var, Connected2_var): Connected?_fun(Connected1_var, Connected2_var, leader_state_adtvar), WaitingForAck(WaitingForAck1_var, WaitingForAck2_var): WaitingForAck?_fun(WaitingForAck1_var, WaitingForAck2_var, leader_state_adtvar) ENDCASES; reduce_ordinal(NotConnected?_fun: ordinal, WaitingForKeyAck?_fun, Connected?_fun, WaitingForAck?_fun: [[nonce, key] -> ordinal]): [leader_state -> ordinal] = LAMBDA (leader_state_adtvar: leader_state): LET red: [leader_state -> ordinal] = reduce_ordinal(NotConnected?_fun, WaitingForKeyAck?_fun, Connected?_fun, WaitingForAck?_fun) IN CASES leader_state_adtvar OF NotConnected: NotConnected?_fun, WaitingForKeyAck(WaitingForKeyAck1_var, WaitingForKeyAck2_var): WaitingForKeyAck?_fun(WaitingForKeyAck1_var, WaitingForKeyAck2_var), Connected(Connected1_var, Connected2_var): Connected?_fun(Connected1_var, Connected2_var), WaitingForAck(WaitingForAck1_var, WaitingForAck2_var): WaitingForAck?_fun(WaitingForAck1_var, WaitingForAck2_var) ENDCASES; REDUCE_ordinal(NotConnected?_fun: [leader_state -> ordinal], WaitingForKeyAck?_fun, Connected?_fun, WaitingForAck?_fun: [[nonce, key, leader_state] -> ordinal]): [leader_state -> ordinal] = LAMBDA (leader_state_adtvar: leader_state): LET red: [leader_state -> ordinal] = REDUCE_ordinal(NotConnected?_fun, WaitingForKeyAck?_fun, Connected?_fun, WaitingForAck?_fun) IN CASES leader_state_adtvar OF NotConnected: NotConnected?_fun(leader_state_adtvar), WaitingForKeyAck(WaitingForKeyAck1_var, WaitingForKeyAck2_var): WaitingForKeyAck?_fun(WaitingForKeyAck1_var, WaitingForKeyAck2_var, leader_state_adtvar), Connected(Connected1_var, Connected2_var): Connected?_fun(Connected1_var, Connected2_var, leader_state_adtvar), WaitingForAck(WaitingForAck1_var, WaitingForAck2_var): WaitingForAck?_fun(WaitingForAck1_var, WaitingForAck2_var, leader_state_adtvar) ENDCASES; END leader_state_adt leader_state_adt_reduce[range: TYPE]: THEORY BEGIN IMPORTING fields IMPORTING leader_state_adt reduce(NotConnected?_fun: range, WaitingForKeyAck?_fun, Connected?_fun, WaitingForAck?_fun: [[nonce, key] -> range]): [leader_state -> range] = LAMBDA (leader_state_adtvar: leader_state): LET red: [leader_state -> range] = reduce(NotConnected?_fun, WaitingForKeyAck?_fun, Connected?_fun, WaitingForAck?_fun) IN CASES leader_state_adtvar OF NotConnected: NotConnected?_fun, WaitingForKeyAck(WaitingForKeyAck1_var, WaitingForKeyAck2_var): WaitingForKeyAck?_fun(WaitingForKeyAck1_var, WaitingForKeyAck2_var), Connected(Connected1_var, Connected2_var): Connected?_fun(Connected1_var, Connected2_var), WaitingForAck(WaitingForAck1_var, WaitingForAck2_var): WaitingForAck?_fun(WaitingForAck1_var, WaitingForAck2_var) ENDCASES; REDUCE(NotConnected?_fun: [leader_state -> range], WaitingForKeyAck?_fun, Connected?_fun, WaitingForAck?_fun: [[nonce, key, leader_state] -> range]): [leader_state -> range] = LAMBDA (leader_state_adtvar: leader_state): LET red: [leader_state -> range] = REDUCE(NotConnected?_fun, WaitingForKeyAck?_fun, Connected?_fun, WaitingForAck?_fun) IN CASES leader_state_adtvar OF NotConnected: NotConnected?_fun(leader_state_adtvar), WaitingForKeyAck(WaitingForKeyAck1_var, WaitingForKeyAck2_var): WaitingForKeyAck?_fun(WaitingForKeyAck1_var, WaitingForKeyAck2_var, leader_state_adtvar), Connected(Connected1_var, Connected2_var): Connected?_fun(Connected1_var, Connected2_var, leader_state_adtvar), WaitingForAck(WaitingForAck1_var, WaitingForAck2_var): WaitingForAck?_fun(WaitingForAck1_var, WaitingForAck2_var, leader_state_adtvar) ENDCASES; END leader_state_adt_reduce $$$leader_state_adt.prf (|leader_state_adt| (|leader_state_WaitingForKeyAck_extensionality_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|leader_state_WaitingForKeyAck_eta_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|leader_state_Connected_extensionality_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|leader_state_Connected_eta_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|leader_state_WaitingForAck_extensionality_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|leader_state_WaitingForAck_eta_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|leader_state_ExpectedNonce_WaitingForKeyAck_TCC1| "" (SUBTYPE-TCC) NIL NIL)) (|leader_state_adt_reduce|) $$$leader_state.pvs %------------------------------------------------ % State maintained by the leader for each user %------------------------------------------------ leader_state : DATATYPE BEGIN IMPORTING fields NotConnected: NotConnected? WaitingForKeyAck(ExpectedNonce: nonce, SessionKey: key): WaitingForKeyAck? Connected(ExpectedNonce: nonce, SessionKey: key): Connected? WaitingForAck(ExpectedNonce: nonce, SessionKey: key): WaitingForAck? END leader_state $$$leader_transitions.pvs leader_transitions : THEORY BEGIN IMPORTING fields, leader_state leader: TYPE = [ user -> leader_state ] v, v1, v2: VAR leader A: VAR user Na, Nl: VAR nonce Ka: VAR key %----------------- % Initial state %----------------- init_leader: leader = lambda A: NotConnected %---------------------------------------- % Reception of a valid request to join % - new key = Ka, expected nonce = Nl %---------------------------------------- rcv_init_req(A, Nl, Ka)(v1, v2): bool = v1(A) = NotConnected AND v2 = v1 WITH [(A) := WaitingForKeyAck(Nl, Ka)] %-------------------------------------- % Reception of a key acknowledgement %-------------------------------------- rcv_key_ack(A, Nl, Na, Ka)(v1, v2): bool = v1(A) = WaitingForKeyAck(Nl, Ka) AND v2 = v1 WITH [(A) := Connected(Na, Ka)] %-------------------------------------- % Sending a group-management message %-------------------------------------- snd_admin(A, Na, Nl, Ka)(v1, v2): bool = v1(A) = Connected(Na, Ka) AND v2 = v1 WITH [(A) := WaitingForAck(Nl, Ka)] %---------------------------------------------- % Reception of a group-admin acknowledgement %---------------------------------------------- rcv_ack(A, Nl, Na, Ka)(v1, v2): bool = v1(A) = WaitingForAck(Nl, Ka) AND v2 = v1 WITH [(A) := Connected(Na, Ka)] %----------------------------------- % Reception of a request to close %----------------------------------- rcv_close(A, Ka)(v1, v2): bool = ((EXISTS Na: v1(A) = Connected(Na, Ka)) OR (EXISTS Nl: v1(A) = WaitingForAck(Nl, Ka))) AND v2 = v1 WITH [(A) := NotConnected] N1, N2: VAR nonce K1, K2: VAR key leader_connected_state: LEMMA Connected(N1, K1) = Connected(N2, K2) IFF N1=N2 AND K1=K2 leader_waiting_state1: LEMMA WaitingForKeyAck(N1, K1) = WaitingForKeyAck(N2, K2) IFF N1=N2 AND K1=K2 leader_waiting_state2: LEMMA WaitingForAck(N1, K1) = WaitingForAck(N2, K2) IFF N1=N2 AND K1=K2 END leader_transitions $$$leader_transitions.prf (|leader_transitions| (|leader_connected_state| "" (REDUCE) (("1" (CASE "SessionKey(Connected(N1!1, K1!1)) = K2!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (CASE "ExpectedNonce(Connected(N1!1, K1!1)) = N2!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|leader_waiting_state1| "" (REDUCE) (("1" (CASE "SessionKey(WaitingForKeyAck(N1!1, K1!1)) = K2!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (CASE "ExpectedNonce(WaitingForKeyAck(N1!1, K1!1)) = N2!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|leader_waiting_state2| "" (REDUCE) (("1" (CASE "SessionKey(WaitingForAck(N1!1, K1!1)) = K2!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (CASE "ExpectedNonce(WaitingForAck(N1!1, K1!1)) = N2!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) $$$user_state_adt.pvs %%% ADT file generated from user_state user_state_adt: THEORY BEGIN IMPORTING fields user_state: TYPE NotConnected?, WaitingForKey?, Connected?: [user_state -> boolean] NotConnected: (NotConnected?) WaitingForKey: [nonce -> (WaitingForKey?)] ExpectedNonce: [(WaitingForKey?) -> nonce] Connected: [[nonce, key] -> (Connected?)] ExpectedNonce: [(Connected?) -> nonce] SessionKey: [(Connected?) -> key] ord(x: user_state): upto(2) = CASES x OF NotConnected: 0, WaitingForKey(WaitingForKey1_var): 1, Connected(Connected1_var, Connected2_var): 2 ENDCASES user_state_NotConnected_extensionality: AXIOM FORALL (NotConnected?_var: (NotConnected?), NotConnected?_var2: (NotConnected?)): NotConnected?_var = NotConnected?_var2; user_state_WaitingForKey_extensionality: AXIOM FORALL (WaitingForKey?_var: (WaitingForKey?), WaitingForKey?_var2: (WaitingForKey?)): ExpectedNonce(WaitingForKey?_var) = ExpectedNonce(WaitingForKey?_var2) IMPLIES WaitingForKey?_var = WaitingForKey?_var2; user_state_WaitingForKey_eta: AXIOM FORALL (WaitingForKey?_var: (WaitingForKey?)): WaitingForKey(ExpectedNonce(WaitingForKey?_var)) = WaitingForKey?_var; user_state_Connected_extensionality: AXIOM FORALL (Connected?_var: (Connected?), Connected?_var2: (Connected?)): ExpectedNonce(Connected?_var) = ExpectedNonce(Connected?_var2) AND SessionKey(Connected?_var) = SessionKey(Connected?_var2) IMPLIES Connected?_var = Connected?_var2; user_state_Connected_eta: AXIOM FORALL (Connected?_var: (Connected?)): Connected(ExpectedNonce(Connected?_var), SessionKey(Connected?_var)) = Connected?_var; user_state_ExpectedNonce_WaitingForKey: AXIOM FORALL (WaitingForKey1_var: nonce): ExpectedNonce(WaitingForKey(WaitingForKey1_var)) = WaitingForKey1_var; user_state_ExpectedNonce_Connected: AXIOM FORALL (Connected1_var: nonce, Connected2_var: key): ExpectedNonce(Connected(Connected1_var, Connected2_var)) = Connected1_var; user_state_SessionKey_Connected: AXIOM FORALL (Connected1_var: nonce, Connected2_var: key): SessionKey(Connected(Connected1_var, Connected2_var)) = Connected2_var; user_state_inclusive: AXIOM FORALL (user_state_var: user_state): NotConnected?(user_state_var) OR WaitingForKey?(user_state_var) OR Connected?(user_state_var); user_state_induction: AXIOM FORALL (p: [user_state -> boolean]): (p(NotConnected) AND (FORALL (WaitingForKey1_var: nonce): p(WaitingForKey(WaitingForKey1_var))) AND (FORALL (Connected1_var: nonce, Connected2_var: key): p(Connected(Connected1_var, Connected2_var)))) IMPLIES (FORALL (user_state_var: user_state): p(user_state_var)); subterm(x, y: user_state): boolean = x = y; <<(x, y: user_state): boolean = FALSE; user_state_well_founded: AXIOM well_founded?[user_state](<<); reduce_nat(NotConnected?_fun: nat, WaitingForKey?_fun: [nonce -> nat], Connected?_fun: [[nonce, key] -> nat]): [user_state -> nat] = LAMBDA (user_state_adtvar: user_state): LET red: [user_state -> nat] = reduce_nat(NotConnected?_fun, WaitingForKey?_fun, Connected?_fun) IN CASES user_state_adtvar OF NotConnected: NotConnected?_fun, WaitingForKey(WaitingForKey1_var): WaitingForKey?_fun(WaitingForKey1_var), Connected(Connected1_var, Connected2_var): Connected?_fun(Connected1_var, Connected2_var) ENDCASES; REDUCE_nat(NotConnected?_fun: [user_state -> nat], WaitingForKey?_fun: [[nonce, user_state] -> nat], Connected?_fun: [[nonce, key, user_state] -> nat]): [user_state -> nat] = LAMBDA (user_state_adtvar: user_state): LET red: [user_state -> nat] = REDUCE_nat(NotConnected?_fun, WaitingForKey?_fun, Connected?_fun) IN CASES user_state_adtvar OF NotConnected: NotConnected?_fun(user_state_adtvar), WaitingForKey(WaitingForKey1_var): WaitingForKey?_fun(WaitingForKey1_var, user_state_adtvar), Connected(Connected1_var, Connected2_var): Connected?_fun(Connected1_var, Connected2_var, user_state_adtvar) ENDCASES; reduce_ordinal(NotConnected?_fun: ordinal, WaitingForKey?_fun: [nonce -> ordinal], Connected?_fun: [[nonce, key] -> ordinal]): [user_state -> ordinal] = LAMBDA (user_state_adtvar: user_state): LET red: [user_state -> ordinal] = reduce_ordinal(NotConnected?_fun, WaitingForKey?_fun, Connected?_fun) IN CASES user_state_adtvar OF NotConnected: NotConnected?_fun, WaitingForKey(WaitingForKey1_var): WaitingForKey?_fun(WaitingForKey1_var), Connected(Connected1_var, Connected2_var): Connected?_fun(Connected1_var, Connected2_var) ENDCASES; REDUCE_ordinal(NotConnected?_fun: [user_state -> ordinal], WaitingForKey?_fun: [[nonce, user_state] -> ordinal], Connected?_fun: [[nonce, key, user_state] -> ordinal]): [user_state -> ordinal] = LAMBDA (user_state_adtvar: user_state): LET red: [user_state -> ordinal] = REDUCE_ordinal(NotConnected?_fun, WaitingForKey?_fun, Connected?_fun) IN CASES user_state_adtvar OF NotConnected: NotConnected?_fun(user_state_adtvar), WaitingForKey(WaitingForKey1_var): WaitingForKey?_fun(WaitingForKey1_var, user_state_adtvar), Connected(Connected1_var, Connected2_var): Connected?_fun(Connected1_var, Connected2_var, user_state_adtvar) ENDCASES; END user_state_adt user_state_adt_reduce[range: TYPE]: THEORY BEGIN IMPORTING fields IMPORTING user_state_adt reduce(NotConnected?_fun: range, WaitingForKey?_fun: [nonce -> range], Connected?_fun: [[nonce, key] -> range]): [user_state -> range] = LAMBDA (user_state_adtvar: user_state): LET red: [user_state -> range] = reduce(NotConnected?_fun, WaitingForKey?_fun, Connected?_fun) IN CASES user_state_adtvar OF NotConnected: NotConnected?_fun, WaitingForKey(WaitingForKey1_var): WaitingForKey?_fun(WaitingForKey1_var), Connected(Connected1_var, Connected2_var): Connected?_fun(Connected1_var, Connected2_var) ENDCASES; REDUCE(NotConnected?_fun: [user_state -> range], WaitingForKey?_fun: [[nonce, user_state] -> range], Connected?_fun: [[nonce, key, user_state] -> range]): [user_state -> range] = LAMBDA (user_state_adtvar: user_state): LET red: [user_state -> range] = REDUCE(NotConnected?_fun, WaitingForKey?_fun, Connected?_fun) IN CASES user_state_adtvar OF NotConnected: NotConnected?_fun(user_state_adtvar), WaitingForKey(WaitingForKey1_var): WaitingForKey?_fun(WaitingForKey1_var, user_state_adtvar), Connected(Connected1_var, Connected2_var): Connected?_fun(Connected1_var, Connected2_var, user_state_adtvar) ENDCASES; END user_state_adt_reduce $$$user_state_adt.prf (|user_state_adt| (|user_state_WaitingForKey_extensionality_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|user_state_WaitingForKey_eta_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|user_state_Connected_extensionality_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|user_state_Connected_eta_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|user_state_ExpectedNonce_WaitingForKey_TCC1| "" (SUBTYPE-TCC) NIL NIL)) (|user_state_adt_reduce|) $$$user_state.pvs user_state : DATATYPE BEGIN IMPORTING fields NotConnected: NotConnected? WaitingForKey(ExpectedNonce: nonce): WaitingForKey? Connected(ExpectedNonce: nonce, SessionKey: key): Connected? END user_state $$$user_transitions.pvs user_transitions : THEORY BEGIN IMPORTING fields, user_state usr: TYPE = [user -> user_state] u, u1, u2: VAR usr A: VAR user Na, Nl, Na2 : VAR nonce Ka: VAR key %----------------- % Initial state %----------------- init_usr: usr = lambda A: NotConnected %------------------------------------- % A requests to join using nonce Na %------------------------------------- init_req(A, Na)(u1, u2): bool = u1(A) = NotConnected AND u2 = u1 WITH [(A) := WaitingForKey(Na)] %----------------------------------------- % A receives a key distribution message % and sends an acknowledgement %----------------------------------------- rcv_key(A, Na, Na2, Ka)(u1, u2): bool = u1(A) = WaitingForKey(Na) AND u2 = u1 WITH [(A) := Connected(Na2, Ka)] %----------------------------------------- % A receives a group-management message % and sends an acknowledgement %----------------------------------------- rcv_admin(A, Na, Na2, Ka)(u1, u2): bool = u1(A) = Connected(Na, Ka) AND u2 = u1 WITH [(A) := Connected(Na2, Ka)] %------------------------ % A leaves the session %------------------------ leave(A, Ka)(u1, u2): bool = (EXISTS Na: u1(A) = Connected(Na, Ka)) AND u2 = u1 WITH [(A) := NotConnected] N1, N2: VAR nonce K1, K2: VAR key user_connected_state: LEMMA Connected(N1, K1) = Connected(N2, K2) IFF N1=N2 AND K1=K2 user_waiting_state: LEMMA WaitingForKey(N1) = WaitingForKey(N2) IFF N1=N2 END user_transitions $$$user_transitions.prf (|user_transitions| (|user_connected_state| "" (REDUCE) (("1" (CASE "SessionKey(Connected(N1!1, K1!1)) = K2!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (CASE "ExpectedNonce(Connected(N1!1, K1!1)) = N2!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|user_waiting_state| "" (REDUCE) (("" (CASE "ExpectedNonce(WaitingForKey(N1!1)) = N2!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) $$$fields.pvs %------------------------------------- % The content of Enclaves's messages %------------------------------------- fields : THEORY BEGIN agent: DATATYPE BEGIN Usr(Id: nat): Usr? Leader: Leader? END agent user: TYPE = (Usr?) nonce: TYPE key: DATATYPE BEGIN Shr(Owner: agent): Shr? % longterm key Ssk(Value: nonce): Ssk? % session key END key data: TYPE = nat field: DATATYPE BEGIN Agent(Name: agent): Agent? Nonce(Seq: nonce): Nonce? Key(Val: key): Key? Data(Val: data): Data? ++(Head, Tail: field): Con? Encr(Crv: key, Text: field): Encr? END field CONVERSION Agent CONVERSION Nonce CONVERSION Key CONVERSION Data %--- Rewrite rules for showing equalities ---% i1, i2: VAR nat a1, a2: VAR agent n1, n2: VAR nonce k1, k2: VAR key d1, d2: VAR data X1, X2, Y1, Y2: VAR field equal_usr: LEMMA Usr(i1) = Usr(i2) IFF i1 = i2 equal_ltkey: LEMMA Shr(a1) = Shr(a2) IFF a1 = a2 equal_stkey: LEMMA Ssk(n1) = Ssk(n2) IFF n1 = n2 equal_agent: LEMMA Agent(a1) = Agent(a2) IFF a1 = a2 equal_nonce: LEMMA Nonce(n1) = Nonce(n2) IFF n1 = n2 equal_key: LEMMA Key(k1) = Key(k2) IFF k1 = k2 equal_data: LEMMA Data(d1) = Data(d2) IFF d1 = d2 equal_conc: LEMMA X1 ++ Y1 = X2 ++ Y2 IFF X1=X2 AND Y1=Y2 equal_encr: LEMMA Encr(k1, X1) = Encr(k2, X2) IFF k1=k2 AND X1=X2 %--- Atomic fields X, Y, Z: VAR field a: VAR agent n: VAR nonce k: VAR key Atom?(X): bool = CASES X OF Agent(n): true, Nonce(n): true, Key(n) : true, Data(n) : true, ++(Y, Z) : false, Encr(k, Y): false ENDCASES LongTermKey?(X): bool = Key?(X) AND Shr?(Val(X)) SessionKey?(X): bool = Key?(X) AND Ssk?(Val(X)) Agent_Atom: JUDGEMENT (Agent?) SUBTYPE_OF (Atom?) Nonce_Atom: JUDGEMENT (Nonce?) SUBTYPE_OF (Atom?) Key_Atom : JUDGEMENT (Key?) SUBTYPE_OF (Atom?) Data_Atom : JUDGEMENT (Data?) SUBTYPE_OF (Atom?) LongTermKey: JUDGEMENT (LongTermKey?) SUBTYPE_OF (Key?) SessionKey : JUDGEMENT (SessionKey?) SUBTYPE_OF (Key?) %--- Parts of a field Parts(X): RECURSIVE set[field] = CASES X OF Agent(n): singleton(X), Nonce(n): singleton(X), Key(n) : singleton(X), Data(n) : singleton(X), ++(Y, Z) : add(X, union(Parts(Y), Parts(Z))), Encr(k, Y): add(X, Parts(Y)) ENDCASES MEASURE X BY << Parts_self: LEMMA Parts(X)(X) Parts_head: LEMMA Parts(X)(Y ++ Z) IMPLIES Parts(X)(Y) Parts_tail: LEMMA Parts(X)(Y ++ Z) IMPLIES Parts(X)(Z) Parts_text: LEMMA Parts(X)(Encr(k, Y)) IMPLIES Parts(X)(Y) %--- Visible parts of a field Visible(X): RECURSIVE set[field] = CASES X OF Agent(n): singleton(X), Nonce(n): singleton(X), Key(n) : singleton(X), Data(n) : singleton(X), ++(Y, Z) : add(X, union(Visible(Y), Visible(Z))), Encr(k, Y): singleton(X) ENDCASES MEASURE X BY << Visible_self: LEMMA Visible(X)(X) Visible_head: LEMMA Visible(X)(Y ++ Z) IMPLIES Visible(X)(Y) Visible_tail: LEMMA Visible(X)(Y ++ Z) IMPLIES Visible(X)(Z) Visible_inclusion: LEMMA subset?(Visible(X), Parts(X)) %--- Agents, Nonces, and Keys present in X Agents(X): RECURSIVE set[agent] = CASES X OF Agent(n): singleton(n), Nonce(n): emptyset, Key(n) : emptyset, Data(n) : emptyset, ++(Y, Z) : union(Agents(Y), Agents(Z)), Encr(k, Y): Agents(Y) ENDCASES MEASURE X BY << Agents_equiv: LEMMA Agents(X)(a) IFF Parts(X)(Agent(a)) Nonces(X): RECURSIVE set[nonce] = CASES X OF Agent(n): emptyset, Nonce(n): singleton(n), Key(n) : emptyset, Data(n) : emptyset, ++(Y, Z) : union(Nonces(Y), Nonces(Z)), Encr(k, Y): Nonces(Y) ENDCASES MEASURE X BY << Nonces_equiv: LEMMA Nonces(X)(n) IFF Parts(X)(Nonce(n)) Keys(X): RECURSIVE set[key] = CASES X OF Agent(n): emptyset, Nonce(n): emptyset, Key(n) : singleton(n), Data(n) : emptyset, ++(Y, Z) : union(Keys(Y), Keys(Z)), Encr(k, Y): Keys(Y) ENDCASES MEASURE X BY << Keys_equiv: LEMMA Keys(X)(k) IFF Parts(X)(Key(k)) END fields $$$fields.prf (|fields| (|equal_usr| "" (SKOLEM!) (("" (GROUND) (("" (CASE "Id(Usr(i1!1)) = i2!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|equal_ltkey| "" (SKOLEM!) (("" (GROUND) (("" (CASE "Owner(Shr(a1!1)) = a2!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|equal_stkey| "" (SKOLEM!) (("" (GROUND) (("" (CASE "Value(Ssk(n1!1)) = n2!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|equal_agent| "" (SKOLEM!) (("" (GROUND) (("" (CASE "Name(Agent(a1!1)) = a2!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|equal_nonce| "" (SKOLEM!) (("" (GROUND) (("" (CASE "Seq(Nonce(n1!1)) = n2!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|equal_key| "" (SKOLEM!) (("" (GROUND) (("" (CASE "Val(Key(k1!1)) = k2!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|equal_data| "" (SKOLEM!) (("" (GROUND) (("" (CASE "Val(Data(d1!1)) = d2!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|equal_conc| "" (SKOLEM!) (("" (GROUND) (("1" (CASE "Head(X1!1 ++ Y1!1) = X2!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (CASE "Tail(X1!1 ++ Y1!1) = Y2!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|equal_encr| "" (SKOLEM!) (("" (GROUND) (("1" (CASE "Crv(Encr(k1!1, X1!1)) = k2!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (CASE "Text(Encr(k1!1, X1!1)) = X2!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Agent_Atom| "" (SUBTYPE-TCC) NIL NIL) (|Nonce_Atom| "" (SUBTYPE-TCC) NIL NIL) (|Key_Atom| "" (SUBTYPE-TCC) NIL NIL) (|Data_Atom| "" (SUBTYPE-TCC) NIL NIL) (|LongTermKey| "" (SUBTYPE-TCC) NIL NIL) (|SessionKey| "" (SUBTYPE-TCC) NIL NIL) (|Parts_TCC1| "" (REPLACE-ETA "<<" "[field, field -> bool]") (("" (REWRITE "field_well_founded") NIL NIL)) NIL) (|Parts_TCC2| "" (TERMINATION-TCC) NIL NIL) (|Parts_TCC3| "" (TERMINATION-TCC) NIL NIL) (|Parts_TCC4| "" (TERMINATION-TCC) NIL NIL) (|Parts_self| "" (EXPAND "Parts") (("" (GRIND) NIL NIL)) NIL) (|Parts_head| "" (SKOLEM + (_ "Y!1" "Z!1")) (("" (INDUCT-AND-SIMPLIFY "X" :REWRITES ("equal_conc")) (("" (REPLACE*) (("" (REWRITE "Parts_self") NIL NIL)) NIL)) NIL)) NIL) (|Parts_tail| "" (SKOLEM + (_ "Y!1" "Z!1")) (("" (INDUCT-AND-SIMPLIFY "X" :REWRITES ("equal_conc")) (("" (REPLACE*) (("" (REWRITE "Parts_self") NIL NIL)) NIL)) NIL)) NIL) (|Parts_text| "" (SKOLEM + (_ "Y!1" "k!1")) (("" (INDUCT-AND-SIMPLIFY "X" :REWRITES ("equal_encr")) (("" (REPLACE*) (("" (REWRITE "Parts_self") NIL NIL)) NIL)) NIL)) NIL) (|Visible_self| "" (EXPAND "Visible") (("" (GRIND) NIL NIL)) NIL) (|Visible_head| "" (SKOLEM + (_ "Y!1" "Z!1")) (("" (INDUCT-AND-SIMPLIFY "X" :REWRITES ("equal_conc" "Visible_self")) (("" (REPLACE*) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|Visible_tail| "" (SKOLEM + (_ "Y!1" "Z!1")) (("" (INDUCT-AND-SIMPLIFY "X" :REWRITES ("equal_conc" "Visible_self")) (("" (REPLACE*) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|Visible_inclusion| "" (INDUCT-AND-SIMPLIFY "X") NIL NIL) (|Agents_equiv| "" (INDUCT-AND-SIMPLIFY "X" :REWRITES ("equal_agent")) NIL NIL) (|Nonces_equiv| "" (INDUCT-AND-SIMPLIFY "X" :REWRITES ("equal_nonce")) NIL NIL) (|Keys_equiv| "" (INDUCT-AND-SIMPLIFY "X" :REWRITES ("equal_key")) NIL NIL)) $$$events.pvs events: THEORY BEGIN IMPORTING fields event: DATATYPE BEGIN tau: tau? %% invisible event msg(snd: agent, rcv: agent, body: field): msg? oops(lost: field): oops? END event e: VAR event content(e): set[field] = CASES e OF tau: emptyset, msg(a, b, x): singleton(x), oops(x): singleton(x) ENDCASES %-------------------------------------------- % Rules for showing subset?(content(x), S) %-------------------------------------------- A, B: VAR agent S: VAR set[field] X: VAR field content_tau: LEMMA subset?(content(tau), S) content_msg: LEMMA subset?(content(msg(A, B, X)), S) IFF S(X) content_oops: LEMMA subset?(content(oops(X)), S) IFF S(X) A1, A2, B1, B2: VAR agent X1, X2: VAR field equal_msg: LEMMA msg(A1, B1, X1) = msg(A2, B2, X2) IFF A1=A2 AND B1=B2 AND X1=X2 equal_oops: LEMMA oops(X1) = oops(X2) IFF X1=X2 END events $$$events.prf (|events| (|content_tau| "" (GRIND) NIL NIL) (|content_msg| "" (GRIND) NIL NIL) (|content_oops| "" (GRIND) NIL NIL) (|equal_msg| "" (SKOLEM!) (("" (GROUND) (("1" (CASE "snd(msg(A1!1, B1!1, X1!1)) = A2!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (CASE "rcv(msg(A1!1, B1!1, X1!1)) = B2!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("3" (CASE "body(msg(A1!1, B1!1, X1!1)) =X2!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|equal_oops| "" (SKOLEM!) (("" (GROUND) (("" (CASE "lost(oops(X1!1)) = X2!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) $$$enclaves_messages.pvs enclaves_messages : THEORY BEGIN IMPORTING events %----------------- % Message types %----------------- auth_init_req: field = Data(0) auth_key_dist: field = Data(1) auth_ack_key: field = Data(2) admin_msg: field = Data(3) ack_admin: field = Data(4) req_close: field = Data(5) %------------ % Messages %------------ A, L: VAR agent Na, Nl: VAR nonce Ka: VAR (Ssk?) AuthInitReq(A, L, Na): event = msg(A, L, auth_init_req ++ Encr(Shr(A), A ++ L ++ Na)) AuthKeyDist(L, A, Na, Nl, Ka): event = msg(L, A, auth_key_dist ++ Encr(Shr(A), L ++ A ++ Na ++ Nl ++ Ka)) AuthAckKey(A, L, Nl, Na, Ka): event = msg(A, L, auth_ack_key ++ Encr(Ka, A ++ L ++ Nl ++ Na)) AdminMsg(L, A, Na, Nl, Ka): event = msg(L, A, admin_msg ++ Encr(Ka, L ++ A ++ Na ++ Nl)) AckAdmin(A, L, Nl, Na, Ka): event = msg(A, L, ack_admin ++ Encr(Ka, A ++ L ++ Nl ++ Na)) ReqClose(A, L, Ka): event = msg(A, L, req_close ++ Encr(Ka, A ++ L)) %----------------------------- % Content of these messages %----------------------------- S: VAR set[field] cont_auth_init_req: LEMMA subset?(content(AuthInitReq(A, L, Na)), S) IFF S(auth_init_req ++ Encr(Shr(A), A ++ L ++ Na)) cont_auth_key_dist: LEMMA subset?(content(AuthKeyDist(L, A, Na, Nl, Ka)), S) IFF S(auth_key_dist ++ Encr(Shr(A), L ++ A ++ Na ++ Nl ++ Ka)) cont_auth_ack_key: LEMMA subset?(content(AuthAckKey(A, L, Nl, Na, Ka)), S) IFF S(auth_ack_key ++ Encr(Ka, A ++ L ++ Nl ++ Na)) cont_admin_msg: LEMMA subset?(content(AdminMsg(L, A, Na, Nl, Ka)), S) IFF S(admin_msg ++ Encr(Ka, L ++ A ++ Na ++ Nl)) cont_ack_admin: LEMMA subset?(content(AckAdmin(A, L, Nl, Na, Ka)), S) IFF S(ack_admin ++ Encr(Ka, A ++ L ++ Nl ++ Na)) cont_req_close: LEMMA subset?(content(ReqClose(A, L, Ka)), S) IFF S(req_close ++ Encr(Ka, A ++ L)) END enclaves_messages $$$enclaves_messages.prf (|enclaves_messages| (|cont_auth_init_req| "" (AUTO-REWRITE "AuthInitReq" "content_msg") (("" (REDUCE) NIL NIL)) NIL) (|cont_auth_key_dist| "" (AUTO-REWRITE "AuthKeyDist" "content_msg") (("" (REDUCE) NIL NIL)) NIL) (|cont_auth_ack_key| "" (AUTO-REWRITE "AuthAckKey" "content_msg") (("" (REDUCE) NIL NIL)) NIL) (|cont_admin_msg| "" (AUTO-REWRITE "AdminMsg" "content_msg") (("" (REDUCE) NIL NIL)) NIL) (|cont_ack_admin| "" (AUTO-REWRITE "AckAdmin" "content_msg") (("" (REDUCE) NIL NIL)) NIL) (|cont_req_close| "" (AUTO-REWRITE "ReqClose" "content_msg") (("" (REDUCE) NIL NIL)) NIL)) $$$enclaves.pvs %-------------------------------------------------- % Simplified state-transition model of Enclaves %-------------------------------------------------- enclaves : THEORY BEGIN IMPORTING enclaves_messages, user_transitions, leader_transitions %------------------------------------------------------- % System state: % - for each user a: its local state u(a) % and the state l(a) that the leader maintains for a % - trace: set of events produced so far %------------------------------------------------------- global: TYPE = [# users: usr, leader: leader, trace: set[event] #] A, A1, A2: VAR user X, Y, Z: VAR field L, B, C, G: VAR agent S: VAR set[field] N, Nl, Nl1, Nl2, Na, Na1, Na2 : VAR nonce K: VAR key Ka, Kg, Kb: VAR (Ssk?) q, q1, q2, q3: VAR global e, e1, e2: VAR event n, n1, n2: VAR nat tr(q): set[event] = q`trace IMPORTING protocols[event, global, content, tr] %------------------ % initial state %------------------ init: global = (# users := init_usr, leader := init_leader, trace := emptyset #) Q0(q): bool = q = init %--------------------- % Initial knowledge %--------------------- IKeys(G): { S | subset?(S, LongTermKey?) } = IF Usr?(G) THEN singleton[field](Shr(G)) ELSE LongTermKey? ENDIF I(G): set[field] = union(IKeys(G), union(Data?, Agent?)) initial_knowledge: JUDGEMENT I HAS_TYPE [agent -> init_set] %------------------------------------------------ % Transition 1: A requests to join the session % A --> L: AuthInitReq { A, L, Na }Pa %------------------------------------------------ T1(A)(q1, e, q2): bool = EXISTS Na: FreshNonces(q1)(Na) AND init_req(A, Na)(q1`users, q2`users) AND q2`leader = q1`leader AND e = AuthInitReq(A, Leader, Na) AND q2`trace = add(e, q1`trace) %-------------------------------------------------- % Transition 2: L receives the request % L --> A: AuthKeyDist { A, L, Na, Nl, Ka }Pa %-------------------------------------------------- T2(A)(q1, e, q2): bool = EXISTS Na, Nl, Ka: member(AuthInitReq(A, Leader, Na), q1`trace) AND FreshNonces(q1)(Nl) AND FreshKeys(q1)(Ka) AND q2`users = q1`users AND rcv_init_req(A, Nl, Ka)(q1`leader, q2`leader) AND e = AuthKeyDist(Leader, A, Na, Nl, Ka) AND q2`trace = add(e, q1`trace) %---------------------------------------------------- % Transition 3: A receives the key and acknowledges % A --> L: AuthAckKey { L, A, Nl, Na }Ka %---------------------------------------------------- T3(A)(q1, e, q2): bool = EXISTS Na, Nl, Na2, Ka: member(AuthKeyDist(Leader, A, Na, Nl, Ka), q1`trace) AND FreshNonces(q1)(Na2) AND rcv_key(A, Na, Na2, Ka)(q1`users, q2`users) AND q2`leader = q1`leader AND e = AuthAckKey(A, Leader, Nl, Na2, Ka) AND q2`trace = add(e, q1`trace) %----------------------------------------------------------- % Transition 4: L receives the key acknowledgement %----------------------------------------------------------- T4(A)(q1, e, q2): bool = EXISTS Nl, Na, Ka: member(AuthAckKey(A, Leader, Nl, Na, Ka), q1`trace) AND q2`users = q1`users AND rcv_key_ack(A, Nl, Na, Ka)(q1`leader, q2`leader) AND e = tau AND q2`trace = add(e, q1`trace) %---------------------------------------------------- % Transition 5: L sends a group-management message % L --> A: AdminMsg { L, A, Na, Nl }Ka %---------------------------------------------------- T5(A)(q1, e, q2): bool = EXISTS Nl, Na, Ka: FreshNonces(q1)(Nl) AND q2`users = q1`users AND snd_admin(A, Na, Nl, Ka)(q1`leader, q2`leader) AND e = AdminMsg(Leader, A, Na, Nl, Ka) AND q2`trace = add(e, q1`trace) %-------------------------------------------------------- % Transition 6: A receives a group-management message % and acknowledges % A --> L: AdminAck {A, L, Nl, Na}Ka %-------------------------------------------------------- T6(A)(q1, e, q2): bool = EXISTS Na, Nl, Na2, Ka: member(AdminMsg(Leader, A, Na, Nl, Ka), q1`trace) AND FreshNonces(q1)(Na2) AND rcv_admin(A, Na, Na2, Ka)(q1`users, q2`users) AND q2`leader = q1`leader AND e = AckAdmin(A, Leader, Nl, Na2, Ka) AND q2`trace = add(e, q1`trace) %------------------------------------------------ % Transition 7: L receives the acknowledgement %------------------------------------------------ T7(A)(q1, e, q2): bool = EXISTS Nl, Na, Ka: member(AckAdmin(A, Leader, Nl, Na, Ka), q1`trace) AND q2`users = q1`users AND rcv_ack(A, Nl, Na, Ka)(q1`leader, q2`leader) AND e = tau AND q2`trace = add(e, q1`trace) %------------------------- % Transition 8: A quits % A --> L: {A, L}Ka %------------------------- T8(A)(q1, e, q2): bool = EXISTS Ka: leave(A, Ka)(q1`users, q2`users) AND q2`leader = q1`leader AND e = ReqClose(A, Leader, Ka) AND q2`trace = add(e, q1`trace) %---------------------------------------- % Transition 9: L receives the request %---------------------------------------- T9(A)(q1, e, q2): bool = EXISTS Ka: member(ReqClose(A, Leader, Ka), q1`trace) AND q2`users = q1`users AND rcv_close(A, Ka)(q1`leader, q2`leader) AND e = oops(Ka) AND q2`trace = add(e, q1`trace) %-------------------------------- % Fake message from an intruder %-------------------------------- Fake(G)(q1, e, q2): bool = EXISTS B, C, X: member(X, Gen(I)(G, q1)) AND e = msg(B, C, X) AND q2`trace = add(e, q1`trace) AND q2`users = q1`users AND q2`leader = q1`leader %----------------------------------------- % Overall system, assuming A0 is honest %----------------------------------------- A0: user Ta(q1, e, q2): bool = T1(A0)(q1, e, q2) OR T3(A0)(q1, e, q2) OR T6(A0)(q1, e, q2) OR T8(A0)(q1, e, q2) Tl(A)(q1, e, q2): bool = T2(A)(q1, e, q2) OR T4(A)(q1, e, q2) OR T5(A)(q1, e, q2) OR T7(A)(q1, e, q2) OR T9(A)(q1, e, q2) T(G)(q1, e, q2): bool = IF G=A0 THEN Ta(q1, e, q2) ELSIF G=Leader THEN (EXISTS A: Tl(A)(q1, e, q2)) ELSE Fake(G)(q1, e, q2) ENDIF %---------------- % Easy lemmas %---------------- ltkey_user: LEMMA I(A)(Shr(A)) ltkey_leader: LEMMA I(Leader)(Shr(G)) init_agent: LEMMA I(G)(B) init_data: LEMMA I(G)(Data(n)) unchanged_leader1: LEMMA Ta(q1, e,q2) => q2`leader = q1`leader unchanged_leader2: LEMMA Fake(G)(q1, e, q2) => q2`leader = q1`leader unchanged_leader3: LEMMA Tl(A)(q1, e, q2) & not A=A1 => q2`leader(A1) = q1`leader(A1) unchanged_user1: LEMMA Tl(A)(q1, e, q2) => q2`users = q1`users unchanged_user2: LEMMA Fake(G)(q1, e, q2) => q2`users = q1`users %-------------------------------------------- % Consequences of the presence of messages %-------------------------------------------- message_present: LEMMA member(msg(B, C, X), q`trace) => FieldsTrace(q)(X) auth_init_req1: LEMMA member(AuthInitReq(A, L, Na), q`trace) => VisibleTrace(q)(Encr(Shr(A), A ++ L ++ Na)) auth_init_req: LEMMA member(AuthInitReq(A, L, Na), q`trace) => PartsTrace(q)(Encr(Shr(A), A ++ L ++ Na)) auth_init_req2: LEMMA member(AuthInitReq(A, Leader, Na), q`trace) => Know(I)(Leader, q)(Na) auth_key_dist1: LEMMA member(AuthKeyDist(L, A, Na, Nl, Ka), q`trace) => VisibleTrace(q)(Encr(Shr(A), L ++ A ++ Na ++ Nl ++ Ka)) auth_key_dist: LEMMA member(AuthKeyDist(L, A, Na, Nl, Ka), q`trace) => PartsTrace(q)(Encr(Shr(A), L ++ A ++ Na ++ Nl ++ Ka)) auth_key_dist2: LEMMA member(AuthKeyDist(L, A, Na, Nl, Ka), q`trace) => Know(I)(A, q)(Nl) & Know(I)(A, q)(Ka) auth_key_dist3: LEMMA member(AuthKeyDist(Leader, A, Na, Nl, Ka), q`trace) => Know(I)(Leader, q)(Ka) auth_key_dist4: LEMMA member(AuthKeyDist(L, A, Na, Nl, Ka), q`trace) => PartsTrace(q)(Ka) auth_ack_key1: LEMMA member(AuthAckKey(A, L, Nl, Na, Ka), q`trace) => VisibleTrace(q)(Encr(Ka, A ++ L ++ Nl ++ Na)) auth_ack_key: LEMMA member(AuthAckKey(A, L, Nl, Na, Ka), q`trace) => PartsTrace(q)(Encr(Ka, A ++ L ++ Nl ++ Na)) auth_ack_key2: LEMMA member(AuthAckKey(A, Leader, Nl, Na, Ka), q`trace) & Know(I)(Leader, q)(Ka) => Know(I)(Leader, q)(Na) admin_msg1: LEMMA member(AdminMsg(L, A, Na, Nl, Ka), q`trace) => VisibleTrace(q)(Encr(Ka, L ++ A ++ Na ++ Nl)) admin_msg: LEMMA member(AdminMsg(L, A, Na, Nl, Ka), q`trace) => PartsTrace(q)(Encr(Ka, L ++ A ++ Na ++ Nl)) admin_msg2: LEMMA member(AdminMsg(L, A, Na, Nl, Ka), q`trace) & Know(I)(A, q)(Ka) => Know(I)(A, q)(Nl) ack_admin1: LEMMA member(AckAdmin(A, L, Nl, Na, Ka), q`trace) => VisibleTrace(q)(Encr(Ka, A ++ L ++ Nl ++ Na)) ack_admin: LEMMA member(AckAdmin(A, L, Nl, Na, Ka), q`trace) => PartsTrace(q)(Encr(Ka, A ++ L ++ Nl ++ Na)) ack_admin2: LEMMA member(AckAdmin(A, Leader, Nl, Na, Ka), q`trace) & Know(I)(Leader, q)(Ka) => Know(I)(Leader, q)(Na) req_close1: LEMMA member(ReqClose(A, L, Ka), q`trace) => VisibleTrace(q)(Encr(Ka, A ++ L)) req_close: LEMMA member(ReqClose(A, L, Ka), q`trace) => PartsTrace(q)(Encr(Ka, A ++ L)) %%%%%%%%%%%%%%%%%%% % Sanity checks % %%%%%%%%%%%%%%%%%%% enclave_protocol: LEMMA Protocol?(I, Q0, T) memory_A: LEMMA Reachable(Q0, T)(q) AND q`users(A0) = Connected(Na, Ka) IMPLIES Know(I)(A0, q)(Ka) memory_L: LEMMA Reachable(Q0, T)(q) AND (EXISTS N: q`leader(A) = WaitingForKeyAck(N, Ka) OR q`leader(A) = Connected(N, Ka) OR q`leader(A) = WaitingForAck(N, Ka)) IMPLIES Know(I)(Leader, q)(Ka) memory_L2: LEMMA Reachable(Q0, T)(q) AND q`leader(A) = Connected(Na, Ka) IMPLIES Know(I)(Leader, q)(Na) enclave_good_protocol: LEMMA GoodProtocol?(I, Q0, T) %-------------------------- % Secrecy of key Shr(A0) %-------------------------- Ag: set[agent] = { G | G=A0 OR G=Leader } enclave_regular: LEMMA Regular?(Ag, Shr(A0))(I, Q0, T) secrecy_ltkey: PROPOSITION Reachable(Q0, T)(q) => Secret(I)(Shr(A0), Ag, q) strong_secrecy: PROPOSITION Reachable(Q0, T)(q) => subset?(FieldsTrace(q), Coideal(Shr(A0))) %--------------------------- % Secrecy of session keys %--------------------------- InUse(Ka, q, A): bool = (EXISTS N: q`leader(A) = Connected(N, Ka) OR q`leader(A) = WaitingForKeyAck(N, Ka) OR q`leader(A) = WaitingForAck(N, Ka)) InUse(Ka, q): bool = InUse(Ka, q, A0) key_in_use1: LEMMA Reachable(Q0, T)(q) AND q`users(A0) = Connected(N, Ka) IMPLIES PartsTrace(q)(Ka) key_in_use2: LEMMA Reachable(Q0, T)(q) AND InUse(Ka, q, A) IMPLIES PartsTrace(q)(Ka) in_use_step1: LEMMA InUse(Ka, q2, A) AND T(G)(q1, e, q2) IMPLIES InUse(Ka, q1, A) OR T2(A)(q1, e, q2) in_use_step2: LEMMA InUse(Ka, q2, A1) AND T2(A2)(q1, e, q2) IMPLIES InUse(Ka, q1, A1) OR A1=A2 key_in_use3: LEMMA Reachable(Q0, T)(q) AND InUse(Ka, q, A1) AND InUse(Ka, q, A2) IMPLIES A1=A2 Secrets(Ka): { S | subset?(S, Atom?) } = { X | X=Key(Ka) OR X=Shr(A0) } secrecy_know_coideal: LEMMA subset?(FieldsTrace(q), Coideal(Secrets(Ka))) IMPLIES Ag(G) OR subset?(Know(I)(G, q), Coideal(Secrets(Ka))) secrecy_gen_coideal: LEMMA Reachable(Q0, T)(q) AND InUse(Ka, q) AND subset?(FieldsTrace(q), Coideal(Secrets(Ka))) IMPLIES Ag(G) OR subset?(Gen(I)(G, q), Coideal(Secrets(Ka))) user_coideal: LEMMA Ta(q1, e, q2) IMPLIES subset?(content(e), Coideal(Secrets(Ka))) leader_coideal: LEMMA Reachable(Q0, T)(q1) AND PartsTrace(q1)(Ka) AND Tl(A)(q1, e, q2) AND InUse(Ka, q2) IMPLIES subset?(content(e), Coideal(Secrets(Ka))) secrecy_of_session_key: PROPOSITION Reachable(Q0, T)(q) AND InUse(Ka, q) IMPLIES subset?(FieldsTrace(q), Coideal(Secrets(Ka))) secrecy_of_session_key2: PROPOSITION Reachable(Q0, T)(q) AND InUse(Ka, q) IMPLIES Secret(I)(Ka, Ag, q) %------------------------------------------------------------ % Fields encrypted with Ka or Shr(A0) can only be replayed %------------------------------------------------------------ replay1: LEMMA Reachable(Q0, T)(q1) AND Fake(G)(q1, e, q2) AND PartsTrace(q2)(Encr(Shr(A0), X)) IMPLIES Ag(G) OR PartsTrace(q1)(Encr(Shr(A0), X)) replay2: LEMMA Reachable(Q0, T)(q1) AND InUse(Ka, q1) AND Fake(G)(q1, e, q2) AND PartsTrace(q2)(Encr(Ka, X)) IMPLIES Ag(G) OR PartsTrace(q1)(Encr(Ka, X)) other_user1: LEMMA Tl(A)(q1, e, q2) AND not A=A0 AND PartsTrace(q2)(Encr(Shr(A0), X)) IMPLIES PartsTrace(q1)(Encr(Shr(A0), X)) other_user2: LEMMA Tl(A)(q1, e, q2) AND not A=A0 AND PartsTrace(q2)(Encr(Ka, Leader ++ A0 ++ X ++ Y)) IMPLIES PartsTrace(q1)(Encr(Ka, Leader ++ A0 ++ X ++ Y)) other_user3: LEMMA Tl(A)(q1, e, q2) AND not A=A0 AND PartsTrace(q2)(Encr(Ka, A0 ++ Leader)) IMPLIES PartsTrace(q1)(Encr(Ka, A0 ++ Leader)) other_user4: LEMMA Tl(A)(q1, e, q2) AND not A=A0 AND PartsTrace(q2)(Encr(Ka, A0 ++ Leader ++ X ++ Y)) IMPLIES PartsTrace(q1)(Encr(Ka, A0 ++ Leader ++ X ++ Y)) new_message: LEMMA q2`trace = add(msg(B, C, X), q1`trace) => (PartsTrace(q2)(Y) IFF Parts(X)(Y) OR PartsTrace(q1)(Y)) oops_event: LEMMA q2`trace = add(oops(X), q1`trace) => (PartsTrace(q2)(Y) IFF Parts(X)(Y) OR PartsTrace(q1)(Y)) no_message: LEMMA q2`trace = add(tau, q1`trace) => (PartsTrace(q2)(X) IFF PartsTrace(q1)(X)) fresh_nonce1: LEMMA FreshNonces(q1)(N) => not PartsTrace(q1)(Encr(K, B ++ C ++ N)) fresh_nonce2: LEMMA FreshNonces(q1)(N) => not PartsTrace(q1)(Encr(K, B ++ C ++ N ++ X)) fresh_nonce3: LEMMA FreshNonces(q1)(N) => not PartsTrace(q1)(Encr(K, B ++ C ++ N ++ X ++ Y)) fresh_key1: LEMMA FreshKeys(q1)(K) => not PartsTrace(q1)(Encr(K, X)) END enclaves $$$enclaves.prf (|enclaves| (|IKeys_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|IKeys_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|initial_knowledge| "" (GRIND) NIL NIL) (A0_TCC1 "" (EXISTENCE-TCC) (("" (INST + "Usr(0)") NIL NIL)) NIL) (|ltkey_user| "" (GRIND) NIL NIL) (|ltkey_leader| "" (GRIND) NIL NIL) (|init_agent| "" (GRIND) NIL NIL) (|init_data| "" (GRIND) NIL NIL) (|unchanged_leader1| "" (GRIND) NIL NIL) (|unchanged_leader2| "" (AUTO-REWRITE "Fake") (("" (REDUCE) NIL NIL)) NIL) (|unchanged_leader3| "" (GRIND) NIL NIL) (|unchanged_user1| "" (AUTO-REWRITE "Tl" "T2" "T4" "T5" "T7" "T9") (("" (REDUCE) NIL NIL)) NIL) (|unchanged_user2| "" (AUTO-REWRITE "Fake") (("" (REDUCE) NIL NIL)) NIL) (|message_present| "" (GRIND) NIL NIL) (|auth_init_req1| "" (SKOSIMP) (("" (EXPAND "AuthInitReq") (("" (FORWARD-CHAIN "message_present") (("" (DELETE -2) (("" (EXPAND "VisibleTrace") (("" (FORWARD-CHAIN "Inj_Visible") (("" (FORWARD-CHAIN "Snd_Visible") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|auth_init_req| "" (AUTO-REWRITE "Visible_PartsTrace" "auth_init_req1") (("" (REDUCE) NIL NIL)) NIL) (|auth_init_req2| "" (SKOSIMP) (("" (FORWARD-CHAIN "auth_init_req1") (("" (DELETE -2) (("" (USE "Know_Visible" ("X" "Encr(Shr(A!1), Agent(A!1) ++ Agent(Leader) ++ Nonce(Na!1))")) (("" (ASSERT) (("" (AUTO-REWRITE "Know_Init" "ltkey_leader") (("" (USE "Know_Encr") (("" (ASSERT) (("" (FORWARD-CHAIN "Know_Conc2") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|auth_key_dist1| "" (SKOSIMP) (("" (EXPAND "AuthKeyDist") (("" (FORWARD-CHAIN "message_present") (("" (DELETE -2) (("" (EXPAND "VisibleTrace") (("" (FORWARD-CHAIN "Inj_Visible") (("" (FORWARD-CHAIN "Snd_Visible") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|auth_key_dist| "" (AUTO-REWRITE "Visible_PartsTrace" "auth_key_dist1") (("" (REDUCE) NIL NIL)) NIL) (|auth_key_dist2| "" (SKOSIMP) (("" (FORWARD-CHAIN "auth_key_dist1") (("" (DELETE -2) (("" (USE "Know_Visible" ("X" "Encr(Shr(A!1), Agent(L!1) ++ Agent(A!1) ++ Nonce(Na!1) ++ Nonce(Nl!1) ++ Key(Ka!1))")) (("" (ASSERT) (("" (AUTO-REWRITE "Know_Init" "ltkey_user") (("" (USE "Know_Encr") (("" (ASSERT) (("" (FORWARD-CHAIN "Know_Conc2") (("" (ASSERT) (("" (FORWARD-CHAIN "Know_Conc1") (("" (FORWARD-CHAIN "Know_Conc2") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|auth_key_dist3| "" (SKOSIMP) (("" (FORWARD-CHAIN "auth_key_dist1") (("" (DELETE -2) (("" (USE "Know_Visible" ("X" "Encr(Shr(A!1), Leader ++ A!1 ++ Na!1 ++ Nl!1 ++ Ka!1)")) (("" (ASSERT) (("" (AUTO-REWRITE "Know_Init" "ltkey_leader") (("" (USE "Know_Encr") (("" (ASSERT) (("" (FORWARD-CHAIN "Know_Conc2") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|auth_key_dist4| "" (SKOSIMP) (("" (AUTO-REWRITE "AuthKeyDist" "content" "tr" "Parts_singleton" "Parts" "PartsTrace" "FieldsTrace" "Parts_equiv" "member") (("" (AUTO-REWRITE-THEORY "sets[field]") (("" (ASSERT) (("" (INST + "auth_key_dist ++ Encr(Shr(A!1), L!1 ++ A!1 ++ Na!1 ++ Nl!1 ++ Ka!1)") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|auth_ack_key1| "" (SKOSIMP) (("" (EXPAND "AuthAckKey") (("" (FORWARD-CHAIN "message_present") (("" (DELETE -2) (("" (EXPAND "VisibleTrace") (("" (FORWARD-CHAIN "Inj_Visible") (("" (FORWARD-CHAIN "Snd_Visible") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|auth_ack_key| "" (AUTO-REWRITE "Visible_PartsTrace" "auth_ack_key1") (("" (REDUCE) NIL NIL)) NIL) (|auth_ack_key2| "" (SKOSIMP) (("" (FORWARD-CHAIN "auth_ack_key1") (("" (USE "Know_Visible" ("X" "Encr(Ka!1, Agent(A!1) ++ Agent(Leader) ++ Nonce(Nl!1) ++ Nonce(Na!1))")) (("" (ASSERT) (("" (FORWARD-CHAIN "Know_Encr") (("" (FORWARD-CHAIN "Know_Conc2") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|admin_msg1| "" (SKOSIMP) (("" (EXPAND "AdminMsg") (("" (FORWARD-CHAIN "message_present") (("" (DELETE -2) (("" (EXPAND "VisibleTrace") (("" (FORWARD-CHAIN "Inj_Visible") (("" (FORWARD-CHAIN "Snd_Visible") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|admin_msg| "" (AUTO-REWRITE "Visible_PartsTrace" "admin_msg1") (("" (REDUCE) NIL NIL)) NIL) (|admin_msg2| "" (SKOSIMP) (("" (FORWARD-CHAIN "admin_msg1") (("" (USE "Know_Visible" ("X" "Encr(Ka!1, Agent(L!1) ++ Agent(A!1) ++ Nonce(Na!1) ++ Nonce(Nl!1))")) (("" (ASSERT) (("" (FORWARD-CHAIN "Know_Encr") (("" (FORWARD-CHAIN "Know_Conc2") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|ack_admin1| "" (SKOSIMP) (("" (EXPAND "AckAdmin") (("" (FORWARD-CHAIN "message_present") (("" (DELETE -2) (("" (EXPAND "VisibleTrace") (("" (FORWARD-CHAIN "Inj_Visible") (("" (FORWARD-CHAIN "Snd_Visible") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|ack_admin| "" (AUTO-REWRITE "Visible_PartsTrace" "ack_admin1") (("" (REDUCE) NIL NIL)) NIL) (|ack_admin2| "" (SKOSIMP) (("" (FORWARD-CHAIN "ack_admin1") (("" (USE "Know_Visible" ("X" "Encr(Ka!1, Agent(A!1) ++ Agent(Leader) ++ Nonce(Nl!1) ++ Nonce(Na!1))")) (("" (ASSERT) (("" (FORWARD-CHAIN "Know_Encr") (("" (FORWARD-CHAIN "Know_Conc2") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|req_close1| "" (SKOSIMP) (("" (EXPAND "ReqClose") (("" (FORWARD-CHAIN "message_present") (("" (DELETE -2) (("" (EXPAND "VisibleTrace") (("" (FORWARD-CHAIN "Inj_Visible") (("" (FORWARD-CHAIN "Snd_Visible") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|req_close| "" (AUTO-REWRITE "Visible_PartsTrace" "req_close1") (("" (REDUCE) NIL NIL)) NIL) (|enclave_protocol| "" (EXPAND "Protocol?") (("" (GROUND) (("1" (GRIND) NIL NIL) ("2" (SKOSIMP) (("2" (AUTO-REWRITE-THEORY "enclaves" :ALWAYS? T) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|memory_A| "" (SKOSIMP) (("" (USE "Reachable_induct2" ("P" "lambda q: (EXISTS N: q`users(A0) = Connected(N, Ka!1)) => Know(I)(A0, q)(Ka!1)")) (("" (GROUND) (("1" (REDUCE) NIL NIL) ("2" (DELETE -1 -2 2) (("2" (GRIND :EXCLUDE ("Know")) NIL NIL)) NIL) ("3" (DELETE -1 -2 2) (("3" (SKOSIMP*) (("3" (LEMMA "enclave_protocol") (("3" (USE "Monotonic_Knowledge") (("3" (ASSERT) (("3" (EXPAND* "subset?" "member") (("3" (INST?) (("3" (ASSERT) (("3" (DELETE -1) (("3" (EXPAND "T") (("3" (SMASH) (("1" (AUTO-REWRITE-THEORY "user_transitions") (("1" (AUTO-REWRITE "Ta" "T1" "T3" "T6" "T8") (("1" (REDUCE :IF-MATCH NIL) (("1" (FORWARD-CHAIN "auth_key_dist2") NIL NIL) ("2" (INST?) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (FORWARD-CHAIN "unchanged_user1") (("2" (REDUCE) NIL NIL)) NIL)) NIL) ("3" (FORWARD-CHAIN "unchanged_user2") (("3" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|memory_L| "" (SKOSIMP) (("" (USE "Reachable_induct2" ("P" "lambda q: (EXISTS N: q`leader(A!1)=WaitingForKeyAck(N, Ka!1) OR q`leader(A!1) = Connected(N, Ka!1) OR q`leader(A!1) = WaitingForAck(N, Ka!1)) => Know(I)(Leader, q)(Ka!1)")) (("" (GROUND) (("1" (REDUCE) NIL NIL) ("2" (DELETE -1 -2 2) (("2" (GRIND :EXCLUDE ("Know")) NIL NIL)) NIL) ("3" (DELETE -1 -2 2) (("3" (SKOSIMP) (("3" (LEMMA "enclave_protocol") (("3" (USE "Monotonic_Knowledge") (("3" (ASSERT) (("3" (EXPAND* "subset?" "member") (("3" (INST?) (("3" (ASSERT) (("3" (DELETE -1) (("3" (EXPAND "T") (("3" (SMASH) (("1" (FORWARD-CHAIN "unchanged_leader1") (("1" (REPLACE*) NIL NIL)) NIL) ("2" (AUTO-REWRITE-THEORY "leader_transitions") (("2" (AUTO-REWRITE "Tl" "T2" "T4" "T5" "T7" "T9") (("2" (SKOLEM!) (("2" (CASE-REPLACE "A!3 = A!1") (("1" (APPLY (THEN (SMASH) (SKOSIMP))) (("1" (REPLACE -8) (("1" (ASSERT) (("1" (SKOSIMP) (("1" (REPLACE*) (("1" (DELETE -1 -2 -3 -4 -5 -6 -7 -8 -9 -11 -12 1 2 3) (("1" (USE "auth_key_dist3") (("1" (AUTO-REWRITE "add" "member") (("1" (REPLACE*) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REDUCE) NIL NIL) ("3" (REPLACE -6) (("3" (ASSERT) (("3" (SKOSIMP) (("3" (INST + "Na!1") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("4" (REPLACE -6) (("4" (ASSERT) (("4" (SKOSIMP) (("4" (INST + "Nl!1") (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("5" (SKOSIMP) (("5" (REPLACE -6) (("5" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE 4) (("2" (FORWARD-CHAIN "unchanged_leader3") (("2" (REPLACE*) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (FORWARD-CHAIN "unchanged_leader2") (("3" (REPLACE*) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|memory_L2| "" (SKOSIMP) (("" (USE "Reachable_induct3" ("P" "lambda q: q`leader(A!1) = Connected(Na!1, Ka!1) => Know(I)(Leader, q)(Na!1)")) (("" (GROUND) (("1" (REDUCE) NIL NIL) ("2" (GRIND :EXCLUDE ("Know")) NIL NIL) ("3" (DELETE -1 -2 2) (("3" (SKOSIMP) (("3" (LEMMA "enclave_protocol") (("3" (USE "Monotonic_Knowledge") (("3" (ASSERT) (("3" (EXPAND* "subset?" "member") (("3" (INST?) (("3" (ASSERT) (("3" (DELETE -1) (("3" (EXPAND "T" -2) (("3" (SMASH) (("1" (FORWARD-CHAIN "unchanged_leader1") (("1" (REPLACE*) NIL NIL)) NIL) ("2" (AUTO-REWRITE-THEORY "leader_transitions") (("2" (AUTO-REWRITE "Tl" "T2" "T4" "T5" "T7" "T9") (("2" (REDUCE) (("1" (USE "memory_L") (("1" (GROUND) (("1" (FORWARD-CHAIN "auth_ack_key2") NIL NIL) ("2" (REPLACE*) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL) ("2" (USE "memory_L") (("2" (GROUND) (("1" (FORWARD-CHAIN "ack_admin2") NIL NIL) ("2" (REPLACE*) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (FORWARD-CHAIN "unchanged_leader2") (("3" (REPLACE*) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|enclave_good_protocol| "" (EXPAND "GoodProtocol?") (("" (LEMMA "enclave_protocol") (("" (ASSERT) (("" (AUTO-REWRITE "content_msg" "content_oops" "content_tau" "Gen_Conc" "Gen_Encr" "Gen_Data" "Gen_Agent" "Gen_LongTermKey" "Gen_SessionKey" "Gen_Nonce" "ltkey_user" "ltkey_leader" "init_agent" "init_data" "Know_Init" "LongTermKey?" "SessionKey?") (("" (SKOSIMP) (("" (EXPAND "T" -3) (("" (SMASH) (("1" (AUTO-REWRITE "Ta" "T1" "T3" "T6" "T8") (("1" (REDUCE) (("1" (DELETE -1 -2 -5 -6 -7 -8) (("1" (EXPAND* "AuthInitReq" "auth_init_req") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (FORWARD-CHAIN "auth_key_dist2") (("2" (DELETE -3 -4 -5 -6 -7 -9 -10 -11 -12) (("2" (EXPAND* "AuthAckKey" "auth_ack_key") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("3" (EXPAND "rcv_admin") (("3" (FLATTEN) (("3" (FORWARD-CHAIN "memory_A") (("3" (FORWARD-CHAIN "admin_msg2") (("3" (DELETE -3 -4 -5 -6 -7 -9 -10 -11 -12 -13) (("3" (EXPAND* "AckAdmin" "ack_admin") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (EXPAND "leave") (("4" (SKOSIMP*) (("4" (FORWARD-CHAIN "memory_A") (("4" (DELETE -2 -3 -4 -5 -6 -7 -8 -9 -10) (("4" (EXPAND* "ReqClose" "req_close") (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (AUTO-REWRITE "Tl" "T2" "T4" "T5" "T7" "T9") (("2" (REDUCE) (("1" (FORWARD-CHAIN "auth_init_req2") (("1" (CASE-REPLACE "A!1 = Leader") (("1" (DELETE -1 -3 -4 -5 -6 -7 -8 -11 -12 -13 -14 1) (("1" (EXPAND* "AuthKeyDist" "auth_key_dist") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (EXPAND "snd_admin") (("2" (FLATTEN) (("2" (USE "memory_L") (("2" (REDUCE) (("2" (FORWARD-CHAIN "memory_L2") (("2" (CASE-REPLACE "A!1 = Leader") (("1" (DELETE -1 -4 -5 -6 -7 -8 -10 -11 -12 -13 -14 1) (("1" (EXPAND* "AdminMsg" "admin_msg") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (EXPAND "rcv_close") (("3" (FLATTEN) (("3" (USE "memory_L") (("3" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (EXPAND* "Fake" "member") (("3" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|enclave_regular_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|enclave_regular| "" (AUTO-REWRITE-THEORY "enclaves_messages") (("" (AUTO-REWRITE-THEORY "sets[field]") (("" (AUTO-REWRITE-THEORY "enclaves" :ALWAYS? T) (("" (AUTO-REWRITE "Regular?" "Parts" "Parts_singleton" "Parts_emptyset" "content" "equal_key" "equal_ltkey") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|secrecy_ltkey| "" (AUTO-REWRITE "enclave_good_protocol" "enclave_regular" "Secrecy_of_long_term_keys" "LongTermKey?") (("" (ASSERT) NIL NIL)) NIL) (|strong_secrecy| "" (USE* "enclave_good_protocol" "enclave_regular") (("" (AUTO-REWRITE "LongTermKey?") (("" (FORWARD-CHAIN "StrongSecrecy_of_long_term_keys") NIL NIL)) NIL)) NIL) (|key_in_use1| "" (SKOSIMP) (("" (USE "Reachable_induct3" ("P" "lambda q: (EXISTS N: q`users(A0) = Connected(N, Ka!1)) => PartsTrace(q)(Ka!1)")) (("" (GROUND) (("1" (REDUCE) NIL NIL) ("2" (DELETE -1 -2 2) (("2" (GRIND :EXCLUDE ("PartsTrace")) NIL NIL)) NIL) ("3" (DELETE -1 -2 2) (("3" (SKOSIMP) (("3" (LEMMA "enclave_protocol") (("3" (FORWARD-CHAIN "PartsTrace_step") (("3" (REPLACE*) (("3" (EXPAND* "union" "member") (("3" (DELETE -1 -2 -3) (("3" (GROUND) (("3" (EXPAND "T") (("3" (SMASH) (("1" (AUTO-REWRITE "Ta" "T1" "T3" "T6" "T8") (("1" (AUTO-REWRITE-THEORY "user_transitions") (("1" (REDUCE) (("1" (FORWARD-CHAIN "auth_key_dist4") NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (FORWARD-CHAIN "unchanged_user1") (("2" (REPLACE*) NIL NIL)) NIL)) NIL) ("3" (FORWARD-CHAIN "unchanged_user2") (("3" (REPLACE*) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|key_in_use2| "" (SKOSIMP) (("" (USE "Reachable_induct3" ("P" "lambda q: InUse(Ka!1, q, A!1) => PartsTrace(q)(Ka!1)")) (("" (GROUND) (("1" (REDUCE) NIL NIL) ("2" (DELETE -1 -2 2) (("2" (GRIND :EXCLUDE ("PartsTrace")) NIL NIL)) NIL) ("3" (DELETE -1 -2 2) (("3" (SKOSIMP) (("3" (LEMMA "enclave_protocol") (("3" (FORWARD-CHAIN "PartsTrace_step") (("3" (REPLACE*) (("3" (EXPAND* "union" "member") (("3" (GROUND) (("3" (DELETE -1 -2 -3) (("3" (EXPAND* "T" "InUse") (("3" (SMASH) (("1" (FORWARD-CHAIN "unchanged_leader1") (("1" (REPLACE*) NIL NIL)) NIL) ("2" (SKOLEM!) (("2" (AUTO-REWRITE "Tl" "T2" "T4" "T5" "T7" "T9") (("2" (AUTO-REWRITE-THEORY "leader_transitions") (("2" (REDUCE :IF-MATCH ALL) (("2" (DELETE -) (("2" (DELETE 1 2 3 4 5 6 7 9) (("2" (AUTO-REWRITE "Parts" "Parts_singleton" "content" "AuthKeyDist") (("2" (AUTO-REWRITE-THEORY "sets[field]") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (FORWARD-CHAIN "unchanged_leader2") (("3" (REPLACE*) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|in_use_step1| "" (SKOSIMP) (("" (EXPAND "T") (("" (SMASH) (("1" (FORWARD-CHAIN "unchanged_leader1") (("1" (DELETE -4 2) (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (USE "unchanged_leader3" ("A" "A!2" "A1" "A!1")) (("2" (GROUND) (("1" (DELETE -4 3) (("1" (GRIND) NIL NIL)) NIL) ("2" (AUTO-REWRITE "Tl" "T4" "T5" "T7" "T9") (("2" (AUTO-REWRITE-THEORY "leader_transitions") (("2" (EXPAND "InUse") (("2" (REDUCE :IF-MATCH ALL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (FORWARD-CHAIN "unchanged_leader2") (("3" (DELETE -3 4) (("3" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|in_use_step2| "" (AUTO-REWRITE-THEORIES "leader_transitions") (("" (EXPAND* "InUse" "T2") (("" (REDUCE) NIL NIL)) NIL)) NIL) (|key_in_use3| "" (SKOSIMP) (("" (USE "Reachable_induct3" ("P" "lambda q: InUse(Ka!1, q, A1!1) AND InUse(Ka!1, q, A2!1) => A1!1 = A2!1")) (("" (GROUND) (("1" (REDUCE) NIL NIL) ("2" (DELETE -1 -2 -3 2) (("2" (GRIND) NIL NIL)) NIL) ("3" (DELETE -1 -2 -3 2) (("3" (SKOSIMP) (("3" (GROUND) (("1" (USE "in_use_step1") (("1" (ASSERT) (("1" (USE "in_use_step2" ("A1" "A2!1")) (("1" (ASSERT) (("1" (FORWARD-CHAIN "key_in_use2") (("1" (DELETE -2 -4 -5 -7 1) (("1" (AUTO-REWRITE-THEORY "leader_transitions") (("1" (AUTO-REWRITE "T2" "FreshKeys" "InUse") (("1" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (USE "in_use_step1") (("2" (ASSERT) (("2" (FORWARD-CHAIN "in_use_step2") (("2" (FORWARD-CHAIN "key_in_use2") (("2" (DELETE -2 -4 -5 -6 1) (("2" (AUTO-REWRITE-THEORY "leader_transitions") (("2" (AUTO-REWRITE "T2" "FreshKeys" "InUse") (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Secrets_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|secrecy_know_coideal| "" (SKOSIMP) (("" (EXPAND "Know") (("" (AUTO-REWRITE "Parts_I" "equal_key" "equal_ltkey" "equal_stkey") (("" (REWRITE "Analz_Closure_Subset") (("" (REWRITE "union_upper_bound") (("" (REWRITE "Subset_Coideal") (("" (DELETE -1 2 3 5) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|secrecy_gen_coideal| "" (SKOSIMP) (("" (EXPAND "Gen") (("" (AUTO-REWRITE "Parts_FreshFields") (("" (USE "secrecy_know_coideal") (("" (GROUND) (("" (EXPAND "InUse") (("" (FORWARD-CHAIN "key_in_use2") (("" (DELETE -3 -4 -5) (("" (REWRITE "Synth_Closure_Subset") (("" (REWRITE "union_upper_bound") (("" (REWRITE "Subset_Coideal") (("" (DELETE -2 2 3 4 5) (("" (GRIND :EXCLUDE ("PartsTrace")) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|user_coideal| "" (AUTO-REWRITE "Secrets" "equal_key" "equal_ltkey" "equal_stkey" "content_msg" "content_tau" "Coideal_Encr" "Coideal_Conc" "Coideal_Atom" "Atom?" "Ta" "T1" "T3" "T6" "T8") (("" (AUTO-REWRITE-THEORY "enclaves_messages") (("" (REDUCE) NIL NIL)) NIL)) NIL) (|leader_coideal| "" (SKOSIMP) (("" (ASSERT) (("" (AUTO-REWRITE "Secrets" "equal_key" "equal_ltkey" "equal_stkey" "content_msg" "content_tau" "content_oops" "Coideal_Encr" "Coideal_Conc" "Coideal_Atom" "Atom?" "Tl" "T2" "T4" "T5" "T7" "T9" "FreshKeys") (("" (AUTO-REWRITE-THEORY "enclaves_messages") (("" (REDUCE) (("" (EXPAND "InUse") (("" (CASE-REPLACE "A!1 = A0") (("1" (DELETE -2 -3 -4 -5 -6 -8 -9 -11) (("1" (GRIND) NIL NIL)) NIL) ("2" (CASE "InUse(Ka!1, q1!1, A!1)") (("1" (STOP-REWRITE "Tl") (("1" (USE "key_in_use3" ("A2" "A0")) (("1" (ASSERT) (("1" (DELETE -1 -2 -3 -4 -5 -6 -7 -9) (("1" (USE "in_use_step1" ("G" "Leader" "q2" "q2!1")) (("1" (ASSERT) (("1" (EXPAND "T") (("1" (INST + "A!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 -2 -3 -4 -5 -7 -8 -9 -10) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|secrecy_of_session_key| "" (SKOSIMP) (("" (USE "Reachable_induct3" ("P" "lambda q: InUse(Ka!1, q) => subset?(FieldsTrace(q), Coideal(Secrets(Ka!1)))")) (("" (GROUND) (("1" (REDUCE) NIL NIL) ("2" (DELETE -1 -2 2) (("2" (GRIND :EXCLUDE ("subset?" "FieldsTrace" "Coideal" "Secrets")) NIL NIL)) NIL) ("3" (DELETE -1 -2 2) (("3" (SKOSIMP) (("3" (LEMMA "enclave_protocol") (("3" (FORWARD-CHAIN "FieldsTrace_step") (("3" (REPLACE*) (("3" (DELETE -1 -2) (("3" (CASE "InUse(Ka!1, q1!1)") (("1" (ASSERT) (("1" (REWRITE "union_upper_bound") (("1" (DELETE 2) (("1" (EXPAND "T" -4) (("1" (SMASH) (("1" (USE "user_coideal") (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOLEM!) (("2" (USE "key_in_use2" ("A" "A0")) (("2" (GROUND) (("1" (FORWARD-CHAIN "leader_coideal") NIL NIL) ("2" (EXPAND "InUse" -1) (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (AUTO-REWRITE "Ag") (("3" (USE "secrecy_gen_coideal" ("G" "A!1")) (("3" (GROUND) (("3" (DELETE -2 -3 -4 -6) (("3" (GRIND :EXCLUDE ("Gen" "Coideal" "Secrets") :REWRITES ("content_msg")) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -2) (("2" (EXPAND "InUse") (("2" (FORWARD-CHAIN "in_use_step1") (("2" (DELETE -3 1) (("2" (AUTO-REWRITE-THEORY "leader_transitions") (("2" (AUTO-REWRITE "InUse" "T2") (("2" (REDUCE :IF-MATCH ALL) (("2" (DELETE -1 -2 -3 -5 -6 -7 -8 -9 -11 -12) (("2" (REWRITE "union_upper_bound") (("1" (AUTO-REWRITE "cont_auth_key_dist" "Coideal_Encr" "Coideal_Conc" "Coideal_Atom" "Atom?" "Secrets" "auth_key_dist") (("1" (DELETE 2) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (DELETE -2 2) (("2" (AUTO-REWRITE "LongTermKey?" "enclave_good_protocol") (("2" (REWRITE "Subset_Coideal") (("2" (USE "enclave_regular") (("2" (USE "Regularity") (("2" (GROUND) (("2" (INST?) (("2" (ASSERT) (("2" (DELETE -1 3) (("2" (GRIND :EXCLUDE ("FieldsTrace" "Parts") :REWRITES ("equal_key" "equal_stkey" "equal_ltkey")) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|secrecy_of_session_key2| "" (SKOSIMP) (("" (FORWARD-CHAIN "secrecy_of_session_key") (("" (EXPAND "Secret") (("" (SKOSIMP) (("" (USE "secrecy_know_coideal") (("" (GROUND) (("" (DELETE -2 -3 -4) (("" (AUTO-REWRITE "subset?" "member" "Coideal_Atom" "Atom?" "Secrets") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|replay1| "" (SKOSIMP) (("" (LEMMA "enclave_protocol") (("" (USE "PartsTrace_step" ("T" "T" "q1" "q1!1" "q2" "q2!1")) (("" (GROUND) (("1" (AUTO-REWRITE "Fake" "union" "member" "content_msg" "FreshKeys" "SessionKey?" "Secret") (("1" (REDUCE) (("1" (DELETE -1 -2 -5 -6 -7 -8) (("1" (FORWARD-CHAIN "secrecy_ltkey") (("1" (USE "Knowledge_step3") (("1" (ASSERT) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 -2 -4 3) (("2" (EXPAND* "T" "Ag") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|replay2| "" (SKOSIMP) (("" (LEMMA "enclave_protocol") (("" (USE "PartsTrace_step" ("T" "T" "q1" "q1!1" "q2" "q2!1")) (("" (GROUND) (("1" (AUTO-REWRITE "Fake" "union" "member" "content_msg" "FreshKeys" "SessionKey?" "Secret") (("1" (REDUCE) (("1" (DELETE -1 -2 -6 -7 -8 -9) (("1" (FORWARD-CHAIN "secrecy_of_session_key2") (("1" (EXPAND "InUse") (("1" (FORWARD-CHAIN "key_in_use2") (("1" (USE "Knowledge_step3") (("1" (ASSERT) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 -2 -3 -5 3) (("2" (EXPAND* "T" "Ag") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|other_user1| "" (SKOSIMP) (("" (USE "enclave_protocol") (("" (USE "PartsTrace_step" ("T" "T" "A" "Leader" "q1" "q1!1" "q2" "q2!1")) (("" (GROUND) (("1" (AUTO-REWRITE-THEORY "sets[field]") (("1" (AUTO-REWRITE-THEORY "enclaves_messages") (("1" (REPLACE*) (("1" (ASSERT) (("1" (DELETE -1 -2 2) (("1" (AUTO-REWRITE "content" "Parts_singleton" "Parts" "Tl" "T2" "T4" "T5" "T7" "T9" "Parts_emptyset" "equal_conc" "equal_encr" "equal_key" "equal_ltkey" "equal_stkey") (("1" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "T" +) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|other_user2| "" (SKOSIMP) (("" (USE "enclave_protocol") (("" (USE "PartsTrace_step" ("T" "T" "A" "Leader" "q1" "q1!1" "q2" "q2!1")) (("" (GROUND) (("1" (AUTO-REWRITE-THEORY "sets[field]") (("1" (AUTO-REWRITE-THEORY "enclaves_messages") (("1" (REPLACE*) (("1" (ASSERT) (("1" (DELETE -1 -2 2) (("1" (AUTO-REWRITE "content" "Parts_singleton" "Parts" "Tl" "T2" "T4" "T5" "T7" "T9" "Parts_emptyset" "equal_conc" "equal_encr" "equal_key" "equal_ltkey" "equal_stkey" "equal_agent") (("1" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "T" +) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|other_user3| "" (SKOSIMP) (("" (USE "enclave_protocol") (("" (USE "PartsTrace_step" ("T" "T" "A" "Leader" "q1" "q1!1" "q2" "q2!1")) (("" (GROUND) (("1" (AUTO-REWRITE-THEORY "sets[field]") (("1" (AUTO-REWRITE-THEORY "enclaves_messages") (("1" (REPLACE*) (("1" (ASSERT) (("1" (DELETE -1 -2 2) (("1" (AUTO-REWRITE "content" "Parts_singleton" "Parts" "Tl" "T2" "T4" "T5" "T7" "T9" "Parts_emptyset" "equal_conc" "equal_encr" "equal_key" "equal_ltkey" "equal_stkey" "equal_agent") (("1" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "T" +) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|other_user4| "" (SKOSIMP) (("" (USE "enclave_protocol") (("" (USE "PartsTrace_step" ("T" "T" "A" "Leader" "q1" "q1!1" "q2" "q2!1")) (("" (GROUND) (("1" (AUTO-REWRITE-THEORY "sets[field]") (("1" (AUTO-REWRITE-THEORY "enclaves_messages") (("1" (REPLACE*) (("1" (ASSERT) (("1" (DELETE -1 -2 2) (("1" (AUTO-REWRITE "content" "Parts_singleton" "Parts" "Tl" "T2" "T4" "T5" "T7" "T9" "Parts_emptyset" "equal_conc" "equal_encr" "equal_key" "equal_ltkey" "equal_stkey" "equal_agent") (("1" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "T" +) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|new_message| "" (SKOSIMP) (("" (EXPAND "PartsTrace") (("" (AUTO-REWRITE "add" "union" "member" "content" "singleton" "Parts_add") (("" (CASE-REPLACE "FieldsTrace(q2!1) = add(X!1, FieldsTrace(q1!1))") (("1" (DELETE -) (("1" (ASSERT) NIL NIL)) NIL) ("2" (DELETE 2) (("2" (EXPAND* "FieldsTrace" "tr") (("2" (REPLACE*) (("2" (DELETE -) (("2" (REDUCE :IF-MATCH NIL) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (REDUCE :IF-MATCH NIL) (("1" (REPLACE -1 * RL) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL) ("3" (INST?) (("3" (ASSERT) NIL NIL)) NIL) ("4" (INST?) (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|oops_event| "" (SKOSIMP) (("" (EXPAND "PartsTrace") (("" (AUTO-REWRITE "add" "union" "member" "content" "singleton" "Parts_add") (("" (CASE-REPLACE "FieldsTrace(q2!1) = add(X!1, FieldsTrace(q1!1))") (("1" (DELETE -) (("1" (ASSERT) NIL NIL)) NIL) ("2" (DELETE 2) (("2" (EXPAND* "FieldsTrace" "tr") (("2" (REPLACE*) (("2" (DELETE -) (("2" (REDUCE :IF-MATCH NIL) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (REDUCE :IF-MATCH NIL) (("1" (REPLACE -1 * RL) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL) ("3" (INST?) (("3" (ASSERT) NIL NIL)) NIL) ("4" (INST?) (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|no_message| "" (SKOSIMP) (("" (EXPAND "PartsTrace") (("" (CASE-REPLACE "FieldsTrace(q2!1) = FieldsTrace(q1!1)") (("1" (ASSERT) NIL NIL) ("2" (DELETE 2) (("2" (EXPAND* "FieldsTrace" "tr") (("2" (AUTO-REWRITE "add" "member" "content" "emptyset") (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (REDUCE :IF-MATCH NIL) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|fresh_nonce1| "" (SKOSIMP) (("" (EXPAND* "FreshNonces" "PartsTrace") (("" (FORWARD-CHAIN "Body_parts") (("" (FORWARD-CHAIN "Snd_parts") NIL NIL)) NIL)) NIL)) NIL) (|fresh_nonce2| "" (SKOSIMP) (("" (EXPAND* "FreshNonces" "PartsTrace") (("" (FORWARD-CHAIN "Body_parts") (("" (FORWARD-CHAIN "Fst_parts") (("" (FORWARD-CHAIN "Snd_parts") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|fresh_nonce3| "" (SKOSIMP) (("" (EXPAND* "FreshNonces" "PartsTrace") (("" (FORWARD-CHAIN "Body_parts") (("" (FORWARD-CHAIN "Fst_parts") (("" (FORWARD-CHAIN "Fst_parts") (("" (FORWARD-CHAIN "Snd_parts") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|fresh_key1| "" (GRIND) NIL NIL))