B model: Improve provability of session_core

The purpose of this ticket is to improve the proof rate of the B components implementing the core of session management, that is modules whose name starts with session_core and the associated basic machines.