For protocols that perform an authenticated key exchange (AKE) we have models such as the extended Canetti-Krawczyk (eCK) to formally analyze their security. However, there are also protocols that do not perform a key exchange in practice, because they are using pre-shared keys.
What model would make sense to show weaknesses in these types of protocols?
Would it potentially make sense to still use a model like eCK, despite being originally designed for AKE, since it can show the weaknesses in an attack game for such protocols as well? The session just wouldn't require any messages (or just one) to be send by any party.
A simple example for a use case: There is one static key known to all legitimate parties and when they communicate with each other they use this key to encrypt and sign message using authenticated encryption (AE).