The Network then aswers to the Phone and the Application the keys and the time to live and the hashed value of that using a hash function named ``Mac''.
The Phone and the Application verify the Mac and then the phone sends a nonce to the phone and the phone answers back with a new nonce and the original nonce.
The Mac was modeled as a hashing function then encryption this was done this way because scyther does not have a way of creating a mac function with keys so the hashing is done first followed by the encrypted so that an attacker can not modify it.
There are 9 overall claims, where only three do not fail. The secrecy of SesK from the perspective of the Network. And agreement over the SesK and the time to live between the Phone and the Network, and the Application and the Network.
The file ag01598\_6644818\_1\_3.spdl contains the fixed version of $\text{protocol}\Pi$
The first change was to require the refresh keys request was to require the application to send a nounce, this nonce is then sent back to application to verify that the key was generated, was requested to the application and not by the attacker.
The second change was to make the network send the identity of the other party to party that is reciving the message. i.e. Sending the identity of the Phone to the Application encrypted with the key Network,Application. This is done to guarantee that the Party reciving the communication is using a key that was intended for this communication.