Publications
Data Processing Diagrams: A Modeling Technique for Privacy in Complex Data Processing Systems Stateful Fuzzing of OPC UA On the (in)efficiency of fuzzing network
protocols Open Access journal version
Uses of Active and Passive Learning in Stateful Fuzzing Fuzzers for Stateful Systems: Survey and Research Directions arXiv:2301.02490 .
Green-Fuzz: Efficient Fuzzing for Network Protocol Implementations Secure Input Handling Evaluating the Fork-Awareness of Coverage-Guided Fuzzers Language-Based Security Security of EV-charging protocols Deep Repulsive Prototypes for Adversarial Robustness Compromised through Compression: Privacy Implications of Smart Meter Traffic Analysis Blockchain Adoption Drivers: The Rationality of Irrational Choices DOI link
Towards Using Probabilistic Models to Design Software Systems with Inherent Uncertainty Adversarial Examples on Object Recognition: A Comprehensive Survey DOI link
Learning to Learn from Mistakes: Robust Optimization for Adversarial Noise Drivers and Impediments: Experts Opinions on Blockchain Adoption in the Netherlands DOI link
Formal Methods for Security Functionality and for Secure
Functionality Formal Methods for Security? Non-Repudiation and End-to-End Security for EV-charging DOI link
Smart metering in the Netherlands: what, how and why DOI link
Adversarial Examples - A Complete Characterisation of the Phenomenon Supervised Learning for State-Sponsored Malware Attribution Assessing Interoperability Solutions for Distributed Ledgers Strings considered harmful (Some) security by construction
through a LangSec approach A security analysis of the ETSI ITS vehicular communications What Blockchain Alternative Do You Need? Is Java Card ready for hash-based signatures? LangSec revisited: input security flaws of the second kind A standard driven functional software architecture for fully autonomous vehicles Privacy by Design for Local Energy Communities Tactical Safety Reasoning. A Case for Autonomous Vehicles Inferring OpenVPN State Machines Using Protocol State Fuzzing The Drivers behind Blockchain Adoption: The Rationality of Irrational Choices Model Learning and Model Checking of SSH
Implementations the inferred models for OpenSSH, DropBear and BitVise and
the source code
Analysing and Improving
Security Code Reviews Logical Attacks on Secured Containers of the
Java Card Platform EMV in a nutshell VerifyThis 2016: A Program Verification
Competition Protocol state fuzzing of TLS
implementations More info, incl. inferred models
Securing the information infrastructure for
EV charging An RFID skimming gate using Higher
Harmonics Protocol state machines and
session languages: specification, implementation,
and security flaws A Security Architecture for the
Publish/Subscribe C-DAX Middleware An Information-Centric Communication
Infrastructure for Real-Time State Estimation of Active
Distribution Networks Analysis of secure key storage solutions on
Android Automated Reverse Engineering using LEGO® movie of our Lego hacker in action .
More info and the inferred models
Digitale handtekeningen: nieuwe technologie & nieuwe wet- en regelgeving [Addendum]
Privacy & Informatie , Vol 1, pp. 2-10, februari 2014.
A security protocol for Information-Centric Networking in smart grids Using Trusted Execution Environments in Two-Factor Authentication: comparing approaches A comparison of time-memory trade-off attacks on stream ciphers Formal models of bank cards for free More info and the inferred models
The Radboud Reader: a minimal trusted smartcard
reader for securing online transactions Designed to fail: a USB-connected reader for online banking Risicoanalyse Slimme Meter Keten: Privacy en Security in het nieuwe marktmodel Formal analysis of the EMV protocol suite F# sources for EMV ]
Rigorous specifications of the SSH Transport Layer Biometrics and Smart Cards in Identity Management Operational and Technical security of Electronic Passports. Midlet Navigation Graphs in JML Electronic Passports in a Nutshell Risicoanalyse EPD-DigiD naar aanleiding van de A5/1 kwetsbaarheid in GSM Teaching program specification and verification using JML and
ESC/Java2 Model-Based Testing of Electronic Passports Type-based Object Immutability with Flexible Initialization Technical report ICIS-R09001 , Radboud University Nijmegen, Jan. 2009
Explicit information flow properties in JML Malicious Code on Java Card Smartcards: Attacks and Countermeasures Formal Nova interface specification: Formal specification of the micro-hypervisor interface Multi-level security, 3 1/2 decades later Fingerprinting Passports BML Reference Manual online
Testing the Java Card Applet Firewall
[Erratum Associated software for these tests ]AHA: Amortized Heap Space Usage Analysis Computer security
through correctness and transparancy The
History of Information Security , pp. 637-653 , Elsevier, 2007
Testing the eSTV program for the Scottish local government electiona s
A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java
Verifying an implementation of SSH
Immutable Objects for a Java-like Language
A Comparison of Java Cards: State-of-Affairs 2006
Mobius: Mobility, ubiquity, security
Tearing Java Cards
JML Reference Manual [HTML]
[PDF]
Beyond Assertions: Advanced Specification and
Verification with JML and ESC/Java2
An overview of JML tools and applications www.springerlink.com
Transactions and non-atomic API methods in Java Card: specification ambiguity and strange implementation behaviours Reasoning about Card Tears and Transactions in Java Card FASE'04 , pp. 114 - 128, LNCS volume 2984, Springer, 2004.
Java Program Verification at Nijmegen: Developments and Perspective Software Security - Theories and Systems (ISSS'03) ,
pp. 134-153, LNCS volume 3233, Springer, 2004.
Formal Techniques for Java-Like Programs
Coalgebras and Monads in the Semantics of Java Theoretical Computer Science , volume 291, Issue 3, pp. 329-349, Elsevier, 2003
Implementing a Formally Verifiable Security Protocol in Java Card SPC'03 ,
First International Conference on Security in Pervasive Computing,
Boppard, Germany, 2003
Verifying JML specifications with model fields ECOOP workshop on Formal Techniques for Java-like Programs (FTfJP'03) ,
Darmstadt, July 2003
An overview of JML tools and applications
From Finite State Machines to Provably Correct JavaCard Applets
Opportunities and challenges for formal specification of Java programs Trusted Components Workshop , Prato, Italy, January 2003
Static Analysis for JML's assignable Clauses FOOL 10
(International Workshop on Foundations of Object-Oriented Languages),
New Orleans, January 2003
A Java Reference Model of Transacted Memory for Smart Cards 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
Formal Techniques for Java-Like Programs
Towards a full formal specification of the Java Card API Smart Card Programming and Security ,
LNCS volume 2140, pp. 165-178, Springer, 2001
Formal Specification and Verification of JavaCard's Application Identifier Class Java on Smart Cards: Programming and Security ,
LNCS volume 2041, pp. 137-150, Springer, 2001
A Coalgebraic Semantics of Subtyping Theoretical Informatics and Applications , volume 35(1), pp. 61-82, 2001
Formal Specification of the JavaCard API in JML: the APDU class Computer Networks , volume 36, Issue 4, pp. 407-421, Elsevier Science, 2001.
On the Role of Invariants in Reasoning about Object-Oriented
Languages ECOOP workshop on Formal Techniques for Java Programs (FTfJP'01) ,
Budapest, June 2001
From Algebras and Coalgebras to Dialgebras Coalgebraic Methods in Computer Science (CMCS'01) ,
volume 44 of ENTCS,
Elsevier, 2001
Formal Techniques for Java-Like Programs
VerifiCard: A European Project for Smart Card Verification.
A Logic for the Java Modeling Language JML FASE'01 , LNCS volume 2029, pp. 284-299, Springer, 2001
JML: notations and tools supporting detailed design in Java
OOPSLA 2000 Companion , Minneapolis, USA, October 2000
Specification of the JavaCard API in JML
Fourth Smart Card Research and Advanced Application IFIP Conference (CARDIS'2000) ,
2000
First steps in formalising JML ECOOP workshop on Formal Techniques for Java Programs (FTfJP'2000) ,
Sophia Antipolis, France, 2000
A Monad for Basic Java Semantics Algebraic Methodology and Software Technology (AMAST'2000) ,
LNCS volume 1816,
pp. 150-164, Springer, 2000
A Coalgebraic Semantics of Subtyping Coalgebraic Methods in Computer Science (CMCS'2000) ,
volume 33 of ENTCS,
Elsevier, 2000
Integrating Computer Algebra and Reasoning through the Type System of Aldor 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 14th International Workshop on Algebraic Development Techniques (WADT'99) ,
LNCS volume 1827, Springer, 2000.
Safe Proof Checking in Type Theory with Y Computer Science Logic (CSL'99) ,
LNCS volume 1683,
pp. 439-452, Springer,
1999
The Type System of Aldor
Book review of "Algebra of Programming" by Richard Bird and Oege de Moor 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 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 Calculemus and Types'98 , Eindhoven, the Netherlands
Behavioural Subtyping for a Type-Theoretic Model of Objects FOOL5: Fifth International Workshop on Foundations of
Object-Oriented Languages , San Diego, USA, 1998
Expansion Postponement for Normalising Pure Type Systems Journal of Functional Programming , volume 8, issue 1, pp. 89-98, 1998
Subtyping and Inheritance for Categorical Datatypes 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 TYPES'97 Workshop on Subtyping, inheritance and
modular development of proofs , Durham, UK, 1997
System F with width-subtyping and record updating Theoretical Aspects of Computer Software (TACS'97) ,
LNCS volume 1281, pp. 439-457, Springer, 1997
Pure Type Systems with Definitions Logical Foundations of Computing Science (LFCS'94) , number 813 in LNCS, pp. 316-328. Springer, 1994
my home page
