A Formal Method for the Analysis of the Veteran’s Ebenefits’ Website

Abstract

Currently, the Ebenefits/VA.gov website has login problems. This is a serious situation because it prevents veterans from accessing critical services: applying for medical disabilities; enrolling in health care services; accessing educational benefits; managing current VA benefits; acquiring home and auto loans, life insurance, burial services; and connecting veteran networks for other community resources. When a service member is unable to access this website, they are unable to help themselves. This adds inefficiencies to the overall VA system and could lead to poor veteran integration to civilian life. In this analysis, we used a technology called probabilistic model checking (a formal method for proving properties about stochastic systems) to identify the optimal process for veterans to login to Ebenefits while adhering to safety constraints for protecting veterans’ sensitive information. To perform this analysis, a veteran in our research group documented multiple login attempts to gain realistic probabilities of the system transitioning between different interface states. Probabilistic model checking was used to quantify the probability of successfully getting from initial states to a successful login. In analyzing these results, the probability of a successful login for Ebenefits was found to be 0.25. Reviewing the data produced by the model checker revealed that a particular state called two factor authentication, utilized to verify the veteran’s identity by a password and passcode sent to a technological device in their possession, was a problematic state. Our analyses also showed that one particular path, the Defense Self-Service Logon Path, was the most successful pathway at 0.98. This pathway begins with the user entering their password, verification of this password, followed up with a second authentication which the end user can skip or chose to add to their cellular device prior to allowing them to have a successful login. Based on this path, we found that use of a Common Access Card was most effective for enabling logins. Further work utilizing formal methods for exposing problems in the Ebenefits website will be explored in the full paper.

Keywords: Prism, formal model specifications, Ebenefits

DOI: 10.54941/ahfe1003779