Nuprl Lemma : nonce-release-lemma2

[s:SecurityTheory]. ∀[bss:Basic1 List].
    (∀[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)= and 
          (thr is one of bss at A))) supposing 
       ((Protocol1(bss) A) and 
  supposing Legal(bss)


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: List int_seg: {i..j-} assert: b uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] not: ¬A apply: a add: m natural_number: $n
Lemmas :  release-before_wf sth-es_wf eclass-val_wf ses-info_wf es-E_wf event-ordering+_subtype event-ordering+_wf ses-new_wf select_wf ses-act_wf sq_stable__le less_than_transitivity2 length_wf le_weakening2 all_wf int_seg_wf not_wf assert_wf in-eclass_wf ses-send_wf es-interface-subtype_rel2 top_wf subtype_top sdata_wf decidable__le false_wf not-le-2 condition-implies-le minus-add minus-one-mul add-swap add-commutes zero-add add_functionality_wrt_le add-associates add-zero le-add-cancel ses-thread-loc_wf ses-protocol1-thread_wf ses-thread_wf ses-protocol1_wf ses-honest_wf Id_wf ses-protocol1-legal_wf list_wf ses-basic-sequence1_wf security-theory_wf nonce-release-lemma

\mforall{}[s:SecurityTheory].  \mforall{}[bss:Basic1  List].
        (\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 
    supposing  Legal(bss)

Date html generated: 2015_07_23-PM-00_19_35
Last ObjectModification: 2015_01_29-AM-01_31_28

Home Index