%% PVS Version 3.1 %% 6.2 [Linux (x86)] (Feb 13, 2003 4:25) $$$pvs-strategies ;; ;; Proof Strategies for the Enclaves Verification Diagrams ;; ;; 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)(assert)) (then (skolem!) (spread (case-replace "A!1=A0") ((then (leader-rewrites)(reduce)(expand Q -)(skosimp)(assert)) (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") (defstep origin-bug (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 0 (tran_Q1-3 "test." 3243631146 3243631177 ("" (origin "Q1") (("1" (message-rewrites) (("1" (expand "Q2") (("1" (inst? +) (("1" (ground) (("1" (skosimp) (("1" (use "new_message") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (message-rewrites) (("2" (expand "Q12") (("2" (new-message) nil nil)) nil)) nil)) nil) proved ((AuthKeyDist const-decl "event" enclaves_messages nil) (auth_key_dist const-decl "field" enclaves_messages nil) (fresh_key1 formula-decl nil enclaves nil) (Q12 const-decl "bool" enclaves_abstraction nil) (AuthInitReq const-decl "event" enclaves_messages nil) (auth_init_req const-decl "field" enclaves_messages nil) (nonce type-decl nil fields nil) (fresh_nonce3 formula-decl nil enclaves nil) (add const-decl "(nonempty?)" sets nil) (union const-decl "set" sets nil) (equal_encr formula-decl nil fields nil) (equal_conc formula-decl nil fields nil) (member const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (Parts def-decl "set[field]" fields nil) (Key adt-constructor-decl "[key -> (Key?)]" fields nil) (Key? adt-recognizer-decl "[field -> boolean]" fields nil) (Nonce adt-constructor-decl "[nonce -> (Nonce?)]" fields nil) (Nonce? adt-recognizer-decl "[field -> boolean]" fields nil) (Agent adt-constructor-decl "[agent -> (Agent?)]" fields nil) (Agent? adt-recognizer-decl "[field -> boolean]" fields nil) (Shr adt-constructor-decl "[agent -> (Shr?)]" fields nil) (Shr? adt-recognizer-decl "[key -> boolean]" fields nil) (Encr adt-constructor-decl "[[key, field] -> (Encr?)]" fields nil) (Encr? adt-recognizer-decl "[field -> boolean]" fields nil) (Data adt-constructor-decl "[data -> (Data?)]" fields nil) (Data? adt-recognizer-decl "[field -> boolean]" fields nil) (data type-eq-decl nil fields nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (++ adt-constructor-decl "[[field, field] -> (Con?)]" fields nil) (Con? adt-recognizer-decl "[field -> boolean]" fields nil) (field type-decl nil fields nil) (Leader adt-constructor-decl "(Leader?)" fields nil) (Leader? adt-recognizer-decl "[agent -> boolean]" fields nil) (new_message formula-decl nil enclaves nil) (Q2 const-decl "bool" enclaves_abstraction nil) (init_req const-decl "bool" user_transitions nil) (T1 const-decl "bool" enclaves nil) (rcv_key const-decl "bool" user_transitions nil) (T3 const-decl "bool" enclaves nil) (rcv_admin const-decl "bool" user_transitions nil) (T6 const-decl "bool" enclaves nil) (leave const-decl "bool" user_transitions nil) (T8 const-decl "bool" enclaves nil) (Ta const-decl "bool" enclaves nil) (rcv_init_req const-decl "bool" leader_transitions nil) (T2 const-decl "bool" enclaves nil) (rcv_key_ack const-decl "bool" leader_transitions nil) (T4 const-decl "bool" enclaves nil) (snd_admin const-decl "bool" leader_transitions nil) (T5 const-decl "bool" enclaves nil) (rcv_ack const-decl "bool" leader_transitions nil) (T7 const-decl "bool" enclaves nil) (rcv_close const-decl "bool" leader_transitions nil) (T9 const-decl "bool" enclaves nil) (Tl const-decl "bool" enclaves nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (key type-decl nil fields nil) (Ssk? adt-recognizer-decl "[key -> boolean]" fields nil) (unchanged_leader3 formula-decl nil enclaves nil) (unchanged_user1 formula-decl nil enclaves nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (Usr? adt-recognizer-decl "[agent -> boolean]" fields nil) (user type-eq-decl nil fields nil) (A0 const-decl "user" enclaves nil) (Q1 const-decl "bool" enclaves_abstraction nil) (unchanged_user2 formula-decl nil enclaves nil) (agent type-decl nil fields nil) (event type-decl nil events nil) (leader type-eq-decl nil leader_transitions nil) (set type-eq-decl nil sets nil) (usr type-eq-decl nil user_transitions nil) (global type-eq-decl nil enclaves nil) (unchanged_leader2 formula-decl nil enclaves nil) (T const-decl "bool" enclaves nil)) 26288 5810 t shostak) (tran_Q1-2 "strategy new-message does not work as before" 3243348139 3243348139 ("" (origin "Q1") (("1" (message-rewrites) (("1" (expand "Q2") (("1" (inst? +) (("1" (assert) (("1" (replace*) (("1" (assert) (("1" (skosimp) (("1" (use "new_message") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (message-rewrites) (("2" (expand "Q12") (("2" (inst? +) (("2" (assert) (("2" (replace*) (("2" (assert) (("2" (new-message) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved nil 438481 8320 t shostak) (tran_Q1-1 nil 3243342778 3243348252 ("" (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) proved ((AuthKeyDist const-decl "event" enclaves_messages nil) (auth_key_dist const-decl "field" enclaves_messages nil) (fresh_key1 formula-decl nil enclaves nil) (Q12 const-decl "bool" enclaves_abstraction nil) (AuthInitReq const-decl "event" enclaves_messages nil) (auth_init_req const-decl "field" enclaves_messages nil) (nonce type-decl nil fields nil) (new_message formula-decl nil enclaves nil) (Leader? adt-recognizer-decl "[agent -> boolean]" fields nil) (Leader adt-constructor-decl "(Leader?)" fields nil) (field type-decl nil fields nil) (Con? adt-recognizer-decl "[field -> boolean]" fields nil) (++ adt-constructor-decl "[[field, field] -> (Con?)]" fields nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (data type-eq-decl nil fields nil) (Data? adt-recognizer-decl "[field -> boolean]" fields nil) (Data adt-constructor-decl "[data -> (Data?)]" fields nil) (Encr? adt-recognizer-decl "[field -> boolean]" fields nil) (Encr adt-constructor-decl "[[key, field] -> (Encr?)]" fields nil) (Shr? adt-recognizer-decl "[key -> boolean]" fields nil) (Shr adt-constructor-decl "[agent -> (Shr?)]" fields nil) (Agent? adt-recognizer-decl "[field -> boolean]" fields nil) (Agent adt-constructor-decl "[agent -> (Agent?)]" fields nil) (Nonce? adt-recognizer-decl "[field -> boolean]" fields nil) (Nonce adt-constructor-decl "[nonce -> (Nonce?)]" fields nil) (Key? adt-recognizer-decl "[field -> boolean]" fields nil) (Key adt-constructor-decl "[key -> (Key?)]" fields nil) (Parts def-decl "set[field]" fields nil) (singleton const-decl "(singleton?)" sets nil) (member const-decl "bool" sets nil) (equal_conc formula-decl nil fields nil) (equal_encr formula-decl nil fields nil) (union const-decl "set" sets nil) (add const-decl "(nonempty?)" sets nil) (fresh_nonce3 formula-decl nil enclaves nil) (Q2 const-decl "bool" enclaves_abstraction nil) (init_req const-decl "bool" user_transitions nil) (T1 const-decl "bool" enclaves nil) (rcv_key const-decl "bool" user_transitions nil) (T3 const-decl "bool" enclaves nil) (rcv_admin const-decl "bool" user_transitions nil) (T6 const-decl "bool" enclaves nil) (leave const-decl "bool" user_transitions nil) (T8 const-decl "bool" enclaves nil) (Ta const-decl "bool" enclaves nil) (rcv_init_req const-decl "bool" leader_transitions nil) (T2 const-decl "bool" enclaves nil) (rcv_key_ack const-decl "bool" leader_transitions nil) (T4 const-decl "bool" enclaves nil) (snd_admin const-decl "bool" leader_transitions nil) (T5 const-decl "bool" enclaves nil) (rcv_ack const-decl "bool" leader_transitions nil) (T7 const-decl "bool" enclaves nil) (rcv_close const-decl "bool" leader_transitions nil) (T9 const-decl "bool" enclaves nil) (Tl const-decl "bool" enclaves nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (key type-decl nil fields nil) (Ssk? adt-recognizer-decl "[key -> boolean]" fields nil) (unchanged_leader3 formula-decl nil enclaves nil) (unchanged_user1 formula-decl nil enclaves nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (Usr? adt-recognizer-decl "[agent -> boolean]" fields nil) (user type-eq-decl nil fields nil) (A0 const-decl "user" enclaves nil) (Q1 const-decl "bool" enclaves_abstraction nil) (unchanged_user2 formula-decl nil enclaves nil) (agent type-decl nil fields nil) (event type-decl nil events nil) (leader type-eq-decl nil leader_transitions nil) (set type-eq-decl nil sets nil) (usr type-eq-decl nil user_transitions nil) (global type-eq-decl nil enclaves nil) (unchanged_leader2 formula-decl nil enclaves nil) (T const-decl "bool" enclaves nil)) 18157 5000 t nil)) (tran_Q2 0 (tran_Q2-1 nil 3243342778 3243348289 ("" (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) untried ((replay1 formula-decl nil enclaves nil) (Ag const-decl "set[agent]" enclaves nil) (other_user1 formula-decl nil enclaves nil) (AuthKeyDist const-decl "event" enclaves_messages nil) (auth_key_dist const-decl "field" enclaves_messages nil) (AuthInitReq const-decl "event" enclaves_messages nil) (auth_init_req const-decl "field" enclaves_messages nil) (Q13 const-decl "bool" enclaves_abstraction nil) (Q3 const-decl "bool" enclaves_abstraction nil) (new_message formula-decl nil enclaves nil) (field type-decl nil fields nil) (Con? adt-recognizer-decl "[field -> boolean]" fields nil) (++ adt-constructor-decl "[[field, field] -> (Con?)]" fields nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (data type-eq-decl nil fields nil) (Data? adt-recognizer-decl "[field -> boolean]" fields nil) (Data adt-constructor-decl "[data -> (Data?)]" fields nil) (Encr? adt-recognizer-decl "[field -> boolean]" fields nil) (Encr adt-constructor-decl "[[key, field] -> (Encr?)]" fields nil) (Shr? adt-recognizer-decl "[key -> boolean]" fields nil) (Shr adt-constructor-decl "[agent -> (Shr?)]" fields nil) (Agent? adt-recognizer-decl "[field -> boolean]" fields nil) (Agent adt-constructor-decl "[agent -> (Agent?)]" fields nil) (Nonce? adt-recognizer-decl "[field -> boolean]" fields nil) (Nonce adt-constructor-decl "[nonce -> (Nonce?)]" fields nil) (Key? adt-recognizer-decl "[field -> boolean]" fields nil) (Key adt-constructor-decl "[key -> (Key?)]" fields nil) (Parts def-decl "set[field]" fields nil) (singleton const-decl "(singleton?)" sets nil) (member const-decl "bool" sets nil) (equal_nonce formula-decl nil fields nil) (equal_conc formula-decl nil fields nil) (equal_key formula-decl nil fields nil) (equal_encr formula-decl nil fields nil) (union const-decl "set" sets nil) (add const-decl "(nonempty?)" sets nil) (fresh_key1 formula-decl nil enclaves nil) (user_waiting_state formula-decl nil user_transitions nil) (auth_key_dist formula-decl nil enclaves nil) (Leader? adt-recognizer-decl "[agent -> boolean]" fields nil) (Leader adt-constructor-decl "(Leader?)" fields nil) (nonce type-decl nil fields nil) (init_req const-decl "bool" user_transitions nil) (T1 const-decl "bool" enclaves nil) (rcv_key const-decl "bool" user_transitions nil) (T3 const-decl "bool" enclaves nil) (rcv_admin const-decl "bool" user_transitions nil) (T6 const-decl "bool" enclaves nil) (leave const-decl "bool" user_transitions nil) (T8 const-decl "bool" enclaves nil) (Ta const-decl "bool" enclaves nil) (rcv_init_req const-decl "bool" leader_transitions nil) (T2 const-decl "bool" enclaves nil) (rcv_key_ack const-decl "bool" leader_transitions nil) (T4 const-decl "bool" enclaves nil) (snd_admin const-decl "bool" leader_transitions nil) (T5 const-decl "bool" enclaves nil) (rcv_ack const-decl "bool" leader_transitions nil) (T7 const-decl "bool" enclaves nil) (rcv_close const-decl "bool" leader_transitions nil) (T9 const-decl "bool" enclaves nil) (Tl const-decl "bool" enclaves nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (key type-decl nil fields nil) (Ssk? adt-recognizer-decl "[key -> boolean]" fields nil) (unchanged_user1 formula-decl nil enclaves nil) (unchanged_leader3 formula-decl nil enclaves nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (Usr? adt-recognizer-decl "[agent -> boolean]" fields nil) (user type-eq-decl nil fields nil) (A0 const-decl "user" enclaves nil) (unchanged_leader2 formula-decl nil enclaves nil) (unchanged_user2 formula-decl nil enclaves nil) (agent type-decl nil fields nil) (event type-decl nil events nil) (leader type-eq-decl nil leader_transitions nil) (set type-eq-decl nil sets nil) (usr type-eq-decl nil user_transitions nil) (global type-eq-decl nil enclaves nil) (Q2 const-decl "bool" enclaves_abstraction nil) (T const-decl "bool" enclaves nil)) 31738 10220 t nil)) (tran_Q3 0 (tran_Q3-1 nil 3243342778 3243348303 ("" (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) untried ((replay2 formula-decl nil enclaves nil) nil nil (Ag const-decl "set[agent]" enclaves nil) (replay1 formula-decl nil enclaves nil) (Key adt-constructor-decl "[key -> (Key?)]" fields nil) (Key? adt-recognizer-decl "[field -> boolean]" fields nil) (other_user1 formula-decl nil enclaves nil) (other_user4 formula-decl nil enclaves nil) (other_user3 formula-decl nil enclaves nil) (auth_ack_key formula-decl nil enclaves nil) (leader_waiting_state1 formula-decl nil leader_transitions nil) (user_waiting_state formula-decl nil user_transitions nil) (AuthAckKey const-decl "event" enclaves_messages nil) (auth_ack_key const-decl "field" enclaves_messages nil) (AuthKeyDist const-decl "event" enclaves_messages nil) (auth_key_dist const-decl "field" enclaves_messages nil) (fresh_nonce2 formula-decl nil enclaves nil) (equal_agent formula-decl nil fields nil) (Parts def-decl "set[field]" fields nil) (singleton const-decl "(singleton?)" sets nil) (member const-decl "bool" sets nil) (equal_nonce formula-decl nil fields nil) (equal_conc formula-decl nil fields nil) (equal_encr formula-decl nil fields nil) (union const-decl "set" sets nil) (add const-decl "(nonempty?)" sets nil) (Nonce adt-constructor-decl "[nonce -> (Nonce?)]" fields nil) (Nonce? adt-recognizer-decl "[field -> boolean]" fields nil) (Agent adt-constructor-decl "[agent -> (Agent?)]" fields nil) (Agent? adt-recognizer-decl "[field -> boolean]" fields nil) (Encr adt-constructor-decl "[[key, field] -> (Encr?)]" fields nil) (Encr? adt-recognizer-decl "[field -> boolean]" fields nil) (Data adt-constructor-decl "[data -> (Data?)]" fields nil) (Data? adt-recognizer-decl "[field -> boolean]" fields nil) (data type-eq-decl nil fields nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (++ adt-constructor-decl "[[field, field] -> (Con?)]" fields nil) (Con? adt-recognizer-decl "[field -> boolean]" fields nil) (field type-decl nil fields nil) (new_message formula-decl nil enclaves nil) (Q4 const-decl "bool" enclaves_abstraction nil) (auth_key_dist formula-decl nil enclaves nil) (Leader? adt-recognizer-decl "[agent -> boolean]" fields nil) (Leader adt-constructor-decl "(Leader?)" fields nil) (nonce type-decl nil fields nil) (init_req const-decl "bool" user_transitions nil) (T1 const-decl "bool" enclaves nil) (rcv_key const-decl "bool" user_transitions nil) (T3 const-decl "bool" enclaves nil) (rcv_admin const-decl "bool" user_transitions nil) (T6 const-decl "bool" enclaves nil) (leave const-decl "bool" user_transitions nil) (T8 const-decl "bool" enclaves nil) (Ta const-decl "bool" enclaves nil) (rcv_init_req const-decl "bool" leader_transitions nil) (T2 const-decl "bool" enclaves nil) (rcv_key_ack const-decl "bool" leader_transitions nil) (T4 const-decl "bool" enclaves nil) (snd_admin const-decl "bool" leader_transitions nil) (T5 const-decl "bool" enclaves nil) (rcv_ack const-decl "bool" leader_transitions nil) (T7 const-decl "bool" enclaves nil) (rcv_close const-decl "bool" leader_transitions nil) (T9 const-decl "bool" enclaves nil) (Tl const-decl "bool" enclaves nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (key type-decl nil fields nil) (Ssk? adt-recognizer-decl "[key -> boolean]" fields nil) (unchanged_user1 formula-decl nil enclaves nil) (unchanged_leader3 formula-decl nil enclaves nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (Usr? adt-recognizer-decl "[agent -> boolean]" fields nil) (user type-eq-decl nil fields nil) (A0 const-decl "user" enclaves nil) (unchanged_leader2 formula-decl nil enclaves nil) (unchanged_user2 formula-decl nil enclaves nil) (agent type-decl nil fields nil) (event type-decl nil events nil) (leader type-eq-decl nil leader_transitions nil) (set type-eq-decl nil sets nil) (usr type-eq-decl nil user_transitions nil) (global type-eq-decl nil enclaves nil) (Q3 const-decl "bool" enclaves_abstraction nil) (T const-decl "bool" enclaves nil)) 7931 5660 nil nil)) (tran_Q4 0 (tran_Q4-1 nil 3243342778 3243349895 ("" (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" (replace*) (("2" (assert) nil 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) untried ((replay2 formula-decl nil enclaves nil) (Ag const-decl "set[agent]" enclaves nil) nil nil (other_user4 formula-decl nil enclaves nil) (other_user2 formula-decl nil enclaves nil) (other_user3 formula-decl nil enclaves nil) (leader_waiting_state1 formula-decl nil leader_transitions nil) (Q5 const-decl "bool" enclaves_abstraction nil) (field type-decl nil fields nil) (Encr? adt-recognizer-decl "[field -> boolean]" fields nil) (Encr adt-constructor-decl "[[key, field] -> (Encr?)]" fields nil) (Con? adt-recognizer-decl "[field -> boolean]" fields nil) (++ adt-constructor-decl "[[field, field] -> (Con?)]" fields nil) (Agent? adt-recognizer-decl "[field -> boolean]" fields nil) (Agent adt-constructor-decl "[agent -> (Agent?)]" fields nil) (Nonce? adt-recognizer-decl "[field -> boolean]" fields nil) (Nonce adt-constructor-decl "[nonce -> (Nonce?)]" fields nil) (no_message formula-decl nil enclaves nil) (auth_ack_key formula-decl nil enclaves nil) (Q9 const-decl "bool" enclaves_abstraction nil) (user_connected_state formula-decl nil user_transitions nil) (admin_msg formula-decl nil enclaves nil) (Leader? adt-recognizer-decl "[agent -> boolean]" fields nil) (Leader adt-constructor-decl "(Leader?)" fields nil) (nonce type-decl nil fields nil) (init_req const-decl "bool" user_transitions nil) (T1 const-decl "bool" enclaves nil) (rcv_key const-decl "bool" user_transitions nil) (T3 const-decl "bool" enclaves nil) (rcv_admin const-decl "bool" user_transitions nil) (T6 const-decl "bool" enclaves nil) (leave const-decl "bool" user_transitions nil) (T8 const-decl "bool" enclaves nil) (Ta const-decl "bool" enclaves nil) (rcv_init_req const-decl "bool" leader_transitions nil) (T2 const-decl "bool" enclaves nil) (rcv_key_ack const-decl "bool" leader_transitions nil) (T4 const-decl "bool" enclaves nil) (snd_admin const-decl "bool" leader_transitions nil) (T5 const-decl "bool" enclaves nil) (rcv_ack const-decl "bool" leader_transitions nil) (T7 const-decl "bool" enclaves nil) (rcv_close const-decl "bool" leader_transitions nil) (T9 const-decl "bool" enclaves nil) (Tl const-decl "bool" enclaves nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (key type-decl nil fields nil) (Ssk? adt-recognizer-decl "[key -> boolean]" fields nil) (unchanged_user1 formula-decl nil enclaves nil) (unchanged_leader3 formula-decl nil enclaves nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (Usr? adt-recognizer-decl "[agent -> boolean]" fields nil) (user type-eq-decl nil fields nil) (A0 const-decl "user" enclaves nil) (unchanged_leader2 formula-decl nil enclaves nil) (unchanged_user2 formula-decl nil enclaves nil) (agent type-decl nil fields nil) (event type-decl nil events nil) (leader type-eq-decl nil leader_transitions nil) (set type-eq-decl nil sets nil) (usr type-eq-decl nil user_transitions nil) (global type-eq-decl nil enclaves nil) (Q4 const-decl "bool" enclaves_abstraction nil) (T const-decl "bool" enclaves nil)) 131023 9760 t nil)) (tran_Q5 0 (tran_Q5-1 nil 3243342778 3243349945 ("" (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" (replace*) (("2" (assert) nil 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) untried (nil nil (Ag const-decl "set[agent]" enclaves nil) (replay2 formula-decl nil enclaves nil) (other_user3 formula-decl nil enclaves nil) (other_user2 formula-decl nil enclaves nil) (req_close formula-decl nil enclaves nil) (leader_connected_state formula-decl nil leader_transitions nil) (Q6 const-decl "bool" enclaves_abstraction nil) (new_message formula-decl nil enclaves nil) (field type-decl nil fields nil) (Con? adt-recognizer-decl "[field -> boolean]" fields nil) (++ adt-constructor-decl "[[field, field] -> (Con?)]" fields nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (data type-eq-decl nil fields nil) (Data? adt-recognizer-decl "[field -> boolean]" fields nil) (Data adt-constructor-decl "[data -> (Data?)]" fields nil) (Encr? adt-recognizer-decl "[field -> boolean]" fields nil) (Encr adt-constructor-decl "[[key, field] -> (Encr?)]" fields nil) (Agent? adt-recognizer-decl "[field -> boolean]" fields nil) (Agent adt-constructor-decl "[agent -> (Agent?)]" fields nil) (Nonce? adt-recognizer-decl "[field -> boolean]" fields nil) (Nonce adt-constructor-decl "[nonce -> (Nonce?)]" fields nil) (add const-decl "(nonempty?)" sets nil) (union const-decl "set" sets nil) (equal_encr formula-decl nil fields nil) (equal_conc formula-decl nil fields nil) (equal_nonce formula-decl nil fields nil) (member const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (Parts def-decl "set[field]" fields nil) (equal_agent formula-decl nil fields nil) (fresh_nonce2 formula-decl nil enclaves nil) (admin_msg const-decl "field" enclaves_messages nil) (AdminMsg const-decl "event" enclaves_messages nil) (Q10 const-decl "bool" enclaves_abstraction nil) (user_connected_state formula-decl nil user_transitions nil) (admin_msg formula-decl nil enclaves nil) (Leader? adt-recognizer-decl "[agent -> boolean]" fields nil) (Leader adt-constructor-decl "(Leader?)" fields nil) (nonce type-decl nil fields nil) (init_req const-decl "bool" user_transitions nil) (T1 const-decl "bool" enclaves nil) (rcv_key const-decl "bool" user_transitions nil) (T3 const-decl "bool" enclaves nil) (rcv_admin const-decl "bool" user_transitions nil) (T6 const-decl "bool" enclaves nil) (leave const-decl "bool" user_transitions nil) (T8 const-decl "bool" enclaves nil) (Ta const-decl "bool" enclaves nil) (rcv_init_req const-decl "bool" leader_transitions nil) (T2 const-decl "bool" enclaves nil) (rcv_key_ack const-decl "bool" leader_transitions nil) (T4 const-decl "bool" enclaves nil) (snd_admin const-decl "bool" leader_transitions nil) (T5 const-decl "bool" enclaves nil) (rcv_ack const-decl "bool" leader_transitions nil) (T7 const-decl "bool" enclaves nil) (rcv_close const-decl "bool" leader_transitions nil) (T9 const-decl "bool" enclaves nil) (Tl const-decl "bool" enclaves nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (key type-decl nil fields nil) (Ssk? adt-recognizer-decl "[key -> boolean]" fields nil) (unchanged_user1 formula-decl nil enclaves nil) (unchanged_leader3 formula-decl nil enclaves nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (Usr? adt-recognizer-decl "[agent -> boolean]" fields nil) (user type-eq-decl nil fields nil) (A0 const-decl "user" enclaves nil) (unchanged_leader2 formula-decl nil enclaves nil) (unchanged_user2 formula-decl nil enclaves nil) (agent type-decl nil fields nil) (event type-decl nil events nil) (leader type-eq-decl nil leader_transitions nil) (set type-eq-decl nil sets nil) (usr type-eq-decl nil user_transitions nil) (global type-eq-decl nil enclaves nil) (Q5 const-decl "bool" enclaves_abstraction nil) (T const-decl "bool" enclaves nil)) 39288 8710 t nil)) (tran_Q6 0 (tran_Q6-1 nil 3243342778 3243348319 ("" (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) untried ((replay2 formula-decl nil enclaves nil) (Ag const-decl "set[agent]" enclaves nil) nil nil (other_user2 formula-decl nil enclaves nil) (other_user4 formula-decl nil enclaves nil) (other_user3 formula-decl nil enclaves nil) (req_close formula-decl nil enclaves nil) (leader_waiting_state2 formula-decl nil leader_transitions nil) (ack_admin formula-decl nil enclaves nil) (Q11 const-decl "bool" enclaves_abstraction nil) (req_close const-decl "field" enclaves_messages nil) (ReqClose const-decl "event" enclaves_messages nil) (user_connected_state formula-decl nil user_transitions nil) (AckAdmin const-decl "event" enclaves_messages nil) (ack_admin const-decl "field" enclaves_messages nil) (AdminMsg const-decl "event" enclaves_messages nil) (admin_msg const-decl "field" enclaves_messages nil) (fresh_nonce2 formula-decl nil enclaves nil) (equal_agent formula-decl nil fields nil) (Parts def-decl "set[field]" fields nil) (singleton const-decl "(singleton?)" sets nil) (member const-decl "bool" sets nil) (equal_nonce formula-decl nil fields nil) (equal_conc formula-decl nil fields nil) (equal_encr formula-decl nil fields nil) (union const-decl "set" sets nil) (add const-decl "(nonempty?)" sets nil) (Nonce adt-constructor-decl "[nonce -> (Nonce?)]" fields nil) (Nonce? adt-recognizer-decl "[field -> boolean]" fields nil) (Agent adt-constructor-decl "[agent -> (Agent?)]" fields nil) (Agent? adt-recognizer-decl "[field -> boolean]" fields nil) (Encr adt-constructor-decl "[[key, field] -> (Encr?)]" fields nil) (Encr? adt-recognizer-decl "[field -> boolean]" fields nil) (Data adt-constructor-decl "[data -> (Data?)]" fields nil) (Data? adt-recognizer-decl "[field -> boolean]" fields nil) (data type-eq-decl nil fields nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (++ adt-constructor-decl "[[field, field] -> (Con?)]" fields nil) (Con? adt-recognizer-decl "[field -> boolean]" fields nil) (field type-decl nil fields nil) (new_message formula-decl nil enclaves nil) (Q7 const-decl "bool" enclaves_abstraction nil) (admin_msg formula-decl nil enclaves nil) (Leader? adt-recognizer-decl "[agent -> boolean]" fields nil) (Leader adt-constructor-decl "(Leader?)" fields nil) (nonce type-decl nil fields nil) (init_req const-decl "bool" user_transitions nil) (T1 const-decl "bool" enclaves nil) (rcv_key const-decl "bool" user_transitions nil) (T3 const-decl "bool" enclaves nil) (rcv_admin const-decl "bool" user_transitions nil) (T6 const-decl "bool" enclaves nil) (leave const-decl "bool" user_transitions nil) (T8 const-decl "bool" enclaves nil) (Ta const-decl "bool" enclaves nil) (rcv_init_req const-decl "bool" leader_transitions nil) (T2 const-decl "bool" enclaves nil) (rcv_key_ack const-decl "bool" leader_transitions nil) (T4 const-decl "bool" enclaves nil) (snd_admin const-decl "bool" leader_transitions nil) (T5 const-decl "bool" enclaves nil) (rcv_ack const-decl "bool" leader_transitions nil) (T7 const-decl "bool" enclaves nil) (rcv_close const-decl "bool" leader_transitions nil) (T9 const-decl "bool" enclaves nil) (Tl const-decl "bool" enclaves nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (key type-decl nil fields nil) (Ssk? adt-recognizer-decl "[key -> boolean]" fields nil) (unchanged_user1 formula-decl nil enclaves nil) (unchanged_leader3 formula-decl nil enclaves nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (Usr? adt-recognizer-decl "[agent -> boolean]" fields nil) (user type-eq-decl nil fields nil) (A0 const-decl "user" enclaves nil) (unchanged_leader2 formula-decl nil enclaves nil) (unchanged_user2 formula-decl nil enclaves nil) (agent type-decl nil fields nil) (event type-decl nil events nil) (leader type-eq-decl nil leader_transitions nil) (set type-eq-decl nil sets nil) (usr type-eq-decl nil user_transitions nil) (global type-eq-decl nil enclaves nil) (Q6 const-decl "bool" enclaves_abstraction nil) (T const-decl "bool" enclaves nil)) 6817 6480 nil nil)) (tran_Q7 0 (tran_Q7-1 nil 3243342778 3243349990 ("" (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" (replace*) (("2" (assert) nil 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) untried ((replay2 formula-decl nil enclaves nil) (Ag const-decl "set[agent]" enclaves nil) nil nil (other_user4 formula-decl nil enclaves nil) (other_user2 formula-decl nil enclaves nil) (other_user3 formula-decl nil enclaves nil) (req_close formula-decl nil enclaves nil) (leader_waiting_state2 formula-decl nil leader_transitions nil) (Q5 const-decl "bool" enclaves_abstraction nil) (field type-decl nil fields nil) (Encr? adt-recognizer-decl "[field -> boolean]" fields nil) (Encr adt-constructor-decl "[[key, field] -> (Encr?)]" fields nil) (Con? adt-recognizer-decl "[field -> boolean]" fields nil) (++ adt-constructor-decl "[[field, field] -> (Con?)]" fields nil) (Agent? adt-recognizer-decl "[field -> boolean]" fields nil) (Agent adt-constructor-decl "[agent -> (Agent?)]" fields nil) (Nonce? adt-recognizer-decl "[field -> boolean]" fields nil) (Nonce adt-constructor-decl "[nonce -> (Nonce?)]" fields nil) (no_message formula-decl nil enclaves nil) (ack_admin formula-decl nil enclaves nil) (Q8 const-decl "bool" enclaves_abstraction nil) (user_connected_state formula-decl nil user_transitions nil) (admin_msg formula-decl nil enclaves nil) (Leader? adt-recognizer-decl "[agent -> boolean]" fields nil) (Leader adt-constructor-decl "(Leader?)" fields nil) (nonce type-decl nil fields nil) (init_req const-decl "bool" user_transitions nil) (T1 const-decl "bool" enclaves nil) (rcv_key const-decl "bool" user_transitions nil) (T3 const-decl "bool" enclaves nil) (rcv_admin const-decl "bool" user_transitions nil) (T6 const-decl "bool" enclaves nil) (leave const-decl "bool" user_transitions nil) (T8 const-decl "bool" enclaves nil) (Ta const-decl "bool" enclaves nil) (rcv_init_req const-decl "bool" leader_transitions nil) (T2 const-decl "bool" enclaves nil) (rcv_key_ack const-decl "bool" leader_transitions nil) (T4 const-decl "bool" enclaves nil) (snd_admin const-decl "bool" leader_transitions nil) (T5 const-decl "bool" enclaves nil) (rcv_ack const-decl "bool" leader_transitions nil) (T7 const-decl "bool" enclaves nil) (rcv_close const-decl "bool" leader_transitions nil) (T9 const-decl "bool" enclaves nil) (Tl const-decl "bool" enclaves nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (key type-decl nil fields nil) (Ssk? adt-recognizer-decl "[key -> boolean]" fields nil) (unchanged_user1 formula-decl nil enclaves nil) (unchanged_leader3 formula-decl nil enclaves nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (Usr? adt-recognizer-decl "[agent -> boolean]" fields nil) (user type-eq-decl nil fields nil) (A0 const-decl "user" enclaves nil) (unchanged_leader2 formula-decl nil enclaves nil) (unchanged_user2 formula-decl nil enclaves nil) (agent type-decl nil fields nil) (event type-decl nil events nil) (leader type-eq-decl nil leader_transitions nil) (set type-eq-decl nil sets nil) (usr type-eq-decl nil user_transitions nil) (global type-eq-decl nil enclaves nil) (Q7 const-decl "bool" enclaves_abstraction nil) (T const-decl "bool" enclaves nil)) 34877 8400 t nil)) (tran_Q8 0 (tran_Q8-2 nil 3243350009 3243350056 ("" (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" (replace*) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (expand "Q1") (("3" (replace*) (("3" (assert) nil nil)) nil)) nil) ("4" (inst?) (("4" (ground) nil nil)) nil) ("5" (inst?) (("5" (ground) nil nil)) nil)) nil) untried ((T const-decl "bool" enclaves nil) (Q8 const-decl "bool" enclaves_abstraction nil) (global type-eq-decl nil enclaves nil) (usr type-eq-decl nil user_transitions nil) (set type-eq-decl nil sets nil) (leader type-eq-decl nil leader_transitions nil) (event type-decl nil events nil) (agent type-decl nil fields nil) (unchanged_user2 formula-decl nil enclaves nil) (unchanged_leader2 formula-decl nil enclaves nil) (A0 const-decl "user" enclaves nil) (user type-eq-decl nil fields nil) (Usr? adt-recognizer-decl "[agent -> boolean]" fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (unchanged_leader3 formula-decl nil enclaves nil) (unchanged_user1 formula-decl nil enclaves nil) (Ssk? adt-recognizer-decl "[key -> boolean]" fields nil) (key type-decl nil fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (Tl const-decl "bool" enclaves nil) (T9 const-decl "bool" enclaves nil) (rcv_close const-decl "bool" leader_transitions nil) (T7 const-decl "bool" enclaves nil) (rcv_ack const-decl "bool" leader_transitions nil) (T5 const-decl "bool" enclaves nil) (snd_admin const-decl "bool" leader_transitions nil) (T4 const-decl "bool" enclaves nil) (rcv_key_ack const-decl "bool" leader_transitions nil) (T2 const-decl "bool" enclaves nil) (rcv_init_req const-decl "bool" leader_transitions nil) (Ta const-decl "bool" enclaves nil) (T8 const-decl "bool" enclaves nil) (leave const-decl "bool" user_transitions nil) (T6 const-decl "bool" enclaves nil) (rcv_admin const-decl "bool" user_transitions nil) (T3 const-decl "bool" enclaves nil) (rcv_key const-decl "bool" user_transitions nil) (T1 const-decl "bool" enclaves nil) (init_req const-decl "bool" user_transitions nil) (Q14 const-decl "bool" enclaves_abstraction nil) (new_message formula-decl nil enclaves nil) (Leader? adt-recognizer-decl "[agent -> boolean]" fields nil) (Leader adt-constructor-decl "(Leader?)" fields nil) (field type-decl nil fields nil) (Con? adt-recognizer-decl "[field -> boolean]" fields nil) (++ adt-constructor-decl "[[field, field] -> (Con?)]" fields nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (data type-eq-decl nil fields nil) (Data? adt-recognizer-decl "[field -> boolean]" fields nil) (Data adt-constructor-decl "[data -> (Data?)]" fields nil) (Encr? adt-recognizer-decl "[field -> boolean]" fields nil) (Encr adt-constructor-decl "[[key, field] -> (Encr?)]" fields nil) (Shr? adt-recognizer-decl "[key -> boolean]" fields nil) (Shr adt-constructor-decl "[agent -> (Shr?)]" fields nil) (Agent? adt-recognizer-decl "[field -> boolean]" fields nil) (Agent adt-constructor-decl "[agent -> (Agent?)]" fields nil) (Nonce? adt-recognizer-decl "[field -> boolean]" fields nil) (Nonce adt-constructor-decl "[nonce -> (Nonce?)]" fields nil) (Key? adt-recognizer-decl "[field -> boolean]" fields nil) (Key adt-constructor-decl "[key -> (Key?)]" fields nil) (Parts def-decl "set[field]" fields nil) (singleton const-decl "(singleton?)" sets nil) (member const-decl "bool" sets nil) (equal_conc formula-decl nil fields nil) (equal_encr formula-decl nil fields nil) (union const-decl "set" sets nil) (add const-decl "(nonempty?)" sets nil) (fresh_nonce3 formula-decl nil enclaves nil) (nonce type-decl nil fields nil) (auth_init_req const-decl "field" enclaves_messages nil) (AuthInitReq const-decl "event" enclaves_messages nil) (leader_waiting_state2 formula-decl nil leader_transitions nil) (Q10 const-decl "bool" enclaves_abstraction nil) (Q1 const-decl "bool" enclaves_abstraction nil)) 45312 4070 t nil) (tran_Q8-1 nil 3243342778 3243348328 ("" (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) unfinished nil 4293 2670 nil nil)) (tran_Q9 0 (tran_Q9-2 nil 3243350070 3243350080 ("" (origin "Q9") (("1" (message-rewrites) (("1" (expand "Q15") (("1" (new-message) nil nil)) nil)) nil) ("2" (expand "Q10") (("2" (inst?) (("2" (replace*) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (inst?) (("3" (assert) nil nil)) nil) ("4" (inst?) (("4" (assert) nil nil)) nil)) nil) untried ((T const-decl "bool" enclaves nil) (Q9 const-decl "bool" enclaves_abstraction nil) (global type-eq-decl nil enclaves nil) (usr type-eq-decl nil user_transitions nil) (set type-eq-decl nil sets nil) (leader type-eq-decl nil leader_transitions nil) (event type-decl nil events nil) (agent type-decl nil fields nil) (unchanged_user2 formula-decl nil enclaves nil) (unchanged_leader2 formula-decl nil enclaves nil) (A0 const-decl "user" enclaves nil) (user type-eq-decl nil fields nil) (Usr? adt-recognizer-decl "[agent -> boolean]" fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (unchanged_leader3 formula-decl nil enclaves nil) (unchanged_user1 formula-decl nil enclaves nil) (Ssk? adt-recognizer-decl "[key -> boolean]" fields nil) (key type-decl nil fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (Tl const-decl "bool" enclaves nil) (T9 const-decl "bool" enclaves nil) (rcv_close const-decl "bool" leader_transitions nil) (T7 const-decl "bool" enclaves nil) (rcv_ack const-decl "bool" leader_transitions nil) (T5 const-decl "bool" enclaves nil) (snd_admin const-decl "bool" leader_transitions nil) (T4 const-decl "bool" enclaves nil) (rcv_key_ack const-decl "bool" leader_transitions nil) (T2 const-decl "bool" enclaves nil) (rcv_init_req const-decl "bool" leader_transitions nil) (Ta const-decl "bool" enclaves nil) (T8 const-decl "bool" enclaves nil) (leave const-decl "bool" user_transitions nil) (T6 const-decl "bool" enclaves nil) (rcv_admin const-decl "bool" user_transitions nil) (T3 const-decl "bool" enclaves nil) (rcv_key const-decl "bool" user_transitions nil) (T1 const-decl "bool" enclaves nil) (init_req const-decl "bool" user_transitions nil) (Q15 const-decl "bool" enclaves_abstraction nil) (new_message formula-decl nil enclaves nil) (Leader? adt-recognizer-decl "[agent -> boolean]" fields nil) (Leader adt-constructor-decl "(Leader?)" fields nil) (field type-decl nil fields nil) (Con? adt-recognizer-decl "[field -> boolean]" fields nil) (++ adt-constructor-decl "[[field, field] -> (Con?)]" fields nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (data type-eq-decl nil fields nil) (Data? adt-recognizer-decl "[field -> boolean]" fields nil) (Data adt-constructor-decl "[data -> (Data?)]" fields nil) (Encr? adt-recognizer-decl "[field -> boolean]" fields nil) (Encr adt-constructor-decl "[[key, field] -> (Encr?)]" fields nil) (Shr? adt-recognizer-decl "[key -> boolean]" fields nil) (Shr adt-constructor-decl "[agent -> (Shr?)]" fields nil) (Agent? adt-recognizer-decl "[field -> boolean]" fields nil) (Agent adt-constructor-decl "[agent -> (Agent?)]" fields nil) (Nonce? adt-recognizer-decl "[field -> boolean]" fields nil) (Nonce adt-constructor-decl "[nonce -> (Nonce?)]" fields nil) (Key? adt-recognizer-decl "[field -> boolean]" fields nil) (Key adt-constructor-decl "[key -> (Key?)]" fields nil) (Parts def-decl "set[field]" fields nil) (singleton const-decl "(singleton?)" sets nil) (member const-decl "bool" sets nil) (equal_conc formula-decl nil fields nil) (equal_encr formula-decl nil fields nil) (union const-decl "set" sets nil) (add const-decl "(nonempty?)" sets nil) (fresh_nonce3 formula-decl nil enclaves nil) (nonce type-decl nil fields nil) (auth_init_req const-decl "field" enclaves_messages nil) (AuthInitReq const-decl "event" enclaves_messages nil) (leader_waiting_state1 formula-decl nil leader_transitions nil) (Q10 const-decl "bool" enclaves_abstraction nil)) 9327 2710 t nil) (tran_Q9-1 nil 3243342778 3243348330 ("" (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) unfinished nil 2769 2560 nil nil)) (tran_Q10 0 (tran_Q10-1 nil 3243342778 3243350122 ("" (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" (replace*) (("3" (assert) nil nil)) nil)) nil) ("4" (inst?) (("4" (assert) nil nil)) nil) ("5" (inst?) (("5" (assert) nil nil)) nil)) nil) untried ((Q1 const-decl "bool" enclaves_abstraction nil) (leader_connected_state formula-decl nil leader_transitions nil) (Q11 const-decl "bool" enclaves_abstraction nil) (fresh_nonce2 formula-decl nil enclaves nil) (equal_nonce formula-decl nil fields nil) (equal_agent formula-decl nil fields nil) (admin_msg const-decl "field" enclaves_messages nil) (AdminMsg const-decl "event" enclaves_messages nil) (AuthInitReq const-decl "event" enclaves_messages nil) (auth_init_req const-decl "field" enclaves_messages nil) (nonce type-decl nil fields nil) (fresh_nonce3 formula-decl nil enclaves nil) (add const-decl "(nonempty?)" sets nil) (union const-decl "set" sets nil) (equal_encr formula-decl nil fields nil) (equal_conc formula-decl nil fields nil) (member const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (Parts def-decl "set[field]" fields nil) (Key adt-constructor-decl "[key -> (Key?)]" fields nil) (Key? adt-recognizer-decl "[field -> boolean]" fields nil) (Nonce adt-constructor-decl "[nonce -> (Nonce?)]" fields nil) (Nonce? adt-recognizer-decl "[field -> boolean]" fields nil) (Agent adt-constructor-decl "[agent -> (Agent?)]" fields nil) (Agent? adt-recognizer-decl "[field -> boolean]" fields nil) (Shr adt-constructor-decl "[agent -> (Shr?)]" fields nil) (Shr? adt-recognizer-decl "[key -> boolean]" fields nil) (Encr adt-constructor-decl "[[key, field] -> (Encr?)]" fields nil) (Encr? adt-recognizer-decl "[field -> boolean]" fields nil) (Data adt-constructor-decl "[data -> (Data?)]" fields nil) (Data? adt-recognizer-decl "[field -> boolean]" fields nil) (data type-eq-decl nil fields nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (++ adt-constructor-decl "[[field, field] -> (Con?)]" fields nil) (Con? adt-recognizer-decl "[field -> boolean]" fields nil) (field type-decl nil fields nil) (Leader adt-constructor-decl "(Leader?)" fields nil) (Leader? adt-recognizer-decl "[agent -> boolean]" fields nil) (new_message formula-decl nil enclaves nil) (Q16 const-decl "bool" enclaves_abstraction nil) (init_req const-decl "bool" user_transitions nil) (T1 const-decl "bool" enclaves nil) (rcv_key const-decl "bool" user_transitions nil) (T3 const-decl "bool" enclaves nil) (rcv_admin const-decl "bool" user_transitions nil) (T6 const-decl "bool" enclaves nil) (leave const-decl "bool" user_transitions nil) (T8 const-decl "bool" enclaves nil) (Ta const-decl "bool" enclaves nil) (rcv_init_req const-decl "bool" leader_transitions nil) (T2 const-decl "bool" enclaves nil) (rcv_key_ack const-decl "bool" leader_transitions nil) (T4 const-decl "bool" enclaves nil) (snd_admin const-decl "bool" leader_transitions nil) (T5 const-decl "bool" enclaves nil) (rcv_ack const-decl "bool" leader_transitions nil) (T7 const-decl "bool" enclaves nil) (rcv_close const-decl "bool" leader_transitions nil) (T9 const-decl "bool" enclaves nil) (Tl const-decl "bool" enclaves nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (key type-decl nil fields nil) (Ssk? adt-recognizer-decl "[key -> boolean]" fields nil) (unchanged_user1 formula-decl nil enclaves nil) (unchanged_leader3 formula-decl nil enclaves nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (Usr? adt-recognizer-decl "[agent -> boolean]" fields nil) (user type-eq-decl nil fields nil) (A0 const-decl "user" enclaves nil) (unchanged_leader2 formula-decl nil enclaves nil) (unchanged_user2 formula-decl nil enclaves nil) (agent type-decl nil fields nil) (event type-decl nil events nil) (leader type-eq-decl nil leader_transitions nil) (set type-eq-decl nil sets nil) (usr type-eq-decl nil user_transitions nil) (global type-eq-decl nil enclaves nil) (Q10 const-decl "bool" enclaves_abstraction nil) (T const-decl "bool" enclaves nil)) 28206 6960 t nil)) (tran_Q11 0 (tran_Q11-2 nil 3243350156 3243350167 ("" (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" (replace*) (("3" (assert) nil nil)) nil)) nil) ("4" (other-user) nil nil) ("5" (replay) nil nil)) nil) untried ((T const-decl "bool" enclaves nil) (Q11 const-decl "bool" enclaves_abstraction nil) (global type-eq-decl nil enclaves nil) (usr type-eq-decl nil user_transitions nil) (set type-eq-decl nil sets nil) (leader type-eq-decl nil leader_transitions nil) (event type-decl nil events nil) (agent type-decl nil fields nil) (unchanged_user2 formula-decl nil enclaves nil) (unchanged_leader2 formula-decl nil enclaves nil) (A0 const-decl "user" enclaves nil) (user type-eq-decl nil fields nil) (Usr? adt-recognizer-decl "[agent -> boolean]" fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (unchanged_leader3 formula-decl nil enclaves nil) (unchanged_user1 formula-decl nil enclaves nil) (Ssk? adt-recognizer-decl "[key -> boolean]" fields nil) (key type-decl nil fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (Tl const-decl "bool" enclaves nil) (T9 const-decl "bool" enclaves nil) (rcv_close const-decl "bool" leader_transitions nil) (T7 const-decl "bool" enclaves nil) (rcv_ack const-decl "bool" leader_transitions nil) (T5 const-decl "bool" enclaves nil) (snd_admin const-decl "bool" leader_transitions nil) (T4 const-decl "bool" enclaves nil) (rcv_key_ack const-decl "bool" leader_transitions nil) (T2 const-decl "bool" enclaves nil) (rcv_init_req const-decl "bool" leader_transitions nil) (Ta const-decl "bool" enclaves nil) (T8 const-decl "bool" enclaves nil) (leave const-decl "bool" user_transitions nil) (T6 const-decl "bool" enclaves nil) (rcv_admin const-decl "bool" user_transitions nil) (T3 const-decl "bool" enclaves nil) (rcv_key const-decl "bool" user_transitions nil) (T1 const-decl "bool" enclaves nil) (init_req const-decl "bool" user_transitions nil) (Q17 const-decl "bool" enclaves_abstraction nil) (new_message formula-decl nil enclaves nil) (Leader? adt-recognizer-decl "[agent -> boolean]" fields nil) (Leader adt-constructor-decl "(Leader?)" fields nil) (field type-decl nil fields nil) (Con? adt-recognizer-decl "[field -> boolean]" fields nil) (++ adt-constructor-decl "[[field, field] -> (Con?)]" fields nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (data type-eq-decl nil fields nil) (Data? adt-recognizer-decl "[field -> boolean]" fields nil) (Data adt-constructor-decl "[data -> (Data?)]" fields nil) (Encr? adt-recognizer-decl "[field -> boolean]" fields nil) (Encr adt-constructor-decl "[[key, field] -> (Encr?)]" fields nil) (Shr? adt-recognizer-decl "[key -> boolean]" fields nil) (Shr adt-constructor-decl "[agent -> (Shr?)]" fields nil) (Agent? adt-recognizer-decl "[field -> boolean]" fields nil) (Agent adt-constructor-decl "[agent -> (Agent?)]" fields nil) (Nonce? adt-recognizer-decl "[field -> boolean]" fields nil) (Nonce adt-constructor-decl "[nonce -> (Nonce?)]" fields nil) (add const-decl "(nonempty?)" sets nil) (union const-decl "set" sets nil) (equal_encr formula-decl nil fields nil) (equal_nonce formula-decl nil fields nil) (equal_conc formula-decl nil fields nil) (member const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (Parts def-decl "set[field]" fields nil) (Key? adt-recognizer-decl "[field -> boolean]" fields nil) (Key adt-constructor-decl "[key -> (Key?)]" fields nil) (fresh_nonce3 formula-decl nil enclaves nil) (nonce type-decl nil fields nil) (auth_init_req const-decl "field" enclaves_messages nil) (AuthInitReq const-decl "event" enclaves_messages nil) (ack_admin formula-decl nil enclaves nil) (leader_waiting_state2 formula-decl nil leader_transitions nil) (Q1 const-decl "bool" enclaves_abstraction nil) (other_user4 formula-decl nil enclaves nil) (replay2 formula-decl nil enclaves nil) (Ag const-decl "set[agent]" enclaves nil) nil nil) 8785 3970 nil nil) (tran_Q11-1 nil 3243342778 3243348338 ("" (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) unfinished nil 3781 3480 nil nil)) (tran_Q12 0 (tran_Q12-1 nil 3243342778 3243348342 ("" (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) untried (nil nil (Ag const-decl "set[agent]" enclaves nil) (replay2 formula-decl nil enclaves nil) (other_user4 formula-decl nil enclaves nil) (leader_waiting_state1 formula-decl nil leader_transitions nil) (auth_ack_key formula-decl nil enclaves nil) (AuthInitReq const-decl "event" enclaves_messages nil) (auth_init_req const-decl "field" enclaves_messages nil) (nonce type-decl nil fields nil) (fresh_nonce3 formula-decl nil enclaves nil) (Key adt-constructor-decl "[key -> (Key?)]" fields nil) (Key? adt-recognizer-decl "[field -> boolean]" fields nil) (Parts def-decl "set[field]" fields nil) (singleton const-decl "(singleton?)" sets nil) (member const-decl "bool" sets nil) (equal_conc formula-decl nil fields nil) (equal_nonce formula-decl nil fields nil) (equal_encr formula-decl nil fields nil) (union const-decl "set" sets nil) (add const-decl "(nonempty?)" sets nil) (Nonce adt-constructor-decl "[nonce -> (Nonce?)]" fields nil) (Nonce? adt-recognizer-decl "[field -> boolean]" fields nil) (Agent adt-constructor-decl "[agent -> (Agent?)]" fields nil) (Agent? adt-recognizer-decl "[field -> boolean]" fields nil) (Shr adt-constructor-decl "[agent -> (Shr?)]" fields nil) (Shr? adt-recognizer-decl "[key -> boolean]" fields nil) (Encr adt-constructor-decl "[[key, field] -> (Encr?)]" fields nil) (Encr? adt-recognizer-decl "[field -> boolean]" fields nil) (Data adt-constructor-decl "[data -> (Data?)]" fields nil) (Data? adt-recognizer-decl "[field -> boolean]" fields nil) (data type-eq-decl nil fields nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (++ adt-constructor-decl "[[field, field] -> (Con?)]" fields nil) (Con? adt-recognizer-decl "[field -> boolean]" fields nil) (field type-decl nil fields nil) (Leader adt-constructor-decl "(Leader?)" fields nil) (Leader? adt-recognizer-decl "[agent -> boolean]" fields nil) (new_message formula-decl nil enclaves nil) (Q13 const-decl "bool" enclaves_abstraction nil) (init_req const-decl "bool" user_transitions nil) (T1 const-decl "bool" enclaves nil) (rcv_key const-decl "bool" user_transitions nil) (T3 const-decl "bool" enclaves nil) (rcv_admin const-decl "bool" user_transitions nil) (T6 const-decl "bool" enclaves nil) (leave const-decl "bool" user_transitions nil) (T8 const-decl "bool" enclaves nil) (Ta const-decl "bool" enclaves nil) (rcv_init_req const-decl "bool" leader_transitions nil) (T2 const-decl "bool" enclaves nil) (rcv_key_ack const-decl "bool" leader_transitions nil) (T4 const-decl "bool" enclaves nil) (snd_admin const-decl "bool" leader_transitions nil) (T5 const-decl "bool" enclaves nil) (rcv_ack const-decl "bool" leader_transitions nil) (T7 const-decl "bool" enclaves nil) (rcv_close const-decl "bool" leader_transitions nil) (T9 const-decl "bool" enclaves nil) (Tl const-decl "bool" enclaves nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (key type-decl nil fields nil) (Ssk? adt-recognizer-decl "[key -> boolean]" fields nil) (unchanged_user1 formula-decl nil enclaves nil) (unchanged_leader3 formula-decl nil enclaves nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (Usr? adt-recognizer-decl "[agent -> boolean]" fields nil) (user type-eq-decl nil fields nil) (A0 const-decl "user" enclaves nil) (unchanged_leader2 formula-decl nil enclaves nil) (unchanged_user2 formula-decl nil enclaves nil) (agent type-decl nil fields nil) (event type-decl nil events nil) (leader type-eq-decl nil leader_transitions nil) (set type-eq-decl nil sets nil) (usr type-eq-decl nil user_transitions nil) (global type-eq-decl nil enclaves nil) (Q12 const-decl "bool" enclaves_abstraction nil) (T const-decl "bool" enclaves nil)) 3610 3320 nil nil)) (tran_Q13 0 (tran_Q13-1 nil 3243342778 3243347009 ("" (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) untried ((replay1 formula-decl nil enclaves nil) (replay2 formula-decl nil enclaves nil) (Ag const-decl "set[agent]" enclaves nil) nil nil (Nonce adt-constructor-decl "[nonce -> (Nonce?)]" fields nil) (Nonce? adt-recognizer-decl "[field -> boolean]" fields nil) (field type-decl nil fields nil) (other_user4 formula-decl nil enclaves nil) (Key adt-constructor-decl "[key -> (Key?)]" fields nil) (Key? adt-recognizer-decl "[field -> boolean]" fields nil) (Agent adt-constructor-decl "[agent -> (Agent?)]" fields nil) (Agent? adt-recognizer-decl "[field -> boolean]" fields nil) (++ adt-constructor-decl "[[field, field] -> (Con?)]" fields nil) (Con? adt-recognizer-decl "[field -> boolean]" fields nil) (other_user1 formula-decl nil enclaves nil) (auth_ack_key formula-decl nil enclaves nil) (leader_waiting_state1 formula-decl nil leader_transitions nil) (nonce type-decl nil fields nil) (Leader adt-constructor-decl "(Leader?)" fields nil) (Leader? adt-recognizer-decl "[agent -> boolean]" fields nil) (auth_key_dist formula-decl nil enclaves nil) (user_waiting_state formula-decl nil user_transitions nil) (init_req const-decl "bool" user_transitions nil) (T1 const-decl "bool" enclaves nil) (rcv_key const-decl "bool" user_transitions nil) (T3 const-decl "bool" enclaves nil) (rcv_admin const-decl "bool" user_transitions nil) (T6 const-decl "bool" enclaves nil) (leave const-decl "bool" user_transitions nil) (T8 const-decl "bool" enclaves nil) (Ta const-decl "bool" enclaves nil) (rcv_init_req const-decl "bool" leader_transitions nil) (T2 const-decl "bool" enclaves nil) (rcv_key_ack const-decl "bool" leader_transitions nil) (T4 const-decl "bool" enclaves nil) (snd_admin const-decl "bool" leader_transitions nil) (T5 const-decl "bool" enclaves nil) (rcv_ack const-decl "bool" leader_transitions nil) (T7 const-decl "bool" enclaves nil) (rcv_close const-decl "bool" leader_transitions nil) (T9 const-decl "bool" enclaves nil) (Tl const-decl "bool" enclaves nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (key type-decl nil fields nil) (Ssk? adt-recognizer-decl "[key -> boolean]" fields nil) (unchanged_user1 formula-decl nil enclaves nil) (unchanged_leader3 formula-decl nil enclaves nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (Usr? adt-recognizer-decl "[agent -> boolean]" fields nil) (user type-eq-decl nil fields nil) (A0 const-decl "user" enclaves nil) (unchanged_leader2 formula-decl nil enclaves nil) (unchanged_user2 formula-decl nil enclaves nil) (agent type-decl nil fields nil) (event type-decl nil events nil) (leader type-eq-decl nil leader_transitions nil) (set type-eq-decl nil sets nil) (usr type-eq-decl nil user_transitions nil) (global type-eq-decl nil enclaves nil) (Q13 const-decl "bool" enclaves_abstraction nil) (T const-decl "bool" enclaves nil)) 3446 3190 nil nil)) (tran_Q14 0 (tran_Q14-1 nil 3243342778 3243348347 ("" (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) untried ((Ag const-decl "set[agent]" enclaves nil) (replay1 formula-decl nil enclaves nil) (other_user1 formula-decl nil enclaves nil) (Q2 const-decl "bool" enclaves_abstraction nil) (singleton const-decl "(singleton?)" sets nil) (Parts def-decl "set[field]" fields nil) (oops_event formula-decl nil enclaves nil) (req_close const-decl "field" enclaves_messages nil) (ReqClose const-decl "event" enclaves_messages nil) (leader_waiting_state2 formula-decl nil leader_transitions nil) (Q16 const-decl "bool" enclaves_abstraction nil) (no_message formula-decl nil enclaves nil) (Key adt-constructor-decl "[key -> (Key?)]" fields nil) (Key? adt-recognizer-decl "[field -> boolean]" fields nil) (Nonce adt-constructor-decl "[nonce -> (Nonce?)]" fields nil) (Nonce? adt-recognizer-decl "[field -> boolean]" fields nil) (Agent adt-constructor-decl "[agent -> (Agent?)]" fields nil) (Agent? adt-recognizer-decl "[field -> boolean]" fields nil) (++ adt-constructor-decl "[[field, field] -> (Con?)]" fields nil) (Con? adt-recognizer-decl "[field -> boolean]" fields nil) (Shr adt-constructor-decl "[agent -> (Shr?)]" fields nil) (Shr? adt-recognizer-decl "[key -> boolean]" fields nil) (Encr adt-constructor-decl "[[key, field] -> (Encr?)]" fields nil) (Encr? adt-recognizer-decl "[field -> boolean]" fields nil) (field type-decl nil fields nil) (ack_admin const-decl "field" enclaves_messages nil) (AckAdmin const-decl "event" enclaves_messages nil) (user_waiting_state formula-decl nil user_transitions nil) (auth_key_dist formula-decl nil enclaves nil) (Leader? adt-recognizer-decl "[agent -> boolean]" fields nil) (Leader adt-constructor-decl "(Leader?)" fields nil) (nonce type-decl nil fields nil) (init_req const-decl "bool" user_transitions nil) (T1 const-decl "bool" enclaves nil) (rcv_key const-decl "bool" user_transitions nil) (T3 const-decl "bool" enclaves nil) (rcv_admin const-decl "bool" user_transitions nil) (T6 const-decl "bool" enclaves nil) (leave const-decl "bool" user_transitions nil) (T8 const-decl "bool" enclaves nil) (Ta const-decl "bool" enclaves nil) (rcv_init_req const-decl "bool" leader_transitions nil) (T2 const-decl "bool" enclaves nil) (rcv_key_ack const-decl "bool" leader_transitions nil) (T4 const-decl "bool" enclaves nil) (snd_admin const-decl "bool" leader_transitions nil) (T5 const-decl "bool" enclaves nil) (rcv_ack const-decl "bool" leader_transitions nil) (T7 const-decl "bool" enclaves nil) (rcv_close const-decl "bool" leader_transitions nil) (T9 const-decl "bool" enclaves nil) (Tl const-decl "bool" enclaves nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (key type-decl nil fields nil) (Ssk? adt-recognizer-decl "[key -> boolean]" fields nil) (unchanged_user1 formula-decl nil enclaves nil) (unchanged_leader3 formula-decl nil enclaves nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (Usr? adt-recognizer-decl "[agent -> boolean]" fields nil) (user type-eq-decl nil fields nil) (A0 const-decl "user" enclaves nil) (unchanged_leader2 formula-decl nil enclaves nil) (unchanged_user2 formula-decl nil enclaves nil) (agent type-decl nil fields nil) (event type-decl nil events nil) (leader type-eq-decl nil leader_transitions nil) (set type-eq-decl nil sets nil) (usr type-eq-decl nil user_transitions nil) (global type-eq-decl nil enclaves nil) (Q14 const-decl "bool" enclaves_abstraction nil) (T const-decl "bool" enclaves nil)) 5508 3740 nil nil)) (tran_Q15 0 (tran_Q15-1 nil 3243342778 3243348350 ("" (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) untried ((Ag const-decl "set[agent]" enclaves nil) (replay1 formula-decl nil enclaves nil) (other_user1 formula-decl nil enclaves nil) (leader_waiting_state1 formula-decl nil leader_transitions nil) (Q16 const-decl "bool" enclaves_abstraction nil) (no_message formula-decl nil enclaves nil) (Key adt-constructor-decl "[key -> (Key?)]" fields nil) (Key? adt-recognizer-decl "[field -> boolean]" fields nil) (Nonce adt-constructor-decl "[nonce -> (Nonce?)]" fields nil) (Nonce? adt-recognizer-decl "[field -> boolean]" fields nil) (Agent adt-constructor-decl "[agent -> (Agent?)]" fields nil) (Agent? adt-recognizer-decl "[field -> boolean]" fields nil) (++ adt-constructor-decl "[[field, field] -> (Con?)]" fields nil) (Con? adt-recognizer-decl "[field -> boolean]" fields nil) (Shr adt-constructor-decl "[agent -> (Shr?)]" fields nil) (Shr? adt-recognizer-decl "[key -> boolean]" fields nil) (Encr adt-constructor-decl "[[key, field] -> (Encr?)]" fields nil) (Encr? adt-recognizer-decl "[field -> boolean]" fields nil) (field type-decl nil fields nil) (auth_ack_key const-decl "field" enclaves_messages nil) (AuthAckKey const-decl "event" enclaves_messages nil) (user_waiting_state formula-decl nil user_transitions nil) (auth_key_dist formula-decl nil enclaves nil) (Leader? adt-recognizer-decl "[agent -> boolean]" fields nil) (Leader adt-constructor-decl "(Leader?)" fields nil) (nonce type-decl nil fields nil) (init_req const-decl "bool" user_transitions nil) (T1 const-decl "bool" enclaves nil) (rcv_key const-decl "bool" user_transitions nil) (T3 const-decl "bool" enclaves nil) (rcv_admin const-decl "bool" user_transitions nil) (T6 const-decl "bool" enclaves nil) (leave const-decl "bool" user_transitions nil) (T8 const-decl "bool" enclaves nil) (Ta const-decl "bool" enclaves nil) (rcv_init_req const-decl "bool" leader_transitions nil) (T2 const-decl "bool" enclaves nil) (rcv_key_ack const-decl "bool" leader_transitions nil) (T4 const-decl "bool" enclaves nil) (snd_admin const-decl "bool" leader_transitions nil) (T5 const-decl "bool" enclaves nil) (rcv_ack const-decl "bool" leader_transitions nil) (T7 const-decl "bool" enclaves nil) (rcv_close const-decl "bool" leader_transitions nil) (T9 const-decl "bool" enclaves nil) (Tl const-decl "bool" enclaves nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (key type-decl nil fields nil) (Ssk? adt-recognizer-decl "[key -> boolean]" fields nil) (unchanged_user1 formula-decl nil enclaves nil) (unchanged_leader3 formula-decl nil enclaves nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (Usr? adt-recognizer-decl "[agent -> boolean]" fields nil) (user type-eq-decl nil fields nil) (A0 const-decl "user" enclaves nil) (unchanged_leader2 formula-decl nil enclaves nil) (unchanged_user2 formula-decl nil enclaves nil) (agent type-decl nil fields nil) (event type-decl nil events nil) (leader type-eq-decl nil leader_transitions nil) (set type-eq-decl nil sets nil) (usr type-eq-decl nil user_transitions nil) (global type-eq-decl nil enclaves nil) (Q15 const-decl "bool" enclaves_abstraction nil) (T const-decl "bool" enclaves nil)) 3285 3020 nil nil)) (tran_Q16 0 (tran_Q16-1 nil 3243342778 3243348355 ("" (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) untried ((Ag const-decl "set[agent]" enclaves nil) (replay1 formula-decl nil enclaves nil) (other_user1 formula-decl nil enclaves nil) (Q2 const-decl "bool" enclaves_abstraction nil) (oops_event formula-decl nil enclaves nil) (req_close const-decl "field" enclaves_messages nil) (ReqClose const-decl "event" enclaves_messages nil) (leader_connected_state formula-decl nil leader_transitions nil) (Q17 const-decl "bool" enclaves_abstraction nil) (new_message formula-decl nil enclaves nil) (field type-decl nil fields nil) (Con? adt-recognizer-decl "[field -> boolean]" fields nil) (++ adt-constructor-decl "[[field, field] -> (Con?)]" fields nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (data type-eq-decl nil fields nil) (Data? adt-recognizer-decl "[field -> boolean]" fields nil) (Data adt-constructor-decl "[data -> (Data?)]" fields nil) (Encr? adt-recognizer-decl "[field -> boolean]" fields nil) (Encr adt-constructor-decl "[[key, field] -> (Encr?)]" fields nil) (Agent? adt-recognizer-decl "[field -> boolean]" fields nil) (Agent adt-constructor-decl "[agent -> (Agent?)]" fields nil) (Nonce? adt-recognizer-decl "[field -> boolean]" fields nil) (Nonce adt-constructor-decl "[nonce -> (Nonce?)]" fields nil) (Parts def-decl "set[field]" fields nil) (singleton const-decl "(singleton?)" sets nil) (member const-decl "bool" sets nil) (equal_agent formula-decl nil fields nil) (equal_conc formula-decl nil fields nil) (equal_nonce formula-decl nil fields nil) (equal_encr formula-decl nil fields nil) (union const-decl "set" sets nil) (add const-decl "(nonempty?)" sets nil) (fresh_nonce2 formula-decl nil enclaves nil) (Shr? adt-recognizer-decl "[key -> boolean]" fields nil) (Shr adt-constructor-decl "[agent -> (Shr?)]" fields nil) (Key? adt-recognizer-decl "[field -> boolean]" fields nil) (Key adt-constructor-decl "[key -> (Key?)]" fields nil) (admin_msg const-decl "field" enclaves_messages nil) (AdminMsg const-decl "event" enclaves_messages nil) (user_waiting_state formula-decl nil user_transitions nil) (auth_key_dist formula-decl nil enclaves nil) (Leader? adt-recognizer-decl "[agent -> boolean]" fields nil) (Leader adt-constructor-decl "(Leader?)" fields nil) (nonce type-decl nil fields nil) (init_req const-decl "bool" user_transitions nil) (T1 const-decl "bool" enclaves nil) (rcv_key const-decl "bool" user_transitions nil) (T3 const-decl "bool" enclaves nil) (rcv_admin const-decl "bool" user_transitions nil) (T6 const-decl "bool" enclaves nil) (leave const-decl "bool" user_transitions nil) (T8 const-decl "bool" enclaves nil) (Ta const-decl "bool" enclaves nil) (rcv_init_req const-decl "bool" leader_transitions nil) (T2 const-decl "bool" enclaves nil) (rcv_key_ack const-decl "bool" leader_transitions nil) (T4 const-decl "bool" enclaves nil) (snd_admin const-decl "bool" leader_transitions nil) (T5 const-decl "bool" enclaves nil) (rcv_ack const-decl "bool" leader_transitions nil) (T7 const-decl "bool" enclaves nil) (rcv_close const-decl "bool" leader_transitions nil) (T9 const-decl "bool" enclaves nil) (Tl const-decl "bool" enclaves nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (key type-decl nil fields nil) (Ssk? adt-recognizer-decl "[key -> boolean]" fields nil) (unchanged_user1 formula-decl nil enclaves nil) (unchanged_leader3 formula-decl nil enclaves nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (Usr? adt-recognizer-decl "[agent -> boolean]" fields nil) (user type-eq-decl nil fields nil) (A0 const-decl "user" enclaves nil) (unchanged_leader2 formula-decl nil enclaves nil) (unchanged_user2 formula-decl nil enclaves nil) (agent type-decl nil fields nil) (event type-decl nil events nil) (leader type-eq-decl nil leader_transitions nil) (set type-eq-decl nil sets nil) (usr type-eq-decl nil user_transitions nil) (global type-eq-decl nil enclaves nil) (Q16 const-decl "bool" enclaves_abstraction nil) (T const-decl "bool" enclaves nil)) 4916 4630 nil nil)) (tran_Q17 0 (tran_Q17-1 nil 3243342778 3243348359 ("" (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) untried ((replay1 formula-decl nil enclaves nil) (replay2 formula-decl nil enclaves nil) (Ag const-decl "set[agent]" enclaves nil) nil nil (other_user4 formula-decl nil enclaves nil) (other_user1 formula-decl nil enclaves nil) (Q2 const-decl "bool" enclaves_abstraction nil) (Key adt-constructor-decl "[key -> (Key?)]" fields nil) (Key? adt-recognizer-decl "[field -> boolean]" fields nil) (field type-decl nil fields nil) (Encr? adt-recognizer-decl "[field -> boolean]" fields nil) (Encr adt-constructor-decl "[[key, field] -> (Encr?)]" fields nil) (Shr? adt-recognizer-decl "[key -> boolean]" fields nil) (Shr adt-constructor-decl "[agent -> (Shr?)]" fields nil) (Con? adt-recognizer-decl "[field -> boolean]" fields nil) (++ adt-constructor-decl "[[field, field] -> (Con?)]" fields nil) (Agent? adt-recognizer-decl "[field -> boolean]" fields nil) (Agent adt-constructor-decl "[agent -> (Agent?)]" fields nil) (Nonce? adt-recognizer-decl "[field -> boolean]" fields nil) (Nonce adt-constructor-decl "[nonce -> (Nonce?)]" fields nil) (singleton const-decl "(singleton?)" sets nil) (Parts def-decl "set[field]" fields nil) (oops_event formula-decl nil enclaves nil) (req_close const-decl "field" enclaves_messages nil) (ReqClose const-decl "event" enclaves_messages nil) (leader_waiting_state2 formula-decl nil leader_transitions nil) (ack_admin formula-decl nil enclaves nil) (user_waiting_state formula-decl nil user_transitions nil) (auth_key_dist formula-decl nil enclaves nil) (Leader? adt-recognizer-decl "[agent -> boolean]" fields nil) (Leader adt-constructor-decl "(Leader?)" fields nil) (nonce type-decl nil fields nil) (init_req const-decl "bool" user_transitions nil) (T1 const-decl "bool" enclaves nil) (rcv_key const-decl "bool" user_transitions nil) (T3 const-decl "bool" enclaves nil) (rcv_admin const-decl "bool" user_transitions nil) (T6 const-decl "bool" enclaves nil) (leave const-decl "bool" user_transitions nil) (T8 const-decl "bool" enclaves nil) (Ta const-decl "bool" enclaves nil) (rcv_init_req const-decl "bool" leader_transitions nil) (T2 const-decl "bool" enclaves nil) (rcv_key_ack const-decl "bool" leader_transitions nil) (T4 const-decl "bool" enclaves nil) (snd_admin const-decl "bool" leader_transitions nil) (T5 const-decl "bool" enclaves nil) (rcv_ack const-decl "bool" leader_transitions nil) (T7 const-decl "bool" enclaves nil) (rcv_close const-decl "bool" leader_transitions nil) (T9 const-decl "bool" enclaves nil) (Tl const-decl "bool" enclaves nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (key type-decl nil fields nil) (Ssk? adt-recognizer-decl "[key -> boolean]" fields nil) (unchanged_user1 formula-decl nil enclaves nil) (unchanged_leader3 formula-decl nil enclaves nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (Usr? adt-recognizer-decl "[agent -> boolean]" fields nil) (user type-eq-decl nil fields nil) (A0 const-decl "user" enclaves nil) (unchanged_leader2 formula-decl nil enclaves nil) (unchanged_user2 formula-decl nil enclaves nil) (agent type-decl nil fields nil) (event type-decl nil events nil) (leader type-eq-decl nil leader_transitions nil) (set type-eq-decl nil sets nil) (usr type-eq-decl nil user_transitions nil) (global type-eq-decl nil enclaves nil) (Q17 const-decl "bool" enclaves_abstraction nil) (T const-decl "bool" enclaves nil)) 4181 3890 nil nil)) (state_space 0 (state_space-1 nil 3243342778 3243347030 ("" (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) untried ((tran_Q17 formula-decl nil enclaves_abstraction nil) (tran_Q16 formula-decl nil enclaves_abstraction nil) (tran_Q15 formula-decl nil enclaves_abstraction nil) (tran_Q14 formula-decl nil enclaves_abstraction nil) (tran_Q13 formula-decl nil enclaves_abstraction nil) (tran_Q12 formula-decl nil enclaves_abstraction nil) (tran_Q11 formula-decl nil enclaves_abstraction nil) (tran_Q10 formula-decl nil enclaves_abstraction nil) (tran_Q9 formula-decl nil enclaves_abstraction nil) (tran_Q8 formula-decl nil enclaves_abstraction nil) (tran_Q7 formula-decl nil enclaves_abstraction nil) (tran_Q6 formula-decl nil enclaves_abstraction nil) (tran_Q5 formula-decl nil enclaves_abstraction nil) (tran_Q4 formula-decl nil enclaves_abstraction nil) (tran_Q3 formula-decl nil enclaves_abstraction nil) (tran_Q2 formula-decl nil enclaves_abstraction nil) (tran_Q1 formula-decl nil enclaves_abstraction nil) (init_leader const-decl "leader" leader_transitions nil) (init_usr const-decl "usr" user_transitions nil) (init const-decl "global" enclaves nil) (tr const-decl "set[event]" enclaves nil) (content const-decl "set[field]" events nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (field type-decl nil fields nil) (global type-eq-decl nil enclaves nil) (usr type-eq-decl nil user_transitions nil) (set type-eq-decl nil sets nil) (leader type-eq-decl nil leader_transitions nil) (event type-decl nil events nil) (T const-decl "bool" enclaves nil) (agent type-decl nil fields nil) (Q0 const-decl "bool" enclaves nil) (Q17 const-decl "bool" enclaves_abstraction nil) (Q16 const-decl "bool" enclaves_abstraction nil) (Q15 const-decl "bool" enclaves_abstraction nil) (Q14 const-decl "bool" enclaves_abstraction nil) (Q13 const-decl "bool" enclaves_abstraction nil) (Q12 const-decl "bool" enclaves_abstraction nil) (Q11 const-decl "bool" enclaves_abstraction nil) (Q10 const-decl "bool" enclaves_abstraction nil) (Q9 const-decl "bool" enclaves_abstraction nil) (Q8 const-decl "bool" enclaves_abstraction nil) (Q7 const-decl "bool" enclaves_abstraction nil) (Q6 const-decl "bool" enclaves_abstraction nil) (Q5 const-decl "bool" enclaves_abstraction nil) (Q4 const-decl "bool" enclaves_abstraction nil) (Q3 const-decl "bool" enclaves_abstraction nil) (Q2 const-decl "bool" enclaves_abstraction nil) (Q1 const-decl "bool" enclaves_abstraction nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (Reachable_induct3 formula-decl nil protocols nil)) 887 720 nil nil)) (session_key_prop 0 (session_key_prop-1 nil 3243342778 3243347031 ("" (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) untried ((state_space formula-decl nil enclaves_abstraction nil) (global type-eq-decl nil enclaves nil) (usr type-eq-decl nil user_transitions nil) (set type-eq-decl nil sets nil) (event type-decl nil events nil) (leader type-eq-decl nil leader_transitions nil) (user_connected_state formula-decl nil user_transitions nil) (leader_waiting_state1 formula-decl nil leader_transitions nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (key type-decl nil fields nil) (Ssk? adt-recognizer-decl "[key -> boolean]" fields nil) (leader_connected_state formula-decl nil leader_transitions nil) (leader_waiting_state2 formula-decl nil leader_transitions nil) nil nil (Q1 const-decl "bool" enclaves_abstraction nil) (Q2 const-decl "bool" enclaves_abstraction nil) (Q3 const-decl "bool" enclaves_abstraction nil) (Q4 const-decl "bool" enclaves_abstraction nil) (Q5 const-decl "bool" enclaves_abstraction nil) (Q6 const-decl "bool" enclaves_abstraction nil) (Q7 const-decl "bool" enclaves_abstraction nil) (Q8 const-decl "bool" enclaves_abstraction nil) (Q9 const-decl "bool" enclaves_abstraction nil) (Q10 const-decl "bool" enclaves_abstraction nil) (Q11 const-decl "bool" enclaves_abstraction nil) (Q12 const-decl "bool" enclaves_abstraction nil) (Q13 const-decl "bool" enclaves_abstraction nil) (Q14 const-decl "bool" enclaves_abstraction nil) (Q15 const-decl "bool" enclaves_abstraction nil) (Q16 const-decl "bool" enclaves_abstraction nil) (Q17 const-decl "bool" enclaves_abstraction nil)) 875 830 nil nil)) (connected_states 0 (connected_states-1 nil 3243342778 3243347031 ("" (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) untried ((state_space formula-decl nil enclaves_abstraction nil) (global type-eq-decl nil enclaves nil) (usr type-eq-decl nil user_transitions nil) (set type-eq-decl nil sets nil) (event type-decl nil events nil) (leader type-eq-decl nil leader_transitions nil) (Ssk? adt-recognizer-decl "[key -> boolean]" fields nil) (key type-decl nil fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (leader_connected_state formula-decl nil leader_transitions nil) (user_connected_state formula-decl nil user_transitions nil) (Q1 const-decl "bool" enclaves_abstraction nil) (Q2 const-decl "bool" enclaves_abstraction nil) (Q3 const-decl "bool" enclaves_abstraction nil) (Q4 const-decl "bool" enclaves_abstraction nil) (Q5 const-decl "bool" enclaves_abstraction nil) (Q6 const-decl "bool" enclaves_abstraction nil) (Q7 const-decl "bool" enclaves_abstraction nil) (Q8 const-decl "bool" enclaves_abstraction nil) (Q9 const-decl "bool" enclaves_abstraction nil) (Q10 const-decl "bool" enclaves_abstraction nil) (Q11 const-decl "bool" enclaves_abstraction nil) (Q12 const-decl "bool" enclaves_abstraction nil) (Q13 const-decl "bool" enclaves_abstraction nil) (Q14 const-decl "bool" enclaves_abstraction nil) (Q15 const-decl "bool" enclaves_abstraction nil) (Q16 const-decl "bool" enclaves_abstraction nil) (Q17 const-decl "bool" enclaves_abstraction nil)) 523 500 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 (Parts_weak_induction 0 (Parts_weak_induction-1 nil 3236722746 nil nil nil nil nil nil nil shostak)) (Parts_induction 0 (Parts_induction-1 nil 3236722746 nil nil nil nil nil nil nil shostak)) (Inj_parts 0 (Inj_parts-1 nil 3236722745 nil ("" (grind) (("" (expand "Parts") (("" (propax) nil nil)) nil)) nil) untried nil nil nil nil nil)) (Fst_parts 0 (Fst_parts-1 nil 3236722745 nil ("" (skosimp) (("" (expand "Parts" +) (("" (reduce) nil nil)) nil)) nil) untried nil nil nil nil nil)) (Snd_parts 0 (Snd_parts-1 nil 3236722745 nil ("" (skosimp) (("" (expand "Parts" +) (("" (reduce) nil nil)) nil)) nil) untried nil nil nil nil nil)) (Body_parts 0 (Body_parts-1 nil 3236722745 nil ("" (skosimp) (("" (expand "Parts" +) (("" (reduce) nil nil)) nil)) nil) untried nil nil nil nil nil)) (Parts_induct 0 (Parts_induct-1 nil 3236722745 nil ("" (skosimp) (("" (expand* "subset?" "member") (("" (rewrite "Parts_induction") (("" (delete 2) (("" (reduce) nil nil)) nil)) nil)) nil)) nil) untried nil nil nil nil nil)) (Parts_sub 0 (Parts_sub-1 nil 3236722745 nil ("" (skosimp*) (("" (expand "Parts") (("" (grind) nil nil)) nil)) nil) untried nil nil nil nil nil)) (Parts_emptyset 0 (Parts_emptyset-1 nil 3236722745 nil ("" (auto-rewrite "subset_emptyset" "emptyset") (("" (rewrite "subset_antisymmetric") (("" (rewrite "Parts_induct") nil nil)) nil)) nil) untried nil nil nil nil nil)) (Parts_subset 0 (Parts_subset-1 nil 3236722745 nil ("" (auto-rewrite "Inj_parts" "Fst_parts" "Snd_parts" "Body_parts") (("" (skosimp) (("" (rewrite "Parts_induct") (("" (delete 2) (("" (grind) nil nil)) nil)) nil)) nil)) nil) untried nil nil nil nil nil)) (Parts_union 0 (Parts_union-1 nil 3236722745 nil ("" (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) untried nil nil nil nil nil)) (Parts_atom 0 (Parts_atom-1 nil 3236722745 nil ("" (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) untried nil nil nil nil nil)) (Parts_member_aux 0 (Parts_member_aux-2 "removed inst!" 3236722791 3236722791 ("" (skolem + ("S!1" _)) (("" (induct-and-simplify "X" :if-match nil :rewrites ("Inj_parts")) (("1" (forward-chain -1) nil nil) ("2" (forward-chain -2) 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" (forward-chain -1) nil nil) ("10" (forward-chain "Body_parts") nil nil)) nil)) nil) proved nil 43762 10470 t shostak) (Parts_member_aux-1 nil 3236722745 nil ("" (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) proved ((field_induction formula-decl nil fields nil) (Parts def-decl "set[field]" fields nil) (subset? const-decl "bool" sets nil) (Parts inductive-decl "bool" basics nil) (set type-eq-decl nil sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (field type-decl nil fields nil) (singleton const-decl "(singleton?)" sets nil) (member const-decl "bool" sets nil) (add const-decl "(nonempty?)" sets nil) (union const-decl "set" sets nil) (Snd_parts formula-decl nil basics nil) (Fst_parts formula-decl nil basics nil) (Body_parts formula-decl nil basics nil) (key type-decl nil fields nil)) nil nil nil nil)) (Parts_member 0 (Parts_member-1 nil 3236722745 nil ("" (auto-rewrite "Parts_member_aux" "Inj_parts") (("" (skosimp) (("" (assert) nil nil)) nil)) nil) untried nil nil nil nil nil)) (Parts_equiv 0 (Parts_equiv-1 nil 3236722745 nil ("" (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) untried nil nil nil nil nil)) (Parts_singleton 0 (Parts_singleton-1 nil 3236722745 nil ("" (skolem!) (("" (expand "singleton") (("" (rewrite "Parts_equiv") (("" (apply-extensionality :hide? t) (("" (reduce) nil nil)) nil)) nil)) nil)) nil) untried nil nil nil nil nil)) (Parts_add 0 (Parts_add-1 nil 3236722745 nil ("" (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) untried nil nil nil nil nil)) (Visible_weak_induction 0 (Visible_weak_induction-1 nil 3236722746 nil nil nil nil nil nil nil shostak)) (Visible_induction 0 (Visible_induction-1 nil 3236722746 nil nil nil nil nil nil nil shostak)) (Inj_Visible 0 (Inj_Visible-1 nil 3236722745 nil ("" (skosimp) (("" (expand "Visible" +) (("" (reduce) nil nil)) nil)) nil) untried nil nil nil nil nil)) (Fst_Visible 0 (Fst_Visible-1 nil 3236722745 nil ("" (skosimp) (("" (expand "Visible" +) (("" (reduce) nil nil)) nil)) nil) untried nil nil nil nil nil)) (Snd_Visible 0 (Snd_Visible-1 nil 3236722745 nil ("" (skosimp) (("" (expand "Visible" +) (("" (reduce) nil nil)) nil)) nil) untried nil nil nil nil nil)) (Visible_induct 0 (Visible_induct-1 nil 3236722745 nil ("" (skosimp) (("" (expand* "subset?" "member") (("" (rewrite "Visible_weak_induction") (("" (reduce) nil nil)) nil)) nil)) nil) untried nil nil nil nil nil)) (Visible_sub 0 (Visible_sub-1 nil 3236722745 nil ("" (grind :rewrites ("Inj_Visible")) nil nil) untried nil nil nil nil nil)) (Visible_emptyset 0 (Visible_emptyset-1 nil 3236722745 nil ("" (use "Visible_induct" ("P" "emptyset[field]")) (("" (auto-rewrite "subset?" "member" "emptyset") (("" (reduce) (("" (apply-extensionality :hide? t) (("" (inst?) nil nil)) nil)) nil)) nil)) nil) untried nil nil nil nil nil)) (Visible_subset 0 (Visible_subset-1 nil 3236722745 nil ("" (auto-rewrite "Inj_Visible" "Fst_Visible" "Snd_Visible") (("" (skosimp) (("" (rewrite "Visible_induct") (("" (delete 2) (("" (grind) nil nil)) nil)) nil)) nil)) nil) untried nil nil nil nil nil)) (Visible_union 0 (Visible_union-1 nil 3236722745 nil ("" (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) untried nil nil nil nil nil)) (Visible_atom 0 (Visible_atom-1 nil 3236722745 nil ("" (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) untried nil nil nil nil nil)) (Visible_member_aux 0 (Visible_member_aux-1 nil 3236722745 nil ("" (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) untried nil nil nil nil nil)) (Visible_member 0 (Visible_member-1 nil 3236722745 nil ("" (auto-rewrite "Visible_member_aux" "Inj_Visible") (("" (skosimp) (("" (assert) nil nil)) nil)) nil) untried nil nil nil nil nil)) (Visible_equiv 0 (Visible_equiv-1 nil 3236722745 nil ("" (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) untried nil nil nil nil nil)) (Visible_singleton 0 (Visible_singleton-1 nil 3236722745 nil ("" (skolem!) (("" (expand "singleton") (("" (rewrite "Visible_equiv") (("" (apply-extensionality :hide? t) (("" (reduce) nil nil)) nil)) nil)) nil)) nil) untried nil nil nil nil nil)) (Visible_add 0 (Visible_add-1 nil 3236722745 nil ("" (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) untried nil nil nil nil nil)) (Analz_weak_induction 0 (Analz_weak_induction-1 nil 3236722746 nil nil nil nil nil nil nil shostak)) (Analz_induction 0 (Analz_induction-1 nil 3236722746 nil nil nil nil nil nil nil shostak)) (Inj_Analz 0 (Inj_Analz-1 nil 3236722745 nil ("" (skosimp) (("" (expand "Analz" +) (("" (reduce) nil nil)) nil)) nil) untried nil nil nil nil nil)) (Fst_Analz 0 (Fst_Analz-1 nil 3236722745 nil ("" (skosimp) (("" (expand "Analz" +) (("" (reduce) nil nil)) nil)) nil) untried nil nil nil nil nil)) (Snd_Analz 0 (Snd_Analz-1 nil 3236722745 nil ("" (skosimp) (("" (expand "Analz" +) (("" (reduce) nil nil)) nil)) nil) untried nil nil nil nil nil)) (Key_Analz 0 (Key_Analz-1 nil 3236722745 nil ("" (skosimp) (("" (expand "Analz" +) (("" (reduce) nil nil)) nil)) nil) untried nil nil nil nil nil)) (Analz_induct 0 (Analz_induct-1 nil 3236722745 nil ("" (skosimp) (("" (expand* "subset?" "member") (("" (rewrite "Analz_induction") (("" (delete 2) (("" (reduce) nil nil)) nil)) nil)) nil)) nil) untried nil nil nil nil nil)) (Analz_sub 0 (Analz_sub-1 nil 3236722745 nil ("" (skosimp*) (("" (expand "Analz") (("" (grind) nil nil)) nil)) nil) untried nil nil nil nil nil)) (Analz_emptyset 0 (Analz_emptyset-1 nil 3236722745 nil ("" (use "Analz_induct" ("P" "emptyset[field]")) (("" (auto-rewrite "subset?" "member" "emptyset") (("" (reduce) (("" (apply-extensionality :hide? t) (("" (inst?) nil nil)) nil)) nil)) nil)) nil) untried nil nil nil nil nil)) (Analz_subset 0 (Analz_subset-1 nil 3236722745 nil ("" (auto-rewrite "Inj_Analz" "Fst_Analz" "Snd_Analz" "Key_Analz") (("" (skosimp) (("" (rewrite "Analz_induct") (("" (delete 2) (("" (grind) nil nil)) nil)) nil)) nil)) nil) untried nil nil nil nil nil)) (Synth_weak_induction 0 (Synth_weak_induction-1 nil 3236722746 nil nil nil nil nil nil nil shostak)) (Synth_induction 0 (Synth_induction-1 nil 3236722746 nil nil nil nil nil nil nil shostak)) (Inj_Synth 0 (Inj_Synth-1 nil 3236722745 nil ("" (skosimp) (("" (expand "Synth" +) (("" (reduce) nil nil)) nil)) nil) untried nil nil nil nil nil)) (Comp_Synth 0 (Comp_Synth-1 nil 3236722745 nil ("" (skosimp) (("" (expand "Synth" +) (("" (reduce) nil nil)) nil)) nil) untried nil nil nil nil nil)) (Key_Synth 0 (Key_Synth-1 nil 3236722745 nil ("" (skosimp) (("" (expand "Synth" +) (("" (reduce) nil nil)) nil)) nil) untried nil nil nil nil nil)) (Synth_induct 0 (Synth_induct-1 nil 3236722745 nil ("" (skosimp) (("" (expand* "subset?" "member") (("" (rewrite "Synth_induction") (("" (delete 2) (("" (reduce) nil nil)) nil)) nil)) nil)) nil) untried nil nil nil nil nil)) (Synth_sub 0 (Synth_sub-1 nil 3236722745 nil ("" (expand "Synth") (("" (grind) nil nil)) nil) untried nil nil nil nil nil)) (Synth_emptyset 0 (Synth_emptyset-1 nil 3236722745 nil ("" (use "Synth_induct" ("P" "emptyset[field]")) (("" (auto-rewrite "subset?" "member" "emptyset") (("" (reduce) (("" (apply-extensionality :hide? t) (("" (inst?) nil nil)) nil)) nil)) nil)) nil) untried nil nil nil nil nil)) (Synth_subset 0 (Synth_subset-1 nil 3236722745 nil ("" (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) untried nil nil nil nil nil)) (Synth_Atom 0 (Synth_Atom-1 nil 3236722745 nil ("" (expand "Synth") (("" (grind) nil nil)) nil) untried nil nil nil nil nil)) (Parts_idempotent 0 (Parts_idempotent-1 nil 3236722745 nil ("" (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) untried nil nil nil nil nil)) (Visible_idempotent 0 (Visible_idempotent-1 nil 3236722745 nil ("" (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) untried nil nil nil nil nil)) (Analz_idempotent 0 (Analz_idempotent-1 nil 3236722745 nil ("" (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) untried nil nil nil nil nil)) (Synth_idempotent 0 (Synth_idempotent-1 nil 3236722745 nil ("" (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) untried nil nil nil nil nil)) (Parts_Analz1 0 (Parts_Analz1-1 nil 3236722745 nil ("" (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) untried nil nil nil nil nil)) (Analz_Visible1 0 (Analz_Visible1-1 nil 3236722745 nil ("" (skolem!) (("" (auto-rewrite "Inj_Analz" "Fst_Analz" "Snd_Analz" "Analz_sub") (("" (rewrite "Visible_induct") nil nil)) nil)) nil) untried nil nil nil nil nil)) (Parts_Visible1 0 (Parts_Visible1-1 nil 3236722745 nil ("" (skolem!) (("" (use* "Parts_Analz1" "Analz_Visible1") (("" (forward-chain "subset_transitive") nil nil)) nil)) nil) untried nil nil nil nil nil)) (Parts_Analz 0 (Parts_Analz-1 nil 3236722746 nil ("" (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) untried nil nil nil nil nil)) (Analz_Parts 0 (Analz_Parts-1 nil 3236722746 nil ("" (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) untried nil nil nil nil nil)) (Parts_Visible 0 (Parts_Visible-1 nil 3236722746 nil ("" (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) untried nil nil nil nil nil)) (Visible_Parts 0 (Visible_Parts-1 nil 3236722746 nil ("" (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) untried nil nil nil nil nil)) (Analz_Visible 0 (Analz_Visible-1 nil 3236722746 nil ("" (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) untried nil nil nil nil nil)) (Visible_Analz 0 (Visible_Analz-1 nil 3236722746 nil ("" (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) untried nil nil nil nil nil)) (Parts_Synth 0 (Parts_Synth-1 nil 3236722746 nil ("" (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) untried nil nil nil nil nil)) (Analz_Synth 0 (Analz_Synth-1 nil 3236722746 nil ("" (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) untried nil nil nil nil nil)) (Visible_Synth 0 (Visible_Synth-1 nil 3236722746 nil ("" (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) untried nil nil nil nil nil)) (Analz_union1 0 (Analz_union1-1 nil 3236722746 nil ("" (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) untried nil nil nil nil nil)) (Analz_union2 0 (Analz_union2-1 nil 3236722746 nil ("" (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) untried nil nil nil nil nil)) (Fake_Parts 0 (Fake_Parts-1 nil 3236722746 nil ("" (skolem!) (("" (expand "Fake") (("" (rewrite "Parts_Synth") (("" (rewrite "Parts_Analz") nil nil)) nil)) nil)) nil) untried nil nil nil nil nil)) (Fake_mono 0 (Fake_mono-1 nil 3236722746 nil ("" (auto-rewrite "Fake" "Synth_subset" "Analz_subset") (("" (reduce) nil nil)) nil) untried nil nil 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_extensionality_TCC2| "" (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_extensionality_TCC2| "" (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_extensionality_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|leader_state_WaitingForAck_eta_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|leader_state_ExpectedNonce_WaitingForKeyAck_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|leader_state_ExpectedNonce_Connected_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|leader_state_ExpectedNonce_WaitingForAck_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_extensionality_TCC2| "" (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_extensionality_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|user_state_Connected_eta_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|user_state_ExpectedNonce_WaitingForKey_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|user_state_ExpectedNonce_Connected_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| "" (GRIND) NIL NIL) (|Parts_TCC2| "" (TERMINATION-TCC) NIL NIL) (|Parts_TCC3| "" (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 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 %% Coercion temporarily used to fix what seems like a bug in PVS2.4 Secrets(Ka): { S | subset?(S, Atom?) } = { X | X=Key(Ka) OR X=Shr(A0)::field } 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))