I see often in literature related to cryptographic protocols that MACs (Message Authentication Codes) are not included in protocol definitions.
For example:
A -> S: {TA, B}KAS
S -> A: {TS, KAB, B}KAS
S -> B: {T'S, KAB, A}KBS
Shouldn't it be defined as follows ? (Encrypt-then-MAC + using second key for MACs)
A -> S: {TA, B}KAS, [{TA, B}KAS]KAS'
S -> A: {TS, KAB, B}KAS, [{TS, KAB, B}KAS]KAS'
S -> B: {T'S, KAB, A}KBS, [{T'S, KAB, A}KBS]KBS'
Isn't integrity a concern, or do protocol analysts generally assume that cipher-text cannot be modified at this level of protocol abstraction? Do you exclude ciphertext-only attacks?