Classic protocol and crypto cleanups.

What is the point of enclosing this in braces ?
I guess it indicates the scope of Proposition S2; but I think that's obvious enough from the comment for proposition S3 on the next non-blank line.
Also: your comments are inconsistent about capitalisation:
* Proposition S2 - Reply ...
* proposition S3 - send