[neonate]

> In the process, we find new attacks on DRKey and SOAP's WS-Security, both protocols which were previously proven secure in traditional symbolic models.

Does that mean the previous proofs were wrong? or that they proved a narrower version of "secure" that didn't include those particular attacks?

[galadran]

The latter. The tools in question (Tamarin and ProVerif) use a model of signatures that goes back to 2000/2001 which is around when these key substitution properties were discovered. Consequently, they were missed from the models and because the properties themselves aren't that well known, it took a while before it was noticed.