An artificial protocol called the "ffgg" protocol is constructed, with a parallel attack exposing a secret data item. It is proved that a parallel attack is necessary, because the protocol is shown to be secure under non-parallel attacks. We use an inductive approach in the PVS verification environment

• ffggpaper.ps