$($d$)$ We modelled the amended protocol by a process System$($t$),$ specified its correctness by a process SPEC,

and checked its correctness by a suitable assertion:

send, receive $|$ USERS

SPEC$=$ know $?$ n : noncesI $$ SPEC

assert SPEC send, receive $|$

In the following, 'explain' means giving an informal explanation showing an understanding of the mod$-$

elling.

$($i$)$ Explain what the process System$($t$)$ means $($describe its components and explain the way they are

connected$).$

$($ii$)$ Explain what the assertion means. Explain all parts of it$,$ in particular, explain the meaning of

$\backslash$ send, receive $|$ and why this part is necessary.

$($iii$)$ Explain which correctness guarantees the successful model checking of this assertion provides for

the protocol.