The page of my PhD-thesis.

The page of a protocol analyser.

Publications

New Linking Schemes for Digital Time-Stamping (together with Ahto Buldas). In The 1^st International Conference on Information Security and Cryptology, pages 3--14, Seoul, Korea, December 18--19, 1998. © Korea Institute of Information Security and Cryptology.

Accountable Certificate Management using Undeniable Attestations (together with Ahto Buldas and Helger Lipmaa). In 7^th ACM Conference on Computer and Communications Security, pages 9--18, Athens, Greece, November 1--4, 2000. © ACM.

Previous paper is superceded by its journal version Eliminating counterevidence with applications to accountable certificate management (same authors), Journal of Computer Security 10(2002), pages 273--296, IOS Press.

Semantics and Program Analysis of Computationally Secure Information Flow. In Programming Languages and Systems, 10th European Symposium On Programming, ESOP 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genoa, Italy, April 2-6, 2001 Proceedings (LNCS 2028), pages 77-91, 2001. © Springer-Verlag (Slides of the talk)

Analysis for Object Inlining in Java. In JOSES: Java Optimization Strategies for Embedded Systems, Genoa, Italy, April 1, 2001. (Slides of the talk)

Encryption Cycles and Two Views of Cryptography. In NORDSEC 2002 - Proceedings of the 7th Nordic Workshop on Secure IT Systems (Karlstad University Studies 2002:31), pages 85-100, Karlstad, Sweden, November 7-8, 2002. (Slides of the talk)

Pseudorandom permutations and equivalence of formal expressions (abstract). In the 14th Nordic Workshop on Programming Theory, NWPT'02, pages 63-65, Tallinn, Estonia, November 20-22, 2002. (Slides of the talk)

Handling Encryption in an Analysis for Secure Information Flow. In Programming Languages and Systems, 12th European Symposium On Programming, ESOP 2003 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003 Warsaw, Poland, April 7-11, 2003 Proceedings (LNCS 2618), pages 159-173, 2003. © Springer-Verlag (Slides of the talk)

Improving the Gnutella protocol against poisoning (together with Meelis Roos and Jan Willemson). In proceedings of NORDSEC 2003, Gjøvik, Norway, October 15-17, 2003.

Sound Computational Interpretation of Formal Encryption with Composed Keys (together with Ricardo Corin). In Information Security and Cryptology - ICISC 2003, 6th International Conference, Seoul, Korea, November 2003, Revised Papers (LNCS 2971), pages 55-66, 2004. © Springer-Verlag (Slides of the talk)

Symmetric encryption in automatic analyses for confidentiality against active adversaries, in proceedings of 2004 IEEE Symposium on Security and Privacy, pages 71-85, Oakland, CA, May 9-12, 2004. © IEEE. (Slides of the talk (replaced 19.10.2005)). A longer version (with proofs) is also available.

A Type System for Computationally Secure Information Flow (together with Varmo Vene). In proceedings of the 15th International Symposium on Fundamentals of Computation Theory, FCT 2005 (LNCS 3623), August 17-20, 2005, Lübeck, Germany, pages 365-377. © Springer-Verlag

Type Systems Equivalent to Data-Flow Analyses of Imperative Languages (Extended Abstract) (together with Tarmo Uustalu and Varmo Vene). In proceedings of the Third Workshop on Applied Semantics (APPSEM05), Frauenchiemsee, Germany, Septermber 12-15, 2005.

The journal version of this paper appeared in Theoretical Computer Science, volume 364, number 3, pages 292-310, 2006. (© Elsevier Science)

Universally Composable Time-Stamping Schemes with Audit (together with Ahto Buldas, Märt Saarepera and Jan Willemson). In Information Security, 8th International Conference, ISC 2005 (LNCS 3650), Singapore, September 20-23, 2005, pp 359-373. © Springer-Verlag

