Network and security protocols occasionally require important but difficult to authenticate parameters such as the number in a communication party. The existing formal proofs of algorithms for verifying the required parameters in protocols by humans are cumbersome. How should a reliable system be designed for the automatic validation of the various parameters in cache coherence, security, network, wireless, and other open systems interconnection layers protocols? Li et al. present a generic method for validating the parameters in protocols that facilitate interoperability and communications by users with different devices and software. The approach initially determines the supplementary invariables, their dependence graph associations and rules from inconsequential occurrences of a protocol, prior to automatically generalizing and sending the parameters to a theorem authenticator called Isabelle.
展开▼
