Let us consider a group of agents. They want to design a protocol that is used to check if an agent is the member or not. They have decided to use symmetric cryptsystems such as DES. They share one symmetric key. They have devised the following protocol:

  1. check  P --> Q : R
  2. reply    Q --> P : E(R)
  3. hello     P --> Q : "hello"

1. Agent P wants to know that agnet Q is a member. So, she generates a really fresh random number R and sends it to Q as a check message.
2. On receipt of the check message, Q encrypts the recevied  number with the shared symmetric key and sends the cipher E(R) to P as a reply message.
3. On receipt of the reply message, P decrypts the received cipher with the shared symmetric key and checks if the obtained number matches the random number R. If so, P judges that Q is a member and sends a hello message to Q.

1. Do you think that this protocol works well? If not, explain why not and modify it.
2. Make a formal model of the protocol. Don't forget the intruder. Describe the model in CafeOBJ.
3. Write proof scores in CafeOBJ showing that the protocol works well, namely that if P sends a hello message to Q, then Q is a member.