|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | +-- SPDX-License-Identifier: MPL-2.0 |
| 3 | +-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 4 | + |
| 5 | +-- EchoDeniability: residue deniability as a first-class echo property. |
| 6 | +-- |
| 7 | +-- A residue-production function f : History → Residue is *perfectly |
| 8 | +-- deniable* when its image is a single point — no opener d can |
| 9 | +-- distinguish histories via their residues, because all residues are |
| 10 | +-- the same. This is the case where f is constant, mirroring |
| 11 | +-- `EchoCharacteristic.collapse : Bool → ⊤`. |
| 12 | +-- |
| 13 | +-- When f is injective (each history maps to a distinct residue), |
| 14 | +-- deniability fails for arbitrary openers but is restored for the |
| 15 | +-- restricted class of *constant openers* — those that ignore the |
| 16 | +-- residue entirely. This is the partial-deniability case from the |
| 17 | +-- companion exploration (DeniabilityPartial.agda). |
| 18 | +-- |
| 19 | +-- This module formalises both cases in the echo-types framework and |
| 20 | +-- makes the structural connections explicit: |
| 21 | +-- |
| 22 | +-- * The perfect case is the `no-section-of-collapsing-map` story: |
| 23 | +-- the production map collapses, so no recovery is possible. |
| 24 | +-- |
| 25 | +-- * The partial case is its dual: the production map is injective, |
| 26 | +-- a section exists (`partial-witness`), so recovery IS possible |
| 27 | +-- for arbitrary openers — deniability only survives for those who |
| 28 | +-- decline to look. |
| 29 | +-- |
| 30 | +-- * `IsConstantOpener` — the class of openers that ignore the |
| 31 | +-- residue — is the type-level analogue of the `affine` mode in |
| 32 | +-- `EchoObservationalEquivalence._≡m_`: at affine, there is |
| 33 | +-- nothing left in the residue to observe, so all openers agree. |
| 34 | +-- |
| 35 | +-- Honest scope: |
| 36 | +-- |
| 37 | +-- * All guarantees are type-level: what pure Agda functions d can |
| 38 | +-- and cannot do under --safe --without-K, zero postulates. |
| 39 | +-- * No claim is made about side-channels, timing, oracle access, |
| 40 | +-- or adversaries with state outside the model. |
| 41 | +-- * `partial-deniable-restricted` is the minimum-viable type-level |
| 42 | +-- boundary. Cryptographic deniability requires additional |
| 43 | +-- structure beyond the structural no-section property. |
| 44 | +-- |
| 45 | +-- Headlines (pinned in Smoke.agda): |
| 46 | +-- |
| 47 | +-- * History -- the two-history type |
| 48 | +-- * Residue -- the two-residue type (Trace / Erased) |
| 49 | +-- * produce-perfect -- constant production: all → Trace |
| 50 | +-- * produce-partial -- injective production: Intact→Trace, Lost→Erased |
| 51 | +-- * IsDeniable -- ∀ d, d ∘ f equal on Intact / Lost |
| 52 | +-- * IsConstantOpener -- the restricted-opener class (d Trace ≡ d Erased) |
| 53 | +-- * perfect-deniable -- IsDeniable produce-perfect |
| 54 | +-- * partial-witness -- the distinguishing opener for produce-partial |
| 55 | +-- * partial-distinguishable -- partial-witness separates the two histories |
| 56 | +-- * partial-not-deniable -- ¬ IsDeniable produce-partial |
| 57 | +-- * partial-deniable-restricted -- restricted deniability for produce-partial |
| 58 | +-- * no-section-produce-perfect -- no section for the collapsing map |
| 59 | +-- * partial-has-section -- section exists for the injective map |
| 60 | + |
| 61 | +module EchoDeniability where |
| 62 | + |
| 63 | +open import Echo using (Echo; echo-intro) |
| 64 | +open import EchoNoSectionGeneric using (no-section-of-collapsing-map) |
| 65 | + |
| 66 | +open import Data.Product.Base using (Σ; _,_) |
| 67 | +open import Data.Unit.Base using (⊤; tt) |
| 68 | +open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl) |
| 69 | +open import Relation.Nullary using (¬_) |
| 70 | + |
| 71 | +------------------------------------------------------------------------ |
| 72 | +-- The two histories and the two residues. |
| 73 | +------------------------------------------------------------------------ |
| 74 | + |
| 75 | +data History : Set where |
| 76 | + Intact : History |
| 77 | + Lost : History |
| 78 | + |
| 79 | +-- Two-constructor residue: Trace is a retained mark; Erased is an |
| 80 | +-- absent one. With one constructor the collapse is trivial (refl); |
| 81 | +-- with two we can witness failure and recovery. |
| 82 | +data Residue : Set where |
| 83 | + Trace : Residue |
| 84 | + Erased : Residue |
| 85 | + |
| 86 | +------------------------------------------------------------------------ |
| 87 | +-- The two production functions. |
| 88 | +-- |
| 89 | +-- produce-perfect: constant — both histories leave the same residue. |
| 90 | +-- Mirrors `EchoCharacteristic.collapse : Bool → ⊤`. |
| 91 | +-- |
| 92 | +-- produce-partial: injective — each history leaves a distinct residue. |
| 93 | +-- Mirrors a Bool-tagged split where the two tags are distinguishable. |
| 94 | +------------------------------------------------------------------------ |
| 95 | + |
| 96 | +produce-perfect : History → Residue |
| 97 | +produce-perfect _ = Trace |
| 98 | + |
| 99 | +produce-partial : History → Residue |
| 100 | +produce-partial Intact = Trace |
| 101 | +produce-partial Lost = Erased |
| 102 | + |
| 103 | +------------------------------------------------------------------------ |
| 104 | +-- Deniability predicate. |
| 105 | +-- |
| 106 | +-- f is deniable when no opener can distinguish which history produced |
| 107 | +-- the residue: d(f Intact) ≡ d(f Lost) for every opener d. |
| 108 | +------------------------------------------------------------------------ |
| 109 | + |
| 110 | +IsDeniable : (History → Residue) → Set |
| 111 | +IsDeniable f = (d : Residue → History) → d (f Intact) ≡ d (f Lost) |
| 112 | + |
| 113 | +------------------------------------------------------------------------ |
| 114 | +-- Perfect deniability: produce-perfect is fully deniable. |
| 115 | +-- |
| 116 | +-- Both histories produce Trace, so d(Trace) ≡ d(Trace) for any d. |
| 117 | +-- The proof is refl: definitional equality after computation. |
| 118 | +------------------------------------------------------------------------ |
| 119 | + |
| 120 | +perfect-deniable : IsDeniable produce-perfect |
| 121 | +perfect-deniable d = refl |
| 122 | + |
| 123 | +------------------------------------------------------------------------ |
| 124 | +-- Distinct residues: Intact ≢ Lost (standard constructor discrimination). |
| 125 | +------------------------------------------------------------------------ |
| 126 | + |
| 127 | +Intact≢Lost : Intact ≢ Lost |
| 128 | +Intact≢Lost () |
| 129 | + |
| 130 | +------------------------------------------------------------------------ |
| 131 | +-- Partial case: counterexample opener. |
| 132 | +-- |
| 133 | +-- partial-witness reads off the history directly from the residue. |
| 134 | +-- It is a left-inverse of produce-partial: section identity holds |
| 135 | +-- by definitional reduction on each constructor. |
| 136 | +------------------------------------------------------------------------ |
| 137 | + |
| 138 | +partial-witness : Residue → History |
| 139 | +partial-witness Trace = Intact |
| 140 | +partial-witness Erased = Lost |
| 141 | + |
| 142 | +partial-distinguishable : |
| 143 | + ¬ (partial-witness (produce-partial Intact) ≡ |
| 144 | + partial-witness (produce-partial Lost)) |
| 145 | +partial-distinguishable () |
| 146 | +-- Reduces to ¬ (Intact ≡ Lost); the empty pattern refutes it. |
| 147 | + |
| 148 | +------------------------------------------------------------------------ |
| 149 | +-- produce-partial is not deniable. |
| 150 | +-- |
| 151 | +-- The witness partial-witness distinguishes the two histories, so |
| 152 | +-- deniability fails for unrestricted openers. |
| 153 | +------------------------------------------------------------------------ |
| 154 | + |
| 155 | +partial-not-deniable : ¬ IsDeniable produce-partial |
| 156 | +partial-not-deniable den = partial-distinguishable (den partial-witness) |
| 157 | + |
| 158 | +------------------------------------------------------------------------ |
| 159 | +-- Restricted class: constant openers ignore the residue. |
| 160 | +-- |
| 161 | +-- An opener is constant when it returns the same verdict on every |
| 162 | +-- residue. This is the type-level analogue of the `affine` mode in |
| 163 | +-- `EchoObservationalEquivalence._≡m_`: at affine, there is nothing |
| 164 | +-- left in the residue to distinguish — all affine observers agree. |
| 165 | +------------------------------------------------------------------------ |
| 166 | + |
| 167 | +IsConstantOpener : (Residue → History) → Set |
| 168 | +IsConstantOpener d = d Trace ≡ d Erased |
| 169 | + |
| 170 | +------------------------------------------------------------------------ |
| 171 | +-- Restricted deniability for produce-partial. |
| 172 | +-- |
| 173 | +-- For any constant opener, the two histories remain indistinguishable |
| 174 | +-- even under injective production: d cannot exploit the residue |
| 175 | +-- difference if it never looks. Goal reduces by computation to |
| 176 | +-- d Trace ≡ d Erased, which is exactly `const`. |
| 177 | +------------------------------------------------------------------------ |
| 178 | + |
| 179 | +partial-deniable-restricted : |
| 180 | + (d : Residue → History) → |
| 181 | + IsConstantOpener d → |
| 182 | + d (produce-partial Intact) ≡ d (produce-partial Lost) |
| 183 | +partial-deniable-restricted d const = const |
| 184 | + |
| 185 | +------------------------------------------------------------------------ |
| 186 | +-- No section for produce-perfect. |
| 187 | +-- |
| 188 | +-- Since produce-perfect collapses Intact and Lost onto the same |
| 189 | +-- residue (Trace ≡ Trace), `no-section-of-collapsing-map` applies |
| 190 | +-- directly: no pure function can recover the history from the residue. |
| 191 | +-- This is the structural dual of perfect deniability — the collapse |
| 192 | +-- that makes deniability free also makes recovery impossible. |
| 193 | +------------------------------------------------------------------------ |
| 194 | + |
| 195 | +no-section-produce-perfect : |
| 196 | + ¬ Σ (Residue → History) (λ s → ∀ h → s (produce-perfect h) ≡ h) |
| 197 | +no-section-produce-perfect = |
| 198 | + no-section-of-collapsing-map produce-perfect Intact Lost Intact≢Lost refl |
| 199 | + |
| 200 | +------------------------------------------------------------------------ |
| 201 | +-- Section exists for produce-partial. |
| 202 | +-- |
| 203 | +-- Since produce-partial is injective, partial-witness is a genuine |
| 204 | +-- left-inverse. This is the dual: injective production gives recovery. |
| 205 | +-- Together with `partial-not-deniable`, it shows that the existence of |
| 206 | +-- a section and the failure of deniability are the same phenomenon. |
| 207 | +------------------------------------------------------------------------ |
| 208 | + |
| 209 | +partial-witness-is-section : ∀ h → partial-witness (produce-partial h) ≡ h |
| 210 | +partial-witness-is-section Intact = refl |
| 211 | +partial-witness-is-section Lost = refl |
| 212 | + |
| 213 | +partial-has-section : |
| 214 | + Σ (Residue → History) (λ s → ∀ h → s (produce-partial h) ≡ h) |
| 215 | +partial-has-section = partial-witness , partial-witness-is-section |
| 216 | + |
| 217 | +------------------------------------------------------------------------ |
| 218 | +-- Echo witnesses: distinct echoes at the same residue (perfect case). |
| 219 | +-- |
| 220 | +-- When produce-perfect collapses both histories to Trace, both Intact |
| 221 | +-- and Lost are valid witnesses for Echo produce-perfect Trace. They |
| 222 | +-- are DISTINCT witnesses (Intact ≢ Lost), yet they share the same |
| 223 | +-- residue. This is structurally identical to the |
| 224 | +-- `EchoCharacteristic.echo-true / echo-false` pair at |
| 225 | +-- `Echo collapse tt`. |
| 226 | +------------------------------------------------------------------------ |
| 227 | + |
| 228 | +echo-intact-perfect : Echo produce-perfect Trace |
| 229 | +echo-intact-perfect = echo-intro produce-perfect Intact |
| 230 | +-- echo-intro f x = (x, refl); result type is Echo f (f x) = Echo produce-perfect Trace. |
| 231 | + |
| 232 | +echo-lost-perfect : Echo produce-perfect Trace |
| 233 | +echo-lost-perfect = echo-intro produce-perfect Lost |
| 234 | +-- produce-perfect Lost = Trace, so the result type is Echo produce-perfect Trace. ✓ |
| 235 | + |
| 236 | +echo-intact-lost-distinct : echo-intact-perfect ≢ echo-lost-perfect |
| 237 | +echo-intact-lost-distinct () |
| 238 | +-- The first Σ-components are Intact and Lost; distinct constructors make |
| 239 | +-- the equality absurd and the empty pattern closes it. |
| 240 | + |
| 241 | +------------------------------------------------------------------------ |
| 242 | +-- Companion remark. |
| 243 | +-- |
| 244 | +-- The two production functions sit at opposite ends of the deniability |
| 245 | +-- spectrum. The structural relationship: |
| 246 | +-- |
| 247 | +-- perfect (constant) partial (injective) |
| 248 | +-- deniable? YES (all d) NO (partial-witness) |
| 249 | +-- has section? NO (no-section-…) YES (partial-witness-is-section) |
| 250 | +-- echo count 2 at Trace 1 at Trace, 1 at Erased |
| 251 | +-- |
| 252 | +-- The `IsConstantOpener` class is the exact cut-point at which |
| 253 | +-- deniability is restored for the partial case. In echo-types terms |
| 254 | +-- it corresponds to the `affine` mode of |
| 255 | +-- `EchoObservationalEquivalence._≡m_`: at affine, the residue |
| 256 | +-- collapses to ⊤, removing all distinguishable content — constant |
| 257 | +-- openers do the same by construction. |
| 258 | +-- |
| 259 | +-- The `no-section / has-section` duality is load-bearing: it explains |
| 260 | +-- WHY perfect deniability is free (the map collapses, so no recovery |
| 261 | +-- is possible) and why partial deniability costs something (the map is |
| 262 | +-- injective, so non-constant openers can recover, and only constant |
| 263 | +-- openers are barred from doing so). |
| 264 | +-- |
| 265 | +-- Honest-bound matched-negative block (grep NotProved catches these): |
| 266 | +------------------------------------------------------------------------ |
| 267 | + |
| 268 | +NotProved-side-channel-safe : Set |
| 269 | +NotProved-side-channel-safe = ⊤ |
| 270 | + |
| 271 | +NotProved-cryptographic-deniability : Set |
| 272 | +NotProved-cryptographic-deniability = ⊤ |
| 273 | + |
| 274 | +NotProved-adaptive-adversary : Set |
| 275 | +NotProved-adaptive-adversary = ⊤ |
0 commit comments