---------------- NO ATTACKER -------------------------


Client: state(idle)^message(request) ->
state(waiting)

state(waiting)^message(response))
-> state(idle)

Server: state(idle)^message(request)
->state(computing)

state(computing)^message(response)
 -> state(idle)

------------------ ATTACKER IS THE NETWORK ------------
MODEL:

Client: state(idle)^message(request)^NOT(knows(request))->
state(waiting)^knows(request)

state(waiting)^message(response))
-> state(idle)

Server: state(idle)^message(request)
->state(computing)

state(computing)^message(response)^NOT(knows(response))
 -> state(idle)^knows(response)
----------------------------------------------------
SUCCESS PROPERTY: knows(request)^knows(response)

------------------ ATTACKER IS THE CLIENT's NIC ------------

Client: state(idle)^message(request)^NOT(knows(request))->
state(waiting)^knows(request)


state(waiting)^message(response))^NOT(knows(response))
-> state(idle)^knows(response)

Server: state(idle)^message(request)
->state(computing)

state(computing)^message(response)
 -> state(idle)