(* QNSQY billing: PQC envelope + ML-DSA-44 subscription token.
   Abstractions: ML-KEM-1024+X25519+AES-256-GCM envelope == probabilistic public-key encryption (aenc/adec);
                 ML-DSA-44 subscription-token signature == sign/checksign.
   Properties:
     Q1  secrecy of the client's API key sent inside the envelope (vs a network/Dolev-Yao attacker)
     Q2  subscription-token UNFORGEABILITY: client accepts a tier-claim only if the server issued it. *)

free net: channel.

type skey.  type pkey.   (* envelope KEM keypair  *)
type sskey. type spkey.  (* token signing keypair *)

fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.
reduc forall m: bitstring, k: skey; adec(aenc(m, pk(k)), k) = m.

fun spk(sskey): spkey.
fun sign(bitstring, sskey): bitstring.
reduc forall m: bitstring, k: sskey; checksign(sign(m, k), spk(k)) = m.

free apikey: bitstring [private].
free tierPro: bitstring.

event TokenIssued(bitstring).
event TokenAccepted(bitstring).

query attacker(apikey).
query t: bitstring; event(TokenAccepted(t)) ==> event(TokenIssued(t)).

let client(pkS: pkey, vk: spkey) =
  out(net, aenc((apikey, tierPro), pkS));
  in(net, sig: bitstring);
  let claim = checksign(sig, vk) in
  event TokenAccepted(claim).

let server(skS: skey, skSign: sskey) =
  in(net, env: bitstring);
  let (ak: bitstring, req: bitstring) = adec(env, skS) in
  event TokenIssued(req);
  out(net, sign(req, skSign)).

process
  new skS: skey;
  new skSign: sskey;
  out(net, pk(skS));
  out(net, spk(skSign));
  ( (! client(pk(skS), spk(skSign))) | (! server(skS, skSign)) )