R. Monroy and M. Carillo (Mexico)
Computer Security, Inductive Approach to Security Proto col Verification, Automated Verification
The inductive approach [1] has been successfully used for verifying a number of security protocols, uncov ering hidden assumptions and even attacks. Yet it requires a high level of skill to use: a user must guide the proof process, selecting the tactic to be applied, inventing a key lemma, etc. Proofs are both onerous and cumbersome. To compound the problem, security guarantees are not built into the logic but proven within it, making it difficult to give an account of proof discovery. We introduce a method, which, given a protocol, automatically formulates most of the properties that the protocol should enjoy in order to en sure security. If proven, these guarantees can be combined to provide a story as to why the protocol achieves security. Otherwise, the unproven goals may be used to uncover hid den assumptions or attacks.
Important Links:
Go Back
