David von Oheimb's Computer Science Curriculum Vitae

Summary (as of 2025) by Perplexity

David von Oheimb’s curriculum vitae traces his evolution from a young electronics enthusiast to a leading expert in formal verification, IT security, and standardization. It documents a steady progression through computing generations, academic research, and industrial innovation.

Early years (1981–1987)

Von Oheimb began with electronics and programmable pocket computers (Sharp PC-1401 and PC-1600), developing low-level tools such as disassemblers and assemblers. His skills led to his first professional engagement authoring manuals and software for a niche computing publisher.

Transition to personal computing (1988–1990)

Using the Commodore Amiga 2000, he learned C programming and multitasking systems. He explored distributed computing concepts like the INMOS Transputer and gained initial professional software experience during his military service by developing database applications.

Academic foundation (1991–1995)

At TU München, he studied computer science with a strong focus on programming language semantics, logics, and distributed systems. He joined research under Prof. Broy and Prof. Nipkow, working on theorem proving with Isabelle and publishing his first academic paper. His master’s thesis extended Isabelle’s HOLCF framework.

Doctoral research (1996–2001)

During his PhD under Prof. Nipkow, von Oheimb contributed to project Bali, formally analyzing Java semantics and type safety using Isabelle. He developed a Hoare logic for Java, published widely, participated in taught courses, and completed his doctorate in 2001.

Industrial research at Siemens (2001–2013)

He joined Siemens Corporate Technology as a research scientist in IT security, developing the Interacting State Machines (ISM) formalism and applying it to smart card certification (EAL5+). Over the decade, he managed EU projects like AVISPA and AVANTSSAR, advanced formal security analysis, taught at Munich universities, and helped improve industrial software verification tools. He later worked on smart metering, SCADA, and embedded system security.

Open-source and standardization leadership (2013–present)

Von Oheimb became deeply involved in open-source security and cryptography: His later work focused on post-quantum cryptography and improving PKI automation protocols, while privately pursuing hobbyist projects combining GPS mapping, renewable energy control, and software engineering excellence.

Overview of my IT-related development before the year 2000

In the 1980s and '90s, departing from the very basics, I got up-to-speed with the overall evolution of information technology and computer science, which can be summarized as:

Area From To
CPUs 8-bit microprocessors 32-bit SPARC/x86
Operating systems Basic proprietary OSes Unix and derivatives
Programming languages Machine code Functional & object-oriented
Debugging Single-stepping the CPU Formal program verification
Application software Numeric calculations Theorem provers

Early experience: pocket computers

1981
First encounter with electronics, in particular logic circuits, on a children's summer camp.
1984
My personal IT career began with an innocent programmable pocket calculator, which I used for facilitating basic gliding performance calculations for model airplanes. Within a week I realized that I needed a more powerful computing device, which, according to my pupil's budget, was a Sharp PC-1401 pocket computer, programmable with BASIC.
1985
Soon I gained more interest in the implementation rather than application of this machine and started learning the machine language of its exotic 8-bit microprocessor. I hand-coded my own disassembler and analyzed parts of its operating system and the BASIC interpreter.
1986
Having earned some money with a summer job, I bought a Sharp PC-1600, featuring much more hardware and software power. Having learnt how to deal with its Zilog Z80 microprocessor, I disassembled and analyzed large chunks of its 96KB ROM and developed my own disassembler, macro assembler, and debugger.
1987
When I started selling this software via a users' magazine, my skills were discovered by a HW&SW distributor and publisher focusing on pocket computers. I got contracted with this (one-man) firm to author a system programmer's manual and develop a text-processor for the PC-1600.

Maturing to state-of-the art computing: home and personal computers

