Discuss the Support model, as a framework for protocol modelling for authentication analysis in LySa.

Discuss the requirements put on the exchange in the Support model, run the tool, and discuss the reported error. Give credits to the piecies, while using them (extractor DIPISA, lysatool IMM, and reflector UEDIN): real integration!

Derive in real time a new model (Support1), by relaxing the requirements, and show that no errors remain, and no reflection is offered.

To finish, discuss briefly the protocol used in the case studies, (establish a secure communication between dynamic partners, by exchanging secure certificates) as a useful one also in the Tomcat scenario, and show that the tool is able to capture the errors in the naive exchange (CertificateExchange08) while the sophisticated version with a shared secret (CertificateExchange06) has no errors.

SessionKeyExchange,Table6, and may be WMF stay there in case of questions.

Using Mikael's words the morale is : You can model a protocol; you add some annotation about a security property; you check the property using the tool; sometimes the tool say that the protocol is okay and other times it says that it isn't.