414-S11-hw4-note

## Re-emphasizing the requirements for hw 4 solution

As stated on hw 4, your solution must meet the requirements of exam 1 and will be graded accordingly. Based on feedback, it is apparent that some of you do not understand what this means. Hence this note.

Consider problem 1 part a, i.e., to show whether or not INV A1 holds, where

A1: hst[j] = [A,p]   ⇒   hst[j-1] = [B,1,p]

### Suppose you want to show that INV A1 does not hold.

Your solution must present an evolution ending in a state that does not satisfy A1, i.e., a state where hst has an entry [A,p] and there is a preceding entry and that entry is not [B,1,p]. Present the evolution by listing a sequence of atomic steps (starting from the initial step); after each step, indicate enough of the state (i.e., values of relevant variables) so that it is easy to check that your evolution is possible.

If the above is not absolutely clear to you, go over the examples of such answers in the posted homework and exam solutions.

### Suppose you want to show that INV A1 holds.

First, identify every atomic step in the program whose execution may falsify A1. In this case, there is only one such step: specifically, step A.2 appending [A,p] to hst. It suffices to prove that just before this happens, the last entry in hst is [B,1,p]. Your proof will be a sequence of sub-proofs; in each sub-proof you conclude something that follows directly from an atomic step of the program and what you have already established. Also, your proof examines the possibilities going backwards in time.

To illustrate, assume that step A.2 appends [A,p] to hst at time t0. Directly from this, all you can conclude is that just before t0, thread A.t is at 2, step A.2 receives [B,A,enc(A.key,[p,nA])] where nA = A.nL. Directly from this, you cannot conclude that [B,1,p] is the last entry in hst, nor can you conclude that [B,A,enc(A.key,[p,nA])] was sent by B (the attacker may have sent it).

Next, consider the entry enc(A.key,[p,nA]) in the message received at t0. You would like to conclude that this entry must have been created by Z. For that, you need to show that A.key is not known to the attacker. So at this point, take a fresh sheet of paper and prove that INV Ψ(A.key) holds. (Note that it is A.key and not key.)

Now let's prove that entry enc(A.key,[p,nA]) in the message received at t0 was generated by Z. We have that step A.2 happened at t0. So the previous step that A did is A.1 at some time t1 prior to t0 (note that this sub-proof takes us backwards in time). At time t1, step A.1 set A.nL to the randomly-obtained quantity nA (otherwise nA = A.nL would not hold at t0). Because nA is random and A does not do anything during [t1,t0], entry enc(A.key,[p,nA]) is generated by Z (because the attacker does not have A.key) at some time t2 inside the duration [t1,t0].

And so on. Ultimately, you want to show that at some time t3 inside duration [t2,t0], step B.2 appends [B,1,p] to hst and hst is unchanged in duration [t3,t0].

Your proof should be such that it can be checked by someone who understands the constructs used in the program but does not have any intuition about the program (e.g., cannot fit the program in his/her head).

If the above is not absolutely clear to you, go over the examples of such answers in the posted homework and exam solutions.

### Suppose you have a preliminary solution to a hw4 problem and want to discuss it with me.

It will cost you 5 points (out of 60) for each discussion. I decide when a discussion ends (and another one starts).

A better alternative is to write down a solution for an equivalent exam or homework problem (without looking at the my posted solution). I'll be happy to evaluate that, and you won't lose any points.

The best alternative is to write down your solution to an equivalent exam or homework problem (without looking at the my posted solution), and then evaluate it yourself. If you can come up with a correct solution in this way, you would have convinced me that you can critically analyze your own writing.