Nuprl Lemma : signature-release-lemma2
∀s:SecurityTheory. ∀bss:Basic1 List.
((Legal(bss) ∧ FreshSignatures(bss))
⇒ (∀A:Id
(Protocol1(bss) A)
⇒ (∀es:EO+(Info). ∀thr:Thread.
((thr is one of bss at A) ⇒ sig-release-thread(sth-es(s);es;A;thr) supposing loc(thr)= A))
supposing Honest(A)))
Proof
Definitions occuring in Statement :
sig-release-thread: sig-release-thread(s;es;A;thr),
fresh-sig-protocol1: FreshSignatures(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,
sth-es: sth-es(s),
security-theory: SecurityTheory,
ses-honest: Honest(A),
ses-info: Info,
event-ordering+: EO+(Info),
Id: Id,
list: T List,
uimplies: b supposing a,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a
Definitions unfolded in proof :
sig-release-thread: sig-release-thread(s;es;A;thr),
all: ∀x:A. B[x],
security-theory: SecurityTheory,
sth-es: sth-es(s),
pi1: fst(t),
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
implies: P ⇒ Q,
and: P ∧ Q,
cand: A c∧ B,
ses-thread: Thread,
prop: ℙ,
es-E-interface: E(X),
int_seg: {i..j-},
guard: {T},
lelt: i ≤ j < k,
decidable: Dec(P),
or: P ∨ Q,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
false: False,
not: ¬A,
top: Top,
less_than: a < b,
squash: ↓T,
subtype_rel: A ⊆r B,
ses-act: Act,
so_lambda: λ2x.t[x],
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
so_apply: x[s],
es-causl: (e < e'),
ses-axioms: SecurityAxioms,
unique-sig-protocol: UniqueSignatures(bss),
noncelike-signatures: noncelike-signatures(s;es;thr),
ses-flow-axiom: PropertyF,
ses-sig: signature(e),
ses-thread-member: e ∈ thr,
le: A ≤ B,
ses-thread-loc: loc(thr)= A,
label: ...$L... t,
true: True,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
release-before: (a released before e)
Latex:
\mforall{}s:SecurityTheory. \mforall{}bss:Basic1 List.
((Legal(bss) \mwedge{} FreshSignatures(bss))
{}\mRightarrow{} (\mforall{}A:Id
(Protocol1(bss) A)
{}\mRightarrow{} (\mforall{}es:EO+(Info). \mforall{}thr:Thread.
((thr is one of bss at A)
{}\mRightarrow{} sig-release-thread(sth-es(s);es;A;thr) supposing loc(thr)= A))
supposing Honest(A)))
Date html generated:
2016_05_17-PM-00_47_12
Last ObjectModification:
2016_01_18-AM-07_47_58
Theory : event-logic-applications
Home
Index