Nuprl Lemma : NSL-authentication-property

{

[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
Definitions : uall:

[x:A]. B[x], member: t

T, prop:

, NSL-authentication-property: NSL-authentication-property{i:l}(sth), and: P

Q, nat:

, le: A

B, not:

A, implies: P

Q, false: False
Lemmas : authentication_wf, sth-es_wf, NSL-protocol_wf, NSL-initiator3_wf, le_wf, NSL-responder3_wf, security-theory_wf

\mforall{}[sth:SecurityTheory]. (NSL-authentication-property\{i:l\}(sth) \mmember{} \mBbbP{}') Date html generated: 2011_08_17-PM-07_54_45 Last ObjectModification: 2011_06_18-PM-01_49_44 Home Index