Nuprl Lemma : member-used-atoms

{

s:SES
(ActionsDisjoint

(

es:EO+(Info).

e:E.

a:Atom1.
((a

UsedAtoms(e))

((

e

Send)

(a

sdata-atoms(Send(e))))

((

e

Decrypt)

((a = cipherText(e))

(a

encryption-key-atoms(key(e)))))

((

e

Verify)

((a = signature(e))

(a

sdata-atoms(signed(e)))))

((

e

Sign)

(a

sdata-atoms(signed(e))))

((

e

Encrypt)

((a

sdata-atoms(plainText(e)))

(a

encryption-key-atoms(key(e)))))))) }

{ Proof }

Definitions occuring in Statement : ses-used-atoms: UsedAtoms(e), ses-disjoint: ActionsDisjoint, ses-cipher: cipherText(e), ses-decryption-key: key(e), ses-decrypt: Decrypt, ses-encryption-key: key(e), ses-encrypted: plainText(e), ses-encrypt: Encrypt, ses-verify-sig: signature(e), ses-verify-signed: signed(e), ses-verify: Verify, ses-signed: signed(e), ses-sign: Sign, ses-send: Send, ses-info: Info, security-event-structure: SES, encryption-key-atoms: encryption-key-atoms(k), sdata-atoms: sdata-atoms(d), eclass-val: X(e), in-eclass: e

X, event-ordering+: EO+(Info), es-E: E, assert:

b, all:

x:A. B[x], iff: P

Q, implies: P

Q, or: P

Q, and: P

Q, equal: s = t, l_member: (x

l), atom: Atom$n
Definitions : false: False, member: t

T, universe: Type, prop:

, security-event-structure: SES, equal: s = t, event-ordering+: EO+(Info), es-E: E, atom: Atom$n, function: x:A

B[x], implies: P

Q, not:

A, cand: A c

B, and: P

Q, union: left + right, or: P

Q, int:

, pair: <a, b>, product: x:A

B[x], dep-isect: Error :dep-isect, eq_atom: x =a y, eq_atom: eq_atom$n(x;y), record+: record+, apply: f a, record-select: r.x, void: Void, assert:

b, ses-info: Info, natural_number: $n, bool:

, ses-new: New, ses-rcv: Rcv, l_member: (x

l), all:

x:A. B[x], subtype_rel: A

r B, strong-subtype: strong-subtype(A;B), so_apply: x[s], guard: {T}, ses-encryption-key: key(e), encryption-key-atoms: encryption-key-atoms(k), ses-encrypted: plainText(e), sdata-atoms: sdata-atoms(d), ses-signed: signed(e), ses-verify-signed: signed(e), ses-verify-sig: signature(e), ses-decryption-key: key(e), ses-cipher: cipherText(e), eclass-val: X(e), list: type List, cons: [car / cdr], nil: [], rev_implies: P

Q, eclass: EClass(A[eo; e]), es-E-interface: E(X), fpf: a:A fp-> B[a], event_ordering: EO, top: Top, set: {x:A| B[x]} , limited-type: LimitedType, so_lambda:

x y.t[x; y], sdata: SecurityData, less_than: a < b, exists:

x:A. B[x], iff: P

Q, subtype: S

T, lambda:

x.A[x], true: True, token: "$token", ifthenelse: if b then t else f fi , atom: Atom, encryption-key: Key, isect:

x:A. B[x], decide: case b of inl(x) => s[x] | inr(y) => t[y], map: map(f;as), hd: hd(l), last: last(L), remove-repeats: remove-repeats(eq;L), select: l[i], tl: tl(l), Knd: Knd, IdLnk: IdLnk, Id: Id, append: as @ bs, decidable: Dec(P), rationals:

, qle: r

s, qless: r < s, q-rel: q-rel(r;x), p-outcome: Outcome, dstype: dstype(TypeNames; d; a), fset-member: a

s, f-subset: xs

