As to dB^2 and dt, the above is correct, but it is important to remember that dt is deterministic and dB is not. The expectation is the limiting form of the problem. Gauss provides a great warning that you can only discuss ill posed problems in their limiting form. Ito's lemma is a method of discussing this ill posed problem by solving the limiting form. I do not know of a proof that shows this limiting form is the unique method to solve this problem. It is possible a different limiting form exists, although I very seriously doubt it unless it arrives at this same place.