structure DY.SubAttackerKnowledge [BytesFunctor] (SubF : Type → Type) : Type

The attacker knowledge is ultimately defined as a Kleene fixpoint, and SubAttackerKnowledge is a component of this fixpoint computation.

For example, to say that the attacker is allowed to concatenate bytes, we can write:

-- attacker knows out when pred p out := ∃ lhs rhs, -- out is the concatenation of lhs and rhs and out = concat lhs rhs ∧ p lhs ∧ -- the attacker knows lhs and p rhs -- the attacker knows rhs.

To prove the scott-continuity of pred (a technical requirement for Kleene fixpoint) it is better to use the Forall predicate like this:

pred p out := ∃ lhs rhs, out = concat lhs rhs ∧ DY.Kleene.Forall p [lhs, rhs]

This allows to rely on the lemma DY.Kleene.isScottContinuous_Forall_lemma, and allow for pred_isScottContinuous to be proved automatically by our tactic script.

The SubF parameter is not useful in this definition. It is only for hygiene, to make sure we don't miss equational theories by using SubAttackerKnowledge.combine

• pred : (Bytes → Prop) → Bytes → Prop
• pred_isScottContinuous : Kleene.IsScottContinuous self.pred

class DY.AttackerKnowledge [BytesFunctor] : Type

• attackerKnowledge : SubAttackerKnowledge BytesF

class DY.AttackerKnowledge.HasStep [BytesFunctor] {SubF1 : Type → Type} {SubF2 : semiOutParam (Type → Type)} (att1 : SubAttackerKnowledge SubF1) (att2 : semiOutParam (SubAttackerKnowledge SubF2)) : Prop

• pf (p : Bytes → Prop) (b : Bytes) : att1.pred p b → att2.pred p b

class DY.AttackerKnowledge.Has [BytesFunctor] [AttackerKnowledge] {SubF : Type → Type} (att : SubAttackerKnowledge SubF) : Prop

• pf (p : Bytes → Prop) (b : Bytes) : att.pred p b → attackerKnowledge.pred p b

instance DY.AttackerKnowledge.instHasBytesFAttackerKnowledge [BytesFunctor] [AttackerKnowledge] : Has attackerKnowledge

instance DY.AttackerKnowledge.instHasOfHasStep [BytesFunctor] [AttackerKnowledge] {SubF1 SubF2 : Type → Type} (att1 : SubAttackerKnowledge SubF1) (att2 : SubAttackerKnowledge SubF2) [inst1 : HasStep att1 att2] [inst2 : Has att2] : Has att1

def DY.SubAttackerKnowledge.combine [BytesFunctor] {t : Type} {SubFs : t → Type → Type} (atts : (id : t) → SubAttackerKnowledge (SubFs id)) : SubAttackerKnowledge (BytesFunctor.combine SubFs)

Equations

• DY.SubAttackerKnowledge.combine atts = { pred := DY.Kleene.combine fun (id : t) => (atts id).pred, pred_isScottContinuous := ⋯ }

def DY.SubAttackerKnowledge.combine' [BytesFunctor] {SubF : Type → Type} {t : Type} (atts : t → SubAttackerKnowledge SubF) : SubAttackerKnowledge SubF

Equations

• DY.SubAttackerKnowledge.combine' atts = { pred := DY.Kleene.combine fun (id : t) => (atts id).pred, pred_isScottContinuous := ⋯ }

def DY.SubAttackerKnowledge.fromPred [BytesFunctor] {SubF : Type → Type} (pred : Bytes → Prop) : SubAttackerKnowledge SubF

Equations

• DY.SubAttackerKnowledge.fromPred pred = { pred := fun (p : DY.Bytes → Prop) (buf : DY.Bytes) => pred buf, pred_isScottContinuous := ⋯ }

instance DY.AttackerKnowledge.instHasStepCombineCombine [BytesFunctor] {t : Type} {SubFs : t → Type → Type} (atts : (id : t) → SubAttackerKnowledge (SubFs id)) (id : t) : HasStep (atts id) (SubAttackerKnowledge.combine atts)

