Security protocols are a prime example of seemingly simple algorithms for which it would be highly desirable, and possibly feasible, to provide formal proofs of their security. Yet despite several decades of active research, this goal has remained elusive. In this talk we will revisit the security protocol problem, why it is so crucial, and how forms of automated reasoning have helped advance the state of the art, using the TLS 1.3 protocol as an example . We highlight some of the many open general questions and how future advancements in automated reasoning might help towards the ultimate goal of deploying provably secure protocols.