attacker[active]

// Úvodná výmena verejných kľúčov (guarded)
// modelovanie znalosti verejných kľúčov
principal Client [
	knows private c
	gc = G^c
]

principal Server [
	knows private s
	gs = G^s
]

Client -> Server: [gc]
Server -> Client: [gs]

// Challenge-Response protokol
principal Client [
	generates nc
]

Client -> Server: nc

principal Server [
	sigs = SIGN(s, nc)
	generates ns
]

Server -> Client: sigs, ns

principal Client [
	validate = SIGNVERIF(gs, nc, sigs)
	sigc = SIGN(c, ns)
]

Client -> Server: sigc

principal Server [
	validate2 = SIGNVERIF(gc, ns, sigc)
]

queries[
	authentication? Client -> Server: sigc
	authentication? Server -> Client: sigs
	freshness? nc
	freshness? ns
]