// SPDX-FileCopyrightText: © 2026 Nadim Kobeissi <nadim@symbolic.software>
// SPDX-License-Identifier: CC-BY-NC-ND-4.0
//
// Expected at 1 session(s): a1a0; 2 session(s): a1a1. Unchecked verification
// permits replacement, and a second session permits replay of the independent
// attestation.

attacker[active]

principal Server[
	knows private s
	gs = PUBKEY(s)
]

principal Client[
	knows private c
	gc = PUBKEY(c)
	generates nonce
]

Client -> Server: nonce

principal Server[
	proof = SIGN(s, nonce)
]

Server -> Client: gs, proof

principal Client[
	valid = SIGNVERIF(gs, nonce, proof)
	generates attestation
	signed = SIGN(c, attestation)
]

Client -> Server: [gc], attestation, signed

principal Server[
	storage = SIGNVERIF(gc, attestation, signed)?
]

queries[
	authentication? Server -> Client: proof
	authentication? Client -> Server: signed
]