proof(E5): Session 6 — single-session NS-Lowe secrecy + headline needham_schroeder_fixed Qed

Session 6 on the E5 full-headline port lands the MANIFEST-expected
headline theorem [needham_schroeder_fixed] for a single honest
session of the Lowe-fixed Needham-Schroeder symmetric-key
protocol, closed against the Dolev-Yao attacker defined in
Sessions 1-3.

Contents landed (§8):

  * [session_state] record  (initiator, responder, N_A, N_B).

  * [single_session_trace] — the three-event wire shape of one
    honest execution:
        1. A -> B : {N_A, A, B}_{K_AB}
        2. B -> A : {N_A, N_B}_{K_AB}
        3. A -> B : {N_B}_{K_AB}

  * [single_session_trace_is_enc_only] — bridge to Session 5's
    [enc_only_trace] predicate: every wire message on a single-
    session trace is [mEnc (shared_key A B) _].

  * [single_session_wire_messages] — explicit wire-message list,
    used for non-membership arguments.

  * [nb_not_on_wire] — [mNonce N_B] is not among the three
    wire-message ciphertexts (constructor discrimination).

  * [any_enc_trace] + [single_session_is_any_enc] +
    [knows_any_enc_trace_is_mEnc_shaped] — structural invariant:
    on a trace whose wire messages are all [mEnc]-shaped, every
    attacker-derivable message is also [mEnc]-shaped.  The
    invariant-based proof avoids the circularity that would
    otherwise sit between "no key derivable" and Session 5's
    enc-only closure.

  * [single_session_no_key_derivable] — the attacker cannot
    derive ANY [mKey k] on a single-session trace (immediate
    corollary of the shape invariant).

  * [ns_lowe_single_session_secrecy] + [ns_lowe_single_session_
    initiator_nonce_secrecy] — keyed secrecy for responder and
    initiator nonces respectively, closed by routing through
    [enc_trace_unobserved_unreachable] (Session 5).

  * [ns_lowe_responder_nonce_secret] + [ns_lowe_initiator_nonce_
    secret] — user-facing forms with the [~ knows tr (mKey _)]
    side obligation discharged automatically by [single_session_
    no_key_derivable].

  * [needham_schroeder_fixed] — the headline theorem:

      forall (ses : session_state) (tr : trace),
        single_session_trace ses tr ->
        ~ knows tr (mNonce (ss_na ses)) /\ ~ knows tr (mNonce (ss_nb ses)).

Verification:
  * coqc E5_needham_schroeder_fix.v — Qed, exit 0.
  * panic-attack assail — 0 weak points on 1079 LOC.
  * grep banned constructs (believe_me/assert_total/Admitted/
    sorry/unsafeCoerce/Obj.magic) — 0 code hits.
  * Suite-wide recompile — 38/38 Qed, no regressions.

MANIFEST pointer remains intact: the headline [needham_schroeder_
fixed] is now Qed-closed for the single-session scope, but the
multi-session composition case (attacker running arbitrarily many
honest and dishonest sessions in parallel, with nonce/key leakage
across sessions) is Session 7+ work.  Per §3.1 honest-accounting,
the MANIFEST entry can be revisited once the multi-session scope
lands.

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

Author: hyperpolymath

proofs/canonical-proof-suite/E5_needham_schroeder_fix.v

@@ -783,11 +783,297 @@ Qed.
 (*    * singleton_enc_trace_recovery: Session 4 recovered         *)
 (*      as a specialisation (sanity check).                       *)
 (*                                                                *)
-(*  Session 6+ target:                                            *)
-(*    * Per-session state record (honest nonces/keys vs.          *)
-(*      attacker-visible messages).                               *)
-(*    * Full Needham-Schroeder-Lowe secrecy invariant and         *)
-(*      headline needham_schroeder_fixed Qed.                     *)
-(* ============================================================ *)
-(*  End of E5 in-progress scaffold.                              *)
+(*  Session 6 (DONE — §8 below): per-session state + headline     *)
+(*  needham_schroeder_fixed Qed for a single honest session.      *)
 (* ============================================================ *)
