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

The attacker knowledge is ultimately defined as a 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.

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_isMonotonic : Fixpoint.IsMonotonic 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] {n : Nat} {SubFs : Fin n → Type → Type} (atts : (id : Fin n) → SubAttackerKnowledge (SubFs id)) : SubAttackerKnowledge (BytesFunctor.combine SubFs)

Equations

• DY.SubAttackerKnowledge.combine atts = { pred := DY.Fixpoint.combine fun (id : Fin n) => (atts id).pred, pred_isMonotonic := ⋯ }

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

Equations

• DY.SubAttackerKnowledge.combine' atts = { pred := DY.Fixpoint.combine fun (id : Fin n) => (atts id).pred, pred_isMonotonic := ⋯ }

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_isMonotonic := ⋯ }

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

instance DY.AttackerKnowledge.instHasStepCombine' [BytesFunctor] {n : Nat} {SubF : Type → Type} (atts : Fin n → SubAttackerKnowledge SubF) (id : Fin n) : 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.Fixpoint.mkLeastFixpoint (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] {n : Nat} {SubF : Type → Type} (atts : Fin n → SubAttackerKnowledge SubF) (p : Bytes → Prop) (pfs : ∀ (id : Fin n), (atts id).Implies p) : (combine' atts).Implies p

theorem DY.SubAttackerKnowledge.combine.implies [BytesFunctor] {n : Nat} {SubFs : Fin n → Type → Type} (atts : (id : Fin n) → SubAttackerKnowledge (SubFs id)) (p : Bytes → Prop) (pfs : ∀ (id : Fin n), (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