1988
Meanwhile, I could afford letting a dream come true: Using the most enhanced home computer of that time, the Commodore Amiga 2000. On this machine I got to know higher-level system programming with C and state-of-the art multitasking system software. Except for a RAM disk driver and some (frustrating) experiments with neuronal network simulations, I did not develop - or even sell - serious software.
1989
Having heard of the INMOS Transputer, I was fascinated by this promising approach and even considered developing system software for the excellent distributed operating system Helios by Perihelion Software. I had already reverse-engineered the kernel of this system (reporting several bugs to its developers), but unfortunately there was general sobering about the Transputer hype, and I also ran out of time as I meanwhile had finished school and my military service began.
1990
Working at the staff unit of an air force base, I was given the nice opportunity to exercise my computer hobby by writing software keeping track of the pilots' training flights. I must, though, admit that this program became quite a mess, written on a PC with dBASE, and I'm not sure if they actually could make good use of it.

The academic approach: workstations and global networks

1991
In this year I began studying Computer Science at the nearest university known for its good education in this area: The TU München. Though the rather high-level teaching there suited my interests and capabilities for mathematics and technology, in particular the math courses in the first two years were quite challenging, but it was worth it.
1992
In the Ferienakademie ('holiday academy', a kind of summer school) of our university in Sarntal (South Tyrol), I encountered the charm of high-level (functional and logic) programming. Somehow connected to this event, I was invited to begin a student job at Prof. Broy's chair. There, among other things, I was introduced to LaTeX and making use of the Internet.
1993
After successfully passing the intermediate tests, I finally could deepen my knowledge in my favorite subjects: the theory of programming languages as an application of discrete mathematics, in particular semantics and logics, but also more technical issues like advanced concepts of operating systems and distributed computing. On the other hand, I also became interested in relating computer science with humane discipline, namely through computational linguistics. (Later, it turned out that I had too high expectations on the maturity of this field, and thus I abandoned it.)
1994
I was lucky to take part in the Ferienakademie again, this time in a course on distributed algorithms and computing. In that year I got to know Prof. Tobias Nipkow and his research assistants working on their interactive theorem prover Isabelle. I was inspired to familiarize with this system and did a major a student project with it: RALL, a proof system for abstract relation algebra, which I had the privilege to publish on the CADE conference later.
1995
As an excursion to the distributed systems track, I did a verification case study with Isabelle for the FOCUS framework as a student job. At the same time I made further use of my Isabelle expertise, developing a datatype package within HOLCF as my master thesis.

My doctorate: developing and applying theory of programming languages

1996
Even before finishing my CS diploma that year, I was invited by Prof. Nipkow to join his new project Bali analyzing Java with Isabelle, which I gladly accepted.
1997
I first investigated the security-related issue of type-safety for the Java language. For this endeavor to become a success, I had to put together all my experience on programming language design and semantics, implementation techniques, formal logic, software engineering, and project management. Of course, also discussions with colleagues (apart from my supervisor, mainly people from England) and analyzing other related work stimulated progress.
1998
This year was dominated by publications of the results obtained by then, giving talks on conferences, seminars and workshops, and writing papers, for example contributing to a survey on Java research. I also took part in some teaching efforts, giving courses on Java to both fresh students and mature maths teachers.
1999
As a second large work package within project Bali, I developed a Hoare logic for Java, where handling side-effecting expressions and planning the (meta-level) soundness and completeness proofs were the main challenges. Besides the project work, I also took part (as a staff member) in the NATO summer school in Marktoberdorf, that year focusing on foundations of secure computation.
2000
After finishing my work on the Hoare logic, this year was governed by writing up my PhD thesis. I finished it exactly at the end of my fourth year of employment as a research assistant. In the autumn I took part in the Ferienakademie the third time, this time as a tutor.
2001
In February, just about two months after submitting my thesis, I had the final (oral) exam, and immediately after this the official PhD party. By the summer, I finished my research work at TUM.

Industrial research and consulting: formal methods applied to IT security

