12, Feb, 2019 11:30-12:30 (1 hour)
CISTER, Porto, Portugal

ABSTRACT:
Cryptographic protocols describe sequences of actions taken by entities to achieve specific goals in a secure way. However, because the design of these protocols is prone to errors, security breaches can be exposed and maliciously exploited. To identify which security properties are guaranteed, and to which attacks the protocol may be exposed, protocols can be submitted to verification techniques that make use of formal methods. Nowadays, formal methods are the basis of many automated tools that have been used in multiple scientific papers that aimed to prove the correctness of cryptographic protocols. ProVerif is one example of automatic cryptographic protocol verifiers. It is based on the formal model (so-called Dolev-Yao model) and can prove the following properties: secrecy (the adversary cannot obtain the secret); authentication and more generally correspondence properties; strong secrecy (the adversary does not see the difference when the value of the secret changes); equivalences between processes that differ only by terms. This talk will then give an overview of how ProVerif works, how one can model security protocols on it, how one should design the verification queries, and also, how to interpret the analysis results.

EVENT  PHOTOS:
At CISTER's Facebook Page / At CISTER's Instagram Page

DOWNLOAD:
Presentation PDF (600KB)
 

CISTER's main roles: