Security protocols are short programs aiming at securing communications overa network. They are widely used in our everyday life. They may achieve var-ious goals depending on the application: confidentiality, authenticity, privacy,anonymity, fairness, etc. Their verification using symbolic models has shown itsinterest for detecting attacks and proving security properties. A famous exampleis the Needham-Schroeder protocol [23] on which G. Lowe discovered a flaw 17years after its publication [20]. Secrecy preservation has been proved to be co-NP-complete for a bounded number of sessions [24], and decidable for an unboundednumber of sessions under some additional restrictions (e.g. [3,12,13,25]). Manytools have also been developed to automatically verify cryptographic protocolslike [8,21].
展开▼
