Prevent integer overflows in sessions

[treiher]

Context and Problem Statement

Integer overflows can occur in various scenarios:

• Additions/multiplications using global variable in multiple states (e.g., incrementing sequence number for each message)
• Additions/multiplications between externally provided values

Potential integer overflows must be detected during session verification. It must be ensured that the code generation can be realized in a way, so that all range checks can be proved.

This is a subproblem of #691.