| July 4-5, 2007 Venice, Italy | organised and funded by ARTIST |
| 9h00 | Registration/welcome |
| 9h30 | Automatic Verification of Simulatability in Security Protocols Tadashi Araragi and Olivier Pereira |
| 10h00 | On the Combination of Functionalities for Secure Protocols Kenji Imamoto, Tadashi Araragi and Kouichi Sakurai. |
| 10h30 | break |
| 11h00 | Adaptive Soundness of Static Equivalence Steve Kremer and Laurent Mazaré. |
| 11h30 | Deciding key cycles for security protocols Veronique Cortier and Eugen Zalinescu |
| 12h00 | lunch |
| 14h00 | Crypto-Verifying Protocol Implementations in ML Karthikeyan Bhargavan, Ricardo Corin and Cedric Fournet. |
| 14h39 | Computationally Sound Mechanized Proof of PKINIT for Kerberos Aaron D. Jaggard, Andre Scedrov and Joe-Kai Tsay. |
| 15h30 | break |
| 16h00 | A Formalism for Parallel Key Search Graham Steel and Judicaël Courant. |
| 16h30 | A Cryptographic Model for Branching Time Security Properties the Case of Contract Signing Protocols Veronique Cortier, Ralf Kuesters and Bogdan Warinschi |
| 17h00 | Computational Soundness of Formal Encryption in Coq Ricardo Corin |
(c) Artist Consortium, All Rights Reserved - 2006, 2007, 2008, 2009