ys, fset: FSet{T}, fset-closed: (s closed under fs), string: Error :string, MaName: MaName, l_disjoint: l_disjoint(T;l1;l2), consensus-state3: consensus-state3(T), cs-not-completed: in state s, a has not completed inning i, cs-archived: by state s, a archived v in inning i, cs-passed: by state s, a passed inning i without archiving a value, cs-inning-committed: in state s, inning i has committed v, cs-inning-committable: in state s, inning i could commit v , cs-archive-blocked: in state s, ws' blocks ws from archiving v in inning i, cs-precondition: state s may consider v in inning i, consensus-rcv: consensus-rcv(V;A), infix_ap: x f y, es-causl: (e < e'), es-locl: (e <loc e'), es-le: e

loc e' , es-causle: e c

e', existse-before:

e<e'.P[e], existse-le:

e

e'.P[e], alle-lt:

e<e'.P[e], alle-le:

e

e'.P[e], alle-between1:

e

[e1,e2).P[e], existse-between1:

e

[e1,e2).P[e], alle-between2:

e

[e1,e2].P[e], existse-between2:

e

[e1,e2].P[e], existse-between3:

e

(e1,e2].P[e], es-fset-loc: i

locs(s), es-r-immediate-pred: es-r-immediate-pred(es;R;e';e), same-thread: same-thread(es;p;e;e'), collect-event: collect-event(es;X;n;v.num[v];L.P[L];e), cut-order: a

(X;f) b, path-goes-thru: x-f*-y thru i, bEvents: Error :bEvents, ses-action: Action(e), nat:

, bfalse: ff, bnot:

b, eq_bool: p =b q, lt_int: i <z j, le_int: i

z j, eq_int: (i =

j), null: null(as), set_blt: a <

b, grp_blt: a <

b, b-exists: (

i<n.P[i])_b, bl-exists: (

x

L.P[x])_b, bl-all: (

x

L.P[x])_b, dcdr-to-bool: [d]

, eq_type: eq_type(T;T'), q_le: q_le(r;s), q_less: q_less(r;s), qeq: qeq(r;s), deq-all-disjoint: deq-all-disjoint(eq;ass;bs), deq-disjoint: deq-disjoint(eq;as;bs), deq-member: deq-member(eq;x;L), es-eq-E: e = e', eq_lnk: a = b, eq_id: a = b, eq_str: Error :eq_str, bimplies: p

q, band: p

q, bor: p

q, btrue: tt, unit: Unit, l_contains: A

B, inject: Inj(A;B;f), reducible: reducible(a), prime: prime(a), squash:

T, l_exists: (

x

L. P[x]), l_all: (

x

L.P[x]), fun-connected: y is f*(x), sq_type: SQType(T), rec: rec(x.A[x]), tree: Tree(E), ses-disjoint: ActionsDisjoint, ses-used-atoms: UsedAtoms(e), MaAuto: Error :MaAuto, Try: Error :Try, CollapseTHEN: Error :CollapseTHEN, ses-decrypt: Decrypt, in-eclass: e

X, CollapseTHENA: Error :CollapseTHENA, ses-encrypt: Encrypt, ses-verify: Verify, ses-sign: Sign, ses-send: Send, Auto: Error :Auto, D: Error :D, THENM: Error :THENM, Unfold: Error :Unfold, RepeatFor: Error :RepeatFor
Lemmas : security-event-structure_wf, ses-disjoint_wf, Id_wf, ifthenelse_wf, decidable__l_member, append_wf, member_append, eqtt_to_assert, iff_transitivity, eqff_to_assert, assert_of_bnot, bnot_wf, not_wf, bool_wf, decidable__atom_equal_1, l_member_subtype, cons_member, true_wf, in-eclass_wf, eclass_wf, es-interface-top, es-interface-subtype_rel2, encryption-key_wf, top_wf, subtype_rel_self, sdata_wf, event-ordering+_inc, event-ordering+_wf, iff_wf, rev_implies_wf, nil_member, ses-send_wf, eclass-val_wf, ses-cipher_wf, ses-decryption-key_wf, ses-verify-sig_wf, ses-verify-signed_wf, ses-signed_wf, sdata-atoms_wf, ses-encrypted_wf, encryption-key-atoms_wf, ses-encryption-key_wf, assert_wf, ses-decrypt_wf, ses-verify_wf, ses-sign_wf, member_wf, ses-encrypt_wf, ses-info_wf, es-E-interface_wf, es-E_wf, subtype_rel_wf, l_member_wf, false_wf

\mforall{}s:SES (ActionsDisjoint {}\mRightarrow{} (\mforall{}es:EO+(Info). \mforall{}e:E. \mforall{}a:Atom1. ((a \mmember{} UsedAtoms(e)) \mLeftarrow{}{}\mRightarrow{} ((\muparrow{}e \mmember{}\msubb{} Send) \mwedge{} (a \mmember{} sdata-atoms(Send(e)))) \mvee{} ((\muparrow{}e \mmember{}\msubb{} Decrypt) \mwedge{} ((a = cipherText(e)) \mvee{} (a \mmember{} encryption-key-atoms(key(e))))) \mvee{} ((\muparrow{}e \mmember{}\msubb{} Verify) \mwedge{} ((a = signature(e)) \mvee{} (a \mmember{} sdata-atoms(signed(e))))) \mvee{} ((\muparrow{}e \mmember{}\msubb{} Sign) \mwedge{} (a \mmember{} sdata-atoms(signed(e)))) \mvee{} ((\muparrow{}e \mmember{}\msubb{} Encrypt) \mwedge{} ((a \mmember{} sdata-atoms(plainText(e))) \mvee{} (a \mmember{} encryption-key-atoms(key(e)))))))) Date html generated: 2011_08_17-PM-07_34_32 Last ObjectModification: 2010_09_24-PM-02_42_51 Home Index