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 A*_{1} holds,
where

*A*_{1}: hst[j] = [A,p] ⇒ hst[j-1] = [B,1,p]

### Suppose you want to show that *INV A*_{1} does not hold.

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

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

And so on.
Ultimately, you want to show that at some time *t*_{3}
inside duration [*t*_{2},*t*_{0}],
step B.2 appends *[B,1,p]* to *hst*
and *hst* is unchanged in duration [*t*_{3},*t*_{0}].

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.