Nuprl Lemma : signature-release-lemma

∀[ses:SES]
  ∀[bss:Basic1 List]
    ∀[A:Id]
      (∀[es:EO+(Info)]. ∀[thr:Thread].
         (∀[i:ℕ||thr||]. ∀[j:ℕi].
            (¬(signature(thr[j]) released before thr[i])) supposing
               ((∀k:{j + 1..i^-}. (¬↑thr[k] ∈_b Send)) and
               (↑thr[j] ∈_b Sign))) supposing
            (loc(thr)= A and
            (thr is one of bss at A))) supposing
         ((Protocol1(bss) A) and
         Honest(A))
    supposing Legal(bss) ∧ UniqueSignatures(bss)
  supposing SecurityAxioms

Proof

Definitions occuring in Statement : unique-sig-protocol: UniqueSignatures(bss), ses-protocol1-legal: Legal(bss), ses-protocol1: Protocol1(bss), ses-protocol1-thread: (thr is one of bss at A), ses-basic-sequence1: Basic1, ses-thread-loc: loc(thr)= A, ses-thread: Thread, ses-axioms: SecurityAxioms, release-before: (a released before e), ses-honest: Honest(A), ses-sig: signature(e), ses-sign: Sign, ses-send: Send, ses-info: Info, security-event-structure: SES, in-eclass: e ∈_b X, event-ordering+: EO+(Info), Id: Id, select: L[n], length: ||as||, list: T List, int_seg: {i..j^-}, assert: ↑b, uimplies: b supposing a, uall: ∀[x:A]. B[x], all: ∀x:A. B[x], not: ¬A, and: P ∧ Q, apply: f a, add: n + m, natural_number: $n
Definitions unfolded in proof : uall: ∀[x:A]. B[x], uimplies: b supposing a, not: ¬A, implies: P ⇒ Q, false: False, member: t ∈ T, prop: ℙ, ses-thread: Thread, and: P ∧ Q, es-E-interface: E(X), int_seg: {i..j^-}, guard: {T}, lelt: i ≤ j < k, all: ∀x:A. B[x], decidable: Dec(P), or: P ∨ Q, satisfiable_int_formula: satisfiable_int_formula(fmla), exists: ∃x:A. B[x], top: Top, less_than: a < b, squash: ↓T, subtype_rel: A ⊆r B, ses-act: Act, so_lambda: λ₂x.t[x], so_apply: x[s], ses-axioms: SecurityAxioms, cand: A c∧ B, ses-thread-loc: loc(thr)= A, ses-thread-member: e ∈ thr, le: A ≤ B, strongwellfounded: SWellFounded(R[x; y]), less_than': less_than'(a;b), nat: ℕ, ge: i ≥ j , so_lambda: λ₂x y.t[x; y], so_apply: x[s1;s2], ses-ordering': ses-ordering'(s), unique-sig-protocol: UniqueSignatures(bss), noncelike-signatures: noncelike-signatures(s;es;thr), ses-sig: signature(e), true: True, iff: P ⇐⇒ Q, rev_implies: P ⇐ Q, ses-action: Action(e), sq_type: SQType(T), assert: ↑b, ifthenelse: if b then t else f fi , btrue: tt, es-locl: (e <loc e'), ses-protocol1: Protocol1(bss), ses-protocol1-legal: Legal(bss), l_member: (x ∈ l), uiff: uiff(P;Q), label: ...$L... t, es-le: e ≤loc e' , ses-disjoint: ActionsDisjoint, release-before: (a released before e)

Latex:
\mforall{}[ses:SES] \mforall{}[bss:Basic1 List] \mforall{}[A:Id] (\mforall{}[es:EO+(Info)]. \mforall{}[thr:Thread]. (\mforall{}[i:\mBbbN{}||thr||]. \mforall{}[j:\mBbbN{}i]. (\mneg{}(signature(thr[j]) released before thr[i])) supposing ((\mforall{}k:\{j + 1..i\msupminus{}\}. (\mneg{}\muparrow{}thr[k] \mmember{}\msubb{} Send)) and (\muparrow{}thr[j] \mmember{}\msubb{} Sign))) supposing (loc(thr)= A and (thr is one of bss at A))) supposing ((Protocol1(bss) A) and Honest(A)) supposing Legal(bss) \mwedge{} UniqueSignatures(bss) supposing SecurityAxioms Date html generated: 2016_05_17-PM-00_46_33 Last ObjectModification: 2016_01_18-AM-07_52_10 Theory : event-logic-applications Home Index