Nuprl Lemma : CRX-protocol-legal

{

s:SES
    Legal([CR-initiator1{i:l}(s);

           CR-initiator2{i:l}(s);

           CR-initiator4{i:l}(s);

           CR-responder4{i:l}(s);

           CR-responder5{i:l}(s); CR-responder6{i:l}(s)]) }

{ Proof }

Definitions occuring in Statement : CR-responder4: CR-responder4{i:l}(s), CR-responder5: CR-responder5{i:l}(s), CR-responder6: CR-responder6{i:l}(s), CR-initiator4: CR-initiator4{i:l}(s), CR-initiator2: CR-initiator2{i:l}(s), CR-initiator1: CR-initiator1{i:l}(s), ses-protocol1-legal: Legal(bss), security-event-structure: SES, all:

x:A. B[x], cons: [car / cdr], nil: []
Definitions : atom: Atom$n, l_member: (x

l), encryption-key-atoms: encryption-key-atoms(k), prop:

, equal: s = t, or: P

Q, false: False, union: left + right, function: x:A

B[x], implies: P

Q, member: t

T, security-event-structure: SES, Id: Id, cons: [car / cdr], all:

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

Q, product: x:A

B[x], and: P

Q, iff: P

Q, guard: {T}, ses-private: Private(A), nil: [], l_all: (

x

L.P[x]), so_lambda:

x.t[x], l_contains: A

B, lambda:

x.A[x], concat: concat(ll), sdata_atoms_id: sdata_atoms_id{sdata_atoms_id_compseq_tag_def:o}(x), sdata_atoms_atom: sdata_atoms_atom{sdata_atoms_atom_compseq_tag_def:o}(a), sdata_atoms_pair: sdata_atoms_pair{sdata_atoms_pair_compseq_tag_def:o}(d2; d1), eq_atom: x =a y, eq_atom: eq_atom$n(x;y), pa-useable: pa-useable(pa), mk-pa: n(v), pa-used: pa-used(pa), lt_int: i <z j, sqequal: s ~ t, map: map(f;as), from-upto: [n, m), natural_number: $n, select: l[i], pair: <a, b>, sdata-pair: <d1, d2>, id-sdata: data(x), atom-sdata: data(a), token: "$token", int_seg: {i..j

}, int:

, le: A

B, less_than: a < b, not:

A, lelt: i

j < k, sq_type: SQType(T), set: {x:A| B[x]} , decidable: Dec(P), list: type List, nat_plus:

, nat:

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

T, l_disjoint: l_disjoint(T;l1;l2), exists:

x:A. B[x], l_exists: (

x

L. P[x]), apply: f a, infix_ap: x f y, fun-connected: y is f*(x), limited-type: LimitedType, 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: String, IdLnk: IdLnk, Knd: Knd, MaName: MaName, 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), es-causl: (e < e'), es-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-E-interface: E(X), 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, es-r-immediate-pred: es-r-immediate-pred(es;R;e';e), same-thread: same-thread(es;p;e;e'), ses-action: Action(e), ses-legal-sequence: Legal(pas) given prvt, real:

, subtype: S

T, universe: Type, subtype_rel: A

r B, strong-subtype: strong-subtype(A;B), spread: spread def, tl: tl(l), hd: hd(l), assert:

b, ses-is-protocol-action: pa(e), ses-is-protocol-actions: pas(thr), ses-basic-sequence1: Basic1, ses-thread: Thread, dep-isect: Error :dep-isect, record+: record+, event-ordering+: EO+(Info), ses-disjoint: ActionsDisjoint, protocol-action: ProtocolAction, CR-responder6: CR-responder6{i:l}(s), ses-legal-thread: Legal(thr)@A, CR-responder5: CR-responder5{i:l}(s), CR-responder4: CR-responder4{i:l}(s), CR-initiator4: CR-initiator4{i:l}(s), CR-initiator2: CR-initiator2{i:l}(s), CR-initiator1: CR-initiator1{i:l}(s), is-basic-seq: thr[A;B] |= bs, basic-seq-1-5: A

B: pas[A;B;m;n;x;y;z], basic-seq-1-3: A

B: pas[A; B; m; n; x], basic-seq-1-1: A

B: pas[A; B; m], ses-protocol1-thread: (thr is one of bss at A), ses-info: Info, ses-protocol1-legal: Legal(bss)
Lemmas : security-event-structure_wf, ses-protocol1-legal_wf, ses-legal-thread_wf, ses-protocol1-thread_wf, CR-initiator1_wf, CR-initiator2_wf, CR-initiator4_wf, CR-responder4_wf, CR-responder5_wf, CR-responder6_wf, ses-thread_wf, event-ordering+_wf, ses-info_wf, Id_wf, ses-basic-sequence1_wf, is-basic-seq_wf, ses-disjoint_wf, ses-private_wf, ses-is-protocol-actions-legal, atom-sdata_wf, mk-pa_wf, sdata-pair_wf, id-sdata_wf, protocol-action_wf, ses-legal-sequence_wf, int_seg_wf, int_seg_properties, decidable__equal_int, int_sq, l_contains_wf, l_all_wf, implies_functionality_wrt_iff, iff_transitivity, cons_member, or_functionality_wrt_iff, iff_wf, rev_implies_wf, nil_member, l_member_wf, false_wf

\mforall{}s:SES Legal([CR-initiator1\{i:l\}(s); CR-initiator2\{i:l\}(s); CR-initiator4\{i:l\}(s); CR-responder4\{i:l\}(s); CR-responder5\{i:l\}(s); CR-responder6\{i:l\}(s)]) Date html generated: 2010_08_28-AM-11_49_40 Last ObjectModification: 2010_03_20-PM-10_14_29 Home Index