Nuprl Lemma : authentication_wf
∀[s:SES]. ∀[prtcl:Id ─→ ℙ']. ∀[bs:Basic1]. ∀[n:ℕ]. (prtcl |= bs authenticates n messages ∈ ℙ')
Proof
Definitions occuring in Statement :
authentication: prtcl |= bs authenticates n messages ,
ses-basic-sequence1: Basic1,
security-event-structure: SES,
Id: Id,
nat: ℕ,
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T,
function: x:A ─→ B[x]
Lemmas :
all_wf,
event-ordering+_wf,
ses-info_wf,
Id_wf,
ses-honest_wf,
not_wf,
equal_wf,
ses-thread_wf,
ses-thread-loc_wf,
is-basic-seq_wf,
exists_wf,
matching-conversation_wf,
nat_wf,
ses-basic-sequence1_wf,
security-event-structure_wf
Latex:
\mforall{}[s:SES]. \mforall{}[prtcl:Id {}\mrightarrow{} \mBbbP{}']. \mforall{}[bs:Basic1]. \mforall{}[n:\mBbbN{}]. (prtcl |= bs authenticates n messages \mmember{} \mBbbP{}')
Date html generated:
2015_07_23-PM-00_15_44
Last ObjectModification:
2015_01_29-AM-01_33_02
Home
Index