// SPDX-FileCopyrightText: © 2026 Nadim Kobeissi <nadim@symbolic.software>
// SPDX-License-Identifier: CC-BY-NC-ND-4.0
//
// Expected at 1 session(s): a0; 2 session(s): a1. The second session supplies
// an accepted replay that still reaches the onward send.

attacker[active]

principal Bob[
	knows private psk
	generates m
	e = ENC(psk, m)
	h = MAC(psk, e)
]

Bob -> Alice: e, h

principal Alice[
	knows private psk
	_ = ASSERT(MAC(psk, e), h)?
	m2 = DEC(psk, e)
]

Alice -> Carol: [m2]

principal Carol[
	_ = HASH(m2)
]

queries[
	authentication? Bob -> Alice: e[
		precondition[Alice -> Carol: m2]
	]
]