Secrecy by Witness-Functions on Increasing Protocols
This addresses the need for formal verification of secrecy in cryptographic protocols, but it appears incremental as it builds on existing static analysis methods.
The authors tackled the problem of statically analyzing cryptographic protocols for secrecy by ensuring security levels of components do not decrease, and they applied this method to an amended Woo-Lam protocol to verify it keeps secret inputs.
In this paper, we present a new formal method to analyze cryptographic protocols statically for the property of secrecy. It consists in inspecting the level of security of every component in the protocol and making sure that it does not diminish during its life cycle. If yes, it concludes that the protocol keeps its secret inputs. We analyze in this paper an amended version of the Woo-Lam protocol using this new method.