proof(E5): msg-size + singleton-trace partial secrecy (Session 4)

Session 4 lands the subterm-size argument that Session 3 had to
defer.  This unblocks a *genuine* partial-secrecy theorem: on a
singleton encrypted trace, the attacker cannot derive the body
without knowing the key.  This is the base case of the eventual
full secrecy induction.

Session 4 contents (all Qed-closed):

  - `msg_size : msg -> nat` — structural size counting constructors.
  - `msg_size_mEnc_eq`: msg_size (mEnc k m) = S (msg_size m).
  - `msg_no_self_mEnc`: m ≠ mEnc k m for all k, m (via size).
  - **`singleton_enc_trace_knows_equals_obs`**: on a 1-event
    encrypted trace, if the attacker does not hold the key, every
    derivable message equals the ciphertext.  Proof is induction
    on the `knows` derivation tree, with each rule's IH yielding
    either the base case or a constructor-discrimination vacuity.
  - **`singleton_enc_trace_without_key_cannot_know_body`**: direct
    corollary — the body is unreachable without the key.

This is the partial-secrecy kernel: Dolev-Yao derivation from a
single-ciphertext trace, without the key, cannot extract the body.
The proof uses no `Admitted`, no banned constructs, and routes
every induction case either through k_obs (identifying the
derived message with the observed ciphertext) or through
constructor-discrimination inversion on IH-derived equalities.

MANIFEST unchanged; runner 35/35 stable; panic-attack 0.

Session 5 target: extend to multi-event traces via trace
induction; introduce per-session state tracking; close the
full secrecy invariant; Qed `needham_schroeder_fixed`.

File grew 586 -> 706 LOC.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

proofs/canonical-proof-suite/E5_needham_schroeder_fix.v

@@ -575,12 +575,132 @@ Proof.
   apply sub_enc. apply sub_refl.
 Qed.
 