instance DY.AttackerKnowledge.instHasStepCombine' [BytesFunctor] {SubF : Type → Type} {t : Type} (atts : t → SubAttackerKnowledge SubF) (id : t) : HasStep (atts id) (SubAttackerKnowledge.combine' atts)

def DY.Bytes.AttackerKnows.baseKnowledge [BytesFunctor] [ExecTraceTypes] [BaseAttackerKnowledge] (tr : ExecTrace) : SubAttackerKnowledge BytesF

Equations

• DY.Bytes.AttackerKnows.baseKnowledge tr = DY.SubAttackerKnowledge.fromPred (DY.Trace.BaseAttackerKnows tr)

def DY.Bytes.AttackerKnows [BytesFunctor] [ExecTraceTypes] [BaseAttackerKnowledge] [AttackerKnowledge] (b : Bytes) (tr : ExecTrace) : Prop

Equations

• b.AttackerKnows tr = DY.Kleene.mkWeakestFixpoint (DY.Bytes.AttackerKnows.attackerKnowledge✝ tr).pred b

theorem DY.Bytes.AttackerKnows_le [BytesFunctor] [ExecTraceTypes] [BaseAttackerKnowledge] [AttackerKnowledge] (b : Bytes) (tr1 tr2 : ExecTrace) : tr1 ≤ tr2 → b.AttackerKnows tr1 → b.AttackerKnows tr2

theorem DY.Bytes.AttackerKnows.prove [BytesFunctor] [ExecTraceTypes] [BaseAttackerKnowledge] [AttackerKnowledge] {SubF : Type → Type} (att : SubAttackerKnowledge SubF) [AttackerKnowledge.Has att] (b : Bytes) (tr : ExecTrace) : att.pred (fun (x : Bytes) => x.AttackerKnows tr) b → b.AttackerKnows tr

Main theorem to prove that the attacker knows some particular value

theorem DY.Bytes.AttackerKnows.prove_from_base [BytesFunctor] [ExecTraceTypes] [BaseAttackerKnowledge] [AttackerKnowledge] (b : Bytes) (tr : ExecTrace) : Trace.BaseAttackerKnows tr b → b.AttackerKnows tr

def DY.SubAttackerKnowledge.Implies [BytesFunctor] {SubF : Type → Type} (att : SubAttackerKnowledge SubF) (p : Bytes → Prop) : Prop

The attacker knowledge AttackerKnows is the weakest predicate P such that every sub-attacker knowledge predicate att, att.pred P b implies P b

The attacker knowledge satisfies this property: this is the theorem by Bytes.AttackerKnows.prove The attacker knowledge is the weakest predicate: this is the theorem Bytes.AttackerKnows.is_least_fixpoint. In other words, if a predicate P has this property, then Bytes.AttackerKnows b => P b

We can use SubAttackerKnowledge.Implies to modularly prove that a predicate P satisfy this property.

Equations

• att.Implies p = ∀ (b : DY.Bytes), att.pred p b → p b

theorem DY.SubAttackerKnowledge.combine'.implies [BytesFunctor] {SubF : Type → Type} {t : Type} (atts : t → SubAttackerKnowledge SubF) (p : Bytes → Prop) (pfs : ∀ (id : t), (atts id).Implies p) : (combine' atts).Implies p

theorem DY.SubAttackerKnowledge.combine.implies [BytesFunctor] {t : Type} {SubFs : t → Type → Type} (atts : (id : t) → SubAttackerKnowledge (SubFs id)) (p : Bytes → Prop) (pfs : ∀ (id : t), (atts id).Implies p) : (combine atts).Implies p

theorem DY.Bytes.AttackerKnows.is_least_fixpoint [BytesFunctor] [ExecTraceTypes] [BaseAttackerKnowledge] [AttackerKnowledge] (pred : Bytes → Prop) (b : Bytes) (tr : ExecTrace) (pf1 : AttackerKnowledge.attackerKnowledge.Implies pred) (pf2 : (baseKnowledge tr).Implies pred) : b.AttackerKnows tr → pred b