Publications Submitted to the nationwide Research Assessment Exercise (RAE), UK 2008

Solved open problem in locally presentable categories from classic book by Gabriel, Ulmer (1971) on characterisations of models for Horn formulas. Solution refuted classification theorem from highly regarded book on locally presentable categories (1994). Triggered further research elsewhere, including a paper by Hebert, Rosicky (2001) salvaging classification theorem for uncountable cardinalities. Results from this output is currently being used by the author to show that satisfiability for classical and inductive logic coincides for fragments of first-order logic exceeding Horn logic, and to demonstrate the soundness of using classical logic to verify cryptographic protocols using the closed world assumption inherent in the usual Dolev-Yao adversary models.

Output 2: M. Abadi and J. Jürjens, Formal Eavesdropping and its Computational Interpretation (paper (ps), paper (pdf), Bibentry, (older) slides), Theoretical Aspects of Computer Software (4th International Symposium, TACS 2001), volume 2215 of Lecture Notes in Computer Science, Springer, 2001, pages 82-94. © Springer-Verlag

Based on a conference article by Abadi and Rogaway (2000), the current paper was the first to deliver a soundness result for symbolic crypto-protocol modelling of complete protocol executions against complexity-theoretical models, and in particular one of the first in a new line of research in formal verification of crypto-protocols. Addresses the question how common symbolic verification models for crypto protocols relate to the more fine-grained complexity-theoretical models used in the cryptography community. Triggered by these two articles over 20 research groups now work on related problems, including groups at Microsoft Research, IBM/Zurich, MIT, Stanford, and Ecole Normale Superieure, resulting in 107 Google Scholar citations (Jan. 2008).

Output 3: Jan Jürjens, Secure Systems Development with UML (Bibentry), © Springer-Verlag, Heidelberg, 2004. 300 pages.

First book on model-based security engineering (a field which was initiated by the author`s FASE`01 paper). Includes the first security extension of UML, its formal foundations, and applications for example to a smart-card based payment system developed by Visa International. The article led to work by the author on automated formal verification of UMLsec models (for which the verification technique was presented at ICSE`05, and tools for it at ICSE`06) and applications at BMW (ICSE`07), O2 (Germany) (ICSE`08) and other companies. Led to keynotes (SECRYPT`06, Software Engineering`07), projects totalling 600K Euros using UMLsec, 3 PhD theses and about 50 related journal and conference papers co-authored by the author between 2001 and 2007, totalling the majority of the over 1000 of the author`s citations at Google Scholar in Jan. 2008 (including 158 for the book itself ).

Output 4: J. Jürjens. Security Analysis of Crypto-based Java Programs using Automated Theorem Provers. In 21st International Conference on Automated Software Engineering (ASE 2006), IEEE/ACM, 2006, pages 167-176. (paper, slides, bibtex)

First formal verification of crypto-protocol legacy implementations for high-level data security requirements. Provides first solution to open problem of insecure crypto-protocol Java implementations (with respect to the Dolev-Yao adversary model) which present security threat to e-commerce applications, which are usually used over computer networks secured by crypto-protocols. Led to first-of-a-kind application to a biometric authentication protocol developed by a large telecommunications company which uncovered three ma jor security flaws regarding a novel kind of attack that were then fixed (ACSAC`05).

Some additional Publications

This article proposes a solution for an open problem in the area of formal verification of security-critical systems, namely the so-called "refinement paradox", which means that in many approaches to formal verification of security, security requirements are not preserved by refinement. This is very unfortunate, since it forces one to redo the verification after each refinement step, and dangerous, because the implemented system will always be a refinement even of the most detailed model. The article solves this problem by presenting a formal approach where important security requirements (formalized in a classical Dolev-Yao style way) are indeed preserved by the standard refinement operator. This is achieved by separating non-determinism in the sense of underspecification from run-time nondeterminism (unpredictability) needed for security functionality.

J. Jürjens, UMLsec: Extending UML for Secure Systems Development (paper (ps), paper (pdf), slides, Bibentry), 5th International Conference on The Unified Modeling Language (UML 2002), volume 2460 of Lecture Notes in Computer Science, Springer, 2002, pages 412-425. © Springer-Verlag

Based on an earlier article by the same author at FASE`01, this article is the first major article in the area of model-based development of secure systems, of which the author is one of the main founders. This field is attracting quickly increasing attention, with several workshops devoted to the topics over the last few years. It also has a significant impact in industry, where it has been successfully used to analyze security-critical systems for vulnerabilities and to correctly design new secure systems. The article defines an extension of UML for secure systems design and demonstrates usefulness at the hand of several case-studies.

J. Jürjens, Sound Methods and Effective Tools for Model-based Security Engineering with UML, (slides, paper, bibtex) 27th International Conference on Software Engineering (ICSE), ACM, 2005, pages 322-331.

This article provides formally based, automated verification tool-support for the security extension of UML defined in earlier work. It thus prepares the way for the results in the area of model-based development of secure systems to be used in a formally sound but automated way by practitioners in industry who may be neither security nor formal methods experts. The tools have subsequently been successfully used in industry to analyze security-critical systems for vulnerabilities and to correctly design new secure systems. The article presents a general tool-suite for formal analysis of UML models, explains one such analysis plug-in based on automated theorem provers for first-order logic in more detail, and demonstrates usefulness at the hand of several industrial case-studies.