(* QNSQY multi-recipient: one DEK wrapped per recipient under their KEM public key,
   payload encrypted once under the DEK (AEAD).
   Abstractions: per-recipient KEM wrap == public-key encryption; AEAD == senc/sdec.
   Properties:
     Q1  an OUTSIDER (holds all public keys + all wraps + ciphertext, but NO recipient private key)
         cannot recover the DEK.
     Q2  ... nor the plaintext payload.
   Design note (not a flaw): the DEK is intentionally shared across slots, so any legitimate
   recipient learns the DEK by design; the property proved is outsider-secrecy. *)

free net: channel.
type skey. type pkey.
fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.
reduc forall m: bitstring, k: skey; adec(aenc(m, pk(k)), k) = m.
fun senc(bitstring, bitstring): bitstring.
reduc forall m: bitstring, k: bitstring; sdec(senc(m, k), k) = m.

free dek: bitstring [private].
free payload: bitstring [private].

query attacker(dek).
query attacker(payload).

let sender(pkR1: pkey, pkR2: pkey, pkR3: pkey) =
  out(net, aenc(dek, pkR1));
  out(net, aenc(dek, pkR2));
  out(net, aenc(dek, pkR3));
  out(net, senc(payload, dek)).

process
  new skR1: skey; new skR2: skey; new skR3: skey;
  out(net, pk(skR1)); out(net, pk(skR2)); out(net, pk(skR3));
  ( ! sender(pk(skR1), pk(skR2), pk(skR3)) )