BCM Seminar: A Short Introduction to Two Approaches in Formal Verification of Security Protocols: Model Checking and Theorem Proving

Mohsen Pourpouneh, postdoc, Department of Food and Resource Economics, will give a seminar titled 'A Short Introduction to Two Approaches in Formal Verification of Security Protocols: Model Checking and Theorem Proving'.

Abstract

In this talk, we shortly review two formal approaches in verification of security protocols; model checking and theorem proving. Model checking is based on studying the behavior of protocols via generating all different behaviors of a protocol and checking whether the desired goals are satisfied in all instances or not. Theorem proving is based on deriving the desired goals from assumption of protocols via a deduction system. We define a deduction system named Simple Logic for Authentication to formally define the notion of authenticated communication based on the structure of the messages.

Access the BCM website here

Practicalities

The seminar is open to all. You are welcome to bring your lunch.
There is limited seating.

Accessability

There are stairs by the entrance which limits access for wheel chair users.
We are able to provide a ramp or assistance.
Please contact us if you have any questions regarding access.