theory LO_Stream
begin

/*
 * LO-Stream: Streaming AEAD (Theorem 13)
 * =======================================
 *
 * Chunked AEAD with counter-derived nonces over XChaCha20-Poly1305.
 * Each stream uses a caller-provided key and a random base_nonce.
 *
 * State partition (§15.3):
 *   Linear (sequential only): next_index, finalized
 *   Persistent (both interfaces): key, base_nonce, caller_aad
 *
 * Nonce: nonce(base_nonce, index, tag_byte) — free constructor,
 *   injectivity by construction (§15.2).
 * AAD: stream_aad(base_nonce, index, tag_byte, caller_aad) — free
 *   constructor, injectivity by construction (§15.4).
 *
 * Properties:
 *   P2: Integrity (INT-CTXT) — no forgery without key
 *   P3: Ordering — chunk accepted at position j only if encrypted at j
 *   P4: Truncation resistance — finalized only via genuine final chunk
 *   P5: Cross-stream isolation — chunk from stream A rejected by stream B
 *
 * Bounded to 3 sequential chunks (indices 0, 1, 2) for termination.
 *
 * EXPECTED RESULTS:
 *   Stream_Sanity:                    VERIFIED
 *   Stream_Sanity_Finalize:           VERIFIED
 *   Theorem13_P2_Integrity:           VERIFIED
 *   Theorem13_P3_Ordering:            VERIFIED
 *   Theorem13_P4_No_False_Final:      VERIFIED
 *   Theorem13_P5_Cross_Stream:        VERIFIED
 *   Theorem13_Key_Secrecy:            VERIFIED
 */

builtins: hashing

// AEAD
functions: aead_enc/4, aead_verify/4, accept/0
equations: aead_verify(k, n, aad, aead_enc(k, n, m, aad)) = accept()

// Nonce and AAD constructors (free → injective)
functions: nonce/3, stream_aad/4

// Tag bytes
functions: nonfinal/0, final/0

// Bounded indices
functions: s/1

restriction Eq:
    "All x y #i. Eq(x,y) @i ==> x = y"

rule Index_Bounds:
    [ ] --> [ !CB('0', s('0')), !CB(s('0'), s(s('0'))) ]


/* ================= STREAM SETUP ================= */

rule Stream_Init:
    [ Fr(~key), Fr(~bn), Fr(~cid) ]
  --[ StreamInit($O, ~key, ~bn, ~cid) ]->
    [ !SP($O, ~key, ~bn, ~cid),
      EncSt($O, ~bn, '0', 'false'),
      DecSt($O, ~bn, '0', 'false'),
      Out(~bn) ]


/* ================= CORRUPTION ================= */

rule Corrupt_StreamKey:
    [ !SP($O, key, bn, cid) ]
  --[ CorruptStream($O, key) ]->
    [ Out(key) ]


/* ================= SEQUENTIAL ENCRYPTION ================= */

// Non-final chunk
rule Enc_Chunk:
    let
        n = nonce(bn, idx, nonfinal)
        aad = stream_aad(bn, idx, nonfinal, cid)
        c = aead_enc(key, n, ~m, aad)
    in
    [ EncSt($O, bn, idx, 'false'), !SP($O, key, bn, cid),
      !CB(idx, next), Fr(~m) ]
  --[ Encrypted($O, bn, idx, nonfinal, c) ]->
    [ EncSt($O, bn, next, 'false'), Out(<c, idx, nonfinal>) ]

// Final chunk — consumes EncSt without replacement (finalized)
rule Enc_Final:
    let
        n = nonce(bn, idx, final)
        aad = stream_aad(bn, idx, final, cid)
        c = aead_enc(key, n, ~m, aad)
    in
    [ EncSt($O, bn, idx, 'false'), !SP($O, key, bn, cid), Fr(~m) ]
  --[ Encrypted($O, bn, idx, final, c), EncFinalized($O, bn, idx) ]->
    [ Out(<c, idx, final>) ]


/* ================= SEQUENTIAL DECRYPTION ================= */

// Non-final chunk — decryptor advances index
rule Dec_Chunk:
    let
        n = nonce(bn, idx, nonfinal)
        aad = stream_aad(bn, idx, nonfinal, cid)
    in
    [ DecSt($O, bn, idx, 'false'), !SP($O, key, bn, cid),
      !CB(idx, next), In(<c, idx, nonfinal>) ]
  --[ Eq(aead_verify(key, n, aad, c), accept()),
      SeqDec($O, bn, idx, nonfinal, c) ]->
    [ DecSt($O, bn, next, 'false') ]

// Final chunk — consumes DecSt without replacement (finalized)
rule Dec_Final:
    let
        n = nonce(bn, idx, final)
        aad = stream_aad(bn, idx, final, cid)
    in
    [ DecSt($O, bn, idx, 'false'), !SP($O, key, bn, cid),
      In(<c, idx, final>) ]
  --[ Eq(aead_verify(key, n, aad, c), accept()),
      SeqDec($O, bn, idx, final, c), DecFinalized($O, bn, idx) ]->
    [ ]


/* ================= RANDOM-ACCESS DECRYPTION ================= */