2001
When looking for a new field of activity that should be both important for our society and challenging to me, I decided to enter IT security. Siemens Corporate Technology offered me a good position as a ``Research Scientist''. This security department there offers security analysis, consulting and specialized solution development to both Siemens-internal and external customers.
2002
Working on a formal security analysis project, I developed the Interacting State Machines (ISMs) formalism for modeling and verifying reactive systems, which has been used e.g. for certifying the Infineon SLE 66 smart card processor according to Common Criteria EAL 5+.
2003
In this year, among others, I extended the ISM formalism and applied it analyzing the complex RBAC of a medical information system by Siemens Healthcare and the memory management system of the Infineon SLE 88, in this way contributing to the EAL 5+ certification of this 32-bit successor of the SLE 66. I also did some fundamental research on information flow.
2004
Having gained more experience with Siemens projects, when our team was re-constructed, I obtained the project management for the Siemens part of the EU project AVISPA: Automated Validation of Internet Security Protocols and Applications, and a security analysis project for the Boeing Electronic Distribution of Software (BEDS), and consequently was promoted to a Senior Research Scientist. I also became secretary of the ForTIA: Formal Techniques Industrial Association. Concerning the verification techniques used, my focus changed from interactive theorem proving to automatic model checking.
2005
I gave talks and tutorials at various occasions on my specific field of activity, formal security analysis. Still having good contacts with academia, I even got a university teaching mandate at both Munich universities to give a lecture on this subject. Moreover, I was proud to be part in the very successful closing of the project AVISPA and assisted in two further EU IST FET Open proposals, including the immediate successor to AVISPA.
2006
I gave two invited talks about formal security analysis in industry, though my focus was gradually shifted to security architecture consulting and certification according to the Common Criteria. I spent a very pleasant and productive month at Boeing Research & Technology in Bellevue near Seattle, examined security architecture alternatives of a digital tachograph, and provided support for evaluating (w.r.t. security) part of the German health card system.
2007
I continued working on the security of the digital tachograph and our projects with Boeing, contributing to three publications with them and spending again more than a month in the Seattle area.
2008
I became the Siemens site leader of the newly started EU project AVANTSSAR: Automated VAlidatioN of Trust and Security of Service-oriented ARchitectures and continued serving as a programme committee member of various IT security related workshops like the ACM SAC Security Track and Open Source Software Certification.
2009
On the scientific side, I co-designed the AVANTSSAR Specification Language (ASLan++). On the business side, I did major contributions to the acquisition and execution of an order by Continental Automotive (formerly VDO, then Siemens VDO) to implement a secure software upgrade module for an embedded system.
2010
At work, I was mostly busy with the third and final year of AVANTSSAR and contributing to the development of the software upgrade module mentioned above. I also spent quite some time on private IT projects, developing a HyperText Bible, fixing a couple of notorious bugs in Thunderbird and Lightning, and getting some familiarity with Android 2.2 and geolocation using GPS. With my HTC Desire featuring a wonderful AMOLED display, I'm meanwhile back to pocket computers - just some 300 times faster and with a million times higher memory capacity than in 1984 :-)
2011
After pretty annoying and time-consuming experience with various regressions and the immature Unity desktop of Ubuntu Linux 11.04, I allowed myself a MacBook Air, and for pragmatic reasons also got a cheap Windows 7 netbook. This certainly opened new horizons for me and made some things simpler, but on the other hand it cost me quite some effort to unify the user interfaces (e.g., keyboard shortcuts) of the three operating systems to allow for their seamless promiscuous use.
2012
Since early 2011 and well into 2013 my work at Siemens was mostly part of AVANTSSAR's successor project SPaCIoS, which aimed at security testing based on various formal methods. I focused on improving and extending the Java implementation of the ASLan++ translator, which - similarly to the other AVANTSSAR Tools - unfortunately were never really finished and only unofficially released. In my spare time I provided major improvements to the Thunderbird add-on Duplicate Contacts Manager.
2013
As part of SPaCIoS, I spent together with two colleagues some effort into research and a related prospective publication enhancing non-interference for state-oriented systems, yet this starved on resources. I was glad that instead my contributions to practical industrial security rose.

Industrial and open-source IT security development and standardization