+
+(* ====================================================================
+   §8  Per-session state + NS-Lowe secrecy invariant.
+   ==================================================================== *)
+
+(** One NS-Lowe session's honest view.  The attacker's view is the
+    list of wire events; this record describes what the honest
+    initiator/responder pair shares about the session — who is
+    talking to whom and which nonces are bound to which role. *)
+Record session_state : Set := mkSession {
+  ss_init : agent;
+  ss_resp : agent;
+  ss_na   : nonce;  (* initiator's fresh nonce, step-1 body *)
+  ss_nb   : nonce   (* responder's fresh nonce, step-2 body *)
+}.
+
+(** The wire-shape of a single honest execution of the Lowe-fixed
+    NS-symmetric protocol.  Exactly three events, in order:
+
+      1. A -> B : {N_A, A, B}_{K_AB}   (fixed_step1_ciphertext)
+      2. B -> A : {N_A, N_B}_{K_AB}    (fixed_step2_ciphertext)
+      3. A -> B : {N_B}_{K_AB}         (fixed_step3_ciphertext)
+
+    This is the honest-world trace; the attacker is the environment
+    sitting next to the wire.  Secrecy in this session is the claim
+    that, without the shared key, the attacker cannot derive N_B. *)
+Definition single_session_trace
+           (ses : session_state) (tr : trace) : Prop :=
+  tr = [ mkEvent (ss_init ses)
+                 (fixed_step1_ciphertext (ss_init ses)
+                                         (ss_resp ses)
+                                         (ss_na ses));
+         mkEvent (ss_resp ses)
+                 (fixed_step2_ciphertext (ss_init ses)
+                                         (ss_resp ses)
+                                         (ss_na ses)
+                                         (ss_nb ses));
+         mkEvent (ss_init ses)
+                 (fixed_step3_ciphertext (ss_init ses)
+                                         (ss_resp ses)
+                                         (ss_nb ses)) ].
+
+(** Every event in a single honest session has its message encrypted
+    under the pair's shared key.  This is the structural fact that
+    connects the protocol-level trace to Session 5's enc-only-trace
+    machinery. *)
+Lemma single_session_trace_is_enc_only :
+  forall (ses : session_state) (tr : trace),
+    single_session_trace ses tr ->
+    enc_only_trace (shared_key (ss_init ses) (ss_resp ses)) tr.
+Proof.
+  intros ses tr Htr. unfold enc_only_trace, single_session_trace in *.
+  subst tr. intros e Hin.
+  simpl in Hin.
+  destruct Hin as [H1 | [H2 | [H3 | []]]]; subst e; simpl.
+  - (* step 1 *)
+    exists (mPair (mNonce (ss_na ses))
+                  (mPair (mAgent (ss_init ses)) (mAgent (ss_resp ses)))).
+    unfold fixed_step1_ciphertext. reflexivity.
+  - (* step 2 *)
+    exists (mPair (mNonce (ss_na ses)) (mNonce (ss_nb ses))).
+    unfold fixed_step2_ciphertext. reflexivity.
+  - (* step 3 *)
+    exists (mNonce (ss_nb ses)).
+    unfold fixed_step3_ciphertext. reflexivity.
+Qed.
+
+(** The observed ciphertexts of a single honest session.  This is
+    exactly [map ev_msg tr].  Stated explicitly so we can reason
+    about non-membership of the responder nonce. *)
+Lemma single_session_wire_messages :
+  forall (ses : session_state) (tr : trace),
+    single_session_trace ses tr ->
+    map ev_msg tr =
+      [ fixed_step1_ciphertext (ss_init ses) (ss_resp ses) (ss_na ses);
+        fixed_step2_ciphertext (ss_init ses) (ss_resp ses) (ss_na ses) (ss_nb ses);
+        fixed_step3_ciphertext (ss_init ses) (ss_resp ses) (ss_nb ses) ].
+Proof.
+  intros ses tr Htr. unfold single_session_trace in Htr. subst tr.
+  simpl. reflexivity.
+Qed.
+
+(** Constructor discrimination: a [mNonce] is never an [mEnc].  This
+    is immediate from the [msg] inductive but we package it for the
+    non-membership argument that drives secrecy. *)
+Lemma mNonce_ne_mEnc :
+  forall (n : nonce) (k : key) (m : msg),
+    mNonce n <> mEnc k m.
+Proof. intros n k m H. inversion H. Qed.
+
+(** The responder nonce is NOT among the observed wire messages of
+    a single honest session.  Every wire message is [mEnc]-shaped;
+    [mNonce _] cannot match. *)
+Lemma nb_not_on_wire :
+  forall (ses : session_state) (tr : trace),
+    single_session_trace ses tr ->
+    ~ In (mNonce (ss_nb ses)) (map ev_msg tr).
+Proof.
+  intros ses tr Htr Hin.
+  rewrite (@single_session_wire_messages ses tr Htr) in Hin.
+  simpl in Hin.
+  destruct Hin as [H1 | [H2 | [H3 | []]]].
+  - unfold fixed_step1_ciphertext in H1. inversion H1.
+  - unfold fixed_step2_ciphertext in H2. inversion H2.
+  - unfold fixed_step3_ciphertext in H3. inversion H3.
+Qed.
+
+(** **NS-Lowe secrecy invariant for a single honest session.**
+
+    Statement.  For any honest single-session trace between the
+    initiator [A = ss_init ses] and the responder [B = ss_resp ses],
+    if the attacker does not know the pair's shared key
+    [K_AB = shared_key A B], then the attacker cannot derive the
+    responder's fresh nonce [N_B = ss_nb ses].
+
+    Proof.  The trace is an enc-only trace under [K_AB] by
+    [single_session_trace_is_enc_only].  By Session 5's
+    [enc_trace_unobserved_unreachable], any message outside the wire
+    is unreachable.  [nb_not_on_wire] says [mNonce N_B] is not on
+    the wire, hence it's unreachable.  *)
+Theorem ns_lowe_single_session_secrecy :
+  forall (ses : session_state) (tr : trace),
+    single_session_trace ses tr ->
+    ~ knows tr (mKey (shared_key (ss_init ses) (ss_resp ses))) ->
+    ~ knows tr (mNonce (ss_nb ses)).
+Proof.
+  intros ses tr Htr Hno_key.
+  apply (@enc_trace_unobserved_unreachable
+           (shared_key (ss_init ses) (ss_resp ses))
+           tr (mNonce (ss_nb ses))).
+  - apply single_session_trace_is_enc_only. exact Htr.
+  - exact Hno_key.
+  - apply nb_not_on_wire. exact Htr.
+Qed.
+
+(** Analogue for the initiator nonce [N_A].  Same proof skeleton:
+    [N_A] is also not on the wire (every wire message is
+    [mEnc]-shaped), and the enc-only/no-key closure gives the bound.
+    A single-session full-secrecy package. *)
+Theorem ns_lowe_single_session_initiator_nonce_secrecy :
+  forall (ses : session_state) (tr : trace),
+    single_session_trace ses tr ->
+    ~ knows tr (mKey (shared_key (ss_init ses) (ss_resp ses))) ->
+    ~ knows tr (mNonce (ss_na ses)).
+Proof.
+  intros ses tr Htr Hno_key.
+  apply (@enc_trace_unobserved_unreachable
+           (shared_key (ss_init ses) (ss_resp ses))
+           tr (mNonce (ss_na ses))).
+  - apply single_session_trace_is_enc_only. exact Htr.
+  - exact Hno_key.
+  - (* mNonce (ss_na ses) is not on the wire. *)
+    intros Hin.
+    rewrite (@single_session_wire_messages ses tr Htr) in Hin.
+    simpl in Hin.
+    destruct Hin as [H1 | [H2 | [H3 | []]]].
+    + unfold fixed_step1_ciphertext in H1. inversion H1.
+    + unfold fixed_step2_ciphertext in H2. inversion H2.
+    + unfold fixed_step3_ciphertext in H3. inversion H3.
+Qed.
+
+(** Combined single-session secrecy: neither party's nonce is
+    derivable by the attacker under honest-key conditions. *)
+Theorem ns_lowe_single_session_full_secrecy :
+  forall (ses : session_state) (tr : trace),
+    single_session_trace ses tr ->
+    ~ knows tr (mKey (shared_key (ss_init ses) (ss_resp ses))) ->
+    ~ knows tr (mNonce (ss_na ses)) /\ ~ knows tr (mNonce (ss_nb ses)).
+Proof.
+  intros ses tr Htr Hno_key.
+  split.
+  - apply ns_lowe_single_session_initiator_nonce_secrecy; assumption.
+  - apply ns_lowe_single_session_secrecy; assumption.
+Qed.
+
+(** Link to the [honest_pair] predicate from Session 3.  The more
+    natural user-facing statement: an honest pair (uncompromised
+    shared key) with a completed honest session has secret nonces.
+
+    Caveat: the [compromised] predicate tracks attacker knowledge of
+    keys as a semantic fact, and ruling out [knows tr (mKey k)]
+    requires showing the trace itself does not expose the key.
+    For the single-session trace, no event has [ev_msg = mKey _],
+    so the key can only be derived via [k_pairL]/[k_pairR]/[k_dec].
+    None of the wire messages are [mPair], and [k_dec] requires
+    another key the attacker already has.  We close this below:
+    on a single-session trace, the attacker cannot derive ANY
+    [mKey _] at all (no matter which key). *)
+
+(** Every wire message of a single honest session has the shape
+    [mEnc _ _] (under any key — we drop the specific [shared_key]
+    index here).  This weaker predicate is enough for the
+    "no-key-derivable" invariant below, and avoids any circularity
+    with [enc_trace_knows_is_observed]. *)
+Definition any_enc_trace (tr : trace) : Prop :=
+  forall ev, In ev tr -> exists k body, ev_msg ev = mEnc k body.
+
+Lemma single_session_is_any_enc :
+  forall ses tr,
+    single_session_trace ses tr -> any_enc_trace tr.
+Proof.
+  intros ses tr Htr. unfold any_enc_trace. intros ev Hin.
+  unfold single_session_trace in Htr. subst tr. simpl in Hin.
+  destruct Hin as [H1 | [H2 | [H3 | []]]]; subst ev; simpl.
+  - eexists. eexists. unfold fixed_step1_ciphertext. reflexivity.
+  - eexists. eexists. unfold fixed_step2_ciphertext. reflexivity.
+  - eexists. eexists. unfold fixed_step3_ciphertext. reflexivity.
+Qed.
+
+(** Structural invariant.  On any trace whose wire messages are all
+    [mEnc]-shaped, every attacker-derivable message is also
+    [mEnc]-shaped.  Proof by induction on [knows]: the [k_obs] case
+    is the hypothesis; the two [k_pair*] cases force [mPair ... =
+    mEnc ...] by IH, contradiction; the [k_dec] case forces
+    [mKey ... = mEnc ...] via [IHkey], contradiction.  The [k_dec]
+    case's conclusion [mbody]-shape is vacuous after that
+    contradiction. *)
+Lemma knows_any_enc_trace_is_mEnc_shaped :
+  forall tr,
+    any_enc_trace tr ->
+    forall m, knows tr m -> exists k body, m = mEnc k body.
+Proof.
+  intros tr Henc m Hknow.
+  induction Hknow as
+    [ ev Hin
+    | l r _ IHpair
+    | l r _ IHpair
+    | k' mbody _ IHenc Hkey IHkey ].
+  - specialize (Henc ev Hin) as [k' [body Hb]].
+    exists k', body. exact Hb.
+  - destruct IHpair as [k' [body Heq]]. inversion Heq.
+  - destruct IHpair as [k' [body Heq]]. inversion Heq.
+  - destruct IHkey as [k'' [body Heq]]. inversion Heq.
+Qed.
+
+(** No key is ever attacker-derivable on a single honest session
+    trace.  Routes through the invariant above: any derived message
+    must be [mEnc]-shaped, but [mKey _] is not. *)
+Lemma single_session_no_key_derivable :
+  forall (ses : session_state) (tr : trace) (k : key),
+    single_session_trace ses tr ->
+    ~ knows tr (mKey k).
+Proof.
+  intros ses tr k Htr Hknow.
+  pose proof (@knows_any_enc_trace_is_mEnc_shaped tr
+                (@single_session_is_any_enc ses tr Htr)
+                (mKey k) Hknow) as [k' [body Heq]].
+  inversion Heq.
+Qed.
+
+(** User-facing NS-Lowe secrecy: on an honest single session, the
+    responder nonce is not attacker-derivable.  No explicit
+    [~ knows tr (mKey _)] hypothesis needed — [single_session_no_
+    key_derivable] closes that side obligation automatically from
+    the enc-only structure of the wire. *)
+Theorem ns_lowe_responder_nonce_secret :
+  forall (ses : session_state) (tr : trace),
+    single_session_trace ses tr ->
+    ~ knows tr (mNonce (ss_nb ses)).
+Proof.
+  intros ses tr Htr.
+  apply ns_lowe_single_session_secrecy.
+  - exact Htr.
+  - apply (@single_session_no_key_derivable ses tr). exact Htr.
+Qed.
+
+Theorem ns_lowe_initiator_nonce_secret :
+  forall (ses : session_state) (tr : trace),
+    single_session_trace ses tr ->
+    ~ knows tr (mNonce (ss_na ses)).
+Proof.
+  intros ses tr Htr.
+  apply ns_lowe_single_session_initiator_nonce_secrecy.
+  - exact Htr.
+  - apply (@single_session_no_key_derivable ses tr). exact Htr.
+Qed.
+
+(** **Headline.**  The Needham-Schroeder-Lowe fix guarantees secrecy
+    of both nonces on an honest single session.  This is the
+    MANIFEST-expected headline for the current scope — single honest
+    session.  Multi-session composition and cross-session
+    interference is Session 7+ work. *)
+Theorem needham_schroeder_fixed :
+  forall (ses : session_state) (tr : trace),
+    single_session_trace ses tr ->
+    ~ knows tr (mNonce (ss_na ses)) /\ ~ knows tr (mNonce (ss_nb ses)).
+Proof.
+  intros ses tr Htr. split.
+  - apply ns_lowe_initiator_nonce_secret. exact Htr.
+  - apply ns_lowe_responder_nonce_secret. exact Htr.
+Qed.