// Stateless — reads only persistent state
rule Dec_At:
    let
        n = nonce(bn, idx, tag)
        aad = stream_aad(bn, idx, tag, cid)
    in
    [ !SP($O, key, bn, cid), In(<c, idx, tag>) ]
  --[ Eq(aead_verify(key, n, aad, c), accept()),
      RaDec($O, bn, idx, tag) ]->
    [ ]


/* ================= SECOND STREAM (cross-stream isolation) ================= */

// Same key, different base_nonce
rule Stream_Init_B:
    [ !SP($O, key, bn_a, cid_a), Fr(~bn_b), Fr(~cid_b) ]
  --[ StreamInitB($O, ~bn_b) ]->
    [ !SPB($O, key, ~bn_b, ~cid_b),
      DecStB($O, ~bn_b, '0', 'false'),
      Out(~bn_b) ]

// Stream B sequential decrypt
rule Dec_Chunk_B:
    let
        n = nonce(bn_b, idx, tag)
        aad = stream_aad(bn_b, idx, tag, cid_b)
    in
    [ DecStB($O, bn_b, idx, 'false'), !SPB($O, key, bn_b, cid_b),
      !CB(idx, next), In(<c, idx, tag>) ]
  --[ Eq(aead_verify(key, n, aad, c), accept()),
      DecB($O, bn_b, idx, tag) ]->
    [ DecStB($O, bn_b, next, 'false') ]

// Stream B random-access decrypt
rule Dec_At_B:
    let
        n = nonce(bn_b, idx, tag)
        aad = stream_aad(bn_b, idx, tag, cid_b)
    in
    [ !SPB($O, key, bn_b, cid_b), In(<c, idx, tag>) ]
  --[ Eq(aead_verify(key, n, aad, c), accept()),
      DecB($O, bn_b, idx, tag) ]->
    [ ]


/* ================= LEMMAS ================= */

// Sanity: encrypt + decrypt a non-final chunk
lemma Stream_Sanity:
    exists-trace
    "Ex O bn idx c #i #j.
        Encrypted(O, bn, idx, nonfinal, c) @i &
        SeqDec(O, bn, idx, nonfinal, c) @j"

// Sanity: encrypt final + reach DecFinalized
lemma Stream_Sanity_Finalize:
    exists-trace
    "Ex O bn idx #i #j.
        EncFinalized(O, bn, idx) @i &
        DecFinalized(O, bn, idx) @j"

// P2 (Integrity): Sequential decryptor accepts only genuine ciphertexts.
// If SeqDec fires at (bn, idx, tag), the encryptor produced a chunk
// at that exact (bn, idx, tag) — or the key was corrupted.
lemma Theorem13_P2_Integrity:
    "All O bn idx tag c #j.
        SeqDec(O, bn, idx, tag, c) @j
    ==>
        (Ex #i. Encrypted(O, bn, idx, tag, c) @i)
        | (Ex key #k. CorruptStream(O, key) @k)
    "

// P3 (Ordering): Implicit in P2 for the symbolic model — the sequential
// decryptor's index is part of the nonce/AAD, so accepting at index j
// requires a ciphertext produced at index j. Stated separately per §9.11(b).
// The adversary captures a chunk encrypted at index i and presents it at
// position j. The nonce/AAD mismatch prevents acceptance.
// P3 (Ordering): The SAME ciphertext c encrypted at index idx1 cannot
// be accepted by the sequential decryptor at a different index idx2.
// The nonce/AAD include the index, so mismatch causes AEAD failure.
lemma Theorem13_P3_Ordering:
    "All O bn idx1 idx2 tag c #i #j.
        Encrypted(O, bn, idx1, tag, c) @i &
        SeqDec(O, bn, idx2, tag, c) @j &
        not (idx1 = idx2)
    ==> (Ex key #k. CorruptStream(O, key) @k)"

// P4 (Truncation Resistance): DecFinalized only reachable via a genuine
// final-chunk ciphertext (tag_byte=final) from the encryptor.
lemma Theorem13_P4_No_False_Final:
    "All O bn idx #j.
        DecFinalized(O, bn, idx) @j
    ==>
        (Ex c #i. Encrypted(O, bn, idx, final, c) @i)
        | (Ex key #k. CorruptStream(O, key) @k)
    "

// P5 (Cross-Stream Isolation): A chunk encrypted on stream A cannot be
// accepted by stream B's decryptor (different base_nonce, same key).
// Covers both sequential (DecB) and random-access (DecB) decryption.
lemma Theorem13_P5_Cross_Stream:
    "All O bn_a bn_b idx tag c #i #j.
        Encrypted(O, bn_a, idx, tag, c) @i &
        DecB(O, bn_b, idx, tag) @j &
        not (bn_a = bn_b)
    ==> (Ex key #k. CorruptStream(O, key) @k)"

// Key secrecy: stream key secret unless directly corrupted
lemma Theorem13_Key_Secrecy:
    "All O key bn cid #i.
        StreamInit(O, key, bn, cid) @i
    ==>
        not (Ex #j. K(key) @j)
        | (Ex #j. CorruptStream(O, key) @j)
    "

end