2013
Since 2011 I had been working on system architecture as well as implementation and certification support for the security of smart metering systems, but also for toll system onboard units and SCADA (i.e., production information and control) systems.
2014
In spring I started working on a new major project: a client-server application prototype for enrolling certificates of field devices, based on the protocol EST and its implementation by Cisco, called libEST.
2015
Early that year I submitted to Cisco a large chunk of source code containing major improvements and extensions of libEST. For the rest of the year we struggled to get these and some further contributions reviewed and accepted by this open-source — but in reality not very open project, with little success.
2016
Partly out of our bad experience with contributing to libEST, but mostly because we found that the more flexible Certificate Management Protocol actually fits our needs better, we moved on to CMP. I started improving and extending CMP for OpenSSL, an implementation by Nokia. I also did minor contributions to the OpenSC project to their PKCS#11 tool.
2017
My contributions to CMPforOpenSSL turned out to take quite much effort, too, but this time it was very fruitful because Martin Peylo, the initiator and maintainer of that open-source project, proved very open to substantial improvements. Related to that activity I started in August actively contributing to the OpenSSL project.
2018
In April we officially (re-)started an upstream contribution of CMP to OpenSSL. To this end we had moved the project to GitHub and submitted the first pull request in late July. After initial feedback we split the contribution in twelve chunks, which we have been contributing since them.
In my spare time I extended and open-sourced my little GPX track converter tool GPXConv and started directly contributing to the Pannellum open-source panorama viewer project. I also revived the Thunderbird add-on Duplicate Contacts Manager on my own repository because the original developers were not reachable any more.
2019
That year I pushed forward the contribution of CMP to OpenSSL, which worked out slowly but steadily. I also made and published major extension to a CMP client implementation for embedded systems with the help of a working student and made the Duplicate Contacts Manager compatible with Thunderbird version 68+.
2020
In January I was invited to become an OpenSSL Committer. This was very helpful in getting the remaining chunks of the CMP contribution included in time — the last chunk was merged in min-June. It also motivated and enabled me to do many more general improvements to OpenSSL, not only regarding certificate handling.
2021
In September, OpenSSL 3.0 was released, including the CMP implementation and many other improvements of mine, for instance on the HTTP client. Over the years before I had developed also a high-level API for it, called generic CMP Client, as well as a convenience layer for OpenSSL certificate management etc. called Security Utilities, both of which were open-sourced around the same time.
2022
For several years we had been working on the Lightweight CMP Profile and related standardization documents regarding CMP. This year we were able to get it through the IETF Working Group Last Call. Partly as a PoC for this standardization, we started developing the CmpRaComponent, which provides a very flexible and easy-to-use CMP core for Registration Authorities in Java. We also continued working on a draft of BRSKI-AE, for which I had taken editorship.
I started developing SolBatSim, a precise simulation for photovoltaic systems optionally including energy storage.
2023
In November, finally the Lightweight CMP Profile and related documents became RFCs, and during this year we continued pushing support of the new CMP features defined there to OpenSSL. For the whole year we were working also on a self-contained version of CMP Updates, called RFC4210bis, where we added support for KEM keys. I mostly finished developing SolBatSim.
2024
In the first months of the year I developed SolBatHome, for control and data capturing of my small PV system with buffer battery, which was a PITA due to the poor design and documentation of the underlying Home Assistant. In the certificate management area, we intensified my involvement in post-quantum cryptography (PQC) support and broadened our development team, further improving our CMP client and server OSS components. I also continued helping out with the standardization of improvements on the EST CSR attributes definition.
2025
This year, finally, we were able to get our RFCs published for BRSKI-AE, as well as for CMPv3 and its HTTP transfer. I developed a CMP client in Go, where AI assistance proved surprisingly helpful in getting started with the language, as well as an EST client, very conveniently based on libcURL.
On the private side, I did major extensions and improvements on my GPXConv tool, in particular for merging parallel GPS recordings. I also started integrating GPX Viewer in order to have full control on presenting my track recordings along with photos taken on the way.
-----------------------------------------------------------------------------------------------
[Valid HTML5] URL: https://ddvo.net/cv.html,  created in 1999, last modified: 2025-10-11