Re-emphasizing the requirements for hw 4 solution

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

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

Suppose you want to show that INV A₁ does not hold.

Your solution must present an evolution ending in a state that does not satisfy A₁, 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 A₁ holds.

First, identify every atomic step in the program whose execution may falsify A₁. 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 t₀. Directly from this, all you can conclude is that just before t₀, 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 t₀. 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 t₀ was generated by Z. We have that step A.2 happened at t₀. So the previous step that A did is A.1 at some time t₁ prior to t₀ (note that this sub-proof takes us backwards in time). At time t₁, step A.1 set A.nL to the randomly-obtained quantity nA (otherwise nA = A.nL would not hold at t₀). Because nA is random and A does not do anything during [t₁,t₀], entry enc(A.key,[p,nA]) is generated by Z (because the attacker does not have A.key) at some time t₂ inside the duration [t₁,t₀].

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

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.

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.