An Automatic Security Verifier based on Horn clauses

The design of cryptographic protocols is difficult and error-prone. This can be illustrated by flaws found inexisting protocols. It is therefore important to have tools to verify the properties of cryptographic protocols.Several techniques can be used to build such tools: theorem proving, model checking, typing and etc. We study a technique based on an abstract representation of the protocol by a set of Horn clauses. This technique yields fully automatic proofs of protocols for an unbounded number of runs.

کلیدواژه ها:

cryptographic protocols ، Horn clauses