Digital Signature in Automatic Analyses for Confidentiality against Active Adversaries (together with Ilja Tšahhirov). In proceedings of Nordsec 2005, 10th Nordic Workshop on Secure IT Systems, Tartu, Estonia, October 20-21, 2005, pp 29-41.

Secrecy Types for a Simulatable Cryptographic Library. In proceedings of the 12th ACM Conference on Computer and Communications Security, Alexandria, VA, USA, November 7-11, 2005, pages 26-35. © ACM (Slides of a bit expanded version of the talk given at Estonian Theory Days in Viinistu)

Computationally Sound Secrecy Proofs by Mechanized Flow Analysis (together with Michael Backes). An extended abstract appeared at the proceedings of the 2nd workshop on Formal and Computational Cryptography, pages 1-6, July 9th, 2006, Venice, Italy (slides of the talk) and a fuller paper at the 13th ACM Conference on Computer and Communications Security, Alexandria, VA, USA, October 30th - November 3rd, 2006, pages 370-379. © ACM. The full paper can be accessed here.

Rational Choice of Security Measures via Multi-Parameter Attack Trees (together with Ahto Buldas, Jaan Priisalu, Märt Saarepera and Jan Willemson). In 1st International Workshop on Critical Information Infrastructures Security (CRITIS'06), August 30 - September 2, 2006, Samos Island, Greece. © Springer-Verlag

Application of Dependency Graphs to Security Protocol Analysis (together with Ilja Tšahhirov). In the 3rd Symposium on Trustworthy Global Computing (TGC 2007), November 5th - 6th, 2007, Sophia-Antipolis, France. © Springer-Verlag

On the Computational Soundness of Cryptographically Masked Flows. In the 35th Annual ACM SIGPLAN—SIGACT Symposium on Principles of Programming Languages (POPL), January 10th - 12th, 2008, San Francisco, CA, USA. © ACM

Typing Computationally Secure Information Flow in Jif (together with Liisi Haav). In proceedings of Nordsec 2008, 13th Nordic Workshop on Secure IT Systems, Lyngby, Denmark, October 9-10, 2008.

Threshold Homomorphic Encryption in the Universally Composable Cryptographic Library (together with Long Ngo). In proceedings of ProvSec 2008 (LNCS 5324), the second conference on provable security, Shanghai, China, October 30 - November 1, 2008,, pp. 298 - 312. © Springer-Verlag

Formal Analysis of the Estonian Mobile-ID Protocol (together with Meelis Roos). In proceedings of Nordsec 2009, 14th Nordic Workshop on Secure IT Systems (LNCS 5838), Oslo, Norway, October 15-16, 2009, pp. 271-286. © Springer-Verlag

A user interface for a game-based protocol verification tool (together with Ilja Tšahhirov). In proceedings of the sixth International Workshop on Formal Aspects in Security and Trust (FAST2009), Eindhoven, Netherlands, November 5-6, 2009. © Springer-Verlag

On the (Im)possibility of Perennial Message Recognition Protocols without Public-Key Cryptography (together with Madeline González Muñiz). In proceedings of the 26th ACM Symposium on Applied Computing, Taichung, Taiwan, March 21-24, 2011. © ACM. See also the full paper.

Implementing Cryptographic Primitives in the Symbolic Model. In proceedings of the 3rd NASA Formal Methods Symposium, Pasadena, CA, USA, April 18-20, 2011. © Springer-Verlag.

Formal Security analysis of OpenID with GBA protocol (together with Abu Shohel Ahmed). In proceedings of the 3rd International ICST Conference on Security and Privacy in Mobile Information and Communication Systems, Aalborg, Denmark, May 17-19, 2011. © Springer-Verlag

Secure Mobile Access to Homecare Patients‘ Data (together with Sven Heiberg, Sigurður Másson and Claus Popp Larsen). In proceedings of ICEGOV 2011, Tallinn, Estonia, September 26-28, 2011. © ACM.

The Application of I-voting for Estonian Parliamentary Elections of 2011 (together with Sven Heiberg and Jan Willemson). In proceedings of VoteID 2011, Tallinn, Estonia, September 29-30, 2011. © Springer-Verlag.

Securing the Future — an Information Flow Analysis of a Distributed OO Language (together with Martin Pettai). In proceedings of SOFSEM 2012, Špindlerův Mlýn, Czech Republic, January 21-27, 2012. © Springer-Verlag. The full version is also available.

Unrefereed publications

Osaliselt tsüklilise monoidi Möbiuse funktsioonist (On the Möbius function of the partially cyclic monoid). BSc thesis, Tartu University, 1997. (In Estonian with English resume)

Üldistatud kontekstivabad grammatikad (Generalised context-free grammars). MSc thesis, Tartu University, 1998. (In Estonian with English resume. The same material is covered in the following two technical reports.)

Automata accepting coupled-context-free languages. Research report CS102/99 of the Software Department of the Institute of Cybernetics of Tallinn Technical University, 1999.

Ogden's lemma for coupled-context-free languages; the set of Lyndon words is not coupled-context-free. Research report CS103/99 of the Software Department of the Institute of Cybernetics of Tallinn Technical University, 1999.

Relative Secrecy and Semantics of Declassification. Research report IT-AR-O-029-040227 of Cybernetica AS, 2004.

A Type System for Computationally Secure Information Flow (together with Varmo Vene). Research report IT-LU-O-043-050307 of Cybernetica AS, 2005.

Slides of some talks

• Slides for a talk given somewhere during the summer term of 2000 at the seminar of the Cryptography and Security group at the University of Saarland.
• Slides (pdf,ps.gz) for my talk at the Dagstuhl-Seminar Effective Implementation of Object-Oriented Programming Languages.
• Slides for my talk at the Dagstuhl-Seminar Security through Analysis and Verification.
• Slides for my talk at the Dagstuhl-Seminar Specification and Analysis of Secure Cryptographic Protocols.
• Kiled ettekandele Küberneetika Instituudi formaalmeetodite mitteformaalseminaris 13. mail 2002.
• Slides for my talk on analysis of cryptographic protocols at CS theory days in Arula, February 4th, 2003.
  • Täiendused neile nädal hiljem Cybernetica Tartu laboris peetud ettekande jaoks.
• Slides for my talk on computationally secure information flow at Helsinki University of Technology, May 27th, 2003.
• Slides for my talk on logics for non-repudiation at the CS theory days in Pedase, October 3rd, 2003.
• Slides for my talk at the Dagstuhl-Seminar Language-Based Security, October 5th - 10th, 2003.
• Kiled Universal composability-t tutvustanud ettekandele Cybernetica AS teadusseminaris 3. juunil 2004.
• Slides for my talk on universally composable time-stamping at the CS theory days in Veskisilla, October 2nd, 2004.
  • Kiled enam-vähem sama sisuga ettekandele seminaril Formaalsed meetodid tarkvara- ja süsteemitehnikas Pedasel, 16. oktoober 2004.
• Slides for my talk on type systems for computationally secure information flow at the CS theory days in Koke, February 6th, 2005.
• Slides for my introductory talk on language-based secure information flow at the CS theory days in Koke, February 5th, 2006.
• Slides for my talk on dependency-graph-based protocol analysis at the CS theory days in Rõuge, January 28th, 2007, as well as at the Dagstuhl-Seminar 07091 on Mobility, Ubiquity and Security.
• Slides for a talk on the computational soundness of cryptographically masked flows at the Declassification Workshop of the MOBIUS-project meeting, June 5th-7th 2007, Dublin, Ireland.
• Slides for a tutorial talk at the Estonian Theory Days in Põlva, January 25th-27th, 2008 (only the first half was presented).
• Slides for a talk on modeling the Laud-Vene type system for computationally secure information flow inside Jif, given at the Declassification Workshop of the MOBIUS-project meeting, June 18th, Munich, Germany.
• Slides for the talk on the encryption cycles in the Abadi-Rogaway soundness theorem, given at CRYPTO 2008 rump session.