Nuprl Lemma : NSL-authentication-property_wf
∀[sth:SecurityTheory]. (NSL-authentication-property{i:l}(sth) ∈ ℙ')
Proof
Definitions occuring in Statement :
NSL-authentication-property: NSL-authentication-property{i:l}(sth),
security-theory: SecurityTheory,
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T
Lemmas :
authentication_wf,
sth-es_wf,
NSL-protocol_wf,
NSL-initiator3_wf,
false_wf,
le_wf,
NSL-responder3_wf,
security-theory_wf
Latex:
\mforall{}[sth:SecurityTheory]. (NSL-authentication-property\{i:l\}(sth) \mmember{} \mBbbP{}')
Date html generated:
2015_07_23-PM-00_26_33
Last ObjectModification:
2015_01_29-AM-01_28_24
Home
Index