First Project

Deadline

The Alloy Model to the second project is due on the 8th of November, 2019, 20:00. 

FAQ

I was checking an assertion and got a counterexample. I fixed it by adding a fact that states exactly the same thing as the assertion. Did I do it right?

NO. This is not the way one should fix the counterexamples. 

Whenever one writes an assertion, one want the stated property to be true. However, it should be true because our system is well-developed. Solving it by adding a fact would mean that the property holds because we don't allow any model that falsifies it. Now, sometimes we might need to add facts otherwise the properties would not follow. This should however be done very conservatively, and to the least extent necessary.

Do honest agents share symmetric encryption keys with the intruder?

Yes. The intruder is an agent and each pair of agents shares a symmetric encryption key.

Regarding requirement 8 of the project: "The intruder can encrypt and decrypt, if he knows the corresponding encryption key." Should we model encryption and decryption explicitly?

No, encryption and decryption are implicit. Consider, for instance, operation
  msg2IntruderToHonest(a,b,n,m),
where a is the recipient; n is a nonce; m consists of the identity of an agent, a nonce and a key. The pre-conditions of this operation should say that the operation can happen if

• the Intruder knows n,
• the Intruder knows m (m has been transmitted earlier) or he knows the encryption key and the nonce, and
• m is what a expects it to be.