Nuprl Lemma : mk-pa_wf
(∀[a:Atom1]. ("new"(a) ∈ ProtocolAction))
∧ (∀[d:SecurityData]. ("send"(d) ∈ ProtocolAction))
∧ (∀[d:SecurityData]. ("rcv"(d) ∈ ProtocolAction))
∧ (∀[tr:SecurityData × Key × Atom1]. ("encrypt"(tr) ∈ ProtocolAction))
∧ (∀[tr:SecurityData × Key × Atom1]. ("decrypt"(tr) ∈ ProtocolAction))
∧ (∀[tr:SecurityData × Id × Atom1]. ("sign"(tr) ∈ ProtocolAction))
∧ (∀[tr:SecurityData × Id × Atom1]. ("verify"(tr) ∈ ProtocolAction))
Proof
Definitions occuring in Statement :
mk-pa: n(v),
protocol-action: ProtocolAction,
encryption-key: Key,
sdata: SecurityData,
Id: Id,
atom: Atom$n,
uall: ∀[x:A]. B[x],
and: P ∧ Q,
member: t ∈ T,
product: x:A × B[x],
token: "$token"
Lemmas :
eq_atom_wf,
bool_wf,
eqtt_to_assert,
assert_of_eq_atom,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
neg_assert_of_eq_atom,
sdata_wf,
encryption-key_wf,
Id_wf,
top_wf
Latex:
(\mforall{}[a:Atom1]. ("new"(a) \mmember{} ProtocolAction))
\mwedge{} (\mforall{}[d:SecurityData]. ("send"(d) \mmember{} ProtocolAction))
\mwedge{} (\mforall{}[d:SecurityData]. ("rcv"(d) \mmember{} ProtocolAction))
\mwedge{} (\mforall{}[tr:SecurityData \mtimes{} Key \mtimes{} Atom1]. ("encrypt"(tr) \mmember{} ProtocolAction))
\mwedge{} (\mforall{}[tr:SecurityData \mtimes{} Key \mtimes{} Atom1]. ("decrypt"(tr) \mmember{} ProtocolAction))
\mwedge{} (\mforall{}[tr:SecurityData \mtimes{} Id \mtimes{} Atom1]. ("sign"(tr) \mmember{} ProtocolAction))
\mwedge{} (\mforall{}[tr:SecurityData \mtimes{} Id \mtimes{} Atom1]. ("verify"(tr) \mmember{} ProtocolAction))
Date html generated:
2015_07_23-PM-00_14_57
Last ObjectModification:
2015_01_29-AM-01_33_24
Home
Index