-(* The structural partial-secrecy result — "singleton-trace body
-   needs key" — requires a subterm-size argument that rules out
-   `m = mEnc k m` as an inductive-msg value.  That size argument
-   is deferred to Session 4 (it requires either a well-founded
-   recursion on msg size or an explicit "no infinite towers"
-   lemma via Acc / Fix).  For Session 3 we land only the
-   compromise-model types + the basic contrapositive routed
-   through `knows_enc_and_key_gives_body`.  No banned constructs
-   lie in this file; the deferred lemma simply isn't here. *)
+(* Session 3 deferred the structural partial-secrecy result
+   (singleton-trace body needs key) to Session 4 because it
+   requires a subterm-size argument.  Session 4 now lands it —
+   see the `Session 4` section below. *)
+
+(* ============================================================ *)
+(*  Session 4 (2026-04-18) — msg-size + singleton-trace secrecy  *)
+(* ============================================================ *)
+
+(* Structural size of a `msg` — counts constructor occurrences.
+   The only use in this file is ruling out `m = mEnc k m` style
+   self-cycles, which inductive `msg` cannot host.  Session 3's
+   deferred singleton-trace-body-needs-key lemma lands on top of
+   this. *)
+
+Fixpoint msg_size (m : msg) : nat :=
+  match m with
+  | mAgent _   => 1
+  | mNonce _   => 1
+  | mKey _     => 1
+  | mPair l r  => S (msg_size l + msg_size r)
+  | mEnc _ b   => S (msg_size b)
+  end.
+
+Lemma msg_size_mEnc_eq :
+  forall k m, msg_size (mEnc k m) = S (msg_size m).
+Proof. intros; simpl; reflexivity. Qed.
+
+(* A `msg` is never its own `mEnc` wrapper. *)
+Lemma msg_no_self_mEnc :
+  forall (k : key) (m : msg), m <> mEnc k m.
+Proof.
+  intros k m Heq.
+  assert (H : msg_size m = msg_size (mEnc k m))
+    by (rewrite <- Heq; reflexivity).
+  rewrite msg_size_mEnc_eq in H.
+  (* H : msg_size m = S (msg_size m) — impossible. *)
+  pose proof (Nat.neq_succ_diag_r (msg_size m)) as Hne.
+  contradiction.
+Qed.
+
+(* Session-3's deferred lemma, now closed.  On a trace containing
+   exactly one event — an encrypted message mEnc k body — if the
+   attacker does NOT know the key k, then every derivable message
+   equals mEnc k body (i.e., the attacker has no capability except
+   re-observing the wire). *)
+
+Lemma singleton_enc_trace_knows_equals_obs :
+  forall (a : agent) (k : key) (body m : msg),
+    let tr := [mkEvent a (mEnc k body)] in
+    ~ knows tr (mKey k) ->
+    knows tr m ->
+    m = mEnc k body.
+Proof.
+  intros a k body m tr Hno_key Hknow.
+  (* We cannot use an ordinary `induction Hknow` because `tr` is
+     a `let`-bound local — the induction principle would generalise
+     `tr` away from our hypothesis.  `remember` + `induction` on
+     the generalised `tr0` gives the right shape. *)
+  unfold tr in *.
+  remember ([mkEvent a (mEnc k body)]) as tr0 eqn:Htr0.
+  induction Hknow as
+    [ ev Hin
+    | l r Hpair IHpair
+    | l r Hpair IHpair
+    | k' mbody Henc IHenc Hkey IHkey ].
+  - (* k_obs: ev ∈ tr0 = [mkEvent a (mEnc k body)], so ev is that event. *)
+    subst tr0. simpl in Hin. destruct Hin as [Heq | []].
+    (* Heq : mkEvent a (mEnc k body) = ev *)
+    subst ev. simpl. reflexivity.
+  - (* k_pairL: knows tr0 (mPair m r) implies mPair m r = mEnc k body by IH.
+       But mPair <> mEnc by constructor discrimination — vacuous. *)
+    assert (Heq : mPair l r = mEnc k body) by (apply IHpair; exact Htr0).
+    inversion Heq.
+  - (* k_pairR: symmetric. *)
+    assert (Heq : mPair l r = mEnc k body) by (apply IHpair; exact Htr0).
+    inversion Heq.
+  - (* k_dec: knows tr (mEnc k' mbody) and knows tr (mKey k').
+       IH on mKey k': mKey k' = mEnc k body — impossible by
+       constructor discrimination. *)
+    assert (Hkeyeq : mKey k' = mEnc k body) by (apply IHkey; exact Htr0).
+    inversion Hkeyeq.
+Qed.
+
+(* Corollary: on such a singleton trace, the attacker cannot derive
+   the body unless body = mEnc k body — which msg_no_self_mEnc
+   rules out. *)
+Lemma singleton_enc_trace_without_key_cannot_know_body :
+  forall (a : agent) (k : key) (body : msg),
+    let tr := [mkEvent a (mEnc k body)] in
+    ~ knows tr (mKey k) ->
+    ~ knows tr body.
+Proof.
+  intros a k body tr Hno_key Hknow_body.
+  assert (Hbody_eq : body = mEnc k body).
+  { eapply singleton_enc_trace_knows_equals_obs.
+    - exact Hno_key.
+    - exact Hknow_body. }
+  exact (msg_no_self_mEnc Hbody_eq).
+Qed.
+
+(* ============================================================ *)
+(*  Session 4 status note (2026-04-18)                           *)
+(* ============================================================ *)
+(*                                                               *)
+(*  Added in Session 4 (above):                                  *)
+(*    * msg_size (structural size, ruling out self-cycles).      *)
+(*    * msg_size_mEnc_eq (definitional rewrite).                 *)
+(*    * msg_no_self_mEnc: m <> mEnc k m for all k, m.            *)
+(*    * singleton_enc_trace_knows_equals_obs: on a 1-event       *)
+(*      encrypted trace, without the key, every derivable        *)
+(*      message equals the ciphertext. Session 3's deferred      *)
+(*      lemma, now Qed-closed.                                   *)
+(*    * singleton_enc_trace_without_key_cannot_know_body:        *)
+(*      corollary — body is unreachable without the key.         *)
+(*                                                               *)
+(*  This is a genuine partial-secrecy result: the attacker's     *)
+(*  knowledge closure is bounded on the simplest protocol-like   *)
+(*  trace (one ciphertext event, no key leak). It is the         *)
+(*  base case of the final secrecy induction.                    *)
+(*                                                               *)
+(*  Session 5 target:                                            *)
+(*    * Extend the singleton-trace result to arbitrary traces    *)
+(*      via trace induction.                                     *)
+(*    * Per-session state record.                                *)
+(*    * Final secrecy invariant + needham_schroeder_fixed Qed.   *)
+(* ============================================================ *)
+(*  End of E5 in-progress scaffold.                              *)
+(* ============================================================ *)