$$$pvs-strategies ;; ;; Proof rules for CSP ;; ;; Each rule corresponds to a step in a proof of A # R |> RankUser(rho) ;; ;; initialisation: install all the automatic rules ;; is assumes that the events are of type ;; "event[id, msg]" (defstep init-csp (id msg) (let ((rank-user-stop (format nil "rank_user_stop[~A,~A]" id msg)) (rank-user-input (format nil "rank_user_input[~A,~A]" id msg)) (rank-user-output (format nil "rank_user_output[~A,~A]" id msg)) (restriction-stop (format nil "restriction_stop[event[~A,~A]]" id msg))) (auto-rewrite rank-user-stop rank-user-input rank-user-output restriction-stop)) "Installs the automatic CSP rules" "Installing CSP rules") ;; choice: applies the simple choice rule (defstep choice () (try (rewrite "restriction_choice") (then (rewrite "rank_user_choice") (ground)) (skip-msg "No change")) "CSP rule for (P1 \/ P2) # R |> RankUser(rho)." "Applying choice rule") ;; choice2: same thing for unbounded choice (defstep choice2 () (try (rewrite "restriction_choice2") (then (rewrite "rank_user_choice2") (skolem!)) (skip-msg "No change")) "CSP rule for Choice(SP) # R |> RankUser(rho)" "Applying choice rule") ;; choice3: parametric choice (defstep choice3 () (try (rewrite "restriction_choice3") (then (rewrite "rank_user_choice3") (skolem!)) (skip-msg "No change")) "CSP rule for Choice! i : P(i) # R |> RankUser(rho)" "Applying choice rule") ;; prefix (defstep prefix () (try (rewrite "restriction_pref") (then* (lift-if) (assert) (prop)) (skip-msg "No change")) "CSP rule for (a >> P) # R |> RankUser(rho)" "Applying prefix rule") ;; parallel composition with synchro (defstep parallel () (try (rewrite "restriction_par") (then (rewrite "rank_user_par")(prop)) (skip-msg "No change")) "CSP rule for Par(A)(P1, P2) # R |> RankUser(rho)" "Applying parallel rule") ;; free parallel composition (defstep interleaving () (try (rewrite "restriction_free_par") (then (rewrite "rank_user_free_par")(prop)) (skip-msg "No change")) "CSP rule for (P1 // P2) # R |> RankUser(rho)" "Applying interleaving rule") ;; multiple parallel composition (defstep parallel2 () (try (rewrite "restriction_par2") (then (rewrite "rank_rule_par2")(skolem!)) (skip-msg "No change")) "CSP rule for Par(A)(lambda i : P(i)) # R |> RankUser(rho)" "Applying parallel rule") ;; multiple interleaving (defstep interleaving2 () (try (rewrite "restriction_free_par2") (then (rewrite "rank_user_free_par2")(skolem!)) (skip-msg "No change")) "CSP rule for (P1 // P2) # R |> RankUser(rho)" "Applying interleaving rule") $$$everything.pvs everything : THEORY BEGIN IMPORTING needham_schroeder, needham_schroeder2, lowe, multiple_runs1, multiple_runs2, concurrent_runs END everything $$$concurrent_runs.pvs % % Needham Schroeder, Lowe's fix, concurrent runs % concurrent_runs : THEORY BEGIN IMPORTING messages IMPORTING network[Identity, message, |-] %% event : TYPE = network[Identity, message, |-].event i, j : VAR Identity x, y, m : VAR message xn, yn : VAR (nonce?) k : VAR key e : VAR event n : VAR int v : VAR Nonce S : VAR set[message] l : VAR nat %-------------------------------- % identities of the two agents %-------------------------------- a : Identity b : { i | i /= a } %---------------------------------- % the run under consideration %---------------------------------- k0 : nat %--------------------------------- % nbk : the secret nonce % na(l) = nonce for a on run l % nb(l) = nonce for b on run l %--------------------------------- nbk : Nonce f : VAR [nat -> Nonce] na : { f | FORALL l : f(l) /= nbk } nb : { f | f(k0) = nbk AND FORALL l : l /= k0 IMPLIES f(l) /= nbk } na_prop : LEMMA FORALL l : na(l) /= nbk nb_prop : LEMMA FORALL l : nb(l) = nbk IFF l = k0 %----------------- % Abbreviations %----------------- Ia : (user?) = user(a) Ib : (user?) = user(b) Na(l) : (nonce?) = nonce(na(l)) Nb(l) : (nonce?) = nonce(nb(l)) pub(i, x) : message = crypto(public(i), x) sec(i, x) : message = crypto(secret(i), x) conc3(x, y, m) : message = conc(conc(x, y), m) %===================================== % Fixed point definition for User A %===================================== X : VAR [nat -> process[event]] Fa(X)(l) : process[event] = (Choice! i, xn : ( trans(a, i, pub(i, conc(Na(l), Ia))) >> ( X(l + 1) // ( rec(a, i, pub(a, conc3(Na(l), xn, user(i)))) >> ( trans(a, i, pub(i, xn)) >> Stop[event] ))))) \/ (Choice! j, yn : ( rec(a, j, pub(a, conc(yn, user(j)))) >> ( X(l + 1) // ( trans(a, j, pub(j, conc3(yn, Na(l), Ia))) >> ( rec(a, j, pub(a, Na(l))) >> Stop[event] ))))) userA : [nat -> process[event]] = mu(Fa) interface_userA : LEMMA subset?(sigma(userA(l)), LocalEvents(a)) %=========================== % Fixed point for User B %=========================== Fb(X)(l) : process[event] = IF l = k0 THEN Choice! y : ( rec(b, a, pub(b, conc(y, Ia))) >> ( X(k0 + 1) // ( trans(b, a, pub(a, conc3(y, Nb(k0), Ib))) >> ( rec(b, a, pub(b, Nb(k0))) >> Stop[event] )))) ELSE (Choice! i, xn : ( trans(b, i, pub(i, conc(Nb(l), Ib))) >> ( X(l + 1) // ( rec(b, i, pub(b, conc3(Nb(l), xn, user(i)))) >> ( trans(b, i, pub(i, xn)) >> Stop[event] ))))) \/ (Choice! j, y : ( rec(b, j, pub(b, conc(y, user(j)))) >> ( X(l + 1) // ( trans(b, j, pub(j, conc3(y, Nb(l), Ib))) >> ( rec(b, j, pub(b, Nb(l))) >> Stop[event] ))))) ENDIF userB : [nat -> process[event]] = mu(Fb) interface_userB : LEMMA subset?(sigma(userB(l)), LocalEvents(b)) %============ % INIT set %============ INIT_nonce : set[message] = { m | EXISTS v : v /= nbk AND m = nonce(v) } INIT_secret : set[message] = { m | EXISTS i : i /= a AND i /= b AND m = secret(i) } INIT : set[message] = { m | user?(m) OR text?(m) OR public?(m) OR INIT_nonce(m) OR INIT_secret(m) } %============================ % Authentication Property %============================ T1 : set[event] = { e | e = rec(b, a, pub(b, Nb(k0))) } R1 : set[event] = { e | e = trans(a, b, pub(b, Nb(k0))) } %----------------- % Rank function %----------------- rank_code(k, m, n) : int = CASES k OF public(j) : IF j = a AND (EXISTS x : m = conc3(x, Nb(k0), Ib)) THEN 1 ELSE n ENDIF, secret(j) : IF j = a AND (EXISTS x : m = pub(a, conc3(x, Nb(k0), Ib))) THEN 0 ELSE n ENDIF ENDCASES rho(m) : RECURSIVE int = CASES m OF text(z) : 1, nonce(z) : IF z = nbk THEN 0 ELSE 1 ENDIF, user(z) : 1, public(z) : 1, secret(z) : IF z = a OR z = b THEN 0 ELSE 1 ENDIF, conc(z1, z2) : min(rho(z1), rho(z2)), code(k, z) : rank_code(k, z, rho(z)) ENDCASES MEASURE size(m) %---------------------- % Constraints on rho %---------------------- validity_rho : LEMMA FORALL S, m : positive(rho, S) AND (S |- m) IMPLIES rho(m) > 0 rank_init : LEMMA positive(rho, INIT) nonpositive_rank : LEMMA non_positive(rho, T1) %------------------- % User properties %------------------- IMPORTING rank_rules2, rank_rules3 rank_user_a : LEMMA userA(l) # R1 |> RankUser(rho) rank_user_b : LEMMA userB(l) # R1 |> RankUser(rho) %---------------- % Consequence %---------------- authentication_origin : PROPOSITION network(enemy(INIT), protocol(a, b, userA(0), userB(0))) |> auth(T1, R1) END concurrent_runs $$$concurrent_runs.prf (|concurrent_runs| (|IMP_network_TCC1| "" (LEMMA "gen_monotonic2") (("" (PROPAX) NIL NIL)) NIL) (|b_TCC1| "" (INST + "a+1") NIL NIL) (|na_TCC1| "" (INST + "lambda l : nbk + 1") NIL NIL) (|nb_TCC1| "" (INST + "lambda l : IF l = k0 THEN nbk ELSE nbk + 1 ENDIF") (("" (SKOSIMP) (("" (LIFT-IF) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|na_prop| "" (TYPEPRED "na") (("" (PROPAX) NIL NIL)) NIL) (|nb_prop| "" (TYPEPRED "nb") (("" (SKOLEM!) (("" (INST - "l!1") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|userA_TCC1| "" (EXPAND "monotonic?") (("" (EXPAND "<=") (("" (SKOSIMP*) (("" (AUTO-REWRITE-THEORY "monotonicity[event[nat, message]]") (("" (INST - "x!1 + 1") (("" (EXPAND "Fa") (("" (REWRITE "monotonic_choice") (("1" (DELETE 2) (("1" (REWRITE "monotonic_choice3") (("1" (SKOLEM!) (("1" (DELETE 2) (("1" (REWRITE "monotonic_free_par") NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (REWRITE "monotonic_choice3") (("2" (SKOLEM!) (("2" (DELETE 2) (("2" (REWRITE "monotonic_free_par") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|interface_userA| "" (AUTO-REWRITE-THEORY "interface_rules[event]" :EXCLUDE ("interface_equiv")) (("" (AUTO-REWRITE "local_transmission" "local_reception" "userA" "userA_TCC1") (("" (ASSERT) (("" (REWRITE "interface_fix2") (("" (DELETE 2) (("" (SKOSIMP*) (("" (INST - "i!1 + 1") (("" (EXPAND "Fa") (("" (ASSERT) (("" (SPLIT) (("1" (REWRITE "interface_choice3") (("1" (SKOLEM!) NIL NIL)) NIL) ("2" (REWRITE "interface_choice3") (("2" (SKOLEM!) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|userB_TCC1| "" (EXPAND "monotonic?") (("" (EXPAND "<=") (("" (SKOSIMP*) (("" (AUTO-REWRITE-THEORY "monotonicity[event[nat, message]]") (("" (INST - "x!1 + 1") (("" (EXPAND "Fb") (("" (LIFT-IF) (("" (GROUND) (("1" (REWRITE "monotonic_choice3") (("1" (SKOLEM!) (("1" (REWRITE "monotonic_free_par") NIL NIL)) NIL)) NIL) ("2" (REWRITE "monotonic_choice") (("1" (DELETE 3) (("1" (REWRITE "monotonic_choice3") (("1" (SKOLEM!) (("1" (REWRITE "monotonic_free_par") NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE 3) (("2" (REWRITE "monotonic_choice3") (("2" (SKOLEM!) (("2" (REWRITE "monotonic_free_par") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|interface_userB| "" (AUTO-REWRITE-THEORY "interface_rules[event]" :EXCLUDE ("interface_equiv")) (("" (AUTO-REWRITE "local_transmission" "local_reception" "userB" "userB_TCC1") (("" (ASSERT) (("" (REWRITE "interface_fix2") (("" (DELETE 2) (("" (SKOSIMP*) (("" (INST - "i!1 + 1") (("" (EXPAND "Fb") (("" (LIFT-IF) (("" (GROUND) (("1" (REWRITE "interface_choice3") (("1" (ASSERT) (("1" (SKOLEM-TYPEPRED) (("1" (REPLACE*) NIL NIL)) NIL)) NIL)) NIL) ("2" (PROP) (("1" (REWRITE "interface_choice3") (("1" (SKOLEM!) NIL NIL)) NIL) ("2" (REWRITE "interface_choice3") (("2" (SKOLEM!) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|rank_code_TCC1| "" (GRIND) NIL NIL) (|rho_TCC1| "" (GRIND) NIL NIL) (|rho_TCC2| "" (GRIND) NIL NIL) (|rho_TCC3| "" (GRIND) NIL NIL) (|validity_rho| "" (REWRITE "rank_valid") (("1" (DELETE 2) (("1" (GRIND) NIL NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND :IF-MATCH NIL) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL) (|rank_init| "" (GRIND) NIL NIL) (|nonpositive_rank| "" (GRIND) NIL NIL) (|rank_user_a| "" (INIT-CSP "Identity" "message") (("" (AUTO-REWRITE "userA_TCC1") (("" (EXPAND "userA") (("" (REWRITE "restriction_fix2") (("" (DELETE 2) (("" (SKOSIMP*) (("" (EXPAND "Fa") (("" (CHOICE) (("1" (REWRITE "restriction_choice3") (("1" (REWRITE "rank_user_choice3[[Identity, (nonce?)], Identity, message]") (("1" (SKOLEM!) (("1" (PREFIX) (("1" (DELETE -1 2) (("1" (LEMMA "na_prop" ("l" "i!1")) (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (INTERLEAVING) (("1" (INST?) NIL NIL) ("2" (PREFIX) (("2" (PREFIX) (("2" (DELETE -2 3 4) (("2" (EXPAND "R1") (("2" (CASE "i!2`1 = b AND i!2`2 = Nb(k0)") (("1" (GROUND) NIL NIL) ("2" (USE "na_prop" ("l" "i!1")) (("2" (DELETE 2) (("2" (GROUND) (("1" (GRIND) (("1" (DECOMPOSE-EQUALITY -2) (("1" (DECOMPOSE-EQUALITY -2) NIL NIL)) NIL)) NIL) ("2" (GRIND) (("2" (APPLY-EXTENSIONALITY) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "restriction_choice3") (("2" (REWRITE "rank_user_choice3[[Identity, (nonce?)], Identity, message]") (("2" (SKOLEM!) (("2" (PREFIX) (("2" (INTERLEAVING) (("1" (INST?) NIL NIL) ("2" (PREFIX) (("1" (EXPAND "R1" +) (("1" (DELETE -2 2 3) (("1" (LEMMA "na_prop" ("l" "i!1")) (("1" (GRIND) (("1" (DECOMPOSE-EQUALITY -2) NIL NIL) ("2" (DECOMPOSE-EQUALITY -2) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (PREFIX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|rank_user_b| "" (INIT-CSP "Identity" "message") (("" (EXPAND "userB") (("" (AUTO-REWRITE "userB_TCC1") (("" (REWRITE "restriction_fix2") (("" (DELETE 2) (("" (SKOSIMP*) (("" (EXPAND "Fb") (("" (LIFT-IF) (("" (PROP) (("1" (REWRITE "restriction_choice3") (("1" (REWRITE "rank_user_choice3[message, Identity, message]") (("1" (SKOLEM!) (("1" (PREFIX) (("1" (INTERLEAVING) (("1" (INST?) NIL NIL) ("2" (PREFIX) (("1" (DELETE -3 2 3) (("1" (GRIND) NIL NIL)) NIL) ("2" (PREFIX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CHOICE) (("1" (REWRITE "restriction_choice3") (("1" (REWRITE "rank_user_choice3[[Identity, (nonce?)], Identity, message]") (("1" (SKOLEM!) (("1" (NAME-REPLACE "j!1" "PROJ_1(i!2)") (("1" (NAME-REPLACE "x!1" "PROJ_2(i!2)") (("1" (PREFIX) (("1" (DELETE -1 2) (("1" (LEMMA "nb_prop" ("l" "i!1")) (("1" (ASSERT) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (INTERLEAVING) (("1" (INST?) NIL NIL) ("2" (PREFIX) (("2" (PREFIX) (("2" (DELETE -2 1 3 4) (("2" (LEMMA "nb_prop" ("l" "i!1")) (("2" (ASSERT) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "restriction_choice3") (("2" (REWRITE "rank_user_choice3[[Identity, message], Identity, message]") (("2" (SKOLEM!) (("2" (NAME-REPLACE "j!1" "PROJ_1(i!2)") (("2" (NAME-REPLACE "x!1" "PROJ_2(i!2)") (("2" (PREFIX) (("2" (INTERLEAVING) (("1" (INST?) NIL NIL) ("2" (PREFIX) (("1" (DELETE -2 2 3) (("1" (LEMMA "nb_prop" ("l" "i!1")) (("1" (ASSERT) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (PREFIX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|authentication_origin| "" (USE "authentication_by_rank2" ("rho" "rho")) (("" (GROUND) (("1" (REWRITE "rank_init") NIL NIL) ("2" (USE "validity_rho") NIL NIL) ("3" (REWRITE "nonpositive_rank") NIL NIL) ("4" (REWRITE "interface_userA") NIL NIL) ("5" (REWRITE "rank_user_a") NIL NIL) ("6" (REWRITE "interface_userB") NIL NIL) ("7" (REWRITE "rank_user_b") NIL NIL)) NIL)) NIL)) $$$multiple_runs2.pvs % % Needham Schroeder, Lowe's fix, successive runs % multiple_runs2 : THEORY BEGIN IMPORTING messages IMPORTING network[Identity, message, |-] %% event : TYPE = network[Identity, message, |-].event i, j : VAR Identity x, y, m : VAR message xn, yn : VAR (nonce?) k : VAR key e : VAR event n : VAR int v : VAR Nonce S : VAR set[message] l : VAR nat %-------------------------------- % identities of the two agents %-------------------------------- a : Identity b : { i | i /= a } %---------------------------------- % the run under consideration %---------------------------------- k0 : nat %--------------------------------- % nbk : the secret nonce % na(l) = nonce for a on run l % nb(l) = nonce for b on run l %--------------------------------- nbk : Nonce na(l) : { v | v /= nbk } nb(l) : { v | v = nbk IFF l = k0 } na_prop : LEMMA FORALL l : na(l) /= nbk nb_prop : LEMMA FORALL l : nb(l) = nbk IFF l = k0 %----------------- % Abbreviations %----------------- Ia : (user?) = user(a) Ib : (user?) = user(b) Na(l) : (nonce?) = nonce(na(l)) Nb(l) : (nonce?) = nonce(nb(l)) pub(i, x) : message = crypto(public(i), x) sec(i, x) : message = crypto(secret(i), x) conc3(x, y, m) : message = conc(conc(x, y), m) %===================================== % Fixed point definition for User A %===================================== X : VAR [nat -> process[event]] Fa(X)(l) : process[event] = (Choice! i, xn : ( trans(a, i, pub(i, conc(Na(l), Ia))) >> ( rec(a, i, pub(a, conc3(Na(l), xn, user(i)))) >> ( trans(a, i, pub(i, xn)) >> X(l + 1) )))) \/ (Choice! j, y : ( rec(a, j, pub(a, conc(y, user(j)))) >> ( trans(a, j, pub(j, conc3(y, Na(l), Ia))) >> ( rec(a, j, pub(a, Na(l))) >> X(l + 1) )))) userA : [nat -> process[event]] = mu(Fa) interface_userA : LEMMA subset?(sigma(userA(l)), LocalEvents(a)) %=========================== % Fixed point for User B %=========================== Fb(X)(l) : process[event] = IF l = k0 THEN Choice! y : ( rec(b, a, pub(b, conc(y, Ia))) >> ( trans(b, a, pub(a, conc3(y, Nb(k0), Ib))) >> ( rec(b, a, pub(b, Nb(k0))) >> X(k0 + 1) ))) ELSE (Choice! i, xn : ( trans(b, i, pub(i, conc(Nb(l), Ib))) >> ( rec(b, i, pub(b, conc3(Nb(l), xn, user(i)))) >> ( trans(b, i, pub(i, xn)) >> X(l + 1) )))) \/ (Choice! j, y : ( rec(b, j, pub(b, conc(y, user(j)))) >> ( trans(b, j, pub(j, conc3(y, Nb(l), Ib))) >> ( rec(b, j, pub(b, Nb(l))) >> X(l + 1) )))) ENDIF userB : [nat -> process[event]] = mu(Fb) interface_userB : LEMMA subset?(sigma(userB(l)), LocalEvents(b)) %============ % INIT set %============ INIT_nonce : set[message] = { m | EXISTS v : v /= nbk AND m = nonce(v) } INIT_secret : set[message] = { m | EXISTS i : i /= a AND i /= b AND m = secret(i) } INIT : set[message] = { m | user?(m) OR text?(m) OR public?(m) OR INIT_nonce(m) OR INIT_secret(m) } %============================ % Authentication Property %============================ T1 : set[event] = { e | e = rec(b, a, pub(b, Nb(k0))) } R1 : set[event] = { e | e = trans(a, b, pub(b, Nb(k0))) } %----------------- % Rank function %----------------- critical(m) : RECURSIVE bool = CASES m OF text(z) : FALSE, nonce(z) : z = nbk, user(z) : FALSE, public(z) : FALSE, secret(z) : FALSE, conc(z1, z2) : critical(z1) OR critical(z2), code(k, z) : FALSE ENDCASES MEASURE size(m) rank_pub_a(m, n) : int = IF (conc?(m) AND critical(x_conc(m)) AND y_conc(m) = Ib) THEN 1 ELSE n ENDIF rank_pub_b(m, n) : int = IF (conc?(m) AND conc?(x_conc(m)) AND critical(x_conc(x_conc(m))) AND y_conc(m) = Ia) THEN 1 ELSE n ENDIF rank_code(k, m, n) : int = CASES k OF public(j) : IF j=a THEN rank_pub_a(m, n) ELSIF j=b THEN rank_pub_b(m, n) ELSE n ENDIF, secret(j) : n ENDCASES rho(m) : RECURSIVE int = CASES m OF text(z) : 1, nonce(z) : IF z = nbk THEN 0 ELSE 1 ENDIF, user(z) : 1, public(z) : 1, secret(z) : IF z = a OR z = b THEN 0 ELSE 1 ENDIF, conc(z1, z2) : min(rho(z1), rho(z2)), code(k, z) : rank_code(k, z, rho(z)) ENDCASES MEASURE size(m) %---------------------- % Constraints on rho %---------------------- validity_rho : LEMMA FORALL S, m : positive(rho, S) AND (S |- m) IMPLIES rho(m) > 0 rank_init : LEMMA positive(rho, INIT) nonpositive_rank : LEMMA non_positive(rho, T1) %------------------- % User properties %------------------- IMPORTING rank_rules2, rank_rules3 rank_user_a : LEMMA userA(l) # R1 |> RankUser(rho) rank_user_b : LEMMA userB(l) # R1 |> RankUser(rho) %---------------- % Consequence %---------------- authentication_origin : PROPOSITION network(enemy(INIT), protocol(a, b, userA(0), userB(0))) |> auth(T1, R1) END multiple_runs2 $$$multiple_runs2.prf (|multiple_runs2| (|IMP_network_TCC1| "" (LEMMA "gen_monotonic2") (("" (PROPAX) NIL NIL)) NIL) (|b_TCC1| "" (INST + "a+1") NIL NIL) (|na_TCC1| "" (INST + "lambda l : nbk + 1") NIL NIL) (|nb_TCC1| "" (INST + "lambda l : IF l = k0 THEN nbk ELSE nbk + 1 ENDIF") (("1" (SKOSIMP) NIL NIL) ("2" (SKOSIMP) NIL NIL)) NIL) (|na_prop| "" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL) (|nb_prop| "" (SKOLEM!) (("" (TYPEPRED "nb(l!1)") (("" (GROUND) NIL NIL)) NIL)) NIL) (|userA_TCC1| "" (EXPAND "monotonic?") (("" (EXPAND "<=") (("" (SKOSIMP*) (("" (AUTO-REWRITE-THEORY "monotonicity[event[nat, message]]") (("" (INST - "x!1 + 1") (("" (EXPAND "Fa") (("" (REWRITE "monotonic_choice") (("1" (DELETE 2) (("1" (REWRITE "monotonic_choice3") NIL NIL)) NIL) ("2" (DELETE 2) (("2" (REWRITE "monotonic_choice3") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|interface_userA| "" (AUTO-REWRITE-THEORY "interface_rules[event]" :EXCLUDE ("interface_equiv")) (("" (AUTO-REWRITE "local_transmission" "local_reception" "userA" "userA_TCC1") (("" (ASSERT) (("" (REWRITE "interface_fix2") (("" (DELETE 2) (("" (SKOSIMP*) (("" (INST - "i!1 + 1") (("" (EXPAND "Fa") (("" (ASSERT) (("" (PROP) (("1" (REWRITE "interface_choice3") NIL NIL) ("2" (REWRITE "interface_choice3") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|userB_TCC1| "" (EXPAND "monotonic?") (("" (EXPAND "<=") (("" (SKOSIMP*) (("" (AUTO-REWRITE-THEORY "monotonicity[event[nat, message]]") (("" (INST - "x!1 + 1") (("" (EXPAND "Fb") (("" (LIFT-IF) (("" (GROUND) (("1" (REWRITE "monotonic_choice3") NIL NIL) ("2" (REWRITE "monotonic_choice") (("1" (DELETE 2) (("1" (REWRITE "monotonic_choice3") NIL NIL)) NIL) ("2" (DELETE 2) (("2" (REWRITE "monotonic_choice3") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|interface_userB| "" (AUTO-REWRITE-THEORY "interface_rules[event]" :EXCLUDE ("interface_equiv")) (("" (AUTO-REWRITE "local_transmission" "local_reception" "userB" "userB_TCC1") (("" (ASSERT) (("" (REWRITE "interface_fix2") (("" (DELETE 2) (("" (SKOSIMP*) (("" (INST - "i!1 + 1") (("" (EXPAND "Fb") (("" (LIFT-IF) (("" (GROUND) (("1" (REWRITE "interface_choice3") NIL NIL) ("2" (SPLIT) (("1" (REWRITE "interface_choice3") NIL NIL) ("2" (REWRITE "interface_choice3") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|critical_TCC1| "" (TERMINATION-TCC) NIL NIL) (|critical_TCC2| "" (TERMINATION-TCC) NIL NIL) (|rank_code_TCC1| "" (CASES-TCC) NIL NIL) (|rho_TCC1| "" (TERMINATION-TCC) NIL NIL) (|rho_TCC2| "" (TERMINATION-TCC) NIL NIL) (|validity_rho| "" (REWRITE "rank_valid") (("1" (DELETE 2) (("1" (GRIND) NIL NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND :EXCLUDE ("critical") :IF-MATCH NIL) NIL NIL)) NIL)) NIL) (|rank_init| "" (GRIND) NIL NIL) (|nonpositive_rank| "" (GRIND) NIL NIL) (|rank_user_a| "" (INIT-CSP "Identity" "message") (("" (AUTO-REWRITE "userA_TCC1") (("" (EXPAND "userA") (("" (REWRITE "restriction_fix2") (("" (DELETE 2) (("" (SKOSIMP*) (("" (EXPAND "Fa") (("" (CHOICE) (("1" (REWRITE "restriction_choice3") (("1" (REWRITE "rank_user_choice3[[Identity, (nonce?)], Identity, message]") (("1" (SKOLEM!) (("1" (PREFIX) (("1" (DELETE -1 2) (("1" (GRIND) NIL NIL)) NIL) ("2" (PREFIX) (("2" (PREFIX) (("1" (DELETE -2 3 4) (("1" (EXPAND "R1") (("1" (GRIND) (("1" (DECOMPOSE-EQUALITY -2) (("1" (APPLY (REPEAT* (APPLY-EXTENSIONALITY :HIDE? T))) NIL NIL)) NIL) ("2" (DECOMPOSE-EQUALITY -2) (("2" (APPLY (REPEAT* (APPLY-EXTENSIONALITY :HIDE? T))) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "restriction_choice3") (("2" (REWRITE "rank_user_choice3[[Identity, message], Identity, message]") (("2" (SKOLEM!) (("2" (PREFIX) (("2" (PREFIX) (("1" (DELETE -2 2 3) (("1" (GRIND) (("1" (DECOMPOSE-EQUALITY -2) NIL NIL)) NIL)) NIL) ("2" (PREFIX) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|rank_user_b| "" (INIT-CSP "Identity" "message") (("" (EXPAND "userB") (("" (AUTO-REWRITE "userB_TCC1") (("" (REWRITE "restriction_fix2") (("" (DELETE 2) (("" (SKOSIMP*) (("" (EXPAND "Fb") (("" (LIFT-IF) (("" (PROP) (("1" (REWRITE "restriction_choice3") (("1" (REWRITE "rank_user_choice3[message, Identity, message]") (("1" (SKOLEM!) (("1" (PREFIX) (("1" (PREFIX) (("1" (DELETE -1 -3 -2 3) (("1" (GRIND) NIL NIL)) NIL) ("2" (PREFIX) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CHOICE) (("1" (REWRITE "restriction_choice3") (("1" (REWRITE "rank_user_choice3[[Identity, (nonce?)], Identity, message]") (("1" (SKOLEM!) (("1" (NAME-REPLACE "j!1" "PROJ_1(i!2)") (("1" (NAME-REPLACE "x!1" "PROJ_2(i!2)") (("1" (PREFIX) (("1" (DELETE -1 2) (("1" (TYPEPRED "nb(i!1)") (("1" (ASSERT) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (PREFIX) (("2" (PREFIX) (("1" (DELETE -2 2 3 4) (("1" (TYPEPRED "nb(i!1)") (("1" (ASSERT) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "restriction_choice3") (("2" (REWRITE "rank_user_choice3[[Identity, message], Identity, message]") (("2" (SKOLEM!) (("2" (NAME-REPLACE "j!1" "PROJ_1(i!2)") (("2" (NAME-REPLACE "x!1" "PROJ_2(i!2)") (("2" (PREFIX) (("2" (PREFIX) (("1" (DELETE -2 2 3) (("1" (TYPEPRED "nb(i!1)") (("1" (ASSERT) (("1" (CASE "user(j!1) = user(a) IMPLIES j!1 = a") (("1" (GRIND) NIL NIL) ("2" (GROUND) (("2" (CASE "x_user(user(j!1)) = a") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (PREFIX) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|authentication_origin| "" (USE "authentication_by_rank2" ("rho" "rho")) (("" (GROUND) (("1" (REWRITE "rank_init") NIL NIL) ("2" (USE "validity_rho") NIL NIL) ("3" (REWRITE "nonpositive_rank") NIL NIL) ("4" (REWRITE "interface_userA") NIL NIL) ("5" (REWRITE "rank_user_a") NIL NIL) ("6" (REWRITE "interface_userB") NIL NIL) ("7" (REWRITE "rank_user_b") NIL NIL)) NIL)) NIL)) $$$multiple_runs1.pvs % % Needham Schroeder, Lowe's fix, successive runs % multiple_runs1 : THEORY BEGIN IMPORTING messages IMPORTING network[Identity, message, |-] %% event : TYPE = network[Identity, message, |-].event i, j : VAR Identity x, y, m : VAR message xn, yn : VAR (nonce?) k : VAR key e : VAR event n : VAR int v : VAR Nonce S : VAR set[message] l : VAR nat %-------------------------------- % identities of the two agents %-------------------------------- a : Identity b : { i | i /= a } %---------------------------------- % the run under consideration %---------------------------------- k0 : nat %--------------------------------- % nbk : the secret nonce % na(l) = nonce for a on run l % nb(l) = nonce for b on run l %--------------------------------- nbk : Nonce f : VAR [nat -> Nonce] na : { f | FORALL l : f(l) /= nbk } nb : { f | f(k0) = nbk AND FORALL l : l /= k0 IMPLIES f(l) /= nbk } na_prop : LEMMA FORALL l : na(l) /= nbk nb_prop : LEMMA FORALL l : nb(l) = nbk IFF l = k0 %----------------- % Abbreviations %----------------- Ia : (user?) = user(a) Ib : (user?) = user(b) Na(l) : (nonce?) = nonce(na(l)) Nb(l) : (nonce?) = nonce(nb(l)) pub(i, x) : message = crypto(public(i), x) sec(i, x) : message = crypto(secret(i), x) conc3(x, y, m) : message = conc(conc(x, y), m) %===================================== % Fixed point definition for User A %===================================== X : VAR [nat -> process[event]] Fa0(X)(l) : process[event] = (Choice! i, xn : ( trans(a, i, pub(i, conc(Na(l), Ia))) >> ( rec(a, i, pub(a, conc3(Na(l), xn, user(i)))) >> ( trans(a, i, pub(i, xn)) >> X(l + 1) )))) \/ (Choice! j, y : ( rec(a, j, pub(a, conc(y, user(j)))) >> ( trans(a, j, pub(j, conc3(y, Na(l), Ia))) >> ( rec(a, j, pub(a, Na(l))) >> X(l + 1) )))) Fa(X)(l) : process[event] = (Choice! i, xn : ( trans(a, i, pub(i, conc(Na(l), Ia))) >> ( rec(a, i, pub(a, conc3(Na(l), xn, user(i)))) >> ( trans(a, i, pub(i, xn)) >> X(l + 1) )))) \/ (Choice! j, yn : ( rec(a, j, pub(a, conc(yn, user(j)))) >> ( trans(a, j, pub(j, conc3(yn, Na(l), Ia))) >> ( rec(a, j, pub(a, Na(l))) >> X(l + 1) )))) userA : [nat -> process[event]] = mu(Fa) interface_userA : LEMMA subset?(sigma(userA(l)), LocalEvents(a)) %=========================== % Fixed point for User B %=========================== Fb(X)(l) : process[event] = IF l = k0 THEN Choice! y : ( rec(b, a, pub(b, conc(y, Ia))) >> ( trans(b, a, pub(a, conc3(y, Nb(k0), Ib))) >> ( rec(b, a, pub(b, Nb(k0))) >> X(k0 + 1) ))) ELSE (Choice! i, xn : ( trans(b, i, pub(i, conc(Nb(l), Ib))) >> ( rec(b, i, pub(b, conc3(Nb(l), xn, user(i)))) >> ( trans(b, i, pub(i, xn)) >> X(l + 1) )))) \/ (Choice! j, y : ( rec(b, j, pub(b, conc(y, user(j)))) >> ( trans(b, j, pub(j, conc3(y, Nb(l), Ib))) >> ( rec(b, j, pub(b, Nb(l))) >> X(l + 1) )))) ENDIF userB : [nat -> process[event]] = mu(Fb) interface_userB : LEMMA subset?(sigma(userB(l)), LocalEvents(b)) %============ % INIT set %============ INIT_nonce : set[message] = { m | EXISTS v : v /= nbk AND m = nonce(v) } INIT_secret : set[message] = { m | EXISTS i : i /= a AND i /= b AND m = secret(i) } INIT : set[message] = { m | user?(m) OR text?(m) OR public?(m) OR INIT_nonce(m) OR INIT_secret(m) } %============================ % Authentication Property %============================ T1 : set[event] = { e | e = rec(b, a, pub(b, Nb(k0))) } R1 : set[event] = { e | e = trans(a, b, pub(b, Nb(k0))) } %----------------- % Rank function %----------------- rank_code(k, m, n) : int = CASES k OF public(j) : IF j = a AND (EXISTS x : m = conc3(x, Nb(k0), Ib)) THEN 1 ELSE n ENDIF, secret(j) : IF j = a AND (EXISTS x : m = pub(a, conc3(x, Nb(k0), Ib))) THEN 0 ELSE n ENDIF ENDCASES rho(m) : RECURSIVE int = CASES m OF text(z) : 1, nonce(z) : IF z = nbk THEN 0 ELSE 1 ENDIF, user(z) : 1, public(z) : 1, secret(z) : IF z = a OR z = b THEN 0 ELSE 1 ENDIF, conc(z1, z2) : min(rho(z1), rho(z2)), code(k, z) : rank_code(k, z, rho(z)) ENDCASES MEASURE size(m) %---------------------- % Constraints on rho %---------------------- validity_rho : LEMMA FORALL S, m : positive(rho, S) AND (S |- m) IMPLIES rho(m) > 0 rank_init : LEMMA positive(rho, INIT) nonpositive_rank : LEMMA non_positive(rho, T1) %------------------- % User properties %------------------- IMPORTING rank_rules2, rank_rules3 rank_user_a : LEMMA userA(l) # R1 |> RankUser(rho) rank_user_b : LEMMA userB(l) # R1 |> RankUser(rho) %---------------- % Consequence %---------------- authentication_origin : PROPOSITION network(enemy(INIT), protocol(a, b, userA(0), userB(0))) |> auth(T1, R1) END multiple_runs1 $$$multiple_runs1.prf (|multiple_runs1| (|IMP_network_TCC1| "" (LEMMA "gen_monotonic2") (("" (PROPAX) NIL NIL)) NIL) (|b_TCC1| "" (INST + "a+1") NIL NIL) (|na_TCC1| "" (INST + "lambda l : nbk + 1") NIL NIL) (|nb_TCC1| "" (INST + "lambda l : IF l = k0 THEN nbk ELSE nbk + 1 ENDIF") (("" (SKOSIMP) (("" (LIFT-IF) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|na_prop| "" (TYPEPRED "na") (("" (PROPAX) NIL NIL)) NIL) (|nb_prop| "" (TYPEPRED "nb") (("" (SKOLEM!) (("" (INST - "l!1") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|userA_TCC1| "" (EXPAND "monotonic?") (("" (EXPAND "<=") (("" (SKOSIMP*) (("" (AUTO-REWRITE-THEORY "monotonicity[event[nat, message]]") (("" (INST - "x!1 + 1") (("" (EXPAND "Fa") (("" (REWRITE "monotonic_choice") (("1" (DELETE 2) (("1" (REWRITE "monotonic_choice3") (("1" (SKOLEM!) NIL NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (REWRITE "monotonic_choice3") (("2" (SKOLEM!) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|interface_userA| "" (AUTO-REWRITE-THEORY "interface_rules[event]" :EXCLUDE ("interface_equiv")) (("" (AUTO-REWRITE "local_transmission" "local_reception" "userA" "userA_TCC1") (("" (ASSERT) (("" (REWRITE "interface_fix2") (("" (DELETE 2) (("" (SKOSIMP*) (("" (INST - "i!1 + 1") (("" (EXPAND "Fa") (("" (ASSERT) (("" (SPLIT) (("1" (REWRITE "interface_choice3") (("1" (SKOLEM!) NIL NIL)) NIL) ("2" (REWRITE "interface_choice3") (("2" (SKOLEM!) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|userB_TCC1| "" (EXPAND "monotonic?") (("" (EXPAND "<=") (("" (SKOSIMP*) (("" (AUTO-REWRITE-THEORY "monotonicity[event[nat, message]]") (("" (INST - "x!1 + 1") (("" (EXPAND "Fb") (("" (LIFT-IF) (("" (GROUND) (("1" (REWRITE "monotonic_choice3") (("1" (DELETE 2) (("1" (REDUCE) NIL NIL)) NIL)) NIL) ("2" (REWRITE "monotonic_choice") (("1" (DELETE 3) (("1" (REWRITE "monotonic_choice3") (("1" (DELETE 2) (("1" (SKOLEM!) NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE 3) (("2" (REWRITE "monotonic_choice3") (("2" (SKOLEM!) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|interface_userB| "" (AUTO-REWRITE-THEORY "interface_rules[event]" :EXCLUDE ("interface_equiv")) (("" (AUTO-REWRITE "local_transmission" "local_reception" "userB" "userB_TCC1") (("" (ASSERT) (("" (REWRITE "interface_fix2") (("" (DELETE 2) (("" (SKOSIMP*) (("" (INST - "i!1 + 1") (("" (EXPAND "Fb") (("" (LIFT-IF) (("" (GROUND) (("1" (REWRITE "interface_choice3") (("1" (REDUCE) NIL NIL)) NIL) ("2" (PROP) (("1" (REWRITE "interface_choice3") (("1" (SKOLEM!) NIL NIL)) NIL) ("2" (REWRITE "interface_choice3") (("2" (SKOLEM!) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|rank_code_TCC1| "" (CASES-TCC) NIL NIL) (|rho_TCC1| "" (TERMINATION-TCC) NIL NIL) (|rho_TCC2| "" (TERMINATION-TCC) NIL NIL) (|rho_TCC3| "" (TERMINATION-TCC) NIL NIL) (|validity_rho| "" (REWRITE "rank_valid") (("1" (DELETE 2) (("1" (GRIND) NIL NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND :IF-MATCH NIL) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL) (|rank_init| "" (GRIND) NIL NIL) (|nonpositive_rank| "" (GRIND) NIL NIL) (|rank_user_a| "" (INIT-CSP "Identity" "message") (("" (AUTO-REWRITE "userA_TCC1") (("" (EXPAND "userA") (("" (REWRITE "restriction_fix2") (("" (DELETE 2) (("" (SKOSIMP*) (("" (EXPAND "Fa") (("" (CHOICE) (("1" (REWRITE "restriction_choice3") (("1" (REWRITE "rank_user_choice3[[Identity, (nonce?)], Identity, message]") (("1" (SKOLEM!) (("1" (PREFIX) (("1" (DELETE -1 2) (("1" (LEMMA "na_prop" ("l" "i!1")) (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (PREFIX) (("2" (PREFIX) (("1" (DELETE -2 3 4) (("1" (EXPAND "R1") (("1" (CASE "i!2`1 = b AND i!2`2 = Nb(k0)") (("1" (GROUND) NIL NIL) ("2" (USE "na_prop" ("l" "i!1")) (("2" (DELETE 3) (("2" (GROUND) (("1" (GRIND) (("1" (DECOMPOSE-EQUALITY -2) (("1" (DECOMPOSE-EQUALITY -2) NIL NIL)) NIL)) NIL) ("2" (GRIND) (("2" (DECOMPOSE-EQUALITY -2) (("2" (DECOMPOSE-EQUALITY -1) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "restriction_choice3") (("2" (REWRITE "rank_user_choice3[[Identity, (nonce?)], Identity, message]") (("2" (SKOLEM!) (("2" (PREFIX) (("2" (PREFIX) (("1" (EXPAND "R1" +) (("1" (DELETE -2 2 3) (("1" (LEMMA "na_prop" ("l" "i!1")) (("1" (GRIND) (("1" (DECOMPOSE-EQUALITY -2) NIL NIL) ("2" (DECOMPOSE-EQUALITY -2) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (PREFIX) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|rank_user_b| "" (INIT-CSP "Identity" "message") (("" (EXPAND "userB") (("" (AUTO-REWRITE "userB_TCC1") (("" (REWRITE "restriction_fix2") (("" (DELETE 2) (("" (SKOSIMP*) (("" (EXPAND "Fb") (("" (LIFT-IF) (("" (PROP) (("1" (REWRITE "restriction_choice3") (("1" (REWRITE "rank_user_choice3[message, Identity, message]") (("1" (SKOLEM!) (("1" (PREFIX) (("1" (PREFIX) (("1" (DELETE -3 2 3) (("1" (GRIND) NIL NIL)) NIL) ("2" (PREFIX) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CHOICE) (("1" (REWRITE "restriction_choice3") (("1" (REWRITE "rank_user_choice3[[Identity, (nonce?)], Identity, message]") (("1" (SKOLEM!) (("1" (NAME-REPLACE "j!1" "PROJ_1(i!2)") (("1" (NAME-REPLACE "x!1" "PROJ_2(i!2)") (("1" (PREFIX) (("1" (DELETE -1 2) (("1" (LEMMA "nb_prop" ("l" "i!1")) (("1" (ASSERT) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (PREFIX) (("2" (PREFIX) (("1" (DELETE -2 2 3 4) (("1" (LEMMA "nb_prop" ("l" "i!1")) (("1" (ASSERT) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "restriction_choice3") (("2" (REWRITE "rank_user_choice3[[Identity, message], Identity, message]") (("2" (SKOLEM!) (("2" (NAME-REPLACE "j!1" "PROJ_1(i!2)") (("2" (NAME-REPLACE "x!1" "PROJ_2(i!2)") (("2" (PREFIX) (("2" (PREFIX) (("1" (DELETE -2 2 3) (("1" (LEMMA "nb_prop" ("l" "i!1")) (("1" (ASSERT) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (PREFIX) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|authentication_origin| "" (USE "authentication_by_rank2" ("rho" "rho")) (("" (GROUND) (("1" (REWRITE "rank_init") NIL NIL) ("2" (USE "validity_rho") NIL NIL) ("3" (REWRITE "nonpositive_rank") NIL NIL) ("4" (REWRITE "interface_userA") NIL NIL) ("5" (REWRITE "rank_user_a") NIL NIL) ("6" (REWRITE "interface_userB") NIL NIL) ("7" (REWRITE "rank_user_b") NIL NIL)) NIL)) NIL)) $$$lowe.pvs % % The Needham Schroeder Protocol: origin authentication % with Lowe's fix % lowe : THEORY BEGIN IMPORTING messages IMPORTING network[Identity, message, |-] %% event : TYPE = network[Identity, message, |-].event i, j : VAR Identity x, y, m : VAR message xn : VAR (nonce?) k : VAR key e : VAR event n : VAR int v : VAR Nonce S : VAR set[message] %-------------------------------- % identities of the two agents %-------------------------------- a : Identity b : { i | i /= a } %----------------------- % Nonces for a and b %----------------------- na : Nonce nb : { v | v /= na } %----------------- % Abbreviations %----------------- Ia : (user?) = user(a) Ib : (user?) = user(b) Na : (nonce?) = nonce(na) Nb : (nonce?) = nonce(nb) pub(i, x) : message = crypto(public(i), x) sec(i, x) : message = crypto(secret(i), x) conc3(x, y, m) : message = conc(conc(x, y), m) %========================== % Protocol Participants %========================== %-------------------------------- % userA : can recognize nonces %-------------------------------- userA : process[event] = Choice! i, xn : ( trans(a, i, pub(i, conc(Na, Ia))) >> ( rec(a, i, pub(a, conc3(Na, xn, user(i)))) >> ( trans(a, i, pub(i, xn)) >> Stop[event] ))) interface_userA : LEMMA subset?(sigma(userA), LocalEvents(a)) %--------- % userB %--------- userB : process[event] = Choice! y: ( rec(b, a, pub(b, conc(y, Ia))) >> ( trans(b, a, pub(a, conc3(y, Nb, Ib))) >> ( rec(b, a, pub(b, Nb)) >> Stop[event] ))) interface_userB : LEMMA subset?(sigma(userB), LocalEvents(b)) %=============================================================== % INIT set: nonce Nb and secret keys of A and B are not known %=============================================================== INIT_nonce : set[message] = { m | EXISTS v : v /= nb AND m = nonce(v) } INIT_secret : set[message] = { m | EXISTS i : i /= a AND i /= b AND m = secret(i) } INIT : set[message] = { m | user?(m) OR text?(m) OR public?(m) OR INIT_nonce(m) OR INIT_secret(m) } %====================================== % Origin authentication (property 5) %====================================== T1 : set[event] = { e | e = rec(b, a, pub(b, Nb)) } R1 : set[event] = { e | e = trans(a, b, pub(b, Nb)) } %----------------- % Rank function %----------------- rank_code(k, m, n) : int = CASES k OF public(j) : IF j = a AND (EXISTS x : m = conc3(x, Nb, Ib)) THEN 1 ELSE n ENDIF, secret(j) : IF j = a AND (EXISTS x : m = pub(a, conc3(x, Nb, Ib))) THEN 0 ELSE n ENDIF ENDCASES rho(m) : RECURSIVE int = CASES m OF text(z) : 1, nonce(z) : IF z = nb THEN 0 ELSE 1 ENDIF, user(z) : 1, public(z) : 1, secret(z) : IF z = a OR z = b THEN 0 ELSE 1 ENDIF, conc(z1, z2) : min(rho(z1), rho(z2)), code(k, z) : rank_code(k, z, rho(z)) ENDCASES MEASURE size(m) %---------------------- % Constraints on rho %---------------------- validity_rho : LEMMA FORALL S, m : positive(rho, S) AND (S |- m) IMPLIES rho(m) > 0 rank_init : LEMMA positive(rho, INIT) nonpositive_rank : LEMMA non_positive(rho, T1) %------------------- % User properties %------------------- IMPORTING rank_rules2, rank_rules3 rank_user_a : LEMMA userA # R1 |> RankUser(rho) rank_user_b : LEMMA userB # R1 |> RankUser(rho) %---------------- % Consequence %---------------- authentication_origin : PROPOSITION network(enemy(INIT), protocol(a, b, userA, userB)) |> auth(T1, R1) END lowe $$$lowe.prf (|lowe| (|IMP_network_TCC1| "" (LEMMA "gen_monotonic2") (("" (PROPAX) NIL NIL)) NIL) (|b_TCC1| "" (INST + "a+1") NIL NIL) (|nb_TCC1| "" (INST + "na +1") NIL NIL) (|interface_userA| "" (AUTO-REWRITE "local_transmission" "local_reception" "interface_pref[event]" "interface_stop[event]") (("" (EXPAND "userA") (("" (REWRITE "interface_choice3") NIL NIL)) NIL)) NIL) (|interface_userB| "" (AUTO-REWRITE "local_transmission" "local_reception" "interface_pref[event]" "interface_stop[event]") (("" (EXPAND "userB") (("" (REWRITE "interface_choice3") NIL NIL)) NIL)) NIL) (|rank_code_TCC1| "" (GRIND) NIL NIL) (|rho_TCC1| "" (GRIND) NIL NIL) (|rho_TCC2| "" (GRIND) NIL NIL) (|rho_TCC3| "" (GRIND) NIL NIL) (|validity_rho| "" (REWRITE "rank_valid") (("1" (DELETE 2) (("1" (GRIND) NIL NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND :IF-MATCH NIL) (("2" (INST + "x!2") NIL NIL)) NIL)) NIL)) NIL) (|rank_init| "" (GRIND) NIL NIL) (|nonpositive_rank| "" (GRIND) NIL NIL) (|rank_user_a| "" (INIT-CSP "Identity" "message") (("" (EXPAND "userA") (("" (REWRITE "restriction_choice3") (("" (REWRITE "rank_user_choice3[[Identity, (nonce?)], Identity, message]") (("" (SKOLEM!) (("" (NAME-REPLACE "i!2" "PROJ_1(i!1)") (("" (NAME-REPLACE "nx!1" "PROJ_2(i!1)") (("" (PREFIX) (("1" (DELETE 2) (("1" (GRIND) NIL NIL)) NIL) ("2" (PREFIX) (("2" (PREFIX) (("2" (EXPAND "R1") (("2" (DELETE 3 4) (("2" (CASE "i!2 = b AND nx!1 = Nb") (("1" (GROUND) NIL NIL) ("2" (GROUND) (("1" (DELETE 2) (("1" (GRIND) (("1" (DECOMPOSE-EQUALITY -2) (("1" (DECOMPOSE-EQUALITY -2) NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND) (("2" (APPLY-EXTENSIONALITY) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|rank_user_b| "" (INIT-CSP "Identity" "message") (("" (EXPAND "userB") (("" (REWRITE "restriction_choice3") (("" (REWRITE "rank_user_choice3[message, Identity, message]") (("" (SKOLEM!) (("" (PREFIX) (("" (PREFIX) (("1" (DELETE 2 3) (("1" (GRIND) NIL NIL)) NIL) ("2" (PREFIX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|authentication_origin| "" (USE "authentication_by_rank2" ("rho" "rho")) (("" (GROUND) (("1" (REWRITE "rank_init") NIL NIL) ("2" (USE "validity_rho") NIL NIL) ("3" (REWRITE "nonpositive_rank") NIL NIL) ("4" (REWRITE "interface_userA") NIL NIL) ("5" (REWRITE "rank_user_a") NIL NIL) ("6" (REWRITE "interface_userB") NIL NIL) ("7" (REWRITE "rank_user_b") NIL NIL)) NIL)) NIL)) $$$needham_schroeder2.pvs % % The Needham Schroeder Protocol: Responder Authentication % needham_schroeder2 : THEORY BEGIN IMPORTING messages IMPORTING network[Identity, message, |-] i, j : VAR Identity x, y, m : VAR message xn : VAR (nonce?) k : VAR key e : VAR event n : VAR int v : VAR Nonce S : VAR set[message] %-------------------------------- % identities of the two agents %-------------------------------- a : Identity b : { i | i /= a } %----------------------- % Nonces for a and b %----------------------- na : Nonce nb : { v | v /= na } %----------------- % Abbreviations %----------------- Ia : (user?) = user(a) Ib : (user?) = user(b) Na : (nonce?) = nonce(na) Nb : (nonce?) = nonce(nb) pub(i, x) : message = crypto(public(i), x) sec(i, x) : message = crypto(secret(i), x) %========================= % Protocol Participants %========================= %--------------------------------------- % userA: initiates a transaction with B %--------------------------------------- userA : process[event] = Choice! xn : ( trans(a, b, pub(b, conc(Na, Ia))) >> ( rec(a, b, pub(a, conc(Na, xn))) >> ( trans(a, b, pub(b, xn)) >> Stop[event] ))) interface_userA : LEMMA subset?(sigma(userA), LocalEvents(a)) %--------- % userB %--------- userB : process[event] = Choice! j, y: ( rec(b, j, pub(b, conc(y, user(j)))) >> ( trans(b, j, pub(j, conc(y, Nb))) >> ( rec(b, j, pub(b, Nb)) >> Stop[event] ))) interface_userB : LEMMA subset?(sigma(userB), LocalEvents(b)) %=============================================================== % INIT set: nonce Na and secret keys of A and B are not known %=============================================================== INIT_nonce : set[message] = { m | EXISTS v : v /= na AND m = nonce(v) } INIT_secret : set[message] = { m | EXISTS i : i /= a AND i /= b AND m = secret(i) } INIT : set[message] = { m | user?(m) OR text?(m) OR public?(m) OR INIT_nonce(m) OR INIT_secret(m) } %========================= % Authentication events %========================= T1 : set[event] = { e | EXISTS xn : e = rec(a, b, pub(a, conc(Na, xn))) } R1 : set[event] = { e | EXISTS xn : e = trans(b, a, pub(a, conc(Na, xn))) } %------------------------------ % Variant: stronger property %------------------------------ T1(xn): set[event] = { e | e = rec(a, b, pub(a, conc(Na, xn))) } R1(xn): set[event] = { e | e = trans(b, a, pub(a, conc(Na, xn))) } %----------------- % Rank function %---------------- % auxiliary function % the rank of code(k, m) assuming the rank of m is n rank_code(k, m, n) : int = CASES k OF public(j) : IF j = b AND m = conc(Na, Ia) THEN 1 ELSE n ENDIF, secret(j) : IF j = b AND m = pub(b, conc(Na, Ia)) THEN 0 ELSE n ENDIF ENDCASES rho(m) : RECURSIVE int = CASES m OF text(z) : 1, nonce(z) : IF z = na THEN 0 ELSE 1 ENDIF, user(z) : 1, public(z) : 1, secret(z) : IF z = a OR z = b THEN 0 ELSE 1 ENDIF, conc(z1, z2) : min(rho(z1), rho(z2)), code(k, z) : rank_code(k, z, rho(z)) ENDCASES MEASURE size(m) %---------------------- % Constraints on rho %---------------------- validity_rho : LEMMA FORALL S, m : positive(rho, S) AND (S |- m) IMPLIES rho(m) > 0 rank_init : LEMMA positive(rho, INIT) nonpositive_rank : LEMMA non_positive(rho, T1) nonpositive_rank2: LEMMA non_positive(rho, T1(xn)) %-------------------- % User constraints %-------------------- IMPORTING rank_rules2, rank_rules3 rank_user_a : LEMMA userA # R1 |> RankUser(rho) rank_user_b : LEMMA userB # R1 |> RankUser(rho) rank_user_a2: LEMMA userA # R1(Nb) |> RankUser(rho) rank_user_b2: LEMMA userB # R1(Nb) |> RankUser(rho) %--------------------------- % authentication property %--------------------------- responder_authentication : PROPOSITION network(enemy(INIT), protocol(a, b, userA, userB)) |> auth(T1, R1) END needham_schroeder2 $$$needham_schroeder2.prf (|needham_schroeder2| (|IMP_network_TCC1| "" (LEMMA "gen_monotonic2") (("" (PROPAX) NIL NIL)) NIL) (|b_TCC1| "" (INST + "a + 1") NIL NIL) (|nb_TCC1| "" (INST + "na+1") NIL NIL) (|interface_userA| "" (AUTO-REWRITE "local_transmission" "local_reception" "interface_pref[event]" "interface_stop[event]") (("" (EXPAND "userA") (("" (REWRITE "interface_choice3") NIL NIL)) NIL)) NIL) (|interface_userB| "" (AUTO-REWRITE "local_transmission" "local_reception" "interface_pref[event]" "interface_stop[event]") (("" (EXPAND "userB") (("" (REWRITE "interface_choice3") NIL NIL)) NIL)) NIL) (|rank_code_TCC1| "" (GRIND) NIL NIL) (|rho_TCC1| "" (GRIND) NIL NIL) (|rho_TCC2| "" (GRIND) NIL NIL) (|rho_TCC3| "" (GRIND) NIL NIL) (|validity_rho| "" (REWRITE "rank_valid") (("1" (DELETE 2) (("1" (GRIND) NIL NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL)) NIL) (|rank_init| "" (GRIND) NIL NIL) (|nonpositive_rank| "" (GRIND) NIL NIL) (|nonpositive_rank2| "" (GRIND) NIL NIL) (|rank_user_a| "" (INIT-CSP "Identity" "message") (("" (EXPAND "userA") (("" (REWRITE "restriction_choice3") (("" (REWRITE "rank_user_choice3[(nonce?), Identity, message]") (("" (SKOLEM!) (("" (PREFIX) (("1" (DELETE 2) (("1" (GRIND) NIL NIL)) NIL) ("2" (PREFIX) (("2" (PREFIX) (("2" (DELETE 1 3 4) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|rank_user_b| "" (INIT-CSP "Identity" "message") (("" (EXPAND "userB") (("" (REWRITE "restriction_choice3") (("" (REWRITE "rank_user_choice3[[Identity, message], Identity, message]") (("" (SKOLEM!) (("" (PREFIX) (("" (PREFIX) (("1" (DELETE 3) (("1" (GRIND) (("1" (DELETE 1 2 3) (("1" (DECOMPOSE-EQUALITY) (("1" (DECOMPOSE-EQUALITY -2) (("1" (INST + "nonce(nb)") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 1 2 3) (("2" (DECOMPOSE-EQUALITY -1) (("2" (DECOMPOSE-EQUALITY -2) (("2" (INST + "nonce(nb)") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (PREFIX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|rank_user_a2| "" (INIT-CSP "Identity" "message") (("" (EXPAND "userA") (("" (REWRITE "restriction_choice3") (("" (REWRITE "rank_user_choice3[(nonce?), Identity, message]") (("" (SKOLEM!) (("" (PREFIX) (("1" (DELETE 2) (("1" (GRIND) NIL NIL)) NIL) ("2" (PREFIX) (("2" (PREFIX) (("2" (DELETE 1 3 4) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|rank_user_b2| "" (INIT-CSP "Identity" "message") (("" (EXPAND "userB") (("" (REWRITE "restriction_choice3") (("" (REWRITE "rank_user_choice3[[Identity, message], Identity, message]") (("" (SKOLEM!) (("" (PREFIX) (("" (PREFIX) (("1" (DELETE 3) (("1" (GRIND) (("1" (DELETE 1 2 3) (("1" (DECOMPOSE-EQUALITY -1) (("1" (DECOMPOSE-EQUALITY -2) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (DECOMPOSE-EQUALITY -1) (("2" (DECOMPOSE-EQUALITY -2) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (PREFIX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|responder_authentication| "" (USE "authentication_by_rank2" ("rho" "rho")) (("" (GROUND) (("1" (REWRITE "rank_init") NIL NIL) ("2" (USE "validity_rho") NIL NIL) ("3" (REWRITE "nonpositive_rank") NIL NIL) ("4" (REWRITE "interface_userA") NIL NIL) ("5" (REWRITE "rank_user_a") NIL NIL) ("6" (REWRITE "interface_userB") NIL NIL) ("7" (REWRITE "rank_user_b") NIL NIL)) NIL)) NIL)) $$$rank_rules3.pvs % % Rules for rank_user. Multiple parallel product % rank_rules3 [ U : NONEMPTY_TYPE, Identity, Message : TYPE ] : THEORY BEGIN IMPORTING rank_rules[Identity, Message] P : VAR [U -> process[event]] i : VAR U A : VAR set[event] rho : VAR [Message -> int] rank_user_par2 : LEMMA (FORALL i : P(i) |> RankUser(rho)) IMPLIES Par(A)(P) |> RankUser(rho) rank_user_free_par2 : LEMMA Interleave(P) |> RankUser(rho) IFF FORALL i : P(i) |> RankUser(rho) END rank_rules3 $$$rank_rules3.prf (|rank_rules3| (|rank_user_par2| "" (AUTO-REWRITE "pos_rec" "pos_trans" "receptions" "transmissions" "RankUser" "Par" "|>" "subset?" "member" "union" "intersection") (("" (SKOSIMP) (("" (ASSERT) (("" (SKOSIMP*) (("" (EXPAND "positive") (("" (FORWARD-CHAIN "sigma_multiprod") (("" (AUTO-REWRITE "sigma_proj[event]") (("" (CASE "FORALL i : positive(rho!1, sigma(proj(t!1(i), trans?)))") (("1" (ASSERT) (("1" (REPLACE -2 +) (("1" (DELETE -2 -3 -4 -5) (("1" (EXPAND "union") (("1" (EXPAND "positive") (("1" (REDUCE) NIL))))))))))) ("2" (SKOLEM!) (("2" (INST - "i!1" "t!1(i!1)") (("2" (ASSERT) (("2" (DELETE -2 1 3) (("2" (REPLACE*) (("2" (EXPAND "union") (("2" (EXPAND "positive") (("2" (REDUCE) NIL))))))))))))))))))))))))))))))) (|rank_user_free_par2| "" (SKOLEM!) (("" (GROUND) (("1" (SKOLEM!) (("1" (REWRITE "sat_free_par3" +) NIL))) ("2" (EXPAND "Interleave") (("2" (REWRITE "rank_user_par2") NIL)))))))) $$$rank_rules2.pvs % % Rules for rank_user. Parametric processes % rank_rules2 [ U : TYPE, Identity, Message : TYPE ] : THEORY BEGIN IMPORTING rank_rules[Identity, Message] P : VAR [U -> process[event]] i : VAR U F : VAR (monotonic?[U, event]) rho : VAR [Message -> int] rank_user_choice3 : LEMMA Choice(P) |> RankUser(rho) IFF FORALL i : P(i) |> RankUser(rho) rank_user_choice3_var : LEMMA (Choice! i: P(i)) |> RankUser(rho) IFF FORALL i : P(i) |> RankUser(rho) rank_user_fix2 : LEMMA (FORALL P : (FORALL i : P(i) |> RankUser(rho)) => (FORALL i : F(P)(i) |> RankUser(rho))) IMPLIES FORALL i : mu(F)(i) |> RankUser(rho) END rank_rules2 $$$rank_rules2.prf (|rank_rules2| (|rank_user_choice3| "" (SKOLEM!) (("" (REWRITE "sat_choice3") (("" (GROUND) (("" (REWRITE "rank_user_stop") NIL))))))) (|rank_user_choice3_var| "" (SKOLEM!) (("" (REWRITE "rank_user_choice3") NIL))) (|rank_user_fix2| "" (SKOSIMP) (("" (REWRITE "param_induction") (("" (SKOLEM!) (("" (REWRITE "rank_user_stop") NIL)))))))) $$$rank_rules.pvs % % Definition of the rank predicates for users and enemy % + Specialized proof rules % rank_rules [ Identity, Message : TYPE ] : THEORY BEGIN IMPORTING csp_traces, csp_rules IMPORTING rank_functions[Identity, Message] i, j : VAR Identity m : VAR Message rho : VAR [Message -> int] A : VAR set[event] tr : VAR trace[event] P, P1, P2 : VAR process[event] SP : VAR set[process[event]] F : VAR (monotonic?[event]) %---------------------------------- % Rank constraint for the enemy %---------------------------------- RankEnemy(rho) : set[trace[event]] = { tr | pos_trans(rho, tr) IMPLIES pos_rec(rho, tr) } %------------------------------------------------------------- % Rank constraint for the processes "user(i)[| R |] Stop" %------------------------------------------------------------- RankUser(rho) : set[trace[event]] = { tr | pos_rec(rho, tr) IMPLIES pos_trans(rho, tr) } %--------------------------------- % Proof rules for RankUser(rho) %--------------------------------- rank_user_stop : LEMMA Stop[event] |> RankUser(rho) rank_user_choice : LEMMA (P1 \/ P2) |> RankUser(rho) IFF P1 |> RankUser(rho) AND P2 |> RankUser(rho) rank_user_choice2 : LEMMA Choice(SP) |> RankUser(rho) IFF FORALL (P : (SP)) : P |> RankUser(rho) rank_user_output : LEMMA (trans(i, j, m) >> P) |> RankUser(rho) IFF rho(m) > 0 AND P |> RankUser(rho) rank_user_input : LEMMA (rec(i, j, m) >> P) |> RankUser(rho) IFF (rho(m) > 0 IMPLIES P |> RankUser(rho)) rank_user_par : LEMMA P1 |> RankUser(rho) AND P2 |> RankUser(rho) IMPLIES Par(A)(P1, P2) |> RankUser(rho) rank_user_free_par : LEMMA P1 // P2 |> RankUser(rho) IFF P1 |> RankUser(rho) AND P2 |> RankUser(rho) rank_user_fix1 : LEMMA (FORALL P : P |> RankUser(rho) IMPLIES F(P) |> RankUser(rho)) IMPLIES mu(F) |> RankUser(rho) END rank_rules $$$rank_rules.prf (|rank_rules| (|rank_user_stop| "" (GRIND :EXCLUDE ("positive" "receptions" "transmissions") :REWRITES ("positive_null" "receptions_null" "transmissions_null")) NIL) (|rank_user_choice| "" (SKOLEM!) (("" (REWRITE "sat_choice1") NIL))) (|rank_user_choice2| "" (SKOLEM!) (("" (REWRITE "sat_choice2") (("" (GROUND) (("" (REWRITE "rank_user_stop") NIL))))))) (|rank_user_output| "" (SKOLEM!) (("" (GRIND :EXCLUDE ("positive" "receptions" "transmissions") :REWRITES ("positive_null" "receptions_null" "transmissions_null" "positive_cons" "receptions_cons1" "receptions_cons2" "transmissions_cons1" "transmissions_cons2") :IF-MATCH NIL) (("1" (INST - "cons(trans(i!1, j!1, m!1), x!1)") (("1" (GROUND) (("1" (INST?) NIL))))) ("2" (INST - "cons(trans(i!1, j!1, m!1), null[event])") (("2" (GROUND) (("2" (INST?) NIL))))) ("3" (INST?) (("3" (ASSERT) NIL))) ("4" (INST?) (("4" (ASSERT) NIL))))))) (|rank_user_input| "" (SKOLEM!) (("" (GRIND :EXCLUDE ("positive" "receptions" "transmissions") :REWRITES ("positive_null" "receptions_null" "transmissions_null" "positive_cons" "receptions_cons1" "receptions_cons2" "transmissions_cons1" "transmissions_cons2") :IF-MATCH NIL) (("1" (INST - "cons(rec(i!1, j!1, m!1), x!1)") (("1" (GROUND) (("1" (INST?) NIL))))) ("2" (CASE-REPLACE "x!1 = null[event]") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))) ("3" (INST?) (("3" (ASSERT) NIL))) ("4" (CASE-REPLACE "x!1 = null[event]") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))) (|rank_user_par| "" (AUTO-REWRITE "pos_rec" "pos_trans" "receptions" "transmissions" "RankUser" "Par" "|>" "subset?" "member" "union" "intersection") (("" (SKOSIMP) (("" (ASSERT) (("" (SKOSIMP*) (("" (INST - "t1!1") (("" (INST - "t2!1") (("" (ASSERT) (("" (EXPAND "positive") (("" (FORWARD-CHAIN "sigma_prod") (("" (AUTO-REWRITE "sigma_proj[event]") (("" (CASE "positive(rho!1, sigma(proj(t1!1, rec?))) AND positive(rho!1, sigma(proj(t2!1, rec?)))") (("1" (GROUND) (("1" (REPLACE -5 +) (("1" (DELETE -3 -4 -5 -6 -7) (("1" (EXPAND "positive") (("1" (REDUCE) NIL))))))))) ("2" (DELETE -2 -3 -4 2) (("2" (GROUND) (("1" (EXPAND "positive") (("1" (REDUCE) NIL))) ("2" (EXPAND "positive") (("2" (REDUCE) NIL))))))))))))))))))))))))))))) (|rank_user_free_par| "" (SKOLEM!) (("" (GROUND) (("1" (FORWARD-CHAIN "sat_free_par1") NIL) ("2" (FORWARD-CHAIN "sat_free_par2") NIL) ("3" (EXPAND "//") (("3" (REWRITE "rank_user_par") NIL))))))) (|rank_user_fix1| "" (SKOSIMP) (("" (REWRITE "induction") (("" (REWRITE "rank_user_stop") NIL)))))) $$$users.pvs % % General User specification % % Parameters: % Identity : users' addresses % Message : messages exchanged % users [ Identity : NONEMPTY_TYPE, Message : TYPE ] : THEORY BEGIN IMPORTING event[Identity, Message], csp_traces i, j : VAR Identity m : VAR Message P : VAR process[event] tr : VAR trace[event] e : VAR event %--------------------------- % Interface of "user(i)" %--------------------------- LocalEvents(i) : setof[event] = { e | EXISTS m, j : e = trans(i, j, m) OR e = rec(i, j, m) } disjoint_events : LEMMA i /= j IMPLIES disjoint?(LocalEvents(i), LocalEvents(j)) local_transmission : LEMMA LocalEvents(i)(trans(i, j, m)) local_reception : LEMMA LocalEvents(i)(rec(i, j, m)) %------------------------------------------ % User process = parametric processes % which satisfy the Interface constraint %------------------------------------------ user_process : TYPE = [ i : Identity -> { P | subset?(sigma(P), LocalEvents(i)) } ] user : VAR user_process %----------------------------------------------------------------- % Local trace: tr of Compose(user) projected over LocalEvents(i) % is a trace of user(i) %----------------------------------------------------------------- disjoint_interfaces : LEMMA i /= j IMPLIES disjoint?(sigma(user(i)), sigma(user(j))) local_traces : LEMMA Interleave(user)(tr) IMPLIES user(i)(proj(tr, LocalEvents(i))) END users $$$users.prf (|users| (|disjoint_events| "" (AUTO-REWRITE-THEORY "sets[event]") (("" (EXPAND "LocalEvents") (("" (ASSERT) (("" (SKOSIMP*) (("" (GROUND) (("1" (CASE "t_snd(x!1) = j!1") (("1" (REPLACE -3) (("1" (ASSERT) NIL NIL)) NIL) ("2" (REPLACE -1) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (CASE "r_rcv(x!1) = j!1") (("1" (REPLACE -3) (("1" (ASSERT) NIL NIL)) NIL) ("2" (REPLACE -1) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|local_transmission| "" (GRIND) NIL NIL) (|local_reception| "" (GRIND) NIL NIL) (|disjoint_interfaces| "" (SKOSIMP) (("" (LEMMA "disjoint_events" ("i" "i!1" "j" "j!1")) (("" (ASSERT) (("" (TYPEPRED "user!1(i!1)" "user!1(j!1)") (("" (DELETE -1 -2 -4 -5 1) (("" (GRIND :DEFS NIL :THEORIES ("sets[event]")) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|local_traces| "" (SKOSIMP) (("" (LEMMA "disjoint_events") (("" (USE "interleave_disjoint[Identity, event]" ("P" "user!1")) (("" (GROUND) (("1" (EXPAND* "subset?" "member") (("1" (INST?) (("1" (ASSERT) (("1" (INST?) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$event_adt.pvs %%% ADT file generated from event event_adt[I: TYPE, M: TYPE]: THEORY BEGIN event: TYPE trans?, rec?: [event -> boolean] trans: [[I, I, M] -> (trans?)] t_snd: [(trans?) -> I] t_rcv: [(trans?) -> I] t_msg: [(trans?) -> M] rec: [[I, I, M] -> (rec?)] r_rcv: [(rec?) -> I] r_snd: [(rec?) -> I] r_msg: [(rec?) -> M] ord(x: event): upto(1) = CASES x OF trans(trans1_var, trans2_var, trans3_var): 0, rec(rec1_var, rec2_var, rec3_var): 1 ENDCASES event_trans_extensionality: AXIOM (FORALL (trans?_var: (trans?), trans?_var2: (trans?)): t_snd(trans?_var) = t_snd(trans?_var2) AND t_rcv(trans?_var) = t_rcv(trans?_var2) AND t_msg(trans?_var) = t_msg(trans?_var2) IMPLIES trans?_var = trans?_var2); event_trans_eta: AXIOM (FORALL (trans?_var: (trans?)): trans(t_snd(trans?_var), t_rcv(trans?_var), t_msg(trans?_var)) = trans?_var); event_rec_extensionality: AXIOM (FORALL (rec?_var: (rec?), rec?_var2: (rec?)): r_rcv(rec?_var) = r_rcv(rec?_var2) AND r_snd(rec?_var) = r_snd(rec?_var2) AND r_msg(rec?_var) = r_msg(rec?_var2) IMPLIES rec?_var = rec?_var2); event_rec_eta: AXIOM (FORALL (rec?_var: (rec?)): rec(r_rcv(rec?_var), r_snd(rec?_var), r_msg(rec?_var)) = rec?_var); event_t_snd_trans: AXIOM (FORALL (trans1_var: I, trans2_var: I, trans3_var: M): t_snd(trans(trans1_var, trans2_var, trans3_var)) = trans1_var); event_t_rcv_trans: AXIOM (FORALL (trans1_var: I, trans2_var: I, trans3_var: M): t_rcv(trans(trans1_var, trans2_var, trans3_var)) = trans2_var); event_t_msg_trans: AXIOM (FORALL (trans1_var: I, trans2_var: I, trans3_var: M): t_msg(trans(trans1_var, trans2_var, trans3_var)) = trans3_var); event_r_rcv_rec: AXIOM (FORALL (rec1_var: I, rec2_var: I, rec3_var: M): r_rcv(rec(rec1_var, rec2_var, rec3_var)) = rec1_var); event_r_snd_rec: AXIOM (FORALL (rec1_var: I, rec2_var: I, rec3_var: M): r_snd(rec(rec1_var, rec2_var, rec3_var)) = rec2_var); event_r_msg_rec: AXIOM (FORALL (rec1_var: I, rec2_var: I, rec3_var: M): r_msg(rec(rec1_var, rec2_var, rec3_var)) = rec3_var); event_inclusive: AXIOM (FORALL (event_var: event): trans?(event_var) OR rec?(event_var)); event_induction: AXIOM (FORALL (p: [event -> boolean]): (FORALL (trans1_var: I, trans2_var: I, trans3_var: M): p(trans(trans1_var, trans2_var, trans3_var))) AND (FORALL (rec1_var: I, rec2_var: I, rec3_var: M): p(rec(rec1_var, rec2_var, rec3_var))) IMPLIES (FORALL (event_var: event): p(event_var))); every(p1: PRED[I], p2: PRED[M])(a: event): boolean = CASES a OF trans(trans1_var, trans2_var, trans3_var): p1(trans1_var) AND p1(trans2_var) AND p2(trans3_var), rec(rec1_var, rec2_var, rec3_var): p1(rec1_var) AND p1(rec2_var) AND p2(rec3_var) ENDCASES; every(p1: PRED[I], p2: PRED[M], a: event): boolean = CASES a OF trans(trans1_var, trans2_var, trans3_var): p1(trans1_var) AND p1(trans2_var) AND p2(trans3_var), rec(rec1_var, rec2_var, rec3_var): p1(rec1_var) AND p1(rec2_var) AND p2(rec3_var) ENDCASES; some(p1: PRED[I], p2: PRED[M])(a: event): boolean = CASES a OF trans(trans1_var, trans2_var, trans3_var): p1(trans1_var) OR p1(trans2_var) OR p2(trans3_var), rec(rec1_var, rec2_var, rec3_var): p1(rec1_var) OR p1(rec2_var) OR p2(rec3_var) ENDCASES; some(p1: PRED[I], p2: PRED[M], a: event): boolean = CASES a OF trans(trans1_var, trans2_var, trans3_var): p1(trans1_var) OR p1(trans2_var) OR p2(trans3_var), rec(rec1_var, rec2_var, rec3_var): p1(rec1_var) OR p1(rec2_var) OR p2(rec3_var) ENDCASES; subterm(x: event, y: event): boolean = x = y; <<(x: event, y: event): boolean = FALSE; event_well_founded: AXIOM well_founded?[event](<<); reduce_nat(trans?_fun: [[I, I, M] -> nat], rec?_fun: [[I, I, M] -> nat]): [event -> nat] = LAMBDA (event_adtvar: event): CASES event_adtvar OF trans(trans1_var, trans2_var, trans3_var): trans?_fun(trans1_var, trans2_var, trans3_var), rec(rec1_var, rec2_var, rec3_var): rec?_fun(rec1_var, rec2_var, rec3_var) ENDCASES; REDUCE_nat(trans?_fun: [[I, I, M, event] -> nat], rec?_fun: [[I, I, M, event] -> nat]): [event -> nat] = LAMBDA (event_adtvar: event): CASES event_adtvar OF trans(trans1_var, trans2_var, trans3_var): trans?_fun(trans1_var, trans2_var, trans3_var, event_adtvar), rec(rec1_var, rec2_var, rec3_var): rec?_fun(rec1_var, rec2_var, rec3_var, event_adtvar) ENDCASES; reduce_ordinal(trans?_fun: [[I, I, M] -> ordinal], rec?_fun: [[I, I, M] -> ordinal]): [event -> ordinal] = LAMBDA (event_adtvar: event): CASES event_adtvar OF trans(trans1_var, trans2_var, trans3_var): trans?_fun(trans1_var, trans2_var, trans3_var), rec(rec1_var, rec2_var, rec3_var): rec?_fun(rec1_var, rec2_var, rec3_var) ENDCASES; REDUCE_ordinal(trans?_fun: [[I, I, M, event] -> ordinal], rec?_fun: [[I, I, M, event] -> ordinal]): [event -> ordinal] = LAMBDA (event_adtvar: event): CASES event_adtvar OF trans(trans1_var, trans2_var, trans3_var): trans?_fun(trans1_var, trans2_var, trans3_var, event_adtvar), rec(rec1_var, rec2_var, rec3_var): rec?_fun(rec1_var, rec2_var, rec3_var, event_adtvar) ENDCASES; END event_adt event_adt_map[I: TYPE, M: TYPE, I1: TYPE, M1: TYPE]: THEORY BEGIN IMPORTING event_adt map(f1: [I -> I1], f2: [M -> M1])(a: event[I, M]): event[I1, M1] = CASES a OF trans(trans1_var, trans2_var, trans3_var): trans(f1(trans1_var), f1(trans2_var), f2(trans3_var)), rec(rec1_var, rec2_var, rec3_var): rec(f1(rec1_var), f1(rec2_var), f2(rec3_var)) ENDCASES; map(f1: [I -> I1], f2: [M -> M1], a: event[I, M]): event[I1, M1] = CASES a OF trans(trans1_var, trans2_var, trans3_var): trans(f1(trans1_var), f1(trans2_var), f2(trans3_var)), rec(rec1_var, rec2_var, rec3_var): rec(f1(rec1_var), f1(rec2_var), f2(rec3_var)) ENDCASES; END event_adt_map event_adt_reduce[I: TYPE, M: TYPE, range: TYPE]: THEORY BEGIN IMPORTING event_adt[I, M] reduce(trans?_fun: [[I, I, M] -> range], rec?_fun: [[I, I, M] -> range]): [event -> range] = LAMBDA (event_adtvar: event): CASES event_adtvar OF trans(trans1_var, trans2_var, trans3_var): trans?_fun(trans1_var, trans2_var, trans3_var), rec(rec1_var, rec2_var, rec3_var): rec?_fun(rec1_var, rec2_var, rec3_var) ENDCASES; REDUCE(trans?_fun: [[I, I, M, event] -> range], rec?_fun: [[I, I, M, event] -> range]): [event -> range] = LAMBDA (event_adtvar: event): CASES event_adtvar OF trans(trans1_var, trans2_var, trans3_var): trans?_fun(trans1_var, trans2_var, trans3_var, event_adtvar), rec(rec1_var, rec2_var, rec3_var): rec?_fun(rec1_var, rec2_var, rec3_var, event_adtvar) ENDCASES; END event_adt_reduce $$$enemy.pvs % % Definition of the enemy % % Parameters: % Identity : users' addresses % Message : messages exchanged % |- : message generation predicate % S |- m means "m can be generated from S" % enemy[ Identity, Message : TYPE, |- : [set[Message], Message -> bool] ] : THEORY BEGIN IMPORTING event[Identity, Message], csp_traces i, j : VAR Identity m : VAR Message %-------------- % Definition %-------------- X : VAR [set[Message] -> process[event]] S : VAR set[Message] F(X)(S) : process[event] = (Choice! i, j, m : trans(i, j, m) >> X(add(m, S))) \/ (Choice! i, j, (m | (S |- m)) : rec(i, j, m) >> X(S)) enemy : [set[Message] -> process[event]] = mu(F) enemy_def : THEOREM enemy(S) = ( (Choice! i, j, m : trans(i, j, m) >> enemy(add(m, S))) \/ (Choice! i, j, (m | S |- m) : rec(i, j, m) >> enemy(S)) ) END enemy $$$enemy.prf (|enemy| (|enemy_TCC1| "" (GRIND :EXCLUDE "add") NIL) (|enemy_def| "" (EXPAND "enemy") (("" (SKOLEM!) (("" (AUTO-REWRITE "enemy_TCC1") (("" (USE "fixed_point" ("G" "F")) (("" (REPLACE -1 + RL) (("" (EXPAND "F" 1 1) (("" (ASSERT) NIL)))))))))))))) $$$monotonicity3.pvs % % Monotonicity rules for indexed parallel composition % monotonicity3 [ U : NONEMPTY_TYPE, T : TYPE ] : THEORY BEGIN IMPORTING csp_traces P, Q : VAR [U -> process[T]] A : VAR set[T] i : VAR U monotonic_par2 : LEMMA (FORALL i : subset?(P(i), Q(i))) IMPLIES subset?(Par[U,T](A)(P), Par[U,T](A)(Q)) monotonic_free_par2 : LEMMA (FORALL i : subset?(P(i), Q(i))) IMPLIES subset?(Interleave(P), Interleave(Q)) END monotonicity3 $$$monotonicity3.prf (|monotonicity3| (|monotonic_par2| "" (GRIND :EXCLUDE ("prefix_closed")) (("" (INST + "t!1") (("" (REDUCE) NIL))))) (|monotonic_free_par2| "" (SKOSIMP) (("" (EXPAND "Interleave") (("" (REWRITE "monotonic_par2") NIL)))))) $$$monotonicity2.pvs % % Monotonicity for parametric choice % monotonicity2 [U, T: TYPE] : THEORY BEGIN IMPORTING csp_traces P, Q : VAR [U -> process[T]] i : VAR U monotonic_choice3 : LEMMA (FORALL i : subset?(P(i), Q(i))) IMPLIES subset?(Choice(P), Choice(Q)) END monotonicity2 $$$monotonicity2.prf (|monotonicity2| (|monotonic_choice3| "" (GRIND :EXCLUDE ("prefix_closed")) NIL)) $$$monotonicity.pvs % % Monotonicity of process operators % monotonicity [ T : TYPE ] : THEORY BEGIN IMPORTING csp_traces P, P1, P2, Q, Q1, Q2 : VAR process[T] SP, SQ : VAR set[process[T]] a : Var T A : VAR set[T] monotonic_stop : LEMMA subset?(Stop[T], P) monotonic_pref : LEMMA subset?(a >> P, a >> Q) IFF subset?(P, Q) monotonic_choice : LEMMA subset?(P1, Q1) AND subset?(P2, Q2) IMPLIES subset?(P1 \/ P2, Q1 \/ Q2) monotonic_choice2 : LEMMA (FORALL (P : (SP)) : EXISTS (Q : (SQ)) : subset?(P, Q)) IMPLIES subset?(Choice(SP), Choice(SQ)) monotonic_par : LEMMA subset?(P1, Q1) AND subset?(P2, Q2) IMPLIES subset?(Par(A)(P1, P2), Par(A)(Q1, Q2)) monotonic_free_par : LEMMA subset?(P1, Q1) AND subset?(P2, Q2) IMPLIES subset?(P1 // P2, Q1 // Q2) END monotonicity $$$monotonicity.prf (|monotonicity| (|monotonic_stop| "" (LEMMA "stop_subset[T]") (("" (PROPAX) NIL))) (|monotonic_pref| "" (SKOLEM!) (("" (GRIND :IF-MATCH NIL) (("1" (INST - "cons(a!1, x!1)") (("1" (GROUND) (("1" (SKOLEM!) (("1" (CASE "cdr(cons(a!1, x!1)) = t1!1") (("1" (ASSERT) NIL) ("2" (REPLACE -1) (("2" (ASSERT) NIL))))))) ("2" (INST?) NIL))))) ("2" (INST?) (("2" (INST?) (("2" (ASSERT) NIL))))))))) (|monotonic_choice| "" (SKOSIMP) (("" (GRIND) NIL))) (|monotonic_choice2| "" (GRIND :EXCLUDE ("prefix_closed") :IF-MATCH NIL) (("" (INST? -) (("" (SKOLEM!) (("" (INST - "x!1") (("" (ASSERT) (("" (INST + "Q!1") NIL))))))))))) (|monotonic_par| "" (SKOSIMP) (("" (GRIND) NIL))) (|monotonic_free_par| "" (SKOSIMP) (("" (EXPAND "//") (("" (REWRITE "monotonic_par") NIL)))))) $$$authentication3.pvs % % Authentication rules: multiple parallel composition % authentication3 [ U : NONEMPTY_TYPE, T : TYPE ] : THEORY BEGIN IMPORTING csp_traces, authentication P : VAR [U -> process[T]] A, B, C : VAR set[T] i : VAR U authentication_par3 : LEMMA (FORALL i : P(i) |> auth(A, B)) IMPLIES Par(C)(P) |> auth(A, B) authentication_par4 : LEMMA P(i) |> auth(A, B) AND subset?(A, C) IMPLIES Par(C)(P) |> auth(A, B) authentication_free_par2 : LEMMA (FORALL i : P(i) |> auth(A, B)) IMPLIES Interleave(P) |> auth(A, B) END authentication3 $$$authentication3.prf (|authentication3| (|authentication_par3| "" (EXPAND* "|>" "auth" "subset?" "member" "Par") (("" (SKOSIMP*) (("" (USE "null_proj_multiprod[U, T]" ("t" "t!1")) (("" (ASSERT) (("" (USE "null_proj_multiprod[U, T]" ("B" "A!1" "t" "t!1")) (("" (ASSERT) (("" (SKOLEM!) (("" (INST?) (("" (INST - "i!1" "t!1(i!1)") (("" (ASSERT) NIL))))))))))))))))))) (|authentication_par3_bug| "" (GRIND :EXCLUDE ("prod" "proj") :IF-MATCH NIL) (("" (USE "null_proj_multiprod[U, T]" ("t" "t!1")) (("" (ASSERT) (("" (USE "null_proj_multiprod[U, T]" ("B" "A!1" "t" "t!1")) (("" (ASSERT) (("" (SKOLEM!) (("" (INST?) (("" (INST - "i!1") (("" (INST - "t!1(i!1)") (("" (ASSERT) NIL))))))))))))))))))) (|authentication_par4| "" (SKOSIMP) (("" (AUTO-REWRITE-DEFS :ALWAYS? T) (("" (AUTO-REWRITE :NAMES ("subset?[trace[T]]")) (("" (STOP-REWRITE :NAMES ("prod" "proj" "subset?")) (("" (ASSERT) (("" (SKOLEM-TYPEPRED) (("" (FLATTEN) (("" (SKOLEM-TYPEPRED) (("" (ASSERT) (("" (USE "null_proj_multiprod[U, T]" ("t" "t!1")) (("" (ASSERT) (("" (INST?) (("" (INST - "t!1(i!1)") (("" (ASSERT) (("" (USE "null_proj_multiprod2[U, T]" ("B" "A!1" "t" "t!1")) (("" (ASSERT) NIL))))))))))))))))))))))))))))))) (|authentication_par4_bug| "" (SKOSIMP) (("" (GRIND :EXCLUDE ("prod" "proj" "subset?") :REWRITES ("subset?[trace[T]]") :IF-MATCH NIL) (("" (USE "null_proj_multiprod[U, T]" ("t" "t!1")) (("" (ASSERT) (("" (INST?) (("" (INST - "t!1(i!1)") (("" (ASSERT) (("" (USE "null_proj_multiprod2[U, T]" ("B" "A!1" "t" "t!1")) (("" (ASSERT) NIL))))))))))))))))) (|authentication_free_par2| "" (SKOSIMP) (("" (EXPAND "Interleave") (("" (REWRITE "authentication_par3") NIL)))))) $$$authentication2.pvs % % More rules for authentication % (parametric processes) % authentication2 [ U, T : TYPE ] : THEORY BEGIN IMPORTING csp_traces, authentication A, B : VAR set[T] P : VAR [U -> process[T]] F : VAR (monotonic?[U, T]) i : VAR U authentication_choice3 : LEMMA (FORALL i : P(i) |> auth(A, B)) IMPLIES (Choice! i : P(i)) |> auth(A, B) authentication_fix2 : LEMMA (FORALL P : (FORALL i : P(i) |> auth(A, B)) IMPLIES (FORALL i : F(P)(i) |> auth(A, B))) IMPLIES (FORALL i : mu(F)(i) |> auth(A, B)) END authentication2 $$$authentication2.prf (|authentication2| (|authentication_choice3| "" (SKOSIMP) (("" (REWRITE "sat_choice3") (("" (GROUND) (("" (REWRITE "authentication_stop") NIL))))))) (|authentication_fix2| "" (SKOSIMP) (("" (REWRITE "param_induction") (("" (SKOLEM!) (("" (REWRITE "authentication_stop") NIL)))))))) $$$authentication.pvs % % Definition of the property "A authenticates B" % and related proof rules (simple processes) % authentication [T : TYPE]: THEORY BEGIN IMPORTING csp_traces, restriction_rules A, B, C : VAR set[T] a, b, c : VAR T P, P1, P2 : VAR process[T] t, u, v : VAR trace[T] SP : VAR (nonempty?[process[T]]) F : VAR (monotonic?[T]) %-------------- % Definition %-------------- auth(A, B) : setof[trace[T]] = { t | proj(t, B) = null IMPLIES proj(t, A) = null } %-------------- % Properties %-------------- auth_subset1 : LEMMA subset?(B, A) IMPLIES subset?(auth(A, C), auth(B, C)) auth_subset2 : LEMMA subset?(B, C) IMPLIES subset?(auth(A, B), auth(A, C)) authentication_equiv : LEMMA P |> auth(A, B) IFF P # B |> { t | proj(t, A) = null } authentication_subset : LEMMA P |> auth(A, B) AND subset?(B, C) IMPLIES P |> auth(A, C) authentication_transitive : LEMMA P |> auth(A, B) AND P |> auth(B, C) IMPLIES P |> auth(A, C) %--------------- % Proof rules %--------------- authentication_stop : LEMMA Stop[T] |> auth(A, B) authentication_pref1 : LEMMA B(a) IMPLIES (a >> P) |> auth(A, B) authentication_pref2 : LEMMA P |> auth(A, B) AND not A(a) IMPLIES (a >> P) |> auth(A, B) authentication_choice : LEMMA P1 |> auth(A, B) AND P2 |> auth(A, B) IMPLIES (P1 \/ P2) |> auth(A, B) authentication_choice2 : LEMMA (FORALL (P : (SP)) : P |> auth(A, B)) IMPLIES Choice(SP) |> auth(A, B) authentication_par1 : LEMMA P1 |> auth(A, B) AND subset?(A, C) IMPLIES Par(C)(P1, P2) |> auth(A, B) authentication_par2 : LEMMA P2 |> auth(A, B) AND subset?(A, C) IMPLIES Par(C)(P1, P2) |> auth(A, B) authentication_par : LEMMA P1 |> auth(A, B) AND P2 |> auth(A, B) IMPLIES Par(C)(P1, P2) |> auth(A, B) authentication_free_par : LEMMA P1 |> auth(A, B) AND P2 |> auth(A, B) IMPLIES (P1 // P2) |> auth(A, B) authentication_fix1 : LEMMA (FORALL P : P |> auth(A, B) IMPLIES F(P) |> auth(A, B)) IMPLIES mu(F) |> auth(A, B) END authentication $$$authentication.prf (|authentication| (|auth_subset1| "" (SKOSIMP) (("" (EXPAND "subset?" +) (("" (EXPAND "member") (("" (EXPAND "auth") (("" (SKOSIMP) (("" (ASSERT) (("" (FORWARD-CHAIN "null_proj_subset") NIL))))))))))))) (|auth_subset2| "" (SKOSIMP) (("" (EXPAND "subset?" +) (("" (EXPAND "member") (("" (EXPAND "auth") (("" (SKOSIMP) (("" (ASSERT) (("" (FORWARD-CHAIN "null_proj_subset") NIL))))))))))))) (|authentication_equiv| "" (SKOLEM!) (("" (GRIND :EXCLUDE ("Par" "proj" "Stop") :REWRITES "restriction_equiv[T]" :IF-MATCH NIL) (("1" (INST?) (("1" (ASSERT) NIL))) ("2" (INST?) (("2" (ASSERT) NIL))))))) (|authentication_subset| "" (SKOSIMP) (("" (GRIND :EXCLUDE ("subset?" "proj") :REWRITES ("subset?[trace[T]]") :IF-MATCH NIL) (("" (INST?) (("" (ASSERT) (("" (USE "null_proj_subset[T]") (("" (ASSERT) NIL))))))))))) (|authentication_transitive| "" (GRIND :EXCLUDE ("prefix_closed")) NIL) (|authentication_stop| "" (GRIND) NIL) (|authentication_pref1| "" (GRIND :EXCLUDE ("prefix_closed")) NIL) (|authentication_pref2| "" (GRIND :EXCLUDE ("prefix_closed") :IF-MATCH NIL) (("" (INST?) (("" (ASSERT) NIL))))) (|authentication_choice| "" (SKOSIMP) (("" (REWRITE "sat_choice1") (("" (GROUND) NIL))))) (|authentication_choice2| "" (SKOSIMP) (("" (REWRITE "sat_choice2") (("" (GROUND) (("" (REWRITE "authentication_stop") NIL))))))) (|authentication_par1| "" (SKOSIMP) (("" (GRIND :EXCLUDE ("prod" "proj" "subset?") :REWRITES ("subset?[trace[T]]") :IF-MATCH NIL) (("" (USE "null_proj_prod1[T]") (("" (ASSERT) (("" (INST - "t1!1") (("" (ASSERT) (("" (FORWARD-CHAIN "null_proj_prod3[T]") (("" (ASSERT) NIL))))))))))))))) (|authentication_par2| "" (SKOSIMP) (("" (REWRITE "par_commutes") (("" (REWRITE "authentication_par1") NIL))))) (|authentication_par| "" (SKOSIMP) (("" (GRIND :EXCLUDE ("proj" "prod") :IF-MATCH NIL) (("" (USE* "null_proj_prod1[T]" "null_proj_prod2[T]") (("" (ASSERT) (("" (INST - "t1!1") (("" (INST - "t2!1") (("" (ASSERT) (("" (USE "null_proj_prod[T]" ("B" "A!1")) (("" (ASSERT) NIL))))))))))))))))) (|authentication_free_par| "" (SKOSIMP) (("" (EXPAND "//") (("" (REWRITE "authentication_par") NIL))))) (|authentication_fix1| "" (SKOSIMP) (("" (REWRITE "induction") (("" (REWRITE "authentication_stop") NIL)))))) $$$restriction_rules3.pvs % % Restriction rules for multiple parallel composition % restriction_rules3 [ U : NONEMPTY_TYPE, T : TYPE ] : THEORY BEGIN IMPORTING restriction_rules P : VAR [U -> process[T]] A, B : VAR set[T] i : VAR U restriction_par2 : LEMMA Par(A)(P) # B = Par(A)(lambda i : P(i) # B) restriction_free_par2 : LEMMA Interleave(P) # B = Interleave ! i : P(i) # B END restriction_rules3 $$$restriction_rules3.prf (|restriction_rules3| (|restriction_par2| "" (SKOLEM!) (("" (AUTO-REWRITE "restriction_equiv[T]") (("" (ASSERT) (("" (EXPAND "Par") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (IFF) (("" (GROUND) (("1" (SKOLEM!) (("1" (USE "null_proj_multiprod[U, T]" ("t" "t!1")) (("1" (ASSERT) (("1" (INST?) (("1" (SKOLEM!) (("1" (INST?) NIL))))))))))) ("2" (SKOLEM!) (("2" (INST?) (("2" (SKOLEM!) (("2" (ASSERT) NIL))))))) ("3" (SKOLEM!) (("3" (USE "null_proj_multiprod[U, T]" ("t" "t!1")) (("3" (GROUND) (("3" (SKOLEM!) (("3" (ASSERT) NIL))))))))))))))))))))))) (|restriction_free_par2| "" (SKOLEM!) (("" (EXPAND "Interleave") (("" (REWRITE "restriction_par2") NIL)))))) $$$restriction_rules2.pvs % % Restriction of parametric choice % restriction_rules2 [ U, T : TYPE ] : THEORY BEGIN IMPORTING restriction_rules P : VAR [U -> process[T]] i : VAR U A : VAR set[T] F : VAR (monotonic?[U, T]) E : VAR [U -> set[trace[T]]] restriction_choice3 : LEMMA Choice(P) # A = Choice! i : P(i) # A restriction_fix2 : LEMMA (FORALL i : Stop[T] |> E(i)) AND (FORALL P : (FORALL i : P(i) # A |> E(i)) => (FORALL i : F(P)(i) # A |> E(i))) IMPLIES (FORALL i : mu(F)(i) # A |> E(i)) END restriction_rules2 $$$restriction_rules2.prf (|restriction_rules2| (|restriction_choice3| "" (SKOLEM!) (("" (AUTO-REWRITE "restriction_equiv[T]") (("" (ASSERT) (("" (EXPAND "Choice") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL))))))))))) (|restriction_fix2| "" (SKOSIMP) (("" (AUTO-REWRITE "restriction_sat_equiv[T]") (("" (ASSERT) (("" (REWRITE "param_induction") (("" (DELETE -2 2) (("" (GRIND :EXCLUDE ("proj")) NIL)))))))))))) $$$restriction_rules.pvs % % Rules for restrictions (simple processes) % % restriction operator: P # B = Par(B)(P, Stop) % restriction_rules [ T : TYPE] : THEORY BEGIN IMPORTING csp_traces P, P1, P2 : VAR process[T] SP : VAR set[process[T]] a : Var T t : VAR trace[T] A, B : VAR set[T]; F : VAR (monotonic?[T]) E : VAR set[trace[T]] %------------------------ % Restriction operator %------------------------ #(P, B) : process[T] = Par(B)(P, Stop) restriction_equiv : LEMMA P # B = { t | P(t) AND proj(t, B) = null } restriction_twice : LEMMA (P # A) # B = P # union(A, B) %--------- % Rules %--------- restriction_stop : LEMMA Stop # B = Stop restriction_pref1 : LEMMA B(a) IMPLIES (a >> P) # B = Stop restriction_pref2 : LEMMA NOT B(a) IMPLIES (a >> P) # B = a >> (P # B) restriction_pref : LEMMA (a >> P) # B = IF B(a) THEN Stop ELSE a >> (P # B) ENDIF restriction_choice : LEMMA (P1 \/ P2) # B = (P1 # B \/ P2 # B) restriction_choice2 : LEMMA Choice(SP) # B = Choice! (P : (SP)) : P # B restriction_par : LEMMA Par(A)(P1, P2) # B = Par(A)(P1 # B, P2 # B) restriction_free_par : LEMMA (P1 // P2) # B = (P1 # B) // (P2 # B) restriction_sat_equiv : LEMMA P # B |> E IFF P |> { t | proj(t, B) = null IMPLIES E(t) } restriction_fix1 : LEMMA Stop[T] |> E AND (FORALL P : P # B |> E IMPLIES F(P) # B |> E) IMPLIES mu(F) # B |> E END restriction_rules $$$restriction_rules.prf (|restriction_rules| (|restriction_equiv| "" (SKOLEM!) (("" (EXPAND "#") (("" (REWRITE "par_stop") NIL NIL)) NIL)) NIL) (|restriction_twice| "" (SKOLEM!) (("" (AUTO-REWRITE "restriction_equiv" "null_proj_union[T]") (("" (NAME-REPLACE "XX" "P!1 # A!1" :HIDE? NIL) (("" (ASSERT) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (REPLACE -1 + RL) (("" (ASSERT) (("" (DELETE -) (("" (IFF) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|restriction_stop| "" (SKOLEM!) (("" (REWRITE "restriction_equiv") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL) (|restriction_pref1| "" (SKOSIMP) (("" (AUTO-REWRITE "restriction_equiv") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL) (|restriction_pref2| "" (SKOSIMP) (("" (AUTO-REWRITE "restriction_equiv") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :IF-MATCH NIL) (("1" (INST?) NIL NIL) ("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|restriction_pref| "" (AUTO-REWRITE "restriction_pref1" "restriction_pref2") (("" (SKOLEM!) (("" (LIFT-IF) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|restriction_choice| "" (SKOLEM!) (("" (AUTO-REWRITE "restriction_equiv") (("" (ASSERT) (("" (EXPAND "\\/") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :EXCLUDE ("proj")) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|restriction_choice2| "" (SKOLEM!) (("" (AUTO-REWRITE "restriction_equiv") (("" (ASSERT) (("" (EXPAND "Choice") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (IFF) (("" (GROUND) (("1" (EXPAND "proj") (("1" (EXPAND "filter") (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (INST + "i!1") NIL NIL)) NIL) ("3" (SKOLEM!) (("3" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|restriction_par| "" (SKOSIMP) (("" (AUTO-REWRITE "restriction_equiv") (("" (ASSERT) (("" (EXPAND "Par") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (IFF) (("" (GROUND) (("1" (SKOLEM!) (("1" (USE "null_proj_prod[T]") (("1" (GROUND) (("1" (INST?) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (INST?) NIL NIL)) NIL) ("3" (SKOLEM-TYPEPRED) (("3" (USE "null_proj_prod[T]") (("3" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|restriction_free_par| "" (SKOLEM!) (("" (EXPAND "//") (("" (REWRITE "restriction_par") NIL NIL)) NIL)) NIL) (|restriction_sat_equiv| "" (SKOLEM!) (("" (REWRITE "restriction_equiv") (("" (GRIND :EXCLUDE ("proj") :IF-MATCH NIL) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|restriction_fix1| "" (SKOSIMP) (("" (AUTO-REWRITE "restriction_sat_equiv") (("" (ASSERT) (("" (REWRITE "induction") (("" (DELETE -2 2) (("" (GRIND :EXCLUDE ("proj")) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$interface_rules3.pvs % % Interface rules for multiple parallel composition % interface_rules3 [ U : NONEMPTY_TYPE, T : TYPE ] : THEORY BEGIN IMPORTING csp_traces P : VAR [U -> process[T]] A, E : VAR set[T] i : VAR U interface_par2 : LEMMA (FORALL i : subset?(sigma(P(i)), E)) IMPLIES subset?(sigma(Par[U,T](A)(P)), E) interface_free_par2 : LEMMA subset?(sigma(Interleave(P)), E) IFF FORALL i : subset?(sigma(P(i)), E) END interface_rules3 $$$interface_rules3.prf (|interface_rules3| (|interface_par2| "" (SKOSIMP) (("" (USE "sigma_par2[U, T]") (("" (EXPAND "union") (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (REDUCE) NIL))))))))) (|interface_free_par2| "" (SKOLEM!) (("" (REWRITE "sigma_free_par2") (("" (EXPAND "union") (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (REDUCE) NIL)))))))))) $$$interface_rules2.pvs % % interface rules for parametric choice % interface_rules2 [ U, T : TYPE ] : THEORY BEGIN IMPORTING interface_rules P : VAR [U -> process[T]] i : VAR U E : VAR set[T] F : VAR (monotonic?[U, T]) interface_choice3 : LEMMA subset?(sigma(Choice(P)), E) IFF FORALL i : subset?(sigma(P(i)), E) interface_fix2 : LEMMA (FORALL P : (FORALL i : subset?(sigma(P(i)), E)) => (FORALL i : subset?(sigma(F(P)(i)), E))) IMPLIES FORALL i : subset?(sigma(mu(F)(i)), E) END interface_rules2 $$$interface_rules2.prf (|interface_rules2| (|interface_choice3| "" (SKOLEM!) (("" (REWRITE "sigma_choice3") (("" (EXPAND "union") (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (REDUCE) NIL))))))))) (|interface_fix2| "" (SKOSIMP) (("" (AUTO-REWRITE "interface_equiv[T]") (("" (USE "interface_stop[T]") (("" (ASSERT) (("" (REWRITE "param_induction") NIL)))))))))) $$$interface_rules.pvs % % Rules for showing that a process's alphabet is % a subset of a given set of event % % 1st part: simple processes % interface_rules [ T : TYPE ] : THEORY BEGIN IMPORTING csp_traces P, P1, P2 : VAR process[T] SP : VAR set[process[T]] a : Var T t : VAR trace[T] A, E : VAR set[T] F : VAR (monotonic?[T]) interface_equiv : LEMMA subset?(sigma(P), E) IFF P |> { t | subset?(sigma(t), E) } interface_stop : LEMMA subset?(sigma(Stop), E) interface_choice : LEMMA subset?(sigma(P1 \/ P2), E) IFF subset?(sigma(P1), E) AND subset?(sigma(P2), E) interface_choice2 : LEMMA subset?(sigma(Choice(SP)), E) IFF FORALL (P : (SP)) : subset?(sigma(P), E) interface_pref : LEMMA subset?(sigma(a >> P), E) IFF E(a) AND subset?(sigma(P), E) interface_free_par : LEMMA subset?(sigma(P1 // P2), E) IFF subset?(sigma(P1), E) AND subset?(sigma(P2), E) interface_par : LEMMA subset?(sigma(P1), E) AND subset?(sigma(P2), E) IMPLIES subset?(sigma(Par(A)(P1, P2)), E) interface_fix1 : LEMMA (FORALL P : subset?(sigma(P), E) IMPLIES subset?(sigma(F(P)), E)) IMPLIES subset?(sigma(mu(F)), E) END interface_rules $$$interface_rules.prf (|interface_rules| (|interface_stop| "" (GRIND :DEFS NIL :REWRITES ("sigma_stop[T]") :THEORIES ("sets[T]")) NIL) (|interface_choice| "" (GRIND :DEFS NIL :REWRITES ("sigma_choice[T]") :THEORIES ("sets[T]")) NIL) (|interface_choice2| "" (SKOLEM!) (("" (REWRITE "sigma_choice2") (("" (EXPAND "union") (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (REDUCE) NIL))))))))) (|interface_pref| "" (GRIND :DEFS NIL :REWRITES ("sigma_pref[T]") :THEORIES ("sets[T]") :IF-MATCH NIL) (("1" (INST?) (("1" (ASSERT) NIL))) ("2" (INST?) (("2" (ASSERT) NIL))) ("3" (INST?) (("3" (ASSERT) NIL))))) (|interface_free_par| "" (GRIND :DEFS NIL :REWRITES ("sigma_free_par[T]") :THEORIES ("sets[T]")) NIL) (|interface_par| "" (SKOSIMP) (("" (USE "sigma_par[T]") (("" (AUTO-REWRITE "subset?" "member" "union") (("" (REDUCE) NIL))))))) (|interface_equiv| "" (SKOLEM!) (("" (EXPAND "|>") (("" (EXPAND "sigma" 1 1) (("" (AUTO-REWRITE "subset?" "member") (("" (REDUCE) NIL))))))))) (|interface_fix1| "" (SKOSIMP) (("" (AUTO-REWRITE "interface_equiv") (("" (USE "interface_stop") (("" (ASSERT) (("" (REWRITE "induction[T]") NIL)))))))))) $$$csp_rules.pvs % % This theory encapsulates all the rules % for restriction and interface % csp_rules : THEORY BEGIN IMPORTING interface_rules, interface_rules2, interface_rules3, restriction_rules, restriction_rules2, restriction_rules3, authentication, authentication2, authentication3, monotonicity, monotonicity2, monotonicity3 END csp_rules $$$network.pvs % % Network: the enemy + the users % network [ Identity : NONEMPTY_TYPE, Message : TYPE, |- : [set[Message], Message -> bool] ] : THEORY BEGIN ASSUMING monotonic_gen : ASSUMPTION FORALL (A, B : set[Message]), (m : Message) : subset?(A, B) AND (A |- m) IMPLIES (B |- m) ENDASSUMING IMPORTING csp_traces, csp_rules IMPORTING enemy[Identity, Message, |-], users[Identity, Message], rank_rules[Identity, Message] i, j : VAR Identity m : VAR Message e : VAR event A, R, T : VAR set[event] tr, u, v : VAR trace[event] rho : VAR [Message -> int] INIT, S: VAR set[Message] user : VAR user_process baddy: VAR process[event] P : VAR [Identity -> process[event]] %=========== % Network %=========== network(baddy, P) : process[event] = Par(fullset)(baddy, Interleave(P)) %-------------------------------------------- % Messages which can be generated from S %-------------------------------------------- Gen(S) : set[Message] = { m | S |- m } %======================================= % Theorem 3.5 and Corollary 3.6 % If rho has the right properties, % the enemy satisfies RnkE(rho) %======================================= Prop(S) : setof[trace[event]] = { tr | subset?(rec_msg(tr), Gen(union(S, trans_msg(tr)))) } enemy_prop : THEOREM enemy(S) |> Prop(S) rank_property : COROLLARY positive(rho, INIT) AND (FORALL S : positive(rho, S) implies positive(rho, Gen(S))) IMPLIES enemy(INIT) |> RankEnemy(rho) %=========================== % Lemmas and Theorem 3.9 %=========================== traces_of_network : LEMMA (network(baddy, user) # R)(tr) IMPLIES baddy(tr) AND FORALL i : (user(i) # R)(proj(tr, LocalEvents(i))) main_result : LEMMA baddy |> RankEnemy(rho) AND (FORALL i : user(i) # R |> RankUser(rho)) IMPLIES network(baddy, user) # R |> { tr | positive(rho, tr) } main_result_bug : LEMMA baddy |> RankEnemy(rho) AND (FORALL i : user(i) # R |> RankUser(rho)) IMPLIES network(baddy, user) # R |> { tr | positive(rho, tr) } authentication_by_rank : THEOREM positive(rho, INIT) AND (FORALL S, m : positive(rho, S) AND (S |- m) implies rho(m) > 0) AND (FORALL i : user(i) # R |> RankUser(rho)) AND non_positive(rho, T) IMPLIES network(enemy(INIT), user) |> auth(T, R) %====================================================== % Specialization to a protocol with two participants %====================================================== a, b : VAR Identity user_a, user_b : VAR process[event] protocol(a, b, user_a, user_b)(i) : process[event] = IF i=a THEN user_a ELSIF i=b THEN user_b ELSE Stop ENDIF authentication_by_rank2 : COROLLARY positive(rho, INIT) AND (FORALL S, m : positive(rho, S) AND (S |- m) implies rho(m) > 0) AND non_positive(rho, T) AND subset?(sigma(user_a), LocalEvents(a)) AND user_a # R |> RankUser(rho) AND subset?(sigma(user_b), LocalEvents(b)) AND user_b # R |> RankUser(rho) IMPLIES network(enemy(INIT), protocol(a, b, user_a, user_b)) |> auth(T, R) END network $$$network.prf (|network| (|enemy_prop| "" (EXPAND "enemy") (("" (AUTO-REWRITE "enemy_TCC1") (("" (CASE "FORALL S : Prop(S)(null)") (("1" (ASSERT) (("1" (USE "param_induction2" ("G" "F")) (("1" (GROUND) (("1" (DELETE 2) (("1" (SKOSIMP*) (("1" (EXPAND "F") (("1" (REWRITE "sat_choice1") (("1" (REWRITE "sat_choice3") (("1" (REWRITE "sat_choice3") (("1" (CASE "Stop[event[Identity, Message]] |> Prop(x!1)") (("1" (ASSERT) (("1" (DELETE -1) (("1" (AUTO-REWRITE "|>" ">>" "subset?[trace[event]]" "member" "add" "union" "rec_msg_cons1" "trans_msg_cons1" "rec_msg_cons2" "trans_msg_cons2") (("1" (SPLIT) (("1" (SKOLEM!) (("1" (NAME-REPLACE "i!1" "PROJ_1(x!2)") (("1" (NAME-REPLACE "j!1" "PROJ_2(x!2)") (("1" (NAME-REPLACE "m!1" "PROJ_3(x!2)") (("1" (INST?) (("1" (INST?) (("1" (REDUCE :IF-MATCH NIL) (("1" (INST?) (("1" (ASSERT) (("1" (DELETE -1 -2 -4) (("1" (EXPAND "Prop") (("1" (ASSERT) (("1" (CASE-REPLACE "union(add(m!1, x!1), trans_msg(t1!1)) = union(x!1, add(m!1, trans_msg(t1!1)))") (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (IFF) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (NAME-REPLACE "i!1" "PROJ_1(x!2)") (("2" (NAME-REPLACE "j!1" "PROJ_2(x!2)") (("2" (NAME-REPLACE "m!1" "PROJ_3(x!2)") (("2" (INST?) (("2" (INST?) (("2" (REDUCE :IF-MATCH NIL) (("2" (INST - "t1!1") (("2" (ASSERT) (("2" (DELETE -1 -2 -4) (("2" (EXPAND "Prop") (("2" (EXPAND "subset?") (("2" (REDUCE :IF-MATCH NIL) (("1" (DELETE -2) (("1" (TYPEPRED "m!1") (("1" (EXPAND "Gen") (("1" (USE "monotonic_gen" ("B" "union(x!1, trans_msg(t1!1))")) (("1" (ASSERT) (("1" (REWRITE "union_subset1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 2) (("2" (GRIND :EXCLUDE "Prop") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|rank_property| "" (SKOSIMP*) (("" (USE "enemy_prop") (("" (USE "sat_transitive2" ("P" "enemy(INIT!1)" "F" "RankEnemy(rho!1)")) (("" (GROUND) (("" (DELETE -1 2) (("" (GRIND :EXCLUDE ("positive" "pos_trans" "pos_rec" "rec_msg" "trans_msg" "Gen") :IF-MATCH NIL :REWRITES ("pos_trans_equiv" "pos_rec_equiv")) (("" (EXPAND "positive") (("" (SKOLEM!) (("" (INST?) (("" (ASSERT) (("" (INST -4 "union(INIT!1, trans_msg(x!1))") (("" (GROUND) (("1" (INST?) NIL NIL) ("2" (DELETE -1 2) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|traces_of_network| "" (SKOSIMP) (("" (AUTO-REWRITE "restriction_equiv[event]" "intersection" "member" "subset?") (("" (ASSERT) (("" (EXPAND "network") (("" (REWRITE "par_full") (("" (ASSERT) (("" (GROUND) (("" (SKOLEM!) (("" (GROUND) (("1" (REWRITE "local_traces") NIL NIL) ("2" (REWRITE "proj_twice") (("2" (USE "null_proj_subset[event]" ("B" "R!1")) (("2" (ASSERT) (("2" (SKOSIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|main_result| "" (SKOSIMP) (("" (EXPAND* "|>" "subset?" "member") (("" (AUTO-REWRITE "positive_add" "positive_proj" "receptions_add1" "transmissions_add1" "receptions_add2" "transmissions_add2" "pos_rec" "pos_trans" "proj_add[event]" "pro_twice[event]") (("" (INDUCT "x" :NAME "add_induction[event]") (("1" (FLATTEN) (("1" (DELETE -) (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (FORWARD-CHAIN "process_add") (("2" (ASSERT) (("2" (DELETE -1) (("2" (FORWARD-CHAIN "positive_receptions") (("2" (FORWARD-CHAIN "positive_transmissions") (("2" (FORWARD-CHAIN "traces_of_network") (("2" (EXPAND "RankEnemy") (("2" (EXPAND "RankUser") (("2" (CASE "EXISTS i, j, m : a!1 = rec(i, j, m)") (("1" (SKOLEM!) (("1" (REPLACE*) (("1" (DELETE -1 -3 -5 -6 -7 -9) (("1" (INST? - :WHERE -1) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "EXISTS i, j, m : a!1 = trans(i, j, m)") (("1" (SKOLEM!) (("1" (REPLACE*) (("1" (DELETE -1 -2 -4 -7 -8 1) (("1" (INST?) (("1" (INST?) (("1" (CASE "LocalEvents(i!1)(trans(i!1, j!1, m!1))") (("1" (ASSERT) (("1" (EXPAND "receptions" +) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (DELETE -1 -2 -3 -4 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 -2 -3 -4 -5 -6 -7 -8 3) (("2" (CASE "rec?(a!1)") (("1" (ASSERT) (("1" (USE "event_rec_eta[Identity, Message]") (("1" (INST? 2) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (USE "event_trans_eta[Identity, Message]") (("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) (|main_result_bug| "" (SKOSIMP) (("" (EXPAND* "|>" "subset?" "member") (("" (AUTO-REWRITE "positive_add" "positive_proj" "receptions_add1" "transmissions_add1" "receptions_add2" "transmissions_add2" "pos_rec" "pos_trans" "proj_add[event]" "pro_twice[event]") (("" (INDUCT "x" :NAME "add_induction[event]") (("1" (FLATTEN) (("1" (DELETE -) (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (FORWARD-CHAIN "process_add") (("2" (ASSERT) (("2" (GROUND) (("2" (DELETE -1) (("2" (FORWARD-CHAIN "positive_receptions") (("2" (FORWARD-CHAIN "positive_transmissions") (("2" (FORWARD-CHAIN "traces_of_network") (("2" (EXPAND "RankEnemy") (("2" (EXPAND "RankUser") (("2" (CASE "EXISTS i, j, m : a!1 = rec(i, j, m)") (("1" (SKOLEM!) (("1" (REPLACE*) (("1" (DELETE -1 -3 -5 -6 -7 -9) (("1" (INST? - :WHERE -1) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "EXISTS i, j, m : a!1 = trans(i, j, m)") (("1" (SKOLEM!) (("1" (REPLACE*) (("1" (DELETE -1 -2 -4 -7 -8 1) (("1" (INST?) (("1" (INST?) (("1" (CASE "LocalEvents(i!1)(trans(i!1, j!1, m!1))") (("1" (ASSERT) (("1" (EXPAND "receptions" +) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (DELETE -1 -2 -3 -4 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 -2 -3 -4 -5 -6 -7 -8 3) (("2" (USE "event_inclusive") (("2" (GROUND) (("1" (INST + "t_snd(a!1)" "t_rcv(a!1)" "t_msg(a!1)") (("1" (REWRITE "event_trans_eta") NIL NIL)) NIL) ("2" (INST 2 "r_rcv(a!1)" "r_snd(a!1)" "r_msg(a!1)") (("2" (REWRITE "event_rec_eta") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|authentication_by_rank| "" (SKOSIMP) (("" (REWRITE "authentication_equiv") (("" (USE "main_result") (("" (GROUND) (("1" (DELETE -2 -3 -4) (("1" (USE "sat_transitive2[event]" ("F" "{ tr | proj(tr, T!1) = null }")) (("1" (ASSERT) (("1" (DELETE -1 2) (("1" (AUTO-REWRITE "subset?" "member") (("1" (ASSERT) (("1" (SKOSIMP) (("1" (FORWARD-CHAIN "nonpos_null_proj") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -3 -4 2) (("2" (USE "rank_property") (("2" (GROUND) (("2" (DELETE -1 2) (("2" (EXPAND "Gen") (("2" (EXPAND "positive" 1 2) (("2" (SKOSIMP* :PREDS? T) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|authentication_by_rank2| "" (SKOSIMP) (("" (USE "authentication_by_rank" ("user" "protocol(a!1, b!1, user_a!1, user_b!1)")) (("1" (GROUND) (("1" (DELETE -1 -2 -3 -4 -6 2) (("1" (EXPAND "protocol") (("1" (SKOLEM!) (("1" (LIFT-IF) (("1" (GROUND) (("1" (REWRITE "restriction_stop") (("1" (REWRITE "rank_user_stop") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 -2 -3 -5 -7 2) (("2" (EXPAND "protocol") (("2" (SKOLEM!) (("2" (LIFT-IF) (("2" (GROUND) (("2" (REWRITE "interface_stop") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$event.pvs % % Events for Needham/Schroeder protocol % (first try) % -> Parameters: I = process identities % M = message type % event[I, M : TYPE] : DATATYPE BEGIN trans(t_snd, t_rcv: I, t_msg: M) : trans? rec(r_rcv, r_snd: I, r_msg: M) : rec? END event $$$fixed_points2.pvs % % Theory for non-parametic fixed points % i.e. of monotonic functions F : [process[T] -> process[T]] % fixed_points2 [ T : TYPE ] : THEORY BEGIN IMPORTING fixed_points F : VAR [process[T] -> process[T]] X, Y : VAR process[T] %----------------------- % Monotonic functions %----------------------- monotonic?(F) : bool = FORALL X, Y : subset?(X, Y) IMPLIES subset?(F(X), F(Y)) G : VAR (monotonic?) %----------------------------------------------------------- % short cut: everything translated to the parametric case %----------------------------------------------------------- dummy : NONEMPTY_TYPE rep : dummy x : VAR dummy H : VAR [dummy -> process[T]] ext(F)(H) : [dummy -> process[T]] = lambda x : F(H(x)) mu(G) : process[T] = mu(ext(G))(rep) closure_mu2 : LEMMA subset?(G(mu(G)), mu(G)) smallest_closed2 : LEMMA subset?(G(X), X) IMPLIES subset?(mu(G), X) fixed_point2 : LEMMA G(mu(G)) = mu(G) least_fixed_point2 : LEMMA G(X) = X IMPLIES subset?(mu(G), X) %--------------------- % Induction rules %--------------------- E : VAR set[trace[T]] induction : PROPOSITION Stop[T] |> E AND (FORALL X : X |> E IMPLIES G(X) |> E) IMPLIES mu(G) |> E induction2 : PROPOSITION E(null) AND (FORALL X : X |> E IMPLIES G(X) |> E) IMPLIES mu(G) |> E END fixed_points2 $$$fixed_points2.prf (|fixed_points2| (|mu_TCC1| "" (GRIND :IF-MATCH NIL) (("" (INST - "X!1(x!1)" "Y!1(x!1)") (("" (REDUCE) NIL))))) (|closure_mu2| "" (SKOLEM!) (("" (AUTO-REWRITE "mu_TCC1" "ext" "<=") (("" (EXPAND "mu") (("" (USE "closure_mu" ("G" "ext(G!1)")) (("" (ASSERT) (("" (INST?) NIL))))))))))) (|smallest_closed2| "" (SKOSIMP) (("" (AUTO-REWRITE "mu_TCC1" "ext" "<=") (("" (EXPAND "mu") (("" (USE "smallest_closed" ("G" "ext(G!1)" "X" "lambda x : X!1")) (("" (GROUND) (("1" (INST?) NIL) ("2" (SKOLEM!) NIL))))))))))) (|fixed_point2| "" (SKOLEM!) (("" (AUTO-REWRITE "mu_TCC1" "ext" "<=") (("" (USE "fixed_point" ("G" "ext(G!1)")) (("" (EXPAND "mu" 1 2) (("" (REPLACE -1 + RL) (("" (ASSERT) (("" (EXPAND "mu" 1 1) (("" (PROPAX) NIL))))))))))))))) (|least_fixed_point2| "" (SKOSIMP) (("" (AUTO-REWRITE "mu_TCC1" "ext" "<=") (("" (EXPAND "mu") (("" (USE "least_fixed_point" ("G" "ext(G!1)" "X" "lambda x : X!1")) (("" (GROUND) (("1" (INST?) NIL) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))))))))) (|induction| "" (SKOSIMP) (("" (AUTO-REWRITE "mu_TCC1" "ext") (("" (EXPAND "mu") (("" (USE "param_induction" ("G" "ext(G!1)" "E" "lambda x : E!1")) (("" (GROUND) (("1" (INST?) NIL) ("2" (SKOLEM!) NIL) ("3" (SKOSIMP*) (("3" (INST?) (("3" (INST?) (("3" (ASSERT) NIL))))))))))))))))) (|induction2| "" (SKOSIMP) (("" (USE "induction") (("" (GROUND) (("" (DELETE -2 2) (("" (GRIND) NIL)))))))))) $$$fixed_points.pvs fixed_points [ U, T : TYPE ] : THEORY BEGIN IMPORTING processes, satisfaction x, x1, x2 : VAR U X, Y, Z : VAR [U -> process[T]]; t : VAR trace[T] Q : VAR process[T] %================================================= % Fixed points of a monotonic function F % F : [[U -> process[T]] -> [U -> process[T]]] %================================================= %-------------------------------------- % Order between parametric processes %-------------------------------------- <=(X, Y) : bool = FORALL x : subset?(X(x), Y(x)) reflexive : LEMMA X <= X antisymmetric : LEMMA X <= Y AND Y <= X IMPLIES X = Y transitive : LEMMA X <= Y AND Y <= Z IMPLIES X <= Z %------------------------ % greater lower bounds %------------------------ SX : VAR set[[U -> process[T]]] glb(SX)(x) : process[T] = { t | FORALL (X : (SX)) : X(x)(t) } glb_is_bound : LEMMA FORALL (X : (SX)) : glb(SX) <= X glb_is_inf : LEMMA (FORALL (X : (SX)) : Y <= X) IMPLIES Y <= glb(SX) %--------------- % Fixed point %--------------- F : VAR [[U -> process[T]] -> [U -> process[T]]] monotonic?(F) : bool = FORALL X, Y : X <= Y IMPLIES F(X) <= F(Y) G : VAR (monotonic?) mu(G) : [U -> process[T]] = glb({X | G(X) <= X}) closure_mu : LEMMA G(mu(G)) <= mu(G) smallest_closed : LEMMA G(X) <= X IMPLIES mu(G) <= X fixed_point : LEMMA G(mu(G)) = mu(G) least_fixed_point : LEMMA G(X) = X IMPLIES mu(G) <= X %------------------- % Induction rule %------------------- E : VAR [ U -> pred[trace[T]] ] <(X, E) : bool = FORALL x : X(x) |> E(x) pseudo_transitive : LEMMA X <= Y AND Y < E IMPLIES X < E SY : VAR { SX | not empty?(SX) } lub(SY)(x) : process[T] = { t | EXISTS (X : (SY)) : X(x)(t) } lub_is_bound : LEMMA FORALL (X : (SY)) : X <= lub(SY) lub_is_sup : LEMMA (FORALL (X : (SY)) : X < E) IMPLIES lub(SY) < E induction_aux : LEMMA (EXISTS X : X < E) AND (FORALL X : X < E implies G(X) < E) IMPLIES mu(G) < E param_induction0 : PROPOSITION (FORALL x : EXISTS Q : Q |> E(x)) AND (FORALL X : (FORALL x : X(x) |> E(x)) => (FORALL x : G(X)(x) |> E(x))) IMPLIES (FORALL x : mu(G)(x) |> E(x)) param_induction : PROPOSITION (FORALL x : Stop[T] |> E(x)) AND (FORALL X : (FORALL x : X(x) |> E(x)) => (FORALL x : G(X)(x) |> E(x))) IMPLIES (FORALL x : mu(G)(x) |> E(x)) param_induction2 : PROPOSITION (FORALL x : E(x)(null)) AND (FORALL X : (FORALL x : X(x) |> E(x)) => (FORALL x : G(X)(x) |> E(x))) IMPLIES (FORALL x : mu(G)(x) |> E(x)) END fixed_points $$$fixed_points.prf (|fixed_points| (|reflexive| "" (GRIND) NIL NIL) (|antisymmetric| "" (GRIND :IF-MATCH NIL) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (INST?) (("" (INST?) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (INST?) (("" (INST?) (("" (BDDSIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|transitive| "" (GRIND) NIL NIL) (|glb_TCC1| "" (GRIND :IF-MATCH NIL :EXCLUDE "prefix") (("" (INST?) (("" (TYPEPRED "X!1(x!1)") (("" (ASSERT) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|glb_is_bound| "" (GRIND) NIL NIL) (|glb_is_inf| "" (GRIND :IF-MATCH BEST) NIL NIL) (|closure_mu| "" (AUTO-REWRITE "glb_is_bound" "mu" "monotonic?") (("" (SKOLEM-TYPEPRED) (("" (ASSERT) (("" (REWRITE "glb_is_inf") (("" (SKOLEM-TYPEPRED) (("" (INST - "mu(G!1)" "X!1") (("" (ASSERT) (("" (USE "transitive" ("X" "G!1(mu(G!1))" "Y" "G!1(X!1)" "Z" "X!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|smallest_closed| "" (AUTO-REWRITE "mu" "glb_is_bound") (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|fixed_point| "" (AUTO-REWRITE "monotonic?") (("" (SKOLEM-TYPEPRED) (("" (USE* "closure_mu" "antisymmetric") (("" (ASSERT) (("" (DELETE 2) (("" (EXPAND "mu" 1 1) (("" (REWRITE "glb_is_bound") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|least_fixed_point| "" (SKOSIMP) (("" (REWRITE "smallest_closed") (("" (REPLACE*) (("" (REWRITE "reflexive") NIL NIL)) NIL)) NIL)) NIL) (|pseudo_transitive| "" (GRIND) NIL NIL) (|lub_TCC1| "" (GRIND :EXCLUDE ("prefix")) (("" (TYPEPRED "X!1(x!1)") (("" (ASSERT) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|lub_is_bound| "" (GRIND) NIL NIL) (|lub_is_sup| "" (GRIND) NIL NIL) (|induction_aux| "" (SKOSIMP) (("" (CASE "empty?({ X | X < E!1})") (("1" (DELETE -3 1) (("1" (GRIND :EXCLUDE ("<" "prefix_closed") :IF-MATCH NIL) (("1" (INST?) NIL NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (DELETE -1 1) (("2" (NAME "Z!1" "lub({X | X < E!1})") (("2" (USE "lub_is_sup" ("E" "E!1")) (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) (("2" (USE "lub_is_bound" ("SY" "{X | X < E!1}" "X" "G!1(Z!1)")) (("2" (REPLACE*) (("2" (FORWARD-CHAIN "smallest_closed") (("2" (FORWARD-CHAIN "pseudo_transitive") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|param_induction0| "" (SKOSIMP) (("" (USE "induction_aux") (("" (EXPAND "<") (("" (GROUND) (("" (DELETE -2 2) (("" (INST + "lambda x : epsilon! Q : Q |> E!1(x)") (("" (ASSERT) (("" (SKOLEM!) (("" (INST?) (("" (USE "epsilon_ax" ("p" "lambda Q : Q |> E!1(x!1)")) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|param_induction| "" (SKOSIMP) (("" (REWRITE "param_induction0") (("" (DELETE -2 2) (("" (SKOLEM!) (("" (INST? -) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|param_induction2| "" (SKOSIMP) (("" (REWRITE "param_induction") (("" (DELETE -2 2) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) $$$satisfaction3.pvs % % Properties of sat and unbounded interleave % satisfaction3 [U : NONEMPTY_TYPE, T : TYPE ] : THEORY BEGIN IMPORTING satisfaction, multipar P : VAR [U -> process[T]] x : VAR U E : VAR set[trace[T]] sat_free_par3 : LEMMA Interleave(P) |> E IMPLIES P(x) |> E END satisfaction3 $$$satisfaction3.prf (|satisfaction3| (|sat_free_par3| "" (SKOSIMP) (("" (USE "interleave_subset3[U, T]") (("" (REWRITE "|>" :DIR RL) (("" (FORWARD-CHAIN "sat_transitive1") NIL)))))))) $$$satisfaction2.pvs satisfaction2 [ T : TYPE, U : TYPE ] : THEORY BEGIN IMPORTING satisfaction, parametric_choice P : VAR [U -> process[T]] x : VAR U E : VAR set[trace[T]] sat_choice3 : LEMMA Choice(P) |> E IFF Stop[T] |> E AND (FORALL x : P(x) |> E) END satisfaction2 $$$satisfaction2.prf (|satisfaction2| (|sat_choice3| "" (GRIND :EXCLUDE ("prefix_closed")) NIL)) $$$satisfaction.pvs % % Definition of the satisfaction relation % - if P is a process, E a trace predicate % P |> E means "P sat E" % - if E is also a process, % P |> E can mean "P is a refinement of E" % satisfaction [T : TYPE ] : THEORY BEGIN IMPORTING processes, process_rules P, Q : VAR process[T] E, F : VAR pred[trace[T]] SP : VAR set[process[T]] |> (P, E) : bool = subset?(P, E) sat_idempotent : LEMMA P |> P sat_transitive1 : LEMMA (P |> Q) AND (Q |> E) IMPLIES (P |> E) sat_transitive2 : LEMMA (P |> E) AND subset?(E, F) IMPLIES (P |> F) sat_choice1 : LEMMA (P \/ Q) |> E IFF P |> E AND Q |> E sat_choice2 : LEMMA Choice(SP) |> E IFF Stop[T] |> E AND (FORALL (P : (SP)) : P |> E ) sat_free_par1 : LEMMA (P // Q) |> E IMPLIES P |> E sat_free_par2 : LEMMA (P // Q) |> E IMPLIES Q |> E END satisfaction $$$satisfaction.prf (|satisfaction| (|sat_idempotent| "" (SKOLEM!) (("" (GRIND) NIL NIL)) NIL) (|sat_transitive1| "" (SKOSIMP) (("" (GRIND) NIL NIL)) NIL) (|sat_transitive2| "" (SKOSIMP) (("" (GRIND) NIL NIL)) NIL) (|sat_choice1| "" (SKOLEM!) (("" (GRIND) NIL NIL)) NIL) (|sat_choice2| "" (GRIND :EXCLUDE ("prefix_closed") :IF-MATCH NIL) (("1" (INST?) (("1" (GROUND) (("1" (INST + "P!1") NIL NIL)) NIL)) NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL) ("3" (INST - "P!1" "x!1") (("3" (ASSERT) NIL NIL)) NIL)) NIL) (|sat_free_par1| "" (SKOSIMP) (("" (USE "interleaves_subset1[T]") (("" (REWRITE "|>" :DIR RL) (("" (FORWARD-CHAIN "sat_transitive1") NIL NIL)) NIL)) NIL)) NIL) (|sat_free_par2| "" (SKOSIMP) (("" (USE "interleaves_subset2[T]") (("" (REWRITE "|>" :DIR RL) (("" (FORWARD-CHAIN "sat_transitive1") NIL NIL)) NIL)) NIL)) NIL)) $$$multiprod.pvs % % products of a non-empty family of traces % multiprod [ U : NONEMPTY_TYPE, T : TYPE ] : THEORY BEGIN IMPORTING traces, parametric_sets t, t1, t2 : VAR [U -> trace[T]] u, v : VAR trace[T] i, j, k : VAR U A, B, C : VAR set[T] S : VAR [U -> set[T]] %---------------------------------------------------------------- % prod(A)(t, u) : "u is a product of the traces {t(i) | i in U} % with synchronisations on A %---------------------------------------------------------------- prod(A)(t, u) : RECURSIVE bool = CASES u OF null: (FORALL i : t(i) = null), cons(x, y): IF A(x) THEN (FORALL i : cons?(t(i)) AND car(t(i)) = x) AND prod(A)(lambda j : cdr(t(j)), y) ELSE EXISTS i : cons?(t(i)) AND car(t(i)) = x AND prod(A)(t with [(i) := cdr(t(i))], y) ENDIF ENDCASES MEASURE length(u) proj_multiprod : LEMMA prod(A)(t, u) IMPLIES FORALL i : proj(t(i), A) = proj(u, A) prefix_multiprod : LEMMA prod(A)(t, u) AND prefix(v, u) IMPLIES EXISTS t1 : prod(A)(t1, v) AND FORALL i : prefix(t1(i), t(i)) multiprod_fullset : LEMMA prod(fullset)(t, u) IFF (FORALL i : t(i) = u) free_multiprod : LEMMA prod(emptyset)((lambda i : null[T]) WITH [(j) := u], u) sigma_multiprod : LEMMA prod(A)(t, u) IMPLIES sigma(u) = union! i : sigma(t(i)) sigma_multiprod_inter : LEMMA prod(A)(t, u) IMPLIES intersection(sigma(t(i)), A) = intersection(sigma(u), A) %---------------------------------------------------------------- % Interleaving when the traces have mutually disjoint alphabets %---------------------------------------------------------------- sub_alphabet(t, S) : bool = FORALL i : subset?(sigma(t(i)), S(i)) disj_alphabet(S) : bool = FORALL i, j : i /= j IMPLIES disjoint?(S(i), S(j)) inter_disjoint : LEMMA disj_alphabet(S) AND sub_alphabet(t, S) AND prod(emptyset)(t, u) IMPLIES FORALL i : t(i) = proj(u, S(i)) %--------------------------------------- % Projections/restrictions %----------------------------------------- inter_proj : LEMMA prod(emptyset)(t, u) IMPLIES prod(emptyset)(lambda i : proj(t(i), B), proj(u, B)) null_proj_multiprod : LEMMA prod(A)(t, u) IMPLIES (proj(u, B) = null IFF FORALL i : proj(t(i), B) = null) null_proj_multiprod2 : LEMMA prod(A)(t, u) AND subset?(B, A) AND proj(t(i), B) = null IMPLIES proj(u, B) = null null_inter_proj : LEMMA prod(emptyset)(t, u) IMPLIES (proj(u, B) = null IFF FORALL i : proj(t(i), B) = null) END multiprod $$$multiprod.prf (|multiprod| (|prod_TCC1| "" (SKOSIMP*) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|prod_TCC2| "" (TERMINATION-TCC) NIL NIL) (|prod_TCC3| "" (TERMINATION-TCC) NIL NIL) (|proj_multiprod| "" (AUTO-REWRITE-DEFS) (("" (SKOLEM + ("A!1" _ _)) (("" (INDUCT "u") (("1" (REDUCE) NIL NIL) ("2" (SKOSIMP*) (("2" (CASE "A!1(cons1_var!1)") (("1" (REDUCE) NIL NIL) ("2" (ASSERT) (("2" (SKOSIMP) (("2" (ASSERT) (("2" (INST?) (("2" (GROUND) (("2" (INST - "i!1") (("2" (CASE "i!1 = i!2") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prefix_multiprod| "" (AUTO-REWRITE "prefix_null[T]" "null_prefix[T]") (("" (SKOLEM + ("A!1" _ _ _)) (("" (INDUCT "u") (("1" (AUTO-REWRITE "prod") (("1" (SKOSIMP) (("1" (INST + "lambda i : null") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (REWRITE "prefix_equiv") (("2" (GROUND) (("1" (AUTO-REWRITE "prod") (("1" (INST + "lambda i : null") (("1" (DELETE -2 -3) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (AUTO-REWRITE "prod") (("2" (CASE "A!1(cons1_var!1)") (("1" (ASSERT) (("1" (GROUND) (("1" (INST - "LAMBDA (i: U): cdr(t!1(i))" "cdr(v!1)") (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST + "lambda i : cons(cons1_var!1, t1!1(i))") (("1" (GROUND) (("1" (LEMMA "eta[U, trace[T]]") (("1" (INST - "t1!1") (("1" (REPLACE -1) (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (INST?) (("2" (INST?) (("2" (REWRITE "prefix_equiv" +) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (INST?) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (SKOSIMP) (("2" (ASSERT) (("2" (INST - "t!1 WITH [(i!1) := cdr(t!1(i!1))]" "cdr(v!1)") (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST + "t1!1 with [(i!1) := cons(cons1_var!1, t1!1(i!1))]") (("2" (GROUND) (("1" (INST + "i!1") (("1" (ASSERT) (("1" (CASE-REPLACE "t1!1 WITH [(i!1):= cons(cons1_var!1, t1!1(i!1)), (i!1) := t1!1(i!1)] = t1!1") (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (CASE "x!1 = i!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (INST - "i!2") (("2" (CASE "i!1 = i!2") (("1" (ASSERT) (("1" (REWRITE "prefix_equiv" +) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|multiprod_fullset| "" (AUTO-REWRITE "fullset" "prod") (("" (INDUCT "u") (("1" (REDUCE) NIL NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (GROUND) (("1" (INST? -3) (("1" (ASSERT) (("1" (SKOLEM!) (("1" (INST?) (("1" (INST?) (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -2 2) (("2" (REDUCE) NIL NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (INST?) (("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("3" (INST? -2) (("1" (ASSERT) (("1" (SKOLEM!) (("1" (INST?) (("1" (REPLACE*) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|free_multiprod| "" (INDUCT-AND-SIMPLIFY "u") NIL NIL) (|sigma_multiprod| "" (INDUCT-AND-SIMPLIFY "u") (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (REDUCE) NIL NIL)) NIL) ("2" (REPLACE*) (("2" (DELETE -1 -4) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (REDUCE) (("1" (INST + "epsilon! i : true") (("1" (REDUCE) NIL NIL)) NIL)) NIL) ("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL) ("3" (REPLACE*) (("3" (DELETE -1 -4) (("3" (APPLY-EXTENSIONALITY :HIDE? T) (("3" (IFF) (("3" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOLEM!) (("2" (INST + "i!2") (("2" (SMASH) NIL NIL)) NIL)) NIL) ("3" (SKOLEM!) (("3" (INST?) (("3" (SMASH) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_multiprod_inter| "" (SKOSIMP) (("" (FORWARD-CHAIN "proj_multiprod") (("" (INST?) (("" (REWRITE "sigma_proj" :DIR RL) (("" (REWRITE "sigma_proj" :DIR RL) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|inter_disjoint| "" (AUTO-REWRITE "prod" "emptyset" "proj" "filter") (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (SKOLEM + ("A!1" _ _)) (("" (INDUCT "u") (("1" (SKOSIMP) (("1" (ASSERT) NIL NIL)) NIL) ("2" (AUTO-REWRITE "sub_alphabet" "disj_alphabet" "sigma" "list2set") (("2" (SKOSIMP) (("2" (SKOSIMP) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST - "t!1 WITH [(i!1) := cdr(t!1(i!1))]") (("2" (GROUND) (("1" (INST? -3) (("1" (INST -3 "cons1_var!1") (("1" (ASSERT) (("1" (SKOLEM!) (("1" (INST?) (("1" (CASE "i!1 = i!2") (("1" (ASSERT) (("1" (APPLY-EXTENSIONALITY) NIL NIL)) NIL) ("2" (INST - "i!1" "i!2") (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 -5 2) (("2" (SKOLEM!) (("2" (INST - "i!2") (("2" (CASE "i!1 = i!2") (("1" (SKOSIMP) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|inter_proj| "" (AUTO-REWRITE "prod" "emptyset" "proj" "filter") (("" (SKOLEM + ("A!1" _ _)) (("" (INDUCT "u") (("1" (REDUCE) NIL NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST? :WHERE -4) (("2" (ASSERT) (("2" (LIFT-IF) (("2" (GROUND) (("1" (INST?) (("1" (ASSERT) (("1" (CASE-REPLACE "(LAMBDA i : filter(t!1(i), A!1)) WITH [(i!1) := filter(cdr(t!1(i!1)), A!1)] = (LAMBDA i : filter(t!1 WITH [(i!1) := cdr(t!1(i!1))](i), A!1))") (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (CASE "x!1 = i!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE-REPLACE "(LAMBDA i : filter(t!1(i), A!1)) = LAMBDA i : filter(t!1 WITH [(i!1) := cdr(t!1(i!1))](i), A!1)") (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (CASE "x!1 = i!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|null_proj_multiprod| "" (SKOSIMP) (("" (AUTO-REWRITE "null_proj_equiv[T]") (("" (ASSERT) (("" (FORWARD-CHAIN "sigma_multiprod") (("" (REPLACE*) (("" (DELETE -) (("" (EXPAND "union") (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|null_proj_multiprod2| "" (SKOSIMP) (("" (AUTO-REWRITE "null_proj_equiv[T]") (("" (ASSERT) (("" (USE "sigma_multiprod_inter") (("" (ASSERT) (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (REDUCE) (("" (CASE "intersection(sigma(t!1(i!1)), A!1)(x!1)") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|null_inter_proj| "" (SKOSIMP) (("" (USE "null_proj_multiprod") (("" (ASSERT) NIL NIL)) NIL)) NIL)) $$$multipar.pvs % % Parallel composition of a non-empty family of processes % % T : event type % U : parameter type % multipar [ U : NONEMPTY_TYPE, T : TYPE ] : THEORY BEGIN IMPORTING processes, multiprod, process_rules P : VAR [U -> process[T]] A : VAR set[T] S : VAR [U -> set[T]] u : VAR trace[T] i, j : VAR U %-------------------------------------------------- % Parallel composition with synchronisation on A %-------------------------------------------------- Par(A)(P) : process[T] = { u | EXISTS (t : [i:U -> (P(i))]) : prod(A)(t, u) } %---------------- % Interleaving %---------------- Interleave(P) : process[T] = Par(emptyset)(P) %-------------- % Properties %-------------- sigma_par2 : LEMMA subset?(sigma(Par(A)(P)), union! i : sigma(P(i))) sigma_free_par2 : LEMMA sigma(Interleave(P)) = union! i : sigma(P(i)) par_full2 : LEMMA Par(fullset)(P) = intersection! i : P(i) interleave_subset3 : LEMMA subset?(P(i), Interleave(P)) %-------------------------------------------------------- % Interleaving when processes have disjoint interfaces %-------------------------------------------------------- interleave_disjoint : LEMMA (FORALL i : subset?(sigma(P(i)), S(i))) AND (FORALL i, j : i /= j IMPLIES disjoint?(S(i), S(j))) IMPLIES subset?(Interleave(P), { u | FORALL i : P(i)(proj(u, S(i))) }) END multipar $$$multipar.prf (|multipar| (|Par_TCC1| "" (SKOLEM!) (("" (GROUND) (("1" (INST + "lambda i : null") (("1" (EXPAND "prod") (("1" (PROPAX) NIL))) ("2" (REDUCE) NIL))) ("2" (AUTO-REWRITE "prefix_closed") (("2" (ASSERT) (("2" (SKOSIMP*) (("2" (FORWARD-CHAIN "prefix_multiprod") (("2" (SKOSIMP) (("2" (INST + "t1!2") (("2" (SKOLEM!) (("2" (INST?) (("2" (TYPEPRED "P!1(x1!1)") (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))))))))))) (|sigma_par2| "" (EXPAND "Par") (("" (EXPAND "sigma") (("" (GRIND :DEFS NIL :THEORIES ("sets[T]" "sets[trace[T]]") :IF-MATCH NIL) (("" (FORWARD-CHAIN "sigma_multiprod") (("" (REPLACE -1) (("" (EXPAND "union") (("" (SKOLEM!) (("" (INST + "i!1") (("" (INST?) NIL))))))))))))))))) (|sigma_free_par2| "" (EXPAND "Interleave") (("" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (IFF) (("" (GROUND) (("1" (USE "sigma_par2") (("1" (EXPAND "subset?") (("1" (EXPAND "member") (("1" (INST?) (("1" (ASSERT) NIL))))))))) ("2" (EXPAND "union") (("2" (EXPAND "Par") (("2" (EXPAND "sigma") (("2" (SKOSIMP* :PREDS? T) (("2" (INST?) (("2" (INST + "lambda i : IF i = i!1 THEN t!1 ELSE null[T] ENDIF") (("1" (LEMMA "free_multiprod" ("j" "i!1" "u" "t!1")) (("1" (CASE-REPLACE "(LAMBDA i: IF i = i!1 THEN t!1 ELSE null[T] ENDIF) = ((LAMBDA i: null[T]) WITH [(i!1) := t!1])") (("1" (DELETE -1 -3 2) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (SMASH) NIL))))))))) ("2" (SKOSIMP) (("2" (ASSERT) NIL))) ("3" (SKOSIMP) (("3" (ASSERT) NIL))))))))))))))))))))))))) (|par_full2| "" (AUTO-REWRITE "Par" "intersection") (("" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (IFF) (("" (GROUND) (("1" (SKOLEM!) (("1" (REWRITE "multiprod_fullset") (("1" (SKOLEM!) (("1" (INST?) (("1" (ASSERT) NIL))))))))) ("2" (INST + "lambda i : x!1") (("2" (REWRITE "multiprod_fullset") NIL))))))))))))) (|interleave_subset3| "" (GRIND :EXCLUDE ("prod")) (("" (USE "free_multiprod[U, T]") (("" (INST + "lambda i : IF i = i!1 THEN x!1 ELSE null[T] ENDIF") (("1" (CASE-REPLACE "(LAMBDA i: IF i = i!1 THEN x!1 ELSE null[T] ENDIF) = (LAMBDA i: null[T]) WITH [(i!1) := x!1]") (("1" (DELETE -1 2) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (REDUCE) NIL))))))) ("2" (SKOSIMP) (("2" (ASSERT) NIL))) ("3" (SKOSIMP) (("3" (ASSERT) NIL))))))))) (|interleave_disjoint| "" (GRIND :EXCLUDE ("proj" "sigma" "disjoint?") :REWRITES ("disj_alphabet[U, T]" "sub_alphabet[U, T]") :IF-MATCH NIL) (("" (USE "inter_disjoint[U, T]" ("t" "t!1")) (("" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL))) ("2" (REWRITE "sub_alphabet") (("2" (SKOSIMP*) (("2" (INST?) (("2" (ASSERT) (("2" (DELETE -2 -3 1 3) (("2" (USE "sigma_subset" ("P" "P!1(i!2)")) (("2" (REDUCE) NIL)))))))))))))))))))) $$$parametric_sets.pvs % % union and intersection of a family of sets % % T : element type % U : index type % parametric_sets [ U, T : TYPE ] : THEORY BEGIN A : VAR [U -> set[T]] i : VAR U x : VAR T S : VAR set[T] %--------------- % Definitions %--------------- union(A) : set[T] = { x | EXISTS i : A(i)(x) } intersection(A) : set[T] = { x | FORALL i : A(i)(x) } %-------------- % Properties %-------------- union_is_bound : LEMMA subset?(A(i), union(A)) union_is_lub : LEMMA (FORALL i : subset?(A(i), S)) IMPLIES subset?(union(A), S) inter_is_bound : LEMMA subset?(intersection(A), A(i)) inter_is_glb : LEMMA (FORALL i : subset?(S, A(i))) IMPLIES subset?(S, intersection(A)) END parametric_sets $$$parametric_sets.prf (|parametric_sets| (|union_is_bound| "" (GRIND) NIL) (|union_is_lub| "" (GRIND) NIL) (|inter_is_bound| "" (GRIND) NIL) (|inter_is_glb| "" (GRIND) NIL)) $$$process_rules.pvs process_rules [ T : TYPE ] : THEORY BEGIN IMPORTING processes, parametric_sets P, P1, P2, P3, P4 : VAR process[T] SP, SP1, SP2 : VAR set[process[T]] a, b, c : VAR T A, B, C : VAR set[T] t : VAR trace[T] %------------------ % Prefix closure %------------------ process_add : LEMMA P(add(t, a)) IMPLIES P(t) %------------------- % Rules for sigma %------------------- sigma_stop : LEMMA sigma(Stop[T]) = emptyset sigma_choice : LEMMA sigma(P1 \/ P2) = union(sigma(P1), sigma(P2)) sigma_choice2 : LEMMA sigma(Choice(SP)) = union! (P : (SP)) : sigma(P) sigma_pref : LEMMA sigma(a >> P) = add(a, sigma(P)) sigma_par : LEMMA subset?(sigma(Par(A)(P1, P2)), union(sigma(P1), sigma(P2))) sigma_free_par : LEMMA sigma(P1 // P2) = union(sigma(P1), sigma(P2)) sigma_empty : LEMMA sigma(P) = emptyset IFF P = Stop[T] sigma_union : LEMMA sigma(P) = union! (t : (P)) : sigma(t) sigma_subset : LEMMA FORALL (t : (P)) : subset?(sigma(t), sigma(P)) %-------------------------------- % Stop is the smallest process %-------------------------------- stop_subset : LEMMA subset?(Stop[T], P) stop_smallest : LEMMA subset?(P, Stop[T]) IFF P = Stop[T] %---------------------------- % Rules for bounded choice %---------------------------- choice_commutes : LEMMA (P1 \/ P2) = (P2 \/ P1) choice_assoc : LEMMA (P1 \/ (P2 \/ P3)) = ((P1 \/ P2) \/ P3) choice_idempotent : LEMMA (P \/ P) = P choice_subset1 : LEMMA subset?(P1, P1 \/ P2) choice_subset2 : LEMMA subset?(P2, P1 \/ P2) choice_stop1 : LEMMA (P \/ Stop[T]) = P choice_stop2 : LEMMA (Stop[T] \/ P) = P choice_stop3 : LEMMA (P1 \/ P2) = Stop[T] IFF P1 = Stop[T] AND P2 = Stop[T] %------------------------------ % Rules for unbounded choice %------------------------------ choice_empty : LEMMA Choice(emptyset[process[T]]) = Stop[T] choice_add : LEMMA Choice(add(P, SP)) = (P \/ Choice(SP)) choice_singleton : LEMMA Choice(singleton(P)) = P choice_union : LEMMA Choice(union(SP1, SP2)) = (Choice(SP1) \/ Choice(SP2)) choice_member : LEMMA FORALL (P : (SP)) : subset?(P, Choice(SP)) %---------------------------------- % Rules for parallel composition %---------------------------------- par_commutes : LEMMA Par(A)(P1, P2) = Par(A)(P2, P1) par_assoc : LEMMA Par(A)(P1, Par(A)(P2, P3)) = Par(A)(Par(A)(P1, P2), P3) par_stop : LEMMA Par(A)(P, Stop) = { t | P(t) AND proj(t, A) = null } par_full : LEMMA Par(fullset)(P1, P2) = intersection(P1, P2) %--------------------------- % Rules for interleaving %--------------------------- interleaves_commutes : LEMMA P1 // P2 = P2 // P1 interleaves_assoc : LEMMA (P1 // P2) // P3 = P1 // (P2 // P3) interleaves_subset1 : LEMMA subset?(P1, P1 // P2) interleaves_subset2 : LEMMA subset?(P2, P1 // P2) interleaves_stop1 : LEMMA P // Stop[T] = P interleaves_stop2 : LEMMA Stop[T] // P = P END process_rules $$$process_rules.prf (|process_rules| (|process_add| "" (AUTO-REWRITE "prefix_closed[T]" "prefix[T]" "add[T]") (("" (SKOSIMP :PREDS? T) (("" (ASSERT) (("" (INST - "t!1" "add(t!1, a!1)") (("" (ASSERT) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_stop| "" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL) (|sigma_choice| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :DEFS NIL :REWRITES ("sigma" "Choice" "\\/") :THEORIES ("sets[T]" "sets[trace[T]]")) NIL NIL)) NIL)) NIL) (|sigma_choice2| "" (AUTO-REWRITE "sigma" "Choice" "union" "emptyset" "list2set") (("" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (IFF) (("" (GROUND) (("1" (SKOLEM-TYPEPRED) (("1" (ASSERT) (("1" (GROUND) (("1" (SKOLEM!) (("1" (INST + "P!1") (("1" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST?) (("2" (FLATTEN) (("2" (INST + "i!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_pref| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :IF-MATCH NIL) (("1" (INST?) NIL NIL) ("2" (INST + "(: a!1 :)") (("1" (ASSERT) NIL NIL) ("2" (INST?) NIL NIL)) NIL) ("3" (INST + "cons(a!1, t!1)") (("1" (ASSERT) NIL NIL) ("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_par| "" (EXPAND "Par") (("" (EXPAND "sigma") (("" (GRIND :DEFS NIL :THEORIES ("sets[T]" "sets[trace[T]]") :IF-MATCH NIL) (("" (FORWARD-CHAIN "sigma_prod") (("" (REPLACE*) (("" (ASSERT) (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_free_par| "" (SKOLEM!) (("" (EXPAND "//") (("" (USE "sigma_par") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (IFF) (("" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (DELETE -2) (("2" (GRIND :DEFS NIL :REWRITES ("Par" "sigma" "free_prod_left[T]" "free_prod_right[T]") :IF-MATCH NIL) (("1" (INST?) (("1" (INST + "t!1" "null") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (INST?) (("2" (INST + "null" "t!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_empty| "" (SKOLEM!) (("" (GROUND) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (EXPAND "Stop") (("1" (REWRITE "emptyset_is_empty?" :DIR RL) (("1" (GRIND) (("1" (INST - "car(x!1)") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE*) (("2" (REWRITE "sigma_stop") NIL NIL)) NIL)) NIL)) NIL) (|sigma_union| "" (EXPAND "sigma" 1 1) (("" (EXPAND "union") (("" (PROPAX) NIL NIL)) NIL)) NIL) (|sigma_subset| "" (SKOLEM!) (("" (REWRITE "sigma_union") (("" (USE "union_is_bound" ("A" "lambda (t: (P!1)): sigma(t)")) NIL NIL)) NIL)) NIL) (|stop_subset| "" (GRIND :EXCLUDE "prefix_closed") NIL NIL) (|stop_smallest| "" (GRIND :EXCLUDE "prefix_closed" :IF-MATCH NIL) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (INST?) (("" (IFF) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|choice_commutes| "" (GRIND :EXCLUDE "prefix_closed") (("" (REWRITE "union_commutative") NIL NIL)) NIL) (|choice_assoc| "" (AUTO-REWRITE "\\/" "Choice") (("" (SKOLEM!) (("" (ASSERT) (("" (REWRITE "union_associative") NIL NIL)) NIL)) NIL)) NIL) (|choice_idempotent| "" (AUTO-REWRITE "\\/" "Choice") (("" (SKOLEM!) (("" (ASSERT) (("" (REWRITE "union_idempotent") NIL NIL)) NIL)) NIL)) NIL) (|choice_subset1| "" (AUTO-REWRITE "\\/" "Choice") (("" (SKOLEM!) (("" (ASSERT) (("" (REWRITE "union_subset1") NIL NIL)) NIL)) NIL)) NIL) (|choice_subset2| "" (SKOLEM!) (("" (REWRITE "choice_commutes") (("" (REWRITE "choice_subset1") NIL NIL)) NIL)) NIL) (|choice_stop1| "" (AUTO-REWRITE "\\/" "Choice") (("" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL) (|choice_stop2| "" (SKOLEM!) (("" (REWRITE "choice_commutes") (("" (REWRITE "choice_stop1") NIL NIL)) NIL)) NIL) (|choice_stop3| "" (AUTO-REWRITE "choice_idempotent" "stop_smallest") (("" (SKOLEM!) (("" (GROUND) (("1" (USE "choice_subset1") (("1" (REPLACE*) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (USE "choice_subset2") (("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("3" (REPLACE*) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|choice_empty| "" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL) (|choice_add| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :EXCLUDE "prefix_closed" :IF-MATCH NIL) (("1" (INST?) NIL NIL) ("2" (INST?) NIL NIL) ("3" (INST?) NIL NIL)) NIL)) NIL)) NIL) (|choice_singleton| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :EXCLUDE "prefix_closed") NIL NIL)) NIL)) NIL) (|choice_union| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :EXCLUDE "prefix_closed") NIL NIL)) NIL)) NIL) (|choice_member| "" (GRIND :EXCLUDE "prefix_closed") NIL NIL) (|par_commutes| "" (SKOLEM!) (("" (EXPAND "Par") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (IFF) (("" (GROUND) (("1" (SKOSIMP) (("1" (REWRITE "prod_commutes") (("1" (INST?) NIL NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (REWRITE "prod_commutes") (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|par_assoc| "" (SKOLEM!) (("" (EXPAND "Par") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (REDUCE :IF-MATCH NIL) (("1" (USE "prod_assoc2" ("u" "t2!1")) (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST + "u1!1" "t2!2") (("1" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (USE "prod_assoc1" ("u" "t1!1")) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST + "t1!2" "u1!1") (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|par_stop| "" (AUTO-REWRITE "Par" "Stop") (("" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (IFF) (("" (PROP) (("1" (SKOLEM-TYPEPRED) (("1" (ASSERT) (("1" (REPLACE*) (("1" (FORWARD-CHAIN "prod_null1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM-TYPEPRED) (("2" (ASSERT) (("2" (REPLACE*) (("2" (FORWARD-CHAIN "proj_prod2") (("2" (AUTO-REWRITE "proj") (("2" (AUTO-REWRITE "proj" "filter") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (FORWARD-CHAIN "prod_null3") (("3" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|par_full| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :EXCLUDE ("prod") :REWRITES ("prod_fullset[T]")) NIL NIL)) NIL)) NIL) (|interleaves_commutes| "" (EXPAND "//") (("" (SKOLEM!) (("" (REWRITE "par_commutes") NIL NIL)) NIL)) NIL) (|interleaves_assoc| "" (SKOLEM!) (("" (EXPAND "//") (("" (REWRITE "par_assoc") NIL NIL)) NIL)) NIL) (|interleaves_subset1| "" (GRIND :EXCLUDE ("prefix_closed" "prod") :IF-MATCH NIL) (("" (INST + "x!1" "null") (("" (REWRITE "free_prod_left") NIL NIL)) NIL)) NIL) (|interleaves_subset2| "" (GRIND :EXCLUDE ("prefix_closed" "prod") :IF-MATCH NIL) (("" (INST + "null" "x!1") (("" (REWRITE "free_prod_right") NIL NIL)) NIL)) NIL) (|interleaves_stop1| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :EXCLUDE ("prod" "prefix_closed") :IF-MATCH NIL) (("1" (USE "prod_null1" ("t1" "t1!1" "t" "x!1")) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST + "x!1" "null") (("2" (REWRITE "free_prod_left") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|interleaves_stop2| "" (SKOLEM!) (("" (REWRITE "interleaves_commutes") (("" (REWRITE "interleaves_stop1") NIL NIL)) NIL)) NIL)) $$$parametric_choice.pvs % % Unbounded choice of a family {P(i) | i in U} % % T = event type % U = parameter type % parametric_choice [ U, T : TYPE] : THEORY BEGIN IMPORTING processes, process_rules P : VAR [U -> process[T]] Q : VAR process[T] t : VAR trace[T] i : VAR U %-------------- % Definition %-------------- Choice(P) : process[T] = { t | null?(t) OR EXISTS i : P(i)(t) } %----------------- % Various rules %----------------- choice_equiv : LEMMA Choice(P) = Choice({ Q | EXISTS i : Q = P(i)}) choice_nonempty_param : LEMMA (EXISTS i : true) IMPLIES Choice(P) = union! i : P(i) choice_empty_param : LEMMA (FORALL i : false) IMPLIES Choice(P) = Stop sigma_choice3 : LEMMA sigma(Choice(P)) = union! i : sigma(P(i)) choice_member2 : LEMMA subset?(P(i), Choice(P)) END parametric_choice $$$parametric_choice.prf (|parametric_choice| (|Choice_TCC1| "" (GRIND :IF-MATCH NIL :EXCLUDE ("prefix")) (("1" (DELETE 2) (("1" (GRIND) NIL NIL)) NIL) ("2" (INST?) (("2" (TYPEPRED "P!1(i!1)") (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|choice_equiv| "" (SKOLEM!) (("" (EXPAND "Choice") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (IFF) (("" (GROUND) (("1" (DELETE 1) (("1" (REDUCE) NIL NIL)) NIL) ("2" (DELETE 1) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|choice_nonempty_param| "" (SKOSIMP*) (("" (TYPEPRED "P!1(i!1)") (("" (DELETE -2) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|choice_empty_param| "" (SKOSIMP) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL) (|sigma_choice3| "" (SKOLEM!) (("" (REWRITE "choice_equiv") (("" (REWRITE "sigma_choice2") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (EXPAND "union") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|choice_member2| "" (SKOLEM!) (("" (REWRITE "choice_nonempty_param") (("1" (USE "union_is_bound" ("A" "lambda i : P!1(i)")) NIL NIL) ("2" (INST + "i!1") NIL NIL)) NIL)) NIL)) $$$more_list_props.pvs % % Extension of the pre-defined operations on lists % and extra properties % more_list_props [ T : TYPE] : THEORY BEGIN l, l1, l2 : VAR list[T] cons_l, cons_l1, cons_l2 : VAR (cons?[T]) a, b, c : VAR T P : VAR [list[T] -> bool] %---------------------------------------- % add(l, a) : append a at the end of l %---------------------------------------- add(l, a) : (cons?[T]) = append(l, cons(a, null)) add_null : LEMMA add(null, a) = (: a :) add_cons : LEMMA add(cons(a, l), b) = cons(a, add(l, b)) %------------------------ % Properties of length %------------------------ length_append : LEMMA length(append(l1, l2)) = length(l1) + length(l2) length_add : LEMMA length(add(l, a)) = length(l) + 1 length_reverse : LEMMA length(reverse(l)) = length(l) length_cdr : LEMMA length(cdr(cons_l)) = length(cons_l) - 1 length_zero : LEMMA length(l) = 0 IFF l = null length_non_zero : LEMMA length(l) > 0 IFF cons?(l) %----------------------- % Induction using add %----------------------- cons_to_add : LEMMA FORALL cons_l : EXISTS a, l : cons_l = add(l, a) add_induction : PROPOSITION P(null) AND (FORALL l, a : P(l) IMPLIES P(add(l, a))) IMPLIES (FORALL l : P(l)) END more_list_props $$$more_list_props.prf (|more_list_props| (|add_TCC1| "" (SKOLEM!) (("" (EXPAND "append") (("" (LIFT-IF) (("" (ASSERT) NIL))))))) (|add_null| "" (GRIND) NIL) (|add_cons| "" (GRIND) NIL) (|length_append| "" (SKOLEM + (_ "l2!1")) (("" (INDUCT-AND-SIMPLIFY "l1") NIL))) (|length_add| "" (AUTO-REWRITE "length" "add" "length_append") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|length_reverse| "" (INDUCT-AND-SIMPLIFY "l" :REWRITES ("length_append")) NIL) (|length_cdr| "" (AUTO-REWRITE "length") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|length_zero| "" (GRIND) NIL) (|length_non_zero| "" (GRIND) NIL) (|cons_to_add| "" (AUTO-REWRITE "add_null" "add_cons") (("" (INDUCT "cons_l") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL) ("3" (SKOSIMP) (("3" (GROUND) (("1" (SKOLEM!) (("1" (INST + "a!1" "cons(cons1_var!1, l!1)") (("1" (ASSERT) NIL))))) ("2" (INST + "cons1_var!1" "null") (("2" (ASSERT) (("2" (ASSERT) NIL))))))))))))) (|add_induction| "" (SKOSIMP) (("" (CASE "FORALL (n : nat), l : length(l) = n IMPLIES P!1(l)") (("1" (SKOLEM!) (("1" (INST - "length(l!1)" "l!1") (("1" (ASSERT) NIL))))) ("2" (DELETE 2) (("2" (AUTO-REWRITE "length_zero" "length_add") (("2" (INDUCT "n") (("1" (SKOSIMP) (("1" (ASSERT) NIL))) ("2" (SKOSIMP*) (("2" (USE "length_non_zero" ("l" "l!1")) (("2" (ASSERT) (("2" (USE "cons_to_add" ("cons_l" "l!1")) (("2" (SKOLEM!) (("2" (REPLACE -1) (("2" (INST - "l!2") (("2" (INST?) (("2" (ASSERT) NIL)))))))))))))))))))))))))))) $$$traces.pvs % % Traces over events of type T % defines operators specific to PVS % % Functions defined in the prelude: % length(t) : nat % member(a, t) : bool % nth(t, i) : T (i : below[length(t)]) % append(t1, t2) : trace % reverse(t) : trace % cons(a, t) : trace % null : trace % car(t) : T % cdr(t) : trace % % filter(t, S) : trace % filter(S)(t) : trace % list2set(t) : set[T] % % Defined in more_list_props % add(t, a) : trace % % Defined in trace % prefix(t1, t2) : bool % proj(t, S) : trace % prod(S)(t1, t2, t) : bool % sigma(t) : set[T] % traces [ T : TYPE ] : THEORY BEGIN IMPORTING more_list_props trace : TYPE = list[T] a, b, c : VAR T A, B, C : VAR setof[T] t, t1, t2, t3 : VAR trace u, u1, u2 : VAR trace %----------- % Prefix %----------- prefix(t1, t2) : bool = EXISTS t : t2 = append(t1, t) prefix_equiv : LEMMA prefix(t1, t2) IFF null?(t1) OR (cons?(t1) AND cons?(t2) AND car(t1) = car(t2) AND prefix(cdr(t1), cdr(t2))) null_prefix : LEMMA prefix(null, t) prefix_null : LEMMA prefix(t, null) IFF t = null cons_prefix : LEMMA prefix(cons(a, t1), cons(b, t2)) IFF a = b AND prefix(t1, t2) prefix_append1 : LEMMA prefix(t1, t2) IMPLIES prefix(t1, append(t2, t3)) prefix_append2 : LEMMA prefix(t1, t2) IMPLIES prefix(append(t, t1), append(t, t2)) prefix_add1 : LEMMA prefix(t, add(t, a)) prefix_add2 : LEMMA prefix(t1, t2) IMPLIES prefix(t1, add(t2, a)) length_prefix : LEMMA prefix(t1, t2) IMPLIES length(t1) <= length(t2) prefix_reflexive : LEMMA prefix(t, t) prefix_transitive : LEMMA prefix(t1, t2) AND prefix(t2, t3) IMPLIES prefix(t1, t3) prefix_antisymmetric : LEMMA prefix(t1, t2) AND prefix(t2, t1) IMPLIES t1 = t2 %-------------- % Projection %-------------- proj : [trace, set[T] -> trace] = filter proj_null : LEMMA proj(null, A) = null proj_cons : LEMMA proj(cons(a, t), A) = IF A(a) THEN cons(a, proj(t, A)) ELSE proj(t, A) ENDIF proj_append : LEMMA proj(append(t1, t2), A) = append(proj(t1, A), proj(t2, A)) proj_add : LEMMA proj(add(t, a), A) = IF A(a) THEN add(proj(t, A), a) ELSE proj(t, A) ENDIF proj_prefix : LEMMA prefix(t1, t2) IMPLIES prefix(proj(t1, A), proj(t2, A)) proj_reverse : LEMMA proj(reverse(t), A) = reverse(proj(t, A)) prefix_of_proj : LEMMA prefix(t1, proj(t, A)) IMPLIES EXISTS t2 : prefix(t2, t) AND t1 = proj(t2, A) prefix_of_proj2 : LEMMA prefix(t1, proj(t, A)) IFF EXISTS t2 : prefix(t2, t) AND t1 = proj(t2, A) proj_twice : LEMMA proj(proj(t, A), B) = proj(t, intersection(A, B)) %------------------------------------------------ % product: for parallel composition % -> prod(A)(t1, t2, t) holds if % % t is a possible interleaving of t1 and t2 % with events in A synchronized %------------------------------------------------- prod(A)(t1, t2, t) : RECURSIVE bool = CASES t OF null : null?(t1) AND null?(t2), cons(x, y) : IF A(x) THEN cons?(t1) AND cons?(t2) AND car(t1) = x AND car(t2) = x AND prod(A)(cdr(t1), cdr(t2), y) ELSE (cons?(t1) AND car(t1) = x AND prod(A)(cdr(t1), t2, y)) OR (cons?(t2) AND car(t2) = x AND prod(A)(t1, cdr(t2), y)) ENDIF ENDCASES MEASURE length(t) prod_commutes : LEMMA prod(A)(t1, t2, t) IFF prod(A)(t2, t1, t) proj_prod1 : LEMMA prod(A)(t1, t2, t) IMPLIES proj(t1, A) = proj(t, A) proj_prod2 : LEMMA prod(A)(t1, t2, t) IMPLIES proj(t2, A) = proj(t, A) prod_null1 : LEMMA prod(A)(t1, null, t) IMPLIES t1 = t prod_null2 : LEMMA prod(A)(null, t2, t) IMPLIES t2 = t prod_null3 : LEMMA proj(t, A) = null IMPLIES prod(A)(t, null, t) prod_null4 : LEMMA proj(t, A) = null IMPLIES prod(A)(null, t, t) prefix_prod : LEMMA prod(A)(t1, t2, t) AND prefix(u, t) IMPLIES EXISTS u1, u2 : prefix(u1, t1) AND prefix(u2, t2) AND prod(A)(u1, u2, u) prod_assoc1 : LEMMA prod(A)(t1, t2, u) AND prod(A)(u, t3, t) IMPLIES EXISTS u1 : prod(A)(t1, u1, t) AND prod(A)(t2, t3, u1) prod_assoc2 : LEMMA prod(A)(t1, u, t) AND prod(A)(t2, t3, u) IMPLIES EXISTS u1 : prod(A)(t1, t2, u1) AND prod(A)(u1, t3, t) prod_assoc : LEMMA (EXISTS u : prod(A)(t1, t2, u) AND prod(A)(u, t3, t)) IFF (EXISTS u : prod(A)(t1, u, t) AND prod(A)(t2, t3, u)) prod_fullset : LEMMA prod(fullset)(t1, t2, u) IFF t1 = u AND t2 = u free_prod_left : LEMMA prod(emptyset)(t, null, t) free_prod_right : LEMMA prod(emptyset)(null, t, t) %--------------------------- % sigma(t) : events of t %-------------------------- sigma : [trace -> set[T]] = list2set sigma_equiv : LEMMA sigma(t) = { a | member(a, t) } sigma_null : LEMMA sigma(null) = emptyset sigma_cons : LEMMA sigma(cons(a, t)) = add(a, sigma(t)) sigma_empty : LEMMA empty?(sigma(t)) IFF t = null sigma_append : LEMMA sigma(append(t1, t2)) = union(sigma(t1), sigma(t2)) sigma_add : LEMMA sigma(add(t, a)) = add(a, sigma(t)) sigma_prefix : LEMMA prefix(t1, t2) IMPLIES subset?(sigma(t1), sigma(t2)) sigma_proj : LEMMA sigma(proj(t, A)) = intersection(sigma(t), A) sigma_prod : LEMMA prod(A)(t1, t2, t) IMPLIES sigma(t) = union(sigma(t1), sigma(t2)) sigma_prod_inter1 : LEMMA prod(A)(t1, t2, t) IMPLIES intersection(sigma(t), A) = intersection(sigma(t1), A) sigma_prod_inter2 : LEMMA prod(A)(t1, t2, t) IMPLIES intersection(sigma(t), A) = intersection(sigma(t2), A) %---------------------- % Empty projections %---------------------- null_proj_equiv : LEMMA proj(t, B) = null IFF disjoint?(sigma(t), B) null_proj_subset : LEMMA subset?(A, B) AND proj(t, B) = null IMPLIES proj(t, A) = null null_proj_union : LEMMA proj(t, union(A, B)) = null IFF proj(t, A) = null AND proj(t, B) = null null_proj_prod : LEMMA prod(A)(t1, t2, t) IMPLIES (proj(t, B) = null IFF proj(t1, B) = null AND proj(t2, B) = null) null_proj_prod1 : LEMMA prod(A)(t1, t2, t) AND proj(t, B) = null IMPLIES proj(t1, B) = null null_proj_prod2 : LEMMA prod(A)(t1, t2, t) AND proj(t, B) = null IMPLIES proj(t2, B) = null null_proj_prod3 : LEMMA prod(A)(t1, t2, t) AND subset?(B, A) AND proj(t1, B) = null IMPLIES proj(t, B) = null null_proj_prod4 : LEMMA prod(A)(t1, t2, t) AND subset?(B, A) AND proj(t2, B) = null IMPLIES proj(t, B) = null END traces $$$traces.prf (|traces| (|prefix_equiv| "" (AUTO-REWRITE "prefix" "append") (("" (SKOLEM!) (("" (GROUND) (("1" (SKOLEM!) (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOLEM!) (("2" (ASSERT) (("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("3" (SKOLEM!) (("3" (INST + "t!1") (("3" (REPLACE*) (("3" (EXPAND "append" 1 1) (("3" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("4" (SKOLEM!) (("4" (INST + "t!1") (("4" (APPLY-EXTENSIONALITY) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|null_prefix| "" (SKOLEM!) (("" (REWRITE "prefix_equiv") NIL NIL)) NIL) (|prefix_null| "" (SKOLEM!) (("" (REWRITE "prefix_equiv") (("" (GROUND) NIL NIL)) NIL)) NIL) (|cons_prefix| "" (SKOLEM!) (("" (GROUND) (("1" (REWRITE "prefix_equiv") NIL NIL) ("2" (REWRITE "prefix_equiv" -) NIL NIL) ("3" (REWRITE "prefix_equiv" +) NIL NIL)) NIL)) NIL) (|prefix_append1| "" (EXPAND "prefix") (("" (SKOSIMP*) (("" (REPLACE*) (("" (INST + "append(t!1, t3!1)") (("" (REWRITE "append_assoc") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|prefix_append2| "" (EXPAND "prefix") (("" (SKOSIMP*) (("" (REPLACE*) (("" (INST + "t!2") (("" (REWRITE "append_assoc") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|prefix_add1| "" (AUTO-REWRITE "add" "prefix") (("" (ASSERT) (("" (SKOLEM!) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL) (|prefix_add2| "" (AUTO-REWRITE "add" "prefix_append1") (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|length_prefix| "" (GRIND :DEFS NIL :REWRITES ("prefix" "length_append[T]")) NIL NIL) (|prefix_reflexive| "" (AUTO-REWRITE "append_null" "prefix") (("" (AUTO-REWRITE "append_null[T]" "prefix") (("" (SKOLEM!) (("" (ASSERT) (("" (INST + "null") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prefix_transitive| "" (EXPAND "prefix") (("" (SKOSIMP*) (("" (REPLACE*) (("" (INST + "append(t!1, t!2)") (("" (REWRITE "append_assoc") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|prefix_antisymmetric| "" (EXPAND "prefix") (("" (SKOSIMP*) (("" (AUTO-REWRITE "length_zero[T]" "append_null[T]") (("" (CASE "length(t!1) = 0") (("1" (ASSERT) (("1" (REPLACE -1) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (USE "length_append[T]") (("2" (USE "length_append[T]" ("l1" "t2!1")) (("2" (STOP-REWRITE "length_zero[T]") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|proj_null| "" (GRIND) NIL NIL) (|proj_cons| "" (AUTO-REWRITE "proj" "filter[T]") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|proj_append| "" (SKOLEM 1 ("A!1" _ "t!2")) (("" (INDUCT-AND-SIMPLIFY "t1") NIL NIL)) NIL) (|proj_add| "" (AUTO-REWRITE "proj_append" "add") (("" (SKOLEM!) (("" (ASSERT) (("" (AUTO-REWRITE "proj" "filter" "append_null[T]") (("" (LIFT-IF) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|proj_prefix| "" (GRIND :EXCLUDE ("append" "proj") :REWRITES ("proj_append")) NIL NIL) (|proj_reverse| "" (INDUCT "t") (("1" (GRIND) NIL NIL) ("2" (SKOSIMP*) (("2" (AUTO-REWRITE "reverse" "proj_append") (("2" (ASSERT) (("2" (AUTO-REWRITE "proj" "filter" "append_null[T]") (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prefix_of_proj| "" (SKOLEM + ("A!1" _ _)) (("" (AUTO-REWRITE "proj" "filter" "prefix_null" "null_prefix" "cons_prefix") (("" (INDUCT "t") (("1" (SKOSIMP) (("1" (ASSERT) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (LIFT-IF) (("2" (GROUND) (("1" (REWRITE "prefix_equiv") (("1" (GROUND) (("1" (INST + "null") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST? -) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST + "cons(cons1_var!1, t2!1)") (("2" (ASSERT) (("2" (APPLY-EXTENSIONALITY) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST? -) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST + "cons(cons1_var!1, t2!1)") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prefix_of_proj2| "" (GRIND :DEFS NIL :IF-MATCH NIL :REWRITES ("prefix_of_proj" "proj_prefix")) NIL NIL) (|proj_twice| "" (SKOLEM 1 ("A!1" "B!1" _)) (("" (INDUCT-AND-SIMPLIFY "t") NIL NIL)) NIL) (|prod_TCC1| "" (GRIND) NIL NIL) (|prod_TCC2| "" (GRIND) NIL NIL) (|prod_TCC3| "" (GRIND) NIL NIL) (|prod_commutes| "" (SKOLEM!) (("" (CASE "FORALL t1, t2, t : prod(A!1)(t1, t2, t) IMPLIES prod(A!1)(t2, t1, t)") (("1" (GRIND :IF-MATCH ALL) NIL NIL) ("2" (DELETE 2) (("2" (AUTO-REWRITE "prod" "proj" "filter") (("2" (INDUCT "t") (("1" (SKOSIMP) (("1" (ASSERT) (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (CASE "A!1(cons1_var!1)") (("1" (ASSERT) (("1" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (SPLIT -) (("1" (FLATTEN) (("1" (INST? - :WHERE 3) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (INST? - :WHERE 2) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|proj_prod1| "" (INDUCT-AND-SIMPLIFY "t") NIL NIL) (|proj_prod2| "" (SKOSIMP) (("" (REWRITE "prod_commutes") (("" (FORWARD-CHAIN "proj_prod1") NIL NIL)) NIL)) NIL) (|prod_null1| "" (INDUCT-AND-SIMPLIFY "t") (("" (APPLY-EXTENSIONALITY) NIL NIL)) NIL) (|prod_null2| "" (SKOSIMP) (("" (REWRITE "prod_commutes") (("" (FORWARD-CHAIN "prod_null1") NIL NIL)) NIL)) NIL) (|prod_null3| "" (INDUCT-AND-SIMPLIFY "t") NIL NIL) (|prod_null4| "" (SKOSIMP) (("" (REWRITE "prod_commutes") (("" (REWRITE "prod_null3") NIL NIL)) NIL)) NIL) (|prefix_prod| "" (SKOLEM + ("A!1" _ _ _ _)) (("" (AUTO-REWRITE "prod" "prefix_null" "null_prefix") (("" (INDUCT "t") (("1" (SKOSIMP) (("1" (ASSERT) (("1" (INST + "null" "null") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (CASE "null?(u!1)") (("1" (DELETE -2 -3) (("1" (INST + "null" "null") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (REWRITE "prefix_equiv") (("2" (ASSERT) (("2" (GROUND) (("1" (INST? -) (("1" (INST? -) (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST + "cons(cons1_var!1, u1!1)" "cons(cons1_var!1, u2!1)") (("1" (ASSERT) (("1" (AUTO-REWRITE "prefix_equiv") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST? -) (("2" (INST? -) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST + "cons(cons1_var!1, u1!1)" "u2!1") (("2" (ASSERT) (("2" (REWRITE "prefix_equiv" +) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (INST? -) (("3" (INST? -) (("3" (ASSERT) (("3" (SKOSIMP) (("3" (INST + "u1!1" "cons(cons1_var!1, u2!1)") (("3" (ASSERT) (("3" (REWRITE "prefix_equiv" +) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prod_assoc1| "" (SKOLEM 1 ("A!1" _ _ _ _ _)) (("" (AUTO-REWRITE "prod") (("" (INDUCT "t") (("1" (REDUCE) NIL NIL) ("2" (SKOSIMP*) (("2" (REDUCE :IF-MATCH NIL) (("1" (INST?) (("1" (INST?) (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST + "cons(cons1_var!1, u1!1)") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST? -) (("2" (INST? -) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (INST? -) (("3" (INST? -) (("3" (ASSERT) (("3" (SKOSIMP) (("3" (INST + "cons(cons1_var!1, u1!1)") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (INST? -) (("4" (INST? -) (("4" (ASSERT) (("4" (SKOSIMP) (("4" (INST + "cons(cons1_var!1, u1!1)") (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prod_assoc2| "" (SKOLEM 1 ("A!1" _ _ _ _ _)) (("" (AUTO-REWRITE "prod") (("" (INDUCT "t") (("1" (REDUCE) NIL NIL) ("2" (SKOSIMP*) (("2" (REDUCE :IF-MATCH NIL) (("1" (INST - "cdr(t1!1)" "cdr(t2!1)" "cdr(t3!1)" "cdr(u!1)") (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST + "cons(cons1_var!1, u1!1)") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST - "cdr(t1!1)" "t2!1" "t3!1" "u!1") (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST + "cons(cons1_var!1, u1!1)") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (INST - "t1!1" "cdr(t2!1)" "t3!1" "cdr(u!1)") (("3" (ASSERT) (("3" (SKOSIMP) (("3" (INST + "cons(cons1_var!1, u1!1)") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("4" (INST - "t1!1" "t2!1" "cdr(t3!1)" "cdr(u!1)") (("4" (ASSERT) (("4" (SKOSIMP) (("4" (INST?) (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prod_assoc| "" (REDUCE :IF-MATCH NIL) (("1" (USE "prod_assoc1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (USE "prod_assoc2") (("2" (ASSERT) NIL NIL)) NIL)) NIL) (|prod_fullset| "" (AUTO-REWRITE "fullset" "prod") (("" (INDUCT "u") (("1" (REDUCE) NIL NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (SPLIT) (("1" (FLATTEN) (("1" (ASSERT) (("1" (INST?) (("1" (GROUND) (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL) ("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (ASSERT) (("2" (INST?) (("2" (REPLACE*) (("2" (DELETE -) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|free_prod_left| "" (INDUCT-AND-SIMPLIFY "t") NIL NIL) (|free_prod_right| "" (INDUCT-AND-SIMPLIFY "t") NIL NIL) (|sigma_equiv| "" (INDUCT-AND-SIMPLIFY "t") (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL) ("2" (REPLACE*) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (SMASH) NIL NIL)) NIL)) NIL)) NIL) (|sigma_null| "" (GRIND) NIL NIL) (|sigma_cons| "" (GRIND) NIL NIL) (|sigma_empty| "" (GRIND) NIL NIL) (|sigma_append| "" (INDUCT-AND-SIMPLIFY "t1") (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL) ("2" (REPLACE*) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (SMASH) NIL NIL)) NIL)) NIL)) NIL) (|sigma_add| "" (EXPAND "add" 1 1) (("" (SKOLEM!) (("" (REWRITE "sigma_append") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_prefix| "" (AUTO-REWRITE "prefix" "sigma_append") (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (REDUCE) NIL NIL)) NIL)) NIL) (|sigma_proj| "" (INDUCT-AND-SIMPLIFY "t") (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL) ("2" (REPLACE*) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (SMASH) NIL NIL)) NIL)) NIL) ("3" (REPLACE*) (("3" (APPLY-EXTENSIONALITY :HIDE? T) (("3" (SMASH) NIL NIL)) NIL)) NIL)) NIL) (|sigma_prod| "" (INDUCT-AND-SIMPLIFY "t") (("1" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL) ("2" (REPLACE*) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (IFF) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("3" (REPLACE*) (("3" (APPLY-EXTENSIONALITY :HIDE? T) (("3" (IFF) (("3" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("4" (REPLACE*) (("4" (APPLY-EXTENSIONALITY :HIDE? T) (("4" (IFF) (("4" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_prod_inter1| "" (SKOSIMP) (("" (FORWARD-CHAIN "proj_prod1") (("" (REWRITE "sigma_proj" :DIR RL) (("" (REWRITE "sigma_proj" :DIR RL) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_prod_inter2| "" (SKOSIMP) (("" (REWRITE "prod_commutes") (("" (FORWARD-CHAIN "sigma_prod_inter1") NIL NIL)) NIL)) NIL) (|null_proj_equiv| "" (SKOLEM + ("B!1" _)) (("" (INDUCT-AND-SIMPLIFY "t") NIL NIL)) NIL) (|null_proj_subset| "" (AUTO-REWRITE "null_proj_equiv") (("" (SKOSIMP) (("" (ASSERT) (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|null_proj_union| "" (AUTO-REWRITE "null_proj_equiv") (("" (SKOLEM!) (("" (ASSERT) (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|null_proj_prod| "" (AUTO-REWRITE "null_proj_equiv") (("" (SKOSIMP) (("" (ASSERT) (("" (FORWARD-CHAIN "sigma_prod") (("" (REPLACE*) (("" (DELETE -) (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|null_proj_prod1| "" (SKOSIMP) (("" (USE "null_proj_prod") (("" (GROUND) NIL NIL)) NIL)) NIL) (|null_proj_prod2| "" (SKOSIMP) (("" (REWRITE "prod_commutes") (("" (FORWARD-CHAIN "null_proj_prod1") NIL NIL)) NIL)) NIL) (|null_proj_prod3| "" (AUTO-REWRITE "null_proj_equiv") (("" (SKOSIMP) (("" (ASSERT) (("" (FORWARD-CHAIN "sigma_prod_inter1") (("" (DELETE -2) (("" (AUTO-REWRITE-THEORY "sets[T]") (("" (REDUCE) (("" (CASE "intersection(sigma(t!1), A!1)(x!1)") (("1" (REPLACE -2) (("1" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|null_proj_prod4| "" (SKOSIMP) (("" (REWRITE "prod_commutes") (("" (FORWARD-CHAIN "null_proj_prod3") NIL NIL)) NIL)) NIL)) $$$processes.pvs % % Processes with alphabet T % (trace semantics) % processes [ T : TYPE ] : THEORY BEGIN IMPORTING traces S : VAR setof[trace[T]] A : VAR setof[T] t, t1, t2 : VAR trace[T] %=================================================== % process: non-empty, prefix closed set of traces %=================================================== prefix_closed(S) : bool = FORALL t1, t2 : prefix(t1, t2) AND S(t2) IMPLIES S(t1) process : TYPE = { S | S(null) AND prefix_closed(S) } P, P1, P2 : VAR process SP : VAR set[process] a : VAR T %=================== % Process algebra %=================== %----------- % Stop[T] %----------- Stop : process = { t | t = null }; %------------------ % Bounded choice %------------------ \/(P1, P2) : process = union(P1, P2) %--------------------- % Unbounded choice %--------------------- Choice(SP) : process = { t | null?(t) OR EXISTS (P : (SP)) : P(t) }; %----------- % a >> P %----------- >> (a, P) : process = { t | null?(t) OR EXISTS (t1 : (P)) : t = cons(a, t1) } %------------------------ % Parallel composition %------------------------ Par(A)(P1, P2) : process = { t | EXISTS (t1 : (P1)), (t2 : (P2)) : prod(A)(t1, t2, t) }; %---------------- % Interleaving %---------------- //(P1, P2) : process = Par(emptyset)(P1, P2) %========================== % sigma(P) = events of P %========================== sigma(P) : setof[T] = { a | EXISTS (t : (P)) : sigma(t)(a) } END processes $$$processes.prf (|processes| (|Stop_TCC1| "" (GRIND :EXCLUDE ("prefix") :REWRITES ("prefix_null[T]")) NIL NIL) (|vee_TCC1| "" (GRIND :EXCLUDE ("prefix")) NIL NIL) (|Choice_TCC1| "" (GRIND :EXCLUDE "prefix" :IF-MATCH NIL) (("1" (DELETE 2) (("1" (EXPAND "prefix") (("1" (REDUCE) NIL NIL)) NIL)) NIL) ("2" (REDUCE) NIL NIL)) NIL) (|doublegreaterp_TCC1| "" (GRIND :DEFS NIL :REWRITES ("prefix_closed") :IF-MATCH NIL) (("1" (REWRITE "prefix_equiv") NIL NIL) ("2" (REWRITE "prefix_equiv") (("2" (GROUND) (("2" (INST? -) (("2" (ASSERT) (("2" (INST + "cdr(t1!1)") (("2" (APPLY-EXTENSIONALITY) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Par_TCC1| "" (SKOLEM-TYPEPRED) (("" (PROP) (("1" (EXPAND "prod") (("1" (INST + "null" "null") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (EXPAND "prefix_closed") (("2" (SKOSIMP*) (("2" (FORWARD-CHAIN "prefix_prod") (("2" (SKOSIMP) (("2" (INST? - :WHERE -1) (("2" (INST? - :WHERE -2) (("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$csp_traces.pvs % % Includes all the basic theories for CSP % trace semantics % csp_traces : THEORY BEGIN IMPORTING processes, parametric_choice, multipar, satisfaction, satisfaction2, satisfaction3, fixed_points, fixed_points2, process_rules END csp_traces $$$message_traces.pvs % % Traces of transmission or reception events % message_traces [I, M : TYPE] : THEORY BEGIN IMPORTING csp_traces, event[I, M] t : VAR trace[event] i, j : VAR I m : VAR M %----------------------------------------------------------------- % Projection of a trace on the reception or transmission events %----------------------------------------------------------------- receptions(t) : trace[event] = proj(t, rec?) transmissions(t) : trace[event] = proj(t, trans?) %-------------------------------------------- % specialization of some projection lemmas %-------------------------------------------- receptions_null : LEMMA receptions(null) = null transmissions_null : LEMMA transmissions(null) = null receptions_add1 : LEMMA receptions(add(t, rec(i, j, m))) = add(receptions(t), rec(i, j, m)) transmissions_add1 : LEMMA transmissions(add(t, trans(i, j, m))) = add(transmissions(t), trans(i, j, m)) receptions_add2 : LEMMA receptions(add(t, trans(i, j, m))) = receptions(t) transmissions_add2 : LEMMA transmissions(add(t, rec(i, j, m))) = transmissions(t) receptions_cons1 : LEMMA receptions(cons(rec(i, j, m), t)) = cons(rec(i, j, m), receptions(t)) transmissions_cons1 : LEMMA transmissions(cons(trans(i, j, m), t)) = cons(trans(i, j, m), transmissions(t)) receptions_cons2 : LEMMA receptions(cons(trans(i, j, m), t)) = receptions(t) transmissions_cons2 : LEMMA transmissions(cons(rec(i, j, m), t)) = transmissions(t) %----------------------- % properties of sigma %----------------------- union_rec_trans : LEMMA sigma(t) = union(sigma(receptions(t)), sigma(transmissions(t))) disjoint_rec_trans : LEMMA disjoint?(sigma(receptions(t)), sigma(transmissions(t))) sigma_receptions : LEMMA subset?(sigma(receptions(t)), sigma(t)) sigma_transmissions : LEMMA subset?(sigma(transmissions(t)), sigma(t)) %------------------------------------ % Messages received or transmitted %------------------------------------ rec_msg(t) : set[M] = { m | EXISTS i, j : member(rec(i, j, m), sigma(t)) } trans_msg(t) : set[M] = { m | EXISTS i, j : member(trans(i, j, m), sigma(t)) } rec_msg_cons1 : LEMMA rec_msg(cons(rec(i, j, m), t)) = add(m, rec_msg(t)) trans_msg_cons1 : LEMMA trans_msg(cons(trans(i, j, m), t)) = add(m, trans_msg(t)) rec_msg_cons2 : LEMMA rec_msg(cons(trans(i, j, m), t)) = rec_msg(t) trans_msg_cons2 : LEMMA trans_msg(cons(rec(i, j, m), t)) = trans_msg(t) rec_msg_add1 : LEMMA rec_msg(add(t, rec(i, j, m))) = add(m, rec_msg(t)) trans_msg_add1 : LEMMA trans_msg(add(t, trans(i, j, m))) = add(m, trans_msg(t)) rec_msg_add2 : LEMMA rec_msg(add(t, trans(i, j, m))) = rec_msg(t) trans_msg_add2 : LEMMA trans_msg(add(t, rec(i, j, m))) = trans_msg(t) END message_traces $$$message_traces.prf (|message_traces| (|receptions_null| "" (AUTO-REWRITE "receptions" "proj_null[event]") (("" (ASSERT) NIL NIL)) NIL) (|transmissions_null| "" (AUTO-REWRITE "transmissions" "proj_null[event]") (("" (ASSERT) NIL NIL)) NIL) (|receptions_add1| "" (AUTO-REWRITE "receptions" "proj_add[event]") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|transmissions_add1| "" (AUTO-REWRITE "transmissions" "proj_add[event]") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|receptions_add2| "" (AUTO-REWRITE "receptions" "proj_add[event]") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|transmissions_add2| "" (AUTO-REWRITE "transmissions" "proj_add[event]") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|receptions_cons1| "" (AUTO-REWRITE "receptions" "proj_cons[event]") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|transmissions_cons1| "" (AUTO-REWRITE "transmissions" "proj_cons[event]") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|receptions_cons2| "" (AUTO-REWRITE "receptions" "proj_cons[event]") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|transmissions_cons2| "" (AUTO-REWRITE "transmissions" "proj_cons[event]") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|union_rec_trans| "" (SKOLEM!) (("" (AUTO-REWRITE "receptions" "transmissions" "sigma_proj[event]") (("" (ASSERT) (("" (AUTO-REWRITE-THEORY "sets[event]") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (IFF) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|disjoint_rec_trans| "" (SKOLEM!) (("" (AUTO-REWRITE "receptions" "transmissions" "sigma_proj[event]") (("" (ASSERT) (("" (AUTO-REWRITE-THEORY "sets[event]") (("" (ASSERT) (("" (SKOLEM!) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_receptions| "" (SKOLEM!) (("" (AUTO-REWRITE "receptions" "transmissions" "sigma_proj[event]") (("" (ASSERT) (("" (AUTO-REWRITE-THEORY "sets[event]") (("" (ASSERT) (("" (SKOLEM!) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_transmissions| "" (SKOLEM!) (("" (AUTO-REWRITE "receptions" "transmissions" "sigma_proj[event]") (("" (ASSERT) (("" (AUTO-REWRITE-THEORY "sets[event]") (("" (ASSERT) (("" (SKOLEM!) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|rec_msg_cons1| "" (SKOLEM!) (("" (AUTO-REWRITE "rec_msg" "receptions_cons1" "sigma_cons[event]") (("" (AUTO-REWRITE-THEORIES "sets[event]" "sets[M]") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (APPLY (THEN* (REDUCE :IF-MATCH NIL) (INST?) (ASSERT))) (("" (CASE "r_msg(rec(i!1, j!1, m!1)) = x!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|trans_msg_cons1| "" (SKOLEM!) (("" (AUTO-REWRITE "trans_msg" "transmissions_cons1" "sigma_cons[event]") (("" (AUTO-REWRITE-THEORIES "sets[event]" "sets[M]") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (APPLY (THEN* (REDUCE :IF-MATCH NIL) (INST?) (ASSERT))) (("" (CASE "t_msg(trans(i!1, j!1, m!1)) = x!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|rec_msg_cons2| "" (SKOLEM!) (("" (AUTO-REWRITE "rec_msg" "sigma_cons[event]") (("" (AUTO-REWRITE-THEORIES "sets[event]" "sets[M]") (("" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL)) NIL)) NIL) (|trans_msg_cons2| "" (SKOLEM!) (("" (AUTO-REWRITE "trans_msg" "sigma_cons[event]") (("" (AUTO-REWRITE-THEORIES "sets[event]" "sets[M]") (("" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL)) NIL)) NIL) (|rec_msg_add1| "" (SKOLEM!) (("" (AUTO-REWRITE "rec_msg" "receptions_add1" "sigma_add[event]") (("" (AUTO-REWRITE-THEORIES "sets[event]" "sets[M]") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (APPLY (THEN* (REDUCE :IF-MATCH NIL) (INST?) (ASSERT))) (("" (CASE "r_msg(rec(i!1, j!1, m!1)) = x!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|trans_msg_add1| "" (SKOLEM!) (("" (AUTO-REWRITE "trans_msg" "transmissions_add1" "sigma_add[event]") (("" (AUTO-REWRITE-THEORIES "sets[event]" "sets[M]") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (APPLY (THEN* (REDUCE :IF-MATCH NIL) (INST?) (ASSERT))) (("" (CASE "t_msg(trans(i!1, j!1, m!1)) = x!1") (("1" (ASSERT) NIL NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|rec_msg_add2| "" (SKOLEM!) (("" (AUTO-REWRITE "rec_msg" "sigma_add[event]") (("" (AUTO-REWRITE-THEORIES "sets[event]" "sets[M]") (("" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL)) NIL)) NIL) (|trans_msg_add2| "" (SKOLEM!) (("" (AUTO-REWRITE "trans_msg" "sigma_add[event]") (("" (AUTO-REWRITE-THEORIES "sets[event]" "sets[M]") (("" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL)) NIL)) NIL)) $$$rank_functions.pvs % % Properties of a rank function on sets and traces % rank_functions [I, M : TYPE] : THEORY BEGIN IMPORTING message_traces[I, M] t : VAR trace[event] m : VAR M i, j : VAR I E, E1, E2 : VAR set[M] A, A1, A2 : VAR set[event] e : VAR event rho : VAR [M -> int] %---------------------------------- % Conversions messages <-> events %---------------------------------- Ev(E) : set[event] = { e | EXISTS i, j, m : E(m) AND (e = rec(i, j, m) OR e = trans(i, j, m)) } Msg(A) : set[M] = { m | EXISTS i, j : A(rec(i, j, m)) OR A(trans(i, j, m)) } msg(e) : M = CASES e OF rec(i, j, m): m, trans(i, j, m) : m ENDCASES %----------------------------------------------------- % rho positive or non-positive on a set of messages %----------------------------------------------------- positive(rho, E) : bool = FORALL (m : (E)) : rho(m) > 0 non_positive(rho, E) : bool = FORALL (m : (E)) : rho(m) <= 0 posmsg_subset : LEMMA subset?(E1, E2) AND positive(rho, E2) IMPLIES positive(rho, E1) %----------------------------------------------------- % rho positive or non-positive on a set of events %----------------------------------------------------- positive(rho, A) : bool = FORALL (e : (A)) : rho(msg(e)) > 0 non_positive(rho, A) : bool = FORALL (e : (A)) : rho(msg(e)) <= 0 positive_subset : LEMMA subset?(A1, A2) AND positive(rho, A2) IMPLIES positive(rho, A1) pos_equiv : LEMMA positive(rho, A) IFF positive(rho, Msg(A)) nonpos_equiv : LEMMA non_positive(rho, A) IFF non_positive(rho, Msg(A)) %--------------------------------- % rho positive on a trace, % on the receptions events, % or on the transmission events %--------------------------------- positive(rho, t) : bool = positive(rho, sigma(t)) pos_rec(rho, t) : bool = positive(rho, receptions(t)) pos_trans(rho, t) : bool = positive(rho, transmissions(t)) positive_null : LEMMA positive(rho, null) positive_cons : LEMMA positive(rho, cons(e, t)) IFF positive(rho, t) AND rho(msg(e)) > 0 positive_add : LEMMA positive(rho, add(t, e)) IFF positive(rho, t) AND rho(msg(e)) > 0 positive_proj : LEMMA positive(rho, t) IMPLIES positive(rho, proj(t, A)) nonpos_null_proj : LEMMA positive(rho, t) AND non_positive(rho, A) IMPLIES proj(t, A) = null pos_rec_equiv : LEMMA pos_rec(rho, t) IFF positive(rho, rec_msg(t)) pos_trans_equiv : LEMMA pos_trans(rho, t) IFF positive(rho, trans_msg(t)) positive_receptions : LEMMA positive(rho, t) IMPLIES pos_rec(rho, t) positive_transmissions : LEMMA positive(rho, t) IMPLIES pos_trans(rho, t) END rank_functions $$$rank_functions.prf (|rank_functions| (|posmsg_subset| "" (GRIND) NIL) (|positive_subset| "" (GRIND :EXCLUDE "msg") NIL) (|pos_equiv| "" (GRIND :REWRITES ("event_trans_eta" "event_rec_eta")) (("1" (INST + "r_rcv(e!1)" "r_snd(e!1)") (("1" (GROUND) NIL))) ("2" (INST + "t_snd(e!1)" "t_rcv(e!1)") (("2" (GROUND) NIL))))) (|nonpos_equiv| "" (GRIND :REWRITES ("event_trans_eta" "event_rec_eta")) (("1" (INST + "r_rcv(e!1)" "r_snd(e!1)") (("1" (GROUND) NIL))) ("2" (INST + "t_snd(e!1)" "t_rcv(e!1)") (("2" (GROUND) NIL))))) (|positive_null| "" (GRIND) NIL) (|positive_cons| "" (AUTO-REWRITE "sigma_cons[event]" "positive") (("" (SKOLEM!) (("" (ASSERT) (("" (AUTO-REWRITE-THEORY "sets[event]") (("" (PROP) (("1" (SKOLEM!) (("1" (INST?) NIL))) ("2" (INST?) NIL) ("3" (SKOLEM-TYPEPRED) (("3" (ASSERT) (("3" (ASSERT) (("3" (INST - "e!2") NIL))))))))))))))))) (|positive_add| "" (AUTO-REWRITE "sigma_add[event]" "positive") (("" (SKOLEM!) (("" (ASSERT) (("" (AUTO-REWRITE-THEORY "sets[event]") (("" (PROP) (("1" (SKOLEM!) (("1" (INST?) NIL))) ("2" (INST?) NIL) ("3" (SKOLEM-TYPEPRED) (("3" (ASSERT) (("3" (ASSERT) (("3" (INST - "e!2") NIL))))))))))))))))) (|positive_proj| "" (SKOSIMP) (("" (EXPAND "positive") (("" (REWRITE "sigma_proj") (("" (GRIND :EXCLUDE ("sigma" "msg")) NIL))))))) (|nonpos_null_proj| "" (SKOSIMP) (("" (REWRITE "null_proj_equiv") (("" (GRIND :EXCLUDE ("sigma" "msg")) NIL))))) (|pos_rec_equiv| "" (GRIND :EXCLUDE ("sigma" "proj") :REWRITES ("sigma_proj[event]" "intersection" "member")) (("" (INST + "r_rcv(e!1)" "r_snd(e!1)") (("" (REWRITE "event_rec_eta") NIL))))) (|pos_trans_equiv| "" (GRIND :EXCLUDE ("sigma" "proj") :REWRITES ("sigma_proj[event]" "intersection" "member")) (("" (INST + "t_snd(e!1)" "t_rcv(e!1)") (("" (REWRITE "event_trans_eta") NIL))))) (|positive_receptions| "" (SKOSIMP) (("" (EXPAND "pos_rec") (("" (EXPAND "receptions") (("" (REWRITE "positive_proj") NIL))))))) (|positive_transmissions| "" (SKOSIMP) (("" (EXPAND "pos_trans") (("" (EXPAND "transmissions") (("" (REWRITE "positive_proj") NIL)))))))) $$$messages.pvs % % Datatype for representing messages % with a public key encryption % % WARNING : NEVER USE THE CONSTRUCTOR code IN PROCESS DEFINITIONS % messages : THEORY BEGIN Identity : NONEMPTY_TYPE = nat Text : NONEMPTY_TYPE Nonce : NONEMPTY_TYPE = nat message : DATATYPE WITH SUBTYPES key, nonkey BEGIN text (x_text : Text) : text? : nonkey nonce (x_nonce : Nonce) : nonce? : nonkey user (x_user : Identity) : user? : nonkey public (x_public : Identity) : public? : key secret (x_secret : Identity) : secret? : key conc (x_conc, y_conc : message) : conc? : nonkey code (x_code : key, y_code : message) : code? : nonkey END message m, m1, m2 : VAR message k : VAR key i, j : VAR Identity S, S1, S2, A, B : VAR set[message] rho : VAR [message -> int] %--------------------------------------------------- % size(m) : measure for recursive definitions %--------------------------------------------------- size(m) : RECURSIVE nat = CASES m OF text(x) : 0, nonce(x) : 0, user(x) : 0, public(x) : 0, secret(x) : 0, conc(x1, x2) : size(x1) + size(x2) + 1, code(x1, x2) : size(x1) + size(x2) + 1 ENDCASES MEASURE m BY << %----------------------------------------------------- % Coding/decoding function % this must be used instead of the constructor code %----------------------------------------------------- crypto(k, m) : message = CASES m OF code(x, y) : CASES k OF public(i) : IF x = secret(i) THEN y ELSE code(k, m) ENDIF, secret(i) : IF x = public(i) THEN y ELSE code(k, m) ENDIF ENDCASES ELSE code(k, m) ENDCASES %---------------------- % Message generation %---------------------- Gen(S)(m) : INDUCTIVE bool = S(m) OR (EXISTS m1, m2 : Gen(S)(m1) AND Gen(S)(m2) AND m = conc(m1, m2)) OR (EXISTS m1 : Gen(S)(conc(m1, m))) OR (EXISTS m2 : Gen(S)(conc(m, m2))) OR (EXISTS m1, k : Gen(S)(m1) AND Gen(S)(k) AND m = crypto(k, m1)); |-(S, m) : bool = Gen(S)(m) gen_msg_induction : PROPOSITION subset?(S, A) AND (FORALL m1, m2 : A(conc(m1, m2)) <=> A(m1) AND A(m2)) AND (FORALL m, k : A(m) AND A(k) => A(crypto(k, m))) IMPLIES subset?(Gen(S), A) gen_monotonic : PROPOSITION subset?(S1, S2) IMPLIES subset?(Gen(S1), Gen(S2)) gen_monotonic2 : COROLLARY subset?(S1, S2) AND (S1 |- m) IMPLIES (S2 |- m) %----------------------------------------------------- % Lemma for showing that a rank function satisfies % the main condition of the authentication theorems %----------------------------------------------------- IMPORTING rank_functions[Identity, message] rank_valid : PROPOSITION (FORALL m1, m2 : rho(conc(m1, m2)) > 0 <=> rho(m1) > 0 AND rho(m2) > 0) AND (FORALL m, k : rho(m) > 0 AND rho(k) > 0 IMPLIES rho(crypto(k, m)) > 0) IMPLIES (FORALL S, m : positive(rho, S) AND (S |- m) IMPLIES rho(m) > 0) END messages $$$messages.prf (|messages| (|size_TCC1| "" (GRIND) NIL NIL) (|size_TCC2| "" (GRIND) NIL NIL) (|size_TCC3| "" (GRIND) NIL NIL) (|size_TCC4| "" (GRIND) NIL NIL) (|crypto_TCC1| "" (SKOSIMP) (("" (TYPEPRED "k!1") (("" (GROUND) NIL NIL)) NIL)) NIL) (|gen_msg_induction| "" (SKOSIMP) (("" (LEMMA "Gen_weak_induction") (("" (INST - "S!1" "A!1") (("" (EXPAND* "subset?" "member") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|gen_monotonic| "" (SKOSIMP) (("" (REWRITE "gen_msg_induction") (("1" (DELETE 2) (("1" (EXPAND "Gen") (("1" (EXPAND "subset?") (("1" (EXPAND "member") (("1" (SKOSIMP) (("1" (INST? -) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 2) (("2" (SKOLEM!) (("2" (GROUND) (("1" (EXPAND "Gen" +) (("1" (FLATTEN) (("1" (INST? 4) NIL NIL)) NIL)) NIL) ("2" (EXPAND "Gen" +) (("2" (FLATTEN) (("2" (INST? 3) NIL NIL)) NIL)) NIL) ("3" (EXPAND "Gen" +) (("3" (FLATTEN) (("3" (INST?) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (DELETE -1 2) (("3" (SKOSIMP) (("3" (EXPAND "Gen" +) (("3" (FLATTEN) (("3" (INST? 5) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|gen_monotonic2| "" (SKOSIMP) (("" (EXPAND "|-") (("" (FORWARD-CHAIN "gen_monotonic") (("" (DELETE -2) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|rank_valid| "" (SKOSIMP*) (("" (LEMMA "gen_msg_induction" ("S" "S!1" "A" "{m | rho!1(m) > 0}")) (("" (GROUND) (("1" (DELETE -2 -3 -4) (("1" (GRIND :EXCLUDE ("Gen")) NIL NIL)) NIL) ("2" (DELETE -1 -2 -4 2) (("2" (GRIND :EXCLUDE ("Gen")) NIL NIL)) NIL)) NIL)) NIL)) NIL)) $$$needham_schroeder.pvs % % The Needham Schroeder Protocol: Origin Authentication % needham_schroeder : THEORY BEGIN IMPORTING messages, network[Identity, message, |-] i, j : VAR Identity x, y, m : VAR message xn : VAR (nonce?) k : VAR key e : VAR event n : VAR int v : VAR Nonce S : VAR set[message] %-------------------------------- % identities of the two agents %-------------------------------- a : Identity b : { i | i /= a } %----------------------- % Nonces for a and b %----------------------- na : Nonce nb : { v | v /= na } %----------------- % Abbreviations %----------------- Ia : (user?) = user(a) Ib : (user?) = user(b) Na : (nonce?) = nonce(na) Nb : (nonce?) = nonce(nb) pub(i, x) : message = crypto(public(i), x) sec(i, x) : message = crypto(secret(i), x) %========================== % Protocol Participants %========================== %-------------------------------- % userA : can recognize nonces %-------------------------------- userA : process[event] = Choice! i, xn : ( trans(a, i, pub(i, conc(Na, Ia))) >> ( rec(a, i, pub(a, conc(Na, xn))) >> ( trans(a, i, pub(i, xn)) >> Stop[event] ))) interface_userA : LEMMA subset?(sigma(userA), LocalEvents(a)) %--------------------------------------------- % userA2 cannot detect whether x is a nonce %--------------------------------------------- userA2 : process[event] = Choice! i, x : ( trans(a, i, pub(i, conc(Na, Ia))) >> ( rec(a, i, pub(a, conc(Na, x))) >> ( trans(a, i, pub(i, x)) >> Stop[event] ))) interface_userA2 : LEMMA subset?(sigma(userA2), LocalEvents(a)) %--------- % userB %--------- userB : process[event] = Choice! y: ( rec(b, a, pub(b, conc(y, Ia))) >> ( trans(b, a, pub(a, conc(y, Nb))) >> ( rec(b, a, pub(b, Nb)) >> Stop[event] ))) interface_userB : LEMMA subset?(sigma(userB), LocalEvents(b)) %=============================================================== % INIT set: nonce Nb and secret keys of A and B are not known %=============================================================== INIT_nonce : set[message] = { m | EXISTS v : v /= nb AND m = nonce(v) } INIT_secret : set[message] = { m | EXISTS i : i /= a AND i /= b AND m = secret(i) } INIT : set[message] = { m | user?(m) OR text?(m) OR public?(m) OR INIT_nonce(m) OR INIT_secret(m) } %====================================== % Origin authentication (property 4) %====================================== %------------------------ % authenticator events %------------------------ T1 : set[event] = { e | e = rec(b, a, pub(b, Nb)) } R1 : set[event] = { e | EXISTS i, xn : e = rec(a, i, pub(a, conc(xn, Nb))) } %------------------- % rank function %------------------ rank_code(k, n) : int = CASES k OF public(z) : IF z = a THEN n + 1 ELSE n ENDIF, secret(z) : IF z = a THEN n - 1 ELSE n ENDIF ENDCASES rho(m) : RECURSIVE int = CASES m OF text(z) : 1, nonce(z) : IF z = nb THEN 0 ELSE 1 ENDIF, user(z) : 1, public(z) : 1, secret(z) : IF z = a OR z = b THEN 0 ELSE 1 ENDIF, conc(z1, z2) : min(rho(z1), rho(z2)), code(k, z) : rank_code(k, rho(z)) ENDCASES MEASURE size(m) %---------------------- % Constraints on rho %---------------------- validity_rho : LEMMA FORALL S, m : positive(rho, S) AND (S |- m) IMPLIES rho(m) > 0 rank_init : LEMMA positive(rho, INIT) nonpositive_rank : LEMMA non_positive(rho, T1) %----------------------------- % User a maintains rho on a %----------------------------- IMPORTING rank_rules2, rank_rules3 rank_user_a : LEMMA userA # R1 |> RankUser(rho) %----------------------------- % User b maintains rho on b %----------------------------- rank_user_b : LEMMA userB # R1 |> RankUser(rho) %---------------- % Consequence %---------------- authentication_origin1 : PROPOSITION network(enemy(INIT), protocol(a, b, userA, userB)) |> auth(T1, R1) %========================================== % Variant: property 4 with weaker typing % A cannot detect whether x is a nonce %========================================== %----------------------------------------------------------------- % the authenticator event is the same: "rec(b, a, pub(b, Nb)))" % the set of events to authenticate is larger %----------------------------------------------------------------- T2 : set[event] = T1 R2 : set[event] = { e | EXISTS i, x : e = rec(a, i, pub(a, conc(x, Nb))) } %-------------------------- % rank function (fixed) %-------------------------- % auxiliary function % the rank of code(k, m) assuming the rank of m is n rank_code2(k, m, n) : int = CASES k OF public(j) : IF j = a AND conc?(m) AND y_conc(m) = Nb THEN n + 1 ELSE n ENDIF, secret(j) : IF j = a AND (EXISTS y : m = pub(a, conc(y, Nb))) THEN n - 1 ELSE n ENDIF ENDCASES rho2(m) : RECURSIVE int = CASES m OF text(z) : 1, nonce(z) : IF z = nb THEN 0 ELSE 1 ENDIF, user(z) : 1, public(z) : 1, secret(z) : IF z = a OR z = b THEN 0 ELSE 1 ENDIF, conc(z1, z2) : min(rho2(z1), rho2(z2)), code(k, z) : rank_code2(k, z, rho2(z)) ENDCASES MEASURE size(m) %----------------------- % Contraints for rho2 %----------------------- validity_rho2 : LEMMA FORALL S, m : positive(rho2, S) AND (S |- m) IMPLIES rho2(m) > 0 rank_init2 : LEMMA positive(rho2, INIT) nonpositive_rank2 : LEMMA non_positive(rho2, T2) %------------------------------- % User A2 maintains rho2 on a %------------------------------- rank_a2_aux : LEMMA rho2(pub(a, conc(Na, x))) > 0 IMPLIES x = Nb OR rho2(pub(i, x)) > 0 rank_user_a2 : LEMMA userA2 # R2 |> RankUser(rho2) %----------------------------- % User b maintains rho2 on b %----------------------------- rank_user_b2 : LEMMA userB # R2 |> RankUser(rho2) %---------------- % Consequence %---------------- authentication_origin2 : PROPOSITION network(enemy(INIT), protocol(a, b, userA2, userB)) |> auth(T2, R2) %============================= % Authentication property 7 %============================= %--------------------------------------------------------------- % rec(b, a, pub(b, Nb)) authenticates trans(a, i, pub(i, Nb)) %--------------------------------------------------------------- T3 : set[event] = T1 R3 : set[event] = { e | EXISTS i : e = trans(a, i, pub(i, Nb)) } %--------------------------------------------- % Rank function: the same as for property 1 %--------------------------------------------- nonpositive_rank3 : LEMMA non_positive(rho, T3) rank_user_a3 : LEMMA userA # R3 |> RankUser(rho) rank_user_a03 : LEMMA userA # R3 |> RankUser(rho) rank_user_b3 : LEMMA userB # R3 |> RankUser(rho) rank_user_b03 : LEMMA userB # R3 |> RankUser(rho) authentication_origin3 : PROPOSITION network(enemy(INIT), protocol(a, b, userA, userB)) |> auth(T3, R3) END needham_schroeder $$$needham_schroeder.prf (|needham_schroeder| (|IMP_network_TCC1| "" (LEMMA "gen_monotonic2") (("" (PROPAX) NIL NIL)) NIL) (|b_TCC1| "" (INST + "a+1") NIL NIL) (|nb_TCC1| "" (INST + "na +1") NIL NIL) (|interface_userA| "" (AUTO-REWRITE "local_transmission" "local_reception" "interface_pref[event]" "interface_stop[event]") (("" (EXPAND "userA") (("" (REWRITE "interface_choice3") NIL NIL)) NIL)) NIL) (|interface_userA2| "" (AUTO-REWRITE "local_transmission" "local_reception" "interface_pref[event]" "interface_stop[event]") (("" (EXPAND "userA2") (("" (REWRITE "interface_choice3") NIL NIL)) NIL)) NIL) (|interface_userB| "" (AUTO-REWRITE "local_transmission" "local_reception" "interface_pref[event]" "interface_stop[event]") (("" (EXPAND "userB") (("" (REWRITE "interface_choice3") NIL NIL)) NIL)) NIL) (|rank_code_TCC1| "" (GRIND) NIL NIL) (|rho_TCC1| "" (GRIND) NIL NIL) (|rho_TCC2| "" (GRIND) NIL NIL) (|rho_TCC3| "" (GRIND) NIL NIL) (|validity_rho| "" (REWRITE "rank_valid") (("1" (DELETE 2) (("1" (GRIND) NIL NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL)) NIL) (|rank_init| "" (GRIND) NIL NIL) (|nonpositive_rank| "" (GRIND) NIL NIL) (|rank_user_a| "" (EXPAND "userA") (("" (REWRITE "restriction_choice3") (("" (REWRITE "rank_user_choice3[[Identity, (nonce?)], Identity, message]") (("" (SKOLEM!) (("" (NAME-REPLACE "i!2" "PROJ_1(i!1)") (("" (NAME-REPLACE "nx!1" "PROJ_2(i!1)") (("" (INIT-CSP "Identity" "message") (("" (PREFIX) (("1" (DELETE 2) (("1" (GRIND) NIL NIL)) NIL) ("2" (PREFIX) (("2" (PREFIX) (("2" (DELETE 1 4) (("2" (EXPAND "R1") (("2" (INST + "i!2" "Na") (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|rank_user_b| "" (INIT-CSP "Identity" "message") (("" (EXPAND "userB") (("" (REWRITE "restriction_choice3") (("" (REWRITE "rank_user_choice3[message, Identity, message]") (("" (SKOLEM!) (("" (PREFIX) (("" (PREFIX) (("1" (DELETE 2) (("1" (GRIND) NIL NIL)) NIL) ("2" (PREFIX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|authentication_origin1| "" (USE "authentication_by_rank2" ("rho" "rho")) (("" (GROUND) (("1" (REWRITE "rank_init") NIL NIL) ("2" (USE "validity_rho") NIL NIL) ("3" (REWRITE "nonpositive_rank") NIL NIL) ("4" (REWRITE "interface_userA") NIL NIL) ("5" (REWRITE "rank_user_a") NIL NIL) ("6" (REWRITE "interface_userB") NIL NIL) ("7" (REWRITE "rank_user_b") NIL NIL)) NIL)) NIL) (|validity_rho2| "" (REWRITE "rank_valid") (("1" (DELETE 2) (("1" (GRIND) NIL NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL)) NIL) (|rank_init2| "" (GRIND) NIL NIL) (|nonpositive_rank2| "" (AUTO-REWRITE-DEFS :ALWAYS? T) (("" (ASSERT) (("" (SKOLEM-TYPEPRED) (("" (EXPAND "T1") (("" (REPLACE*) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|rank_a2_aux| "" (GRIND) NIL NIL) (|rank_user_a2| "" (EXPAND "userA2") (("" (REWRITE "restriction_choice3") (("" (REWRITE "rank_user_choice3[[Identity, message], Identity, message]") (("" (SKOLEM!) (("" (NAME-REPLACE "i!2" "PROJ_1(i!1)") (("" (NAME-REPLACE "x!1" "PROJ_2(i!1)") (("" (AUTO-REWRITE "rank_user_stop[Identity, message]" "rank_user_input[Identity, message]" "rank_user_output[Identity, message]" "restriction_stop[event[Identity, message]]") (("" (REWRITE "restriction_pref") (("" (LIFT-IF) (("" (GROUND) (("" (GROUND) (("1" (DELETE 2) (("1" (GRIND) NIL NIL)) NIL) ("2" (REWRITE "restriction_pref") (("2" (LIFT-IF) (("2" (GROUND) (("2" (GROUND) (("2" (REWRITE "restriction_pref") (("2" (LIFT-IF) (("2" (GROUND) (("2" (DELETE 1 4) (("2" (EXPAND "R2") (("2" (USE "rank_a2_aux") (("2" (ASSERT) (("2" (INST + "i!2" "Na") (("2" (ASSERT) 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) (|rank_user_b2| "" (EXPAND "userB") (("" (REWRITE "restriction_choice3") (("" (REWRITE "rank_user_choice3[message, Identity, message]") (("" (SKOLEM!) (("" (AUTO-REWRITE "rank_user_stop[Identity, message]" "rank_user_input[Identity, message]" "rank_user_output[Identity, message]" "restriction_stop[event[Identity, message]]") (("" (REWRITE "restriction_pref") (("" (LIFT-IF) (("" (ASSERT) (("" (GROUND) (("" (REWRITE "restriction_pref") (("" (LIFT-IF) (("" (ASSERT) (("" (GROUND) (("1" (DELETE 2 3) (("1" (GRIND) NIL NIL)) NIL) ("2" (REWRITE "restriction_pref") (("2" (LIFT-IF) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|authentication_origin2| "" (USE "authentication_by_rank2" ("rho" "rho2")) (("" (GROUND) (("1" (REWRITE "rank_init2") NIL NIL) ("2" (USE "validity_rho2") NIL NIL) ("3" (REWRITE "nonpositive_rank2") NIL NIL) ("4" (REWRITE "interface_userA2") NIL NIL) ("5" (REWRITE "rank_user_a2") NIL NIL) ("6" (REWRITE "interface_userB") NIL NIL) ("7" (REWRITE "rank_user_b2") NIL NIL)) NIL)) NIL) (|nonpositive_rank3| "" (EXPAND "T3") (("" (REWRITE "nonpositive_rank") NIL NIL)) NIL) (|rank_user_a3| "" (INIT-CSP "Identity" "message") (("" (EXPAND "userA") (("" (REWRITE "restriction_choice3") (("" (REWRITE "rank_user_choice3[[Identity, (nonce?)], Identity, message]") (("" (SKOLEM!) (("" (NAME-REPLACE "i!2" "PROJ_1(i!1)") (("" (NAME-REPLACE "nx!1" "PROJ_2(i!1)") (("" (PREFIX) (("1" (DELETE 2) (("1" (GRIND) NIL NIL)) NIL) ("2" (PREFIX) (("2" (PREFIX) (("2" (DELETE 3 4) (("2" (GRIND) (("2" (REPLACE -1 + RL) (("2" (REPLACE-ETA "nx!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|rank_user_a03| "" (EXPAND "userA") (("" (REWRITE "restriction_choice3") (("" (REWRITE "rank_user_choice3[[Identity, (nonce?)], Identity, message]") (("" (SKOLEM!) (("" (NAME-REPLACE "i!2" "PROJ_1(i!1)") (("" (NAME-REPLACE "nx!1" "PROJ_2(i!1)") (("" (AUTO-REWRITE "rank_user_stop[Identity, message]" "rank_user_input[Identity, message]" "rank_user_output[Identity, message]" "restriction_stop[event]") (("" (REWRITE "restriction_pref") (("" (LIFT-IF) (("" (ASSERT) (("" (PROP) (("1" (DELETE 2) (("1" (GRIND) NIL NIL)) NIL) ("2" (REWRITE "restriction_pref") (("2" (LIFT-IF) (("2" (ASSERT) (("2" (PROP) (("2" (REWRITE "restriction_pref") (("2" (LIFT-IF) (("2" (ASSERT) (("2" (PROP) (("2" (DELETE 3 4) (("2" (GRIND) (("2" (REPLACE -1 + RL) (("2" (REPLACE-ETA "nx!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|rank_user_b3| "" (INIT-CSP "Identity" "message") (("" (EXPAND "userB") (("" (REWRITE "restriction_choice3") (("" (REWRITE "rank_user_choice3[message, Identity, message]") (("" (SKOLEM!) (("" (PREFIX) (("" (PREFIX) (("1" (DELETE 2 3) (("1" (GRIND) NIL NIL)) NIL) ("2" (PREFIX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|rank_user_b03| "" (EXPAND "userB") (("" (REWRITE "restriction_choice3") (("" (REWRITE "rank_user_choice3[message, Identity, message]") (("" (SKOLEM!) (("" (AUTO-REWRITE "rank_user_stop[Identity, message]" "rank_user_input[Identity, message]" "rank_user_output[Identity, message]" "restriction_stop[event[Identity, message]]") (("" (REWRITE "restriction_pref") (("" (LIFT-IF) (("" (ASSERT) (("" (GROUND) (("" (REWRITE "restriction_pref") (("" (LIFT-IF) (("" (ASSERT) (("" (GROUND) (("1" (DELETE 2 3) (("1" (GRIND) NIL NIL)) NIL) ("2" (REWRITE "restriction_pref") (("2" (LIFT-IF) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|authentication_origin3| "" (USE "authentication_by_rank2" ("rho" "rho")) (("" (GROUND) (("1" (REWRITE "rank_init") NIL NIL) ("2" (USE "validity_rho") NIL NIL) ("3" (REWRITE "nonpositive_rank3") NIL NIL) ("4" (REWRITE "interface_userA") NIL NIL) ("5" (REWRITE "rank_user_a3") NIL NIL) ("6" (REWRITE "interface_userB") NIL NIL) ("7" (REWRITE "rank_user_b3") NIL NIL)) NIL)) NIL))