* Fix errors in abstract noticed by Vicky.
* Fix `ackonowledgements', noticed by Nicko.
* Improve notation in prop:rog-and-lor
* Remove redundant IV-prediction algorithm from mode definition.
* Fix statement of prop:enc-info-to-real.
* Expand and fix proof of prop:enc-hybrid.
* Fix IV notation in CBC proof (v_0 -> V_0).
* Expand note on IV-stealing.
* Expand and explain material on sliding strings.