That works fine for some crypto algorithms, but as stated in the paper not for everything.

As I understand it, this proof needs to support conditionals for example.