An artificial protocol called the ``ffgg'' protocol is constructed, with an assumed security objective to keep a certain data item secret. A message modification attack is given that exposes the data item; in this attack there are two concurrently-running responder processes belonging to the same agent. To show that a concurrent attack is necessary, we use an inductive approach in the PVS verification environment to prove that the protocol is secure under the assumption that role concurrency is excluded. This is one of a family of protocols conjectured to require an attack with N concurrent responders.