Nuprl Lemma : member-useable-atoms

{

s:SES
(ActionsDisjoint

(

es:EO+(Info).

e:E.

a:Atom1.
((a

UseableAtoms(e))

((

e

Rcv)

(a

sdata-atoms(Rcv(e))))

((

e

Decrypt)

(a

sdata-atoms(plainText(e))))

((

e

New)

(a = New(e)))

((

e

Sign)

(a = signature(e)))

((

e

Encrypt)

(a = cipherText(e)))))) }

{ Proof }

Definitions occuring in Statement : ses-useable-atoms: UseableAtoms(e), ses-disjoint: ActionsDisjoint, ses-decrypted: plainText(e), ses-decrypt: Decrypt, ses-crypt: cipherText(e), ses-encrypt: Encrypt, ses-sig: signature(e), ses-sign: Sign, ses-rcv: Rcv, ses-new: New, ses-info: Info, security-event-structure: SES, 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, security-event-structure: SES, event-ordering+: EO+(Info), es-E: E, atom: Atom$n, function: x:A

B[x], implies: P

Q, not:

A, assert:

b, equal: s = t, product: x:A

B[x], and: P

Q, natural_number: $n, apply: f a, int:

, ses-new: New, eclass-val: X(e), true: True, l_member: (x

l), union: left + right, or: P

Q, member: t

T, universe: Type, prop:

, cand: A c

B, ses-crypt: cipherText(e), ses-sig: signature(e), all:

x:A. B[x], ses-info: Info, eclass: EClass(A[eo; e]), subtype: S

T, event_ordering: EO, dep-isect: Error :dep-isect, top: Top, token: "$token", eq_atom: x =a y, ifthenelse: if b then t else f fi , atom: Atom, subtype_rel: A

r B, eq_atom: eq_atom$n(x;y), record-select: r.x, record+: record+, lambda:

x.A[x], so_lambda:

x y.t[x; y], es-E-interface: E(X), ses-decrypted: plainText(e), sdata-atoms: sdata-atoms(d), ses-rcv: Rcv, pair: <a, b>, void: Void, decide: case b of inl(x) => s[x] | inr(y) => t[y], bool:

, ses-send: Send, in-eclass: e

X, ses-verify: Verify, ses-sign: Sign, ses-encrypt: Encrypt, ses-decrypt: Decrypt, fpf: a:A fp-> B[a], strong-subtype: strong-subtype(A;B), fpf-dom: x

dom(f), less_than: a < b, rev_implies: P

Q, iff: P

Q, hd: hd(l), last: last(L), cons: [car / cdr], remove-repeats: remove-repeats(eq;L), select: l[i], tl: tl(l), Knd: Knd, IdLnk: IdLnk, Id: Id, so_apply: x[s], guard: {T}, list: type List, nil: [], set: {x:A| B[x]} , limited-type: LimitedType, sdata: SecurityData, append: as @ bs, locl: locl(a), exists:

x:A. B[x], isect:

x:A. B[x], 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, infix_ap: x f y, 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, sq_type: SQType(T), encryption-key: Key, map: map(f;as), eq_knd: a = b, nat:

, intensional-universe: IType, rec: rec(x.A[x]), tree: Tree(E), ses-disjoint: ActionsDisjoint, ses-useable-atoms: UseableAtoms(e), THENL_cons: Error :THENL_nil, THENL_cons: Error :THENL_cons, Auto: Error :Auto, CollapseTHEN: Error :CollapseTHEN, MaAuto: Error :MaAuto, CollapseTHENA: Error :CollapseTHENA, THENL_v2: Error :THENL, Repeat: Error :Repeat, D: Error :D, THENM: Error :THENM, Unfold: Error :Unfold, RepeatFor: Error :RepeatFor
Lemmas : nil_member, security-event-structure_wf, ses-disjoint_wf, intensional-universe_wf, Id_wf, ifthenelse_wf, l_member_subtype, encryption-key_wf, eqtt_to_assert, iff_transitivity, eqff_to_assert, assert_of_bnot, bnot_wf, not_wf, bool_wf, in-eclass_wf, eclass_wf, es-interface-top, es-interface-subtype_rel2, top_wf, sdata_wf, iff_wf, rev_implies_wf, ses-rcv_wf, sdata-atoms_wf, ses-decrypted_wf, ses-sig_wf, ses-crypt_wf, assert_wf, ses-decrypt_wf, ses-sign_wf, member_wf, ses-encrypt_wf, es-E-interface_wf, subtype_rel_wf, l_member_wf, member_singleton, true_wf, eclass-val_wf, es-E_wf, subtype_rel_self, event-ordering+_inc, event-ordering+_wf, ses-info_wf, ses-new_wf, false_wf

\mforall{}s:SES (ActionsDisjoint {}\mRightarrow{} (\mforall{}es:EO+(Info). \mforall{}e:E. \mforall{}a:Atom1. ((a \mmember{} UseableAtoms(e)) \mLeftarrow{}{}\mRightarrow{} ((\muparrow{}e \mmember{}\msubb{} Rcv) \mwedge{} (a \mmember{} sdata-atoms(Rcv(e)))) \mvee{} ((\muparrow{}e \mmember{}\msubb{} Decrypt) \mwedge{} (a \mmember{} sdata-atoms(plainText(e)))) \mvee{} ((\muparrow{}e \mmember{}\msubb{} New) \mwedge{} (a = New(e))) \mvee{} ((\muparrow{}e \mmember{}\msubb{} Sign) \mwedge{} (a = signature(e))) \mvee{} ((\muparrow{}e \mmember{}\msubb{} Encrypt) \mwedge{} (a = cipherText(e)))))) Date html generated: 2011_08_17-PM-07_34_03 Last ObjectModification: 2010_09_24-PM-02_43_07 Home Index