Publications

• A comparison of time-memory trade-off attacks on stream ciphers
  Fabian van den Broek and Erik Poll,
  AfricaCrypt, LNCS, Springer, 2013. To appear.
• Formal models of bank cards for free
  Fides Aarts, Erik Poll, and Joeri de Ruiter,
  SECTEST 2013, IEEE, 2013.
• The Radboud Reader: a minimal trusted smartcard reader for securing online transactions
  Erik Poll and Joeri de Ruiter
  Third IFIP WG 11.6 Working Conference, IDMAN 2013. IFIP Advances in Information and Communication Technology, Volume 396, p. 107-120, Springer, 2013
• Designed to fail: a USB-connected reader for online banking      [press announcement (in Dutch)]
  Arjan Blom, Gerhard de Koning Gans, Erik Poll, Joeri de Ruiter and Roel Verdult.
  NordSec 2012, LNCS volume 7616, pp 1-16, 2012.
• Formal analysis of the EMV protocol suite  [F# sources for EMV]
  Joeri de Ruiter and Erik Poll
  Theory of Security and Applications (TOSCA 2011), LNCS volume 6993, pp. 113-129, 2012.
• Lecture Notes on Language-Based Security
  Manuscript, 2011.
• Rigorous specifications of the SSH Transport Layer
  Erik Poll and Aleksy Schubert, 2011.
  Technical Report ICIS-R11004, Radboud University Nijmegen, 2011.
• Biometrics and Smart Cards in Identity Management
  Bart Jacobs and Erik Poll
  In `Innovating Government. Normative, policy and technological dimensions of modern government', S. van der Hof and M. M. Groothuis (eds), pages 419-439, T.M.C. Asser Press/Springer, 2011.
• Midlet Navigation Graphs in JML
  Wojciech Mostowski and Erik Poll
  13th Brazilian Symposium on Formal Methods (SBMF 2010), LNCS volume 6527, pp. 17-32, 2010.
• Electronic Passports in a Nutshell
  Wojciech Mostowski and Erik Poll
  Technical Report ICIS-R10004, Radboud University Nijmegen, the Netherlands, 2010.
• Teaching program specification and verification using JML and ESC/Java2
  Erik Poll
  Teaching Formal Methods (TFM 2009), LNCS volume 5846, pp. 92-104, 2009
• Model-Based Testing of Electronic Passports
  Wojciech Mostowski, Erik Poll, Julien Schmaltz, Jan Tretmans en Ronny Wichers Schreur
  FMICS 2009, LNCS volume 5825, pp. 207-209, Springer, 2009
• Type-based Object Immutability with Flexible Initialization
  Christian Haack and Erik Poll
  ECOOP 2009, LNCS volume 5653, pp. 520-545, Springer, 2009
  A longer version of the paper is available as Technical report ICIS-R09001, Radboud University Nijmegen, Jan. 2009
• Explicit information flow properties in JML
  Christian Haack, Erik Poll, and Aleksy Schubert
  WISSEC 2008
• Malicious Code on Java Card Smartcards: Attacks and Countermeasures
  Wojciech Mostowski and Erik Poll
  CARDIS 2008, LNCS volume 5189, pp. 1-16, Springer, 2008
• Multi-level security, 3 1/2 decades later
  Erik Muller, Tim Grant and Erik Poll
  13th International Command and Control Research and Technology Symposium (ICCRTS'08), Bellevue, Washington, USA, 2008
• Fingerprinting Passports
  Henning Richter, Wojciech Mostowski, and Erik Poll
  NLUUG 2008 Spring Conference on Security, pp. 21-30, 2008
• BML Reference Manual
  Jacek Chrzaszcz, Marieke Huisman, Aleksy Schubert, Joe Kiniry, Mariela Pavlova and Erik Poll
  In progress. Available online
• Testing the Java Card Applet Firewall [Erratum] [Associated software for these tests]
  Wojciech Mostowski and Erik Poll
  Technical Report ICIS-R07029, Radboud University Nijmegen, the Netherlands, December 2007
  
• AHA: Amortized Heap Space Usage Analysis
  Marko van Eekelen, Olha Shkaravska, Ron van Kesteren, Bart Jacobs, Erik Poll and Sjaak Smetsers.
  In: M. Morazán and H. Nillsson (eds). Trends in Functional Programming volume 8 (Selected Papers of the Eighth Symposium on Trends in Functional Programming, TFP 2007), 2008. pp. 36-53.
• Computer security through correctness and transparancy
  Hans Meijer, Jaap-Henk Hoepman, Bart Jacobs, and Erik Poll
  In: K. de Leeuw, J. Bergstra (eds.), The History of Information Security, pp. 637-653 , Elsevier, 2007
• A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java
  Gary T. Leavens, Joseph R. Kiniry, and Erik Poll
  CAV'07, LNCS volume 4590, pp. 37, Springer, 2007.
• Verifying an implementation of SSH
  Erik Poll and Aleksy Schubert
  WITS'07, pp. 164-177, 2007 [Figure 2 corrected since publication in WITS'07]
• Immutable Objects for a Java-like Language
  Christian Haack, Erik Poll, Jan Schäfer, and Aleksy Schubert
  ESOP'07, LNCS volume 4421, pp. 347-362, Springer, 2007
  • Extended version with additional examples and proofs, Technical report, ICIS-R07009, Radboud University Nijmegen, 2007
  • Earlier `informal' version discussing motivation: Immutable Objects in Java, Technical report, ICIS-R06010, Radboud University Nijmegen, 2006
• A Comparison of Java Cards: State-of-Affairs 2006
  Wojciech Mostowski, Jing Pan, Srikanth Akkiraju, Erik de Vink, Erik Poll, and Jerry den Hartog
  CS-Report CSR 07-06, TU Eindhoven, 2007.
• Mobius: Mobility, ubiquity, security
  G. Barthe, L. Beringer, P. Crégut, B. Gregoire, M. Hoffman, P. Müller, E. Poll, G. Puebla, I. Stark, and E. Vétillard. In Trustworthy Global Computing (TGC'06), LNCS volume 4661, pp 10-29, Springer, 2007
• Tearing Java Cards
  Engelbert Hubbers, Wojciech Mostowski, and Erik Poll
  e-Smart 2006
• JML Reference Manual [HTML] [PDF]
  Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin
  In progress, 2002-...
• Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2
  Patrice Chalin, Joe Kiniry, Gary Leavens, and Erik Poll
  FMCO'05, LNCS volume 4111, pp. 342-363, Springer, 2005
• An overview of JML tools and applications
  Lilian Burdy, Yoonsik Cheon, David Cok, Michael Ernst, Joe Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll
  STTT, volume 7, Number 3, pp. 212-232, Springer, 2005 Available at www.springerlink.com
• Transactions and non-atomic API methods in Java Card: specification ambiguity and strange implementation behaviours
  Engelbert Hubbers and Erik Poll
  Technical Report NIII-R0438, Radboud University Nijmegen, 2004
  
• Reasoning about Card Tears and Transactions in Java Card
  Engelbert Hubbers and Erik Poll
  FASE'04, pp. 114 - 128, LNCS volume 2984, Springer, 2004.
• Java Program Verification at Nijmegen: Developments and Perspective
  Bart Jacobs and Erik Poll
  Software Security - Theories and Systems (ISSS'03), pp. 134-153, LNCS volume 3233, Springer, 2004.
• Formal Techniques for Java-Like Programs
  Susan Eisenbach, Gary T. Leavens, Peter Müller, Arnd Poetzsch-Heffter, and Erik Poll
  ECOOP 2003 Workshop Reader, LNCS volume 3013, pp. 62-71, 2004
• Coalgebras and Monads in the Semantics of Java
  Bart Jacobs and Erik Poll
  Theoretical Computer Science, volume 291, Issue 3, pp. 329-349, Elsevier, 2003
• Implementing a Formally Verifiable Security Protocol in Java Card
  Engelbert Hubbers, Martijn Oostdijk, and Erik Poll
  SPC'03, First International Conference on Security in Pervasive Computing, Boppard, Germany, 2003
• Verifying JML specifications with model fields
  Cees-Bart Breunesse and Erik Poll
  ECOOP workshop on Formal Techniques for Java-like Programs (FTfJP'03), Darmstadt, July 2003
• An overview of JML tools and applications
  Lilian Burdy, Yoonsik Cheon, David Cok, Michael Ernst, Joe Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll
  FMICS'03, volume 80 of ENTCS, Elsevier, 2003
  
• From Finite State Machines to Provably Correct JavaCard Applets
  Engelbert Hubbers, Martijn Oostdijk, and Erik Poll
  Workshop of IFIP WG 11.2 - Small Systems Security, SEC'03, Athens, May 2003
• Opportunities and challenges for formal specification of Java programs
  Joseph Kiniry and Erik Poll
  Position paper, Trusted Components Workshop, Prato, Italy, January 2003
• Static Analysis for JML's assignable Clauses
  Fausto Spoto and Erik Poll
  FOOL 10 (International Workshop on Foundations of Object-Oriented Languages), New Orleans, January 2003
  
• A Java Reference Model of Transacted Memory for Smart Cards
  Erik Poll, Pieter Hartel, and Eduard de Jong
  Fifth Smart Card Research and Advanced Application Conference (CARDIS'02), pp. 75-86, USENIX, 2002
• Formal specifications for the Java Card API 2.1.1
  written in the specification language JML
• Formal Techniques for Java-Like Programs
  Sophia Drossopoulou, Susan Eisenbach, Gary T. Leavens, Arnd Poetzsch-Heffter, and Erik Poll
  ECOOP 2002 Workshop Reader, LNCS volume 2548, pp. 203-210, 2002
• Towards a full formal specification of the Java Card API
  Hans Meijer and Erik Poll
  Smart Card Programming and Security, LNCS volume 2140, pp. 165-178, Springer, 2001
  
• Formal Specification and Verification of JavaCard's Application Identifier Class
  Joachim van den Berg, Bart Jacobs, and Erik Poll
  Java on Smart Cards: Programming and Security, LNCS volume 2041, pp. 137-150, Springer, 2001
  
• A Coalgebraic Semantics of Subtyping
  Erik Poll
  Theoretical Informatics and Applications, volume 35(1), pp. 61-82, 2001
  
• Formal Specification of the JavaCard API in JML: the APDU class
  Erik Poll, Joachim van den Berg, Bart Jacobs
  Computer Networks, volume 36, Issue 4, pp. 407-421, Elsevier Science, 2001.
  
• On the Role of Invariants in Reasoning about Object-Oriented Languages
  Joachim van den Berg, Cees-Bart Breunesse, Bart Jacobs, Erik Poll
  ECOOP workshop on Formal Techniques for Java Programs (FTfJP'01), Budapest, June 2001
• From Algebras and Coalgebras to Dialgebras
  Erik Poll and Jan Zwanenburg
  Coalgebraic Methods in Computer Science (CMCS'01), volume 44 of ENTCS, Elsevier, 2001
  
• Formal Techniques for Java-Like Programs
  Sophia Drossopoulou, Susan Eisenbach, Gary T. Leavens, Arnd Poetzsch-Heffter, and Erik Poll
  ECOOP 2001 Workshop Reader, LNCS volume 2323, pp. 30-40, 2001
• VerifiCard: A European Project for Smart Card Verification.
  Bart Jacobs, Hans Meijer, and Erik Poll
  In: Newsletter 5 of the Dutch Association for Theoretical Computer Science (NVTI), 2001
  
• A Logic for the Java Modeling Language JML
  Bart Jacobs and Erik Poll
  FASE'01, LNCS volume 2029, pp. 284-299, Springer, 2001
  
• JML: notations and tools supporting detailed design in Java
  Gary T. Leavens, K. Rustan M. Leino, Erik Poll, Clyde Ruby, and Bart Jacobs
  OOPSLA 2000 Companion, Minneapolis, USA, October 2000
  
• Specification of the JavaCard API in JML
  Erik Poll, Joachim van den Berg, Bart Jacobs
  Fourth Smart Card Research and Advanced Application IFIP Conference (CARDIS'2000), 2000
  
• First steps in formalising JML
  Joachim van den Berg, Bart Jacobs, and Erik Poll
  ECOOP workshop on Formal Techniques for Java Programs (FTfJP'2000), Sophia Antipolis, France, 2000
  
• A Monad for Basic Java Semantics
  Bart Jacobs and Erik Poll
  Algebraic Methodology and Software Technology (AMAST'2000), LNCS volume 1816, pp. 150-164, Springer, 2000
  
• A Coalgebraic Semantics of Subtyping
  Erik Poll
  Coalgebraic Methods in Computer Science (CMCS'2000), volume 33 of ENTCS, Elsevier, 2000
  
• Integrating Computer Algebra and Reasoning through the Type System of Aldor
  Erik Poll and Simon Thompson
  Frontiers of Combining Systems (FroCoS'2000), LNCS volume 1794, pp. 136-150, Springer, 2000
  
• A Type-Theoretic Memory Model for Verification of Sequential Java Programs
  Joachim van den Berg, Marieke Huisman, Bart Jacobs, and Erik Poll
  14th International Workshop on Algebraic Development Techniques (WADT'99), LNCS volume 1827, Springer, 2000.
  
• Safe Proof Checking in Type Theory with Y
  Herman Geuvers, Erik Poll, and Jan Zwanenburg
  Computer Science Logic (CSL'99), LNCS volume 1683, pp. 439-452, Springer, 1999
  
• The Type System of Aldor
  Erik Poll and Simon Thompson
  Technical Report 11-99 University of Kent at Canterbury, 1999.
  Also as Technical Report CSI-R9928, University of Nijmegen, 1999
  
• Book review of "Algebra of Programming" by Richard Bird and Oege de Moor
  Erik Poll and Simon Thompson
  Journal of Functional Programming, volume 9, issue 3, pp. 347-354, May 1999. © Cambridge University Press
  
• A Logic for Abstract Data Types as Existential Types
  Erik Poll and Jan Zwanenburg
  Typed Lambda Calculus and Applications (TLCA'99), LNCS volume 1581, pp. 310-324, Springer, 1999
  
• Adding the axioms to Axiom: Towards a system of automated reasoning in Aldor
  Erik Poll and Simon Thompson
  Calculemus and Types'98, Eindhoven, the Netherlands
  Also as Technical Report 6-98, University of Kent at Canterbury, 1998.
  
• Behavioural Subtyping for a Type-Theoretic Model of Objects
  Erik Poll
  FOOL5: Fifth International Workshop on Foundations of Object-Oriented Languages, San Diego, USA, 1998
  
• Expansion Postponement for Normalising Pure Type Systems
  Erik Poll
  Journal of Functional Programming, volume 8, issue 1, pp. 89-98, 1998
  
• Subtyping and Inheritance for Categorical Datatypes
  Erik Poll
  Theories of Types and Proofs (TTP-Kyoto), RIMS Lecture Notes 1023, pp. 112-125, Kyoto University Research Insitute for Mathematical Sciences, 1997
  
• Subtyping and Inheritance for Inductive Types
  Erik Poll
  TYPES'97 Workshop on Subtyping, inheritance and modular development of proofs, Durham, UK, 1997
  
• System F with width-subtyping and record updating
  Erik Poll
  Theoretical Aspects of Computer Software (TACS'97), LNCS volume 1281, pp. 439-457, Springer, 1997
  
• Pure Type Systems with Definitions
  Paula Severi and Erik Poll
  Logical Foundations of Computing Science (LFCS'94), number 813 in LNCS, pp. 316-328. Springer, 1994