Nuprl Lemma : nonce-release-lemma2
∀[s:SecurityTheory]. ∀[bss:Basic1 List].
  ∀[A:Id]
    (∀[es:EO+(Info)]. ∀[thr:Thread].
       (∀[i:ℕ||thr||]. ∀[j:ℕi].
          (¬(New(thr[j]) released before thr[i])) supposing 
             ((∀k:{j + 1..i-}. (¬↑thr[k] ∈b Send)) and 
             (↑thr[j] ∈b New))) supposing 
          (loc(thr)= A and 
          (thr is one of bss at A))) supposing 
       ((Protocol1(bss) A) and 
       Honest(A)) 
  supposing Legal(bss)
Proof
Definitions occuring in Statement : 
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
, 
sth-es: sth-es(s)
, 
security-theory: SecurityTheory
, 
release-before: (a released before e)
, 
ses-honest: Honest(A)
, 
ses-send: Send
, 
ses-new: New
, 
ses-info: Info
, 
eclass-val: X(e)
, 
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
, 
apply: f a
, 
add: n + m
, 
natural_number: $n
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
uimplies: b supposing a
, 
not: ¬A
, 
implies: P 
⇒ Q
, 
false: False
, 
prop: ℙ
, 
so_lambda: λ2x y.t[x; y]
, 
subtype_rel: A ⊆r B
, 
so_apply: x[s1;s2]
, 
ses-thread: Thread
, 
int_seg: {i..j-}
, 
guard: {T}
, 
lelt: i ≤ j < k
, 
and: P ∧ Q
, 
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
, 
ses-act: Act
, 
so_lambda: λ2x.t[x]
, 
so_apply: x[s]
, 
security-theory: SecurityTheory
, 
sth-es: sth-es(s)
, 
pi1: fst(t)
Latex:
\mforall{}[s:SecurityTheory].  \mforall{}[bss:Basic1  List].
    \mforall{}[A:Id]
        (\mforall{}[es:EO+(Info)].  \mforall{}[thr:Thread].
              (\mforall{}[i:\mBbbN{}||thr||].  \mforall{}[j:\mBbbN{}i].
                    (\mneg{}(New(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{}  New)))  supposing 
                    (loc(thr)=  A  and 
                    (thr  is  one  of  bss  at  A)))  supposing 
              ((Protocol1(bss)  A)  and 
              Honest(A)) 
    supposing  Legal(bss)
Date html generated:
2016_05_17-PM-00_46_39
Last ObjectModification:
2016_01_18-AM-07_41_04
Theory : event-logic-applications
Home
Index