theory LO_Auth
begin

/* 
 * 1. CRYPTOGRAPHIC PRIMITIVES (Abstracted per §2)
 */

builtins: signing, hashing

// Hybrid KEM (X-Wing) abstraction per §2.1
// We treat it as a single IND-CCA2 KEM.
// kem_decaps recovers the encapsulation randomness r (a subterm of the
// ciphertext), and both sides derive the shared secret via kem_ss(pk, r).
// This formulation is subterm-convergent: the RHS `r` is a subterm of the LHS.
functions: kem_pk/1, kem_c/2, kem_ss/2, kem_decaps/2
equations: kem_decaps(sk, kem_c(kem_pk(sk), r)) = r

// MAC (HMAC-SHA3-256) per §2.3
// Modeled as an opaque function.
functions: mac/2

// Constant-time equality check helper
restriction Eq:
    "All x y #i. Eq(x,y) @i ==> x = y"

/* 
 * 2. ADVERSARY MODEL & PKI (§8.2)
 */

// Generate Identity Keys (IK)
rule Generate_IK:
    [ Fr(~sk_IK) ]
  --[ LtkGen($P, ~sk_IK) ]->[ !Ltk($P, ~sk_IK), !Pk($P, kem_pk(~sk_IK)), Out(kem_pk(~sk_IK)) ]

// Corrupt IK (§8.2: Corrupt(IK, P))
rule Corrupt_IK:[ !Ltk($P, sk_IK) ]
  --[ CorruptIK($P) ]->[ Out(sk_IK) ]

// Corrupt RNG (§8.2: Corrupt(RNG, P, t))
// We model this by allowing the adversary to learn the randomness `~r` used in a specific step.
rule Corrupt_RNG:
    [ !RNG_State($P, ~r) ]
  --[ CorruptRNG($P, ~r) ]->
    [ Out(~r) ]

/* 
 * 3. LO-Auth PROTOCOL (§6)
 */

// Server -> Client: Challenge
rule LO_Auth_Challenge:
    let 
        c = kem_c(pk_IK_client, ~r)
        ss = kem_ss(pk_IK_client, ~r)
        token = mac(ss, 'lo-auth-v1')
    in[ !Pk($Client, pk_IK_client), Fr(~r) ]
  --[ 
      AuthChallenge($Server, $Client, ~r, token)
    ]->[ 
      Out( c ),
      // §8.3: Linear fact to enforce single-use challenge
      AuthPending($Server, $Client, token),
      // Expose RNG state for potential corruption
      !RNG_State($Server, ~r)
    ]

// Client -> Server: Proof Generation
rule LO_Auth_Client_Response:
    let
        r = kem_decaps(sk_IK_client, c)
        ss = kem_ss(kem_pk(sk_IK_client), r)
        proof = mac(ss, 'lo-auth-v1')
    in[ !Ltk($Client, sk_IK_client), In( c ) ]
  --[ 
      AuthResponse($Client, c, proof) 
    ]->
    [ 
      Out( proof ) 
    ]

// Server: Verify
// Consumes AuthPending ensuring the challenge cannot be replayed successfully
rule LO_Auth_Verify_Success:
    [ AuthPending($Server, $Client, token), In( proof ) ]
  --[ 
      Eq(token, proof), // Represents constant-time accept
      AuthAccepted($Server, $Client, token) 
    ]->
    [ ]

// (Optional) Server: Timeout
// §8.3: AuthTimeout consumes the pending state without producing AuthAccepted
rule LO_Auth_Timeout:[ AuthPending($Server, $Client, token) ]
  --[ AuthTimeout($Server, $Client, token) ]->
    [ ]

/*
 * 3b. CCA2 DECAPSULATION ORACLE (§8.3 compositional note)
 *
 * In the composed setting where LO-Auth and LO-KEX share sk_IK[XWing],
 * each LO-Auth session gives the adversary an interactive Decaps oracle:
 * submit arbitrary c, receive MAC(Decaps(sk_IK, c), 'lo-auth-v1').
 * This accounts for the CCA2 queries in Theorem 1's advantage bound.
 */
// kem_decaps returns r (subterm-convergent), then kem_ss(pk, r) gives ss.
rule LO_Auth_Decaps_Oracle:
    let
        r_adv = kem_decaps(sk_IK_client, c_adv)
        ss_adv = kem_ss(kem_pk(sk_IK_client), r_adv)
    in
    [ !Ltk($Client, sk_IK_client), In( c_adv ) ]
  --[ DecapsOracle($Client, c_adv) ]->
    [ Out( mac(ss_adv, 'lo-auth-v1') ) ]


/*
 * 4. LEMMAS (§8.6)
 */

// Sanity: Can the protocol run to completion?
lemma Auth_Exists:
    exists-trace
    "Ex S C token #i. AuthAccepted(S, C, token) @ i"

// Sanity: Challenge temporally precedes acceptance.
lemma Auth_Ordering:
    "All S C r token #chal #verify.
        AuthChallenge(S, C, r, token) @ chal &
        AuthAccepted(S, C, token) @ verify
    ==>
        chal < verify
    "

// §8.3 single-use: AuthPending is linear, so a given token is accepted at most once.
lemma Auth_Single_Use:
    "All S C token #i #j.
        AuthAccepted(S, C, token) @ i &
        AuthAccepted(S, C, token) @ j
    ==>
        #i = #j
    "

// §8.3: If the challenge timed out, acceptance is impossible (AuthPending was consumed).
lemma Auth_No_Accept_After_Timeout:
    "All S C token #t #a.
        AuthTimeout(S, C, token) @ t &
        AuthAccepted(S, C, token) @ a
    ==>
        F
    "

// Each Fr(~r) is unique, so distinct challenges produce distinct tokens.
lemma Auth_Unique_Challenge:
    "All S1 S2 C1 C2 r token1 token2 #i #j.
        AuthChallenge(S1, C1, r, token1) @ i &
        AuthChallenge(S2, C2, r, token2) @ j
    ==>
        #i = #j
    "

// Theorem 6 (LO-Auth Key Possession):
// If the server accepts, then either the adversary corrupted the client's IK,
// corrupted the server's RNG for this challenge, used the Decaps oracle
// (which yields a valid MAC for any ciphertext), or the client responded.
lemma Theorem6_Key_Possession:
    "All S C r token #chal #verify.
        AuthChallenge(S, C, r, token) @ chal &
        AuthAccepted(S, C, token) @ verify
    ==>
        (Ex #j. CorruptIK(C) @ j) |
        (Ex #j. CorruptRNG(S, r) @ j) |
        (Ex c_adv #j. DecapsOracle(C, c_adv) @ j) |
        (Ex c #resp. AuthResponse(C, c, token) @ resp)
    "

// Theorem 6, strengthened: under an honest client, honest RNG, and no
// oracle use, the adversary cannot forge a proof.
lemma Theorem6_No_Oracle:
    "All S C r token #chal #verify.
        AuthChallenge(S, C, r, token) @ chal &
        AuthAccepted(S, C, token) @ verify &
        not (Ex #j. CorruptIK(C) @ j) &
        not (Ex #j. CorruptRNG(S, r) @ j) &
        not (Ex c_adv #j. DecapsOracle(C, c_adv) @ j)
    ==>
        (Ex c #resp. AuthResponse(C, c, token) @ resp)
    "

end