`PublicECDLPData`

definition

show as: view math explainer →

module: IndisputableMonolith.Cryptography.ECDLPWatch
domain: Cryptography
line: 112 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cryptography.ECDLPWatch on GitHub at line 112.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 109
 110/-- Public data available to an adversary. This structure exists to keep later
 111RS invariants honest: they may depend only on these fields. -/
 112structure PublicECDLPData (p : ℕ) where
 113  curve : ShortWeierstrassCurve p
 114  base : ECPoint p
 115  target : ECPoint p
 116  order : ℕ
 117  cofactor : ℕ
 118  family : CurveFamily
 119
 120def ECDLPInstance.publicData {p : ℕ} (inst : ECDLPInstance p) : PublicECDLPData p where
 121  curve := inst.curve
 122  base := inst.base
 123  target := inst.target
 124  order := inst.order
 125  cofactor := inst.cofactor
 126  family := inst.family
 127
 128/-- A watch invariant is admissible only if it is computed from public data. -/
 129structure PublicInvariant where
 130  score : ∀ {p : ℕ}, PublicECDLPData p → ℝ
 131
 132/-- Known weak-curve classes must be separated from any standard-curve claim. -/
 133def isKnownWeakFamily : CurveFamily → Prop
 134  | CurveFamily.anomalous => True
 135  | CurveFamily.supersingular => True
 136  | CurveFamily.smallEmbeddingDegree => True
 137  | _ => False
 138
 139/-- Watch predicate: a candidate invariant is being tested only on public data
 140and against an explicitly tagged curve family. This carries no security claim. -/
 141structure InvariantWatchRecord (I : PublicInvariant) where
 142  family : CurveFamily

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.