User Authentication through Keystroke Dynamics by means of Model Checking: A Proposal