☰

Dr. Andreas Lochbihler

mail@andreas-lochbihler.de

About me

I am now a principal engineer at Digital Asset working on the Canton protocol. This is my private homepage and its content does not necessarily represent Digital Asset's views or positions.

From 2013 to 2018, I was a senior researcher in the Information Security Group at ETH Zürich. My research revolved around the theory and tools to formalise protocols and their proofs such that definitions and proofs can be check mechanically. My framework CryptHOL brings to cryptography the expressiveness and rigour of higher-order logic and coalgebraic methods as implemented in the proof assistant Isabelle/HOL.

Before joining ETH, I was a member of Programming Paradigms group at the Karlsruhe Institute of Technology and of the Sofware Systems group at the University of Passau. I received my PhD from the KIT in 2012. In my thesis, I built a formal model of Java concurrency which formalises source code, bytecode, a virtual machine, the compiler and the Java memory model in Isabelle/HOL.

Publications ↥

Listing on DBLP and Google Scholar.

Drafts and Preprints

  1. Andreas Lochbihler: A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks with Applications to Probability Theory. To appear in Journal of Automated Reasoning.
    • Original article available at springerlink.com
    • Preprint PDF
    • Long version
    • Abstract Abstract. Aharoni et al. proved the max-flow min-cut theorem for countable networks, namely that in every countable network with finite edge capacities, there exists a ow and a cut such that the ow saturates all outgoing edges of the cut and is zero on all incoming edges. In this paper, we formalize their proof in Isabelle/HOL and thereby identify and fix several problems with their proof. We also provide a simpler proof for networks where the total outgoing capacity of all vertices other than the source and the sink is finite. This proof is based on the max-flow min-cut theorem for finite networks. As a use case, we formalize a characterization theorem for relation lifting on discrete probability distributions and two of its applications.

Journals

  1. Basil Führer, Andreas Lochbihler, Joshua Schneider, and Dmitriy Traytel: Quotients of Bounded Natural Functors. Logical Methods in Computer Science, 18(1), 2022.
    • Link
    • arXiv
    • BibTeX
    • Abstract Abstract. The functorial structure of type constructors is the foundation for many definition and proof principles in higher-order logic (HOL). For example, inductive and coinductive datatypes can be built modularly from bounded natural functors (BNFs), a class of well-behaved type constructors. Composition, fixpoints, and, under certain conditions, subtypes are known to preserve the BNF structure. In this article, we tackle the preservation question for quotients, the last important principle for introducing new types in HOL. We identify sufficient conditions under which a quotient inherits the BNF structure from its underlying type. Surprisingly, lifting the structure in the obvious manner fails for some quotients, a problem that also affects the quotients of polynomial functors used in the Lean proof assistant. We provide a strictly more general lifting scheme that supports such problematic quotients. We extend the Isabelle/HOL proof assistant with a command that automates the registration of a quotient type as a BNF, reducing the proof burden on the user from the full set of BNF axioms to our inheritance conditions. We demonstrate the command's usefulness through several case studies.
  2. David Butler, Andreas Lochbihler, David Aspinall and Adria Gascon: Formalizing Σ-Protocols and Commitment Schemes using CryptHOL. Journal of Automated Reasoning 65:521-567, 2021.
    Presented at the 3rd ZKProof workshop, 2020.
    • Original article available at springerlink.com
    • Cryptology ePrint Archive 2019/1185
    • BibTeX
    • Abstract Abstract. Machine-checked proofs of security are important to increase the rigour of provable security. In this work we present a formalised theory of two fundamental two party cryptographic primitives: Σ-protocols and Commitment Schemes. Σ-protocols allow a prover to convince a verifier that they possess some knowledge without leaking information about the knowledge. Commitment schemes allow a committer to commit to a message and keep it secret until revealing it at a later time.
      We use CryptHOL to formalise both primitives and prove secure multiple examples namely: the Schnorr, Chaum-Pedersen and Okamoto Σ-protocols as well as a construction that allows for compound (AND and OR) Σ-protocols and the Pedersen and Rivest commitment schemes.
      A highlight of the work is a formalisation of the construction of commitment schemes from Σ-protocols. We formalise this proof at an abstract level using the modularity available in Isabelle/HOL and CryptHOL. This way, the proofs of the instantiations come for free.
  3. David A. Basin, Andreas Lochbihler, and S. Reza Sefidgar: CryptHOL: Game-based proofs in higher-order logic. Journal of Cryptology, 33:494-566, 2020.
    • Original article available at springerlink.com
    • Cryptology ePrint Archive 2017/753
    • BibTeX
    • Abstract Abstract. Game-based proofs are a well-established paradigm for structuring security arguments and simplifying their understanding. We present a novel framework, CryptHOL, for rigorous game-based proofs that is supported by mechanical theorem proving. CryptHOL is based on a new semantic domain with an associated functional programming language for expressing games. We embed our framework in the Isabelle/HOL theorem prover and, using the theory of relational parametricity, we tailor Isabelle's existing proof automation to game-based proofs.
      By basing our framework on a conservative extension of higher-order logic and providing sufficient automation support, the resulting proofs are trustworthy and comprehensible, and the framework is extensible and widely applicable. We evaluate our framework by formalizing different game-based proofs from the literature and comparing the results with existing formal-methods tools.
  4. Andreas Lochbihler: Effect polymorphism in higher-order logic (proof pearl). Journal of Automated Reasoning, 63(2):439-462, 2019.
    • Original article available at springerlink.com
    • Preprint
    • BibTeX
    • Abstract Abstract. The notion of a monad cannot be expressed within higher-order logic (HOL) due to type system restrictions. I show that if a monad is restricted to values of a fixed type, this notion can be formalised in HOL. Based on this idea, I develop a library of effect specifications and implementations of monads and monad transformers. Hence, I can abstract over the concrete monad in HOL definitions and thus use the same definition for different (combinations of) effects. I illustrate the usefulness of effect polymorphism with a monadic interpreter.
  5. Peter Lammich and Andreas Lochbihler: Automatic Refinement to Efficient Data Structures - A comparison of two approaches. Journal of Automated Reasoning, 63(1):53-94, 2019.
    • Original article available at springerlink.com
    • Preprint
    • BibTeX
    • Abstract Abstract. We consider the problem of formally verifying an algorithm in a proof assistant and generating efficient code. Reasoning about correctness is best done at an abstract level, but efficiency of the generated code often requires complicated data structures. Data refinement has been successfully used to reconcile these conflicting requirements, but usability calls for automatic tool support. In the context of Isabelle/HOL, two frameworks for automating data refinement have been proposed. In this paper, we present and compare the two frameworks and their underlying ideas in depth. Thereby, we identify the challenges of automating data refinement, highlight the similarities and differences of the two approaches, and show their strengths and limitations both from the implementer's and the user's perspectives. A case study demonstrates how to combine both frameworks, benefiting from the strengths of each.
  6. Andreas Lochbihler: Mechanising a type-safe model of multithreaded Java with a verified compiler. Journal of Automated Reasoning 61(1-4):243-332, June 2018.
    • Original article available at springerlink.com
    • Preprint
    • BibTeX
    • Abstract Abstract. This article presents JinjaThreads, a unified, type-safe model of multithreaded Java source code and bytecode formalised in the proof assistant Isabelle/HOL. The semantics strictly separates sequential aspects from multithreading features like locks, forks and joins, interrupts, and the wait-notify mechanism. This separation yields an interleaving framework and a notion of deadlocks that are independent of the language, and makes the type safety proofs modular. JinjaThreads's non-optimising compiler translates source code into bytecode. Its correctness proof guarantees that the generated bytecode exhibits exactly the same observable behaviours as the source code, even for infinite executions and under the Java memory model. The semantics and the compiler are executable.
      JinjaThreads builds on and reuses the Java formalisations Jinja, Bali, mJava, and Java light by Nipkow's group. Being the result of more than fifteen years of studying Java in Isabelle/HOL, it constitutes a large and long-lasting case study. It shows that fairly standard formalisation techniques scale well and highlights the challenges, benefits, and drawbacks of formalisation reuse.
  7. Andreas Lochbihler: Making the Java Memory Model Safe. ACM Transactions on Programming Languages and Systems 35(4), Article 12 (65 pages), 2014.
    • Link
    • Preprint
    • BibTeX
    • Abstract Abstract. This work presents a machine-checked formalisation of the Java memory model and connects it to an operational semantics for Java and Java bytecode. For the whole model, I prove the data race freedom guarantee and type safety. The model extends previous formalisations by dynamic memory allocation, thread spawns and joins, infinite executions, the wait-notify mechanism, and thread interruption, all of which interact in subtle ways with the memory model. The formalisation resulted in numerous clarifications of and fixes to the existing JMM specification.
    a preliminary version is available as Karlsruhe Reports in Informatics 2012-23, 2012
  8. Andreas Lochbihler: Analysing Java's safety guarantees under concurrency. it - Information Technology 56(2):82-86, 2014.
    • Link
    • BibTeX
    • Abstract Abstract. Two features distinguish Java from other main-stream programming languages like C and C++: its built-in support for concurrency and safety guarantees such as type safety or safe execution in a sandbox. In this work, we build a formal, unified model of Java concurrency, validate it empirically, and analyse it with respect to the safety guarantees using a proof assistant. We show that type safety and Java's data race freedom guarantee hold. Our analysis, however, revealed a weakness in the Java security architecture, because the Java memory model theoretically allows pointer forgery. As a result, this work clarifies the specification of the Java memory model.
  9. Andreas Lochbihler: Ein maschinengeprüftes, typsicheres Modell der Nebenläufigkeit in Java: Sprachdefinition, virtuelle Maschine, Speichermodell und verifizierter Compiler, In: Steffen Hölldobler et al. (Eds.): Ausgezeichnete Informatikdissertationen 2012, Lecture Notes in Informatics D-13, pp. 211-220, Gesellschaft für Informatik, 2013.
    • Preprint
    • BibTeX
    • Abstract Abstract. Charakteristisch für die Programmiersprache Java sind sowohl ihre Sicherheitsgarantien wie beispielsweise Typsicherheit und die Sicherheitsarchitektur als auch die direkte Unterstützung von Threads. In der hier vorgestellten Dissertation wird ein maschinengeprüftes Modell von nebenläufigem Java einschließlich des Java-Speichermodells entwickelt und die Auswirkungen der Nebenläufigkeit auf diese Garantien untersucht. Aus dem formalen Modell wurde automatisch ein ausführbarer Interpreter, Übersetzer und eine virtuelle Maschine einschließlich eines Bytecode-Verifizierers generiert, mit dem das Modell empirisch gegen Java-Benchmarks validiert wurde.
  10. Andreas Lochbihler and Gregor Snelting: On Temporal Path Conditions in Dependence Graphs. Journal of Automated Software Engineering, Vol. 16(2), pp. 263--290, June 2009.
    • Original article available at springerlink.com
    • Preprint
    • BibTeX
    • Abstract Abstract. Program dependence graphs are a well-established device to represent possible information flow in a program. Path conditions in dependence graphs have been proposed to express more detailed circumstances of a particular flow; they provide precise necessary conditions for information flow along a path or chop in a dependence graph. Ordinary boolean path conditions, however, cannot express temporal properties, e.g. that for a specific flow it is necessary that some condition holds, and later another specific condition holds.
      In this contribution, we introduce temporal path conditions, which extend ordinary path conditions by temporal operators in order to express temporal dependencies between conditions for a flow. We present motivating examples, generation and simplification rules, application of model checking to generate witnesses for a specific flow, and a case study. We prove the following soundness property: if a temporal path condition for a path is satisfiable, then the ordinary boolean path condition for the path is satisfiable. The converse does not hold, indicating that temporal path conditions are more precise.
  11. Kousha Etessami and Andreas Lochbihler: The Computational Complexity of Evolutionarily Stable Strategies. International Journal of Game Theory, Vol. 31(1), pp. 93--113, April 2008.
    • Link
    • BibTeX
    • Abstract Abstract. The concept of evolutionarily stable strategies (ESS) has been central to applications of game theory in evolutionary biology, and it has also had an influence on the modern development of game theory. A regular ESS is an important refinement the ESS concept. Although there is a substantial literature on computing evolutionarily stable strategies, the precise computational complexity of determining the existence of an ESS in a symmetric two-player strategic form game has remained open, though it has been speculated that the problem is NP-hard. In this paper we show that determining the existence of an ESS is both NP-hard and coNP-hard, and that the problem is contained in ΣΠ2, the second level of the polynomial time hierarchy. We also show that determining the existence of a regular ESS is indeed NP-complete. Our upper bounds also yield algorithms for computing a (regular) ESS, if one exists, with the same complexities.
    a preliminary version is available as ECCC tech report TR04-055, 2004.

Conferences ↥

  1. Andreas Lochbihler: A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks. In: Liron Cohen and Cezary Caliszyk (Eds.), Interactive Theorem Proving (ITP 2021), LIPIcs vol. 193, pp. 25:1-25:18, Schloss Dagstuhl, 2021.
    • DOI
    • Long version
    • BibTeX
    • Slides
    • Abstract Abstract. Aharoni et al. [Ron Aharoni et al., 2010] proved the max-flow min-cut theorem for countable networks, namely that in every countable network with finite edge capacities, there exists a flow and a cut such that the flow saturates all outgoing edges of the cut and is zero on all incoming edges. In this paper, we formalize their proof in Isabelle/HOL and thereby identify and fix several problems with their proof. We also provide a simpler proof for networks where the total outgoing capacity of all vertices other than the source is finite. This proof is based on the max-flow min-cut theorem for finite networks.
  2. David Basin, Andreas Lochbihler, S. Reza Sefidgar, and Ueli Maurer: Abstract Modeling of System Communication in Constructive Cryptography using CryptHOL. Computer Security Foundations (CSF 2021), pp. 1-16, IEEE, 2021.
    • DOI
    • Preprint
    • BibTeX
    • Abstract Abstract. Proofs in simulation-based frameworks have the greatest rigor when they are machine checked. But the level of details in these proofs surpasses what the formal-methods community can handle with existing tools. Existing formal results consider streamlined versions of simulation-based frameworks to cope with this complexity. Hence, a central question is how to abstract details from composability results and enable their formal verification.
      In this paper, we focus on the modeling of system communication in composable security statements. Existing formal models consider fixed communication patterns to reduce the complexity of their proofs. However, as we will show, this can affect the reusability of security statements. We propose an abstract approach to modeling system communication in Constructive Cryptography that avoids this problem. Our approach is suitable for mechanized verification and we use CryptHOL, a framework for developing mechanized cryptography proofs, to implement it in the Isabelle/HOL theorem prover. As a case study, we formalize the construction of a secure channel using Diffie-Hellman key exchange and a one-time-pad.
  3. Andreas Lochbihler and Ognjen Maric: Authenticated Data Structures as Functors in Isabelle/HOL. In: Bruno Bernardo and Diego Marmsoler (Eds.), Formal Methods for Blockchain (FMBC 2020), OASIcs vol. 84, pp. 6:1-6:16, 2020.
    Also presented at the Isabelle Workshop 2020.
    • DOI
    • Preprint
    • Long version
    • BibTeX
    • Isabelle workshop recording
    • Abstract Abstract. Merkle trees are ubiquitous in blockchains and other distributed ledger technologies (DLTs). They guarantee that the involved systems are referring to the same binary tree, even if each of them knows only the cryptographic hash of the root. Inclusion proofs allow knowledgeable systems to share subtrees with other systems and the latter can verify the subtrees' authenticity. Often, blockchains and DLTs use data structures more complicated than binary trees; authenticated data structures generalize Merkle trees to such structures.
      We show how to formally define and reason about authenticated data structures, their inclusion proofs, and operations thereon as datatypes in Isabelle/HOL. The construction lives in the symbolic model, i.e., we assume that no hash collisions occur. Our approach is modular and allows us to construct complicated trees from reusable building blocks, which we call Merkle functors. Merkle functors include sums, products, and function spaces and are closed under composition and least fixpoints. As a practical application, we model the hierarchical transactions of Canton, a practical interoperability protocol for distributed ledgers, as authenticated data structures. This is a first step towards formalizing the Canton protocol and verifying its integrity and security guarantees.
  4. Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel: Quotients of Bounded Natural Functors. In: Nicolas Peltier and Viorica Sofronie-Stokkermans (Eds.), Automated Reasoning (IJCAR 2020), LNCS 12167, pp. 58-78, Springer, 2020.
    • Original article available at springerlink.com
    • Preprint
    • Long version
    • BibTeX
    • Abstract Abstract. The functorial structure of type constructors is the foundation for many definition and proof principles in higher-order logic (HOL). For example, inductive and coinductive datatypes can be built modularly from bounded natural functors (BNFs), a class of well-behaved type constructors. Composition, fixpoints, and-under certain conditions-subtypes are known to preserve the BNF structure. In this paper, we tackle the preservation question for quotients, the last important principle for introducing new types in HOL. We identify sufficient conditions under which a quotient inherits the BNF structure from its underlying type. We extend the Isabelle proof assistant with a command that automates the registration of a quotient type as a BNF by lifting the underlying type's BNF structure. We demonstrate the command's usefulness through several case studies.
  5. Andreas Lochbihler, S. Reza Sefidgar, David A. Basin, and Ueli Maurer: Formalizing Constructive Cryptography using CryptHOL. Computer Security Foundations (CSF 2019), pp. 152-166, IEEE, 2019.
    • Link
    • Preprint
    • BibTeX
    • Slides
    • Abstract Abstract. Computer-aided cryptography increases the rigour of cryptographic proofs by mechanizing their verification. Existing tools focus mainly on game-based proofs, and efforts to formalize composable frameworks such as Universal Composability have met with limited success. In this paper, we formalize an instance of Constructive Cryptography, a generic theory allowing for clean, composable cryptographic security statements. Namely, we extend CryptHOL, a framework for game-based proofs, with an abstract model of Random Systems and provide proof rules for their equality and composition. We formalize security as a special kind of system construction in which a complex system is built from simpler ones. As a simple case study, we formalize the construction of an information-theoretically secure channel from a key, a random function, and an insecure channel.
  6. Damien Desfontaines, Andreas Lochbihler, and David A. Basin: Cardinality estimators do not preserve privacy. Privacy Enhancing Technologies (PoPETs), 2019(2):26-46, 2019.
    • Link
    • Preprint
    • BibTeX
    • arXiv 1808:05879
    • Abstract Abstract. Cardinality estimators like HyperLogLog are sketching algorithms that estimate the number of distinct elements in a large multiset. Their use in privacysensitive contexts raises the question of whether they leak private information. In particular, can they provide any privacy guarantees while preserving their strong aggregation properties?
      We formulate an abstract notion of cardinality estimators, that captures this aggregation requirement: one can merge sketches without losing precision. We propose an attacker model and a corresponding privacy definition, strictly weaker than differential privacy: we assume that the attacker has no prior knowledge of the data. We then show that if a cardinality estimator satisfies this definition, then it cannot have a reasonable level of accuracy. We prove similar results for weaker versions of our definition, and analyze the privacy of existing algorithms, showing that their average privacy loss is significant, even for multisets with large cardinalities. We conclude that strong aggregation requirements are incompatible with any reasonable definition of privacy, and that cardinality estimators should be considered as sensitive as raw data. We also propose risk mitigation strategies for their real-world applications.
  7. Andreas Lochbihler and Joshua Schneider: Relational parametricity and quotient preservation for modular (co)datatypes. In: Jeremy Avigad and Assia Mahboubi (Eds.), Interactive Theorem Proving (ITP 2018), LNCS 10895, pp. 411-431, Springer, 2018.
    • Original article available at springerlink.com
    • Long version
    • BibTeX
    • Abstract Abstract. Bounded natural functors (BNFs) provide a modular framework for the construction of (co)datatypes in higher-order logic. Their functorial operations, the mapper and relator, are restricted to a subset of the parameters, namely those where recursion can take place. For certain applications, such as free theorems, data refinement, quotients, and generalised rewriting, it is desirable that these operations do not ignore the other parameters. In this paper, we generalise BNFs such that the mapper and relator act on both covariant and contravariant parameters. Our generalisation, BNFCC, is closed under functor composition and least and greatest fixpoints. In particular, every (co)datatype is a BNFCC. We prove that subtypes inherit the BNFCC structure under conditions that generalise those for the BNF case. We also identify sufficient conditions under which a BNFCC preserves quotients. Our development is formalised abstractly in Isabelle/HOL in such a way that it integrates seamlessly with the existing parametricity infrastructure.
  8. Andreas Lochbihler: Fast machine words in Isabelle/HOL. In: Jeremy Avigad and Assia Mahboubi (Eds.), Interactive Theorem Proving (ITP 2018), LNCS 10895, pp. 388-410, Springer, 2018.
    • Original article available at springerlink.com
    • Preprint
    • BibTeX
    • Slides
    • Abstract Abstract. Code generated from a verified formalisation typically runs faster when it uses machine words instead of a syntactic representation of integers. This paper presents a library for Isabelle/HOL that links the existing formalisation of words to the machine words that the four target languages of Isabelle/HOL's code generator provide. Our design ensures that (i) Isabelle/HOL machine words can be mapped soundly and efficiently to all target languages despite the differences in the APIs; (ii) they can be used uniformly with the three evaluation engines in Isabelle/HOL, namely code generation, normalisation by evaluation, and term rewriting; and (iii) they blend in with the existing formalisations of machine words. Several large-scale formalisation projects use our library to speed up their generated code.
      To validate the unverified link between machine words in the logic and those in the target languages, we extended Isabelle/HOL with a general-purpose testing facility that compiles test cases expressed within Isabelle/HOL to the four target languages and runs them with the most common implementations of each language. When we applied this to our library of machine words, we discovered miscomputations in the 64-bit word library of one of the target-language implementations.
  9. Andreas Lochbihler and Pascal Stoop: Lazy algebraic types in Isabelle/HOL. In: Isabelle Workshop, 2018.
    • PDF
    • BibTeX
    • Slides
    • Demo
    • Abstract Abstract. This paper presents the tool CodeLazy for Isabelle/HOL. It hooks into Isabelle's code generator such that the generated code evaluates a user-specified set of type constructors lazily, even in target languages with eager evaluation. The lazy type must be algebraic, i.e., values must be built from constructors and a corresponding case operator decomposes them. Every datatype and codatatype is algebraic and thus eligible for lazification.

      Lazification is transparent to the user: definitions, theorems, and the reasoning in HOL need not be changed. Instead, CodeLazy transforms the code equations for functions on lazy types when code is generated. It thus makes code-generation-based Isabelle tools like evaluation and quickcheck available for codatatypes, where eager evaluation frequently causes non-termination. The transformations preserve the code generator's correctness guarantees as they are checked by Isabelle's kernel.
  10. Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, and Dmitriy Traytel: Friends with Benefits: Implementing Corecursion in Foundational Proof Assistants. In: H. Yang (Ed.), Programming Languages and Systems (ESOP 2017), LNCS 10201, pp. 111-140, Springer, 2017.
    • Original article available at springerlink.com
    • Preprint
    • BibTeX
    • Long version
    • Abstract Abstract. We introduce AmiCo, a tool that extends a proof assistant, Isabelle/HOL, with flexible function definitions well beyond primitive corecursion. All definitions are certified by the assistant's inference kernel to guard against inconsistencies. A central notion is that of friends: functions that preserve the productivity of their arguments and that are allowed in corecursive call contexts. As new friends are registered, corecursion benefits by becoming more expressive. We describe this process and its implementation, from the user's specification to the synthesis of a higher-order definition to the registration of a friend. We show some substantial case studies where our approach makes a difference.
  11. Andreas Lochbihler: Effect polymorphism in higher-order logic (proof pearl). In: Cesar Munoz and Mauricio Ayala-Rincon (Eds.): Interactive Theorem Proving (ITP 2017), LNCS 10499, pp. 389-409, Springer, 2017.
    • Original article availabe at springerlink.com
    • Preprint
    • BibTeX
    • Slides
    • Abstract Abstract. The notion of a monad cannot be expressed within higher-order logic (HOL) due to type system restrictions. We show that if a monad is used with values of only one type, this notion can be formalised in HOL. Based on this idea, we develop a library of effect specifications and implementations of monads and monad transformers. Hence, we can abstract over the concrete monad in HOL definitions and thus use the same definition for different (combinations of) effects. We illustrate the usefulness of effect polymorphism with a monadic interpreter.
  12. Julian Biendarra, Jasmin Christian Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondrej Kuncar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, and Dmitriy Traytel. Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. In: Claire Dixon and Marcelo Finger (Eds.): Frontiers of Combining Systems (FroCoS 2017), LNCS 10483, pp. 3-21, Springer, 2017.
    • Original article availabe on springerlink.com
    • Preprint
    • BibTeX
    • Abstract Abstract. We describe a line of work that started in 2011 towards enriching Isabelle/HOL's language with coinductive datatypes, which allow infinite values, and with a more expressive notion of inductive datatype than previously supported by any system based on higher-order logic. These (co)datatypes are complemented by definitional principles for (co)recursive functions and reasoning principles for (co)induction. In contrast with other systems offering codatatypes, no additional axioms or logic extensions are necessary with our approach.
  13. Andreas Lochbihler: Probabilistic Functions and Cryptographic Oracles in Higher-Order Logic. In: Peter Thiemann (Ed.), Programming Languages and Systems (ESOP 2016), LNCS 9632, pp. 503-531, Springer, 2016.
    • Original article available at springerlink.com
    • Preprint
    • BibTeX
    • Slides
    • Sources
    • Abstract Abstract. This paper presents a shallow embedding of a probabilistic functional programming language in higher order logic. The language features monadic sequencing, recursion, random sampling, failures and failure handling, and black-box access to oracles. Oracles are probabilistic functions which maintain hidden state between different invocations. To that end, we propose generative probabilistic systems as the semantic domain in which the operators of the language are de ned. We prove that these operators are parametric and derive a relational program logic for reasoning about programs from parametricity. Several examples demonstrate that our language is suitable for conducting cryptographic proofs.
  14. Andreas Lochbihler and Joshua Schneider: Equational reasoning with applicative functors. In: Jasmin Christian Blanchette and Stefan Merz (Eds.), Interactive Theorem Proving (ITP 2016). LNCS 9807, pp. 252-273, Springer, 2016.
    • Original article available at springerlink.com
    • Preprint
    • BibTeX
    • Slides
    • Abstract Abstract. In reasoning about e ectful computations, it often suces to focus on the effect-free parts. We present a package for automatically lifting equations to effects modelled by applicative functors. It exploits properties of the concrete functor thanks to a modular classification based on combinators. We formalise the meta-theory and demonstrate the usability of our Isabelle/HOL package with two case studies. This is a first step towards practical reasoning with effectful computations.
  15. Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel: Friends with Benefits: Implementing Foundational Corecursion in Isabelle/HOL. In: Isabelle Workshop 2016.
    • PDF
    • BibTeX
    • Demo
    • Abstract Abstract. We describe AmiCo, a tool that extends Isabelle/HOL with flexible function definitions well beyond primitive corecursion. All definitions are certified by the assistant's inference kernel to guard against inconsistencies. A central notion is that of friends: functions that preserve the productivity of their arguments and that may occur in corecursive call contexts. As new friends are registered, corecursion benefits by becoming more expressive.
  16. Andreas Lochbihler and Alexandra Maximova: Stream Fusion for Isabelle's Code Generator (Rough Diamond). In: Christian Urban and Xingyuan Zhang (Eds.), Interactive Theorem Proving (ITP 2015), LNCS 9236, pp. 220-227, Springer, 2015.
    • Original article available at springerlink.com
    • Preprint
    • BibTeX
    • Slides
    • Abstract Abstract. Stream fusion eliminates intermediate lists in functional code. We formalise stream fusion for finite and coinductive lists in Isabelle/HOL and implement the transformation in the code preprocessor. Our initial results show that optimisations during code extraction can boost the performance of the generated code, but the transformation requires further engineering to be usable in practice.
  17. Johannes Hölzl, Andreas Lochbihler, and Dmitriy Traytel: A Formalized Hierarchy of Probabilistic System Types (Proof Pearl). In: Christian Urban and Xingyuan Zhang (Eds.), Interactive Theorem Proving (ITP 2015), LNCS 9236, pp. 203-220, Springer, 2015.
    • Original article availabe at springerlink.com
    • Preprint
    • BibTeX
    • Abstract Abstract. Numerous models of probabilistic systems are studied in the literature. Coalgebra has been used to classify them into system types and compare their expressiveness. In this work, we formalize the resulting hierarchy of probabilistic system types in Isabelle/HOL by modeling the semantics of the different systems as codatatypes. This approach yields simple and concise proofs, as bisimilarity coincides with equality for codatatypes. On the way, we develop libraries of bounded sets and discrete probability distributions and integrate them with the facility for (co)datatype definitions.
  18. Andreas Lochbihler and Johannes Hölzl: Recursive Functions on Lazy Lists via Domains and Topologies. In: Gerwin Klein and Ruben Gamboa (Eds.), Interactive Theorem Proving (ITP 2014), LNCS (LNAI) 8558, pp. 341-357, Springer, 2014.
    • Original article available at springerlink.com
    • Preprint
    • BibTeX
    • Slides
    • Abstract Abstract. The usual definition facilities in theorem provers cannot handle all recursive functions on lazy lists; the filter function is a prime counterexample. We present two new ways of directly de ning functions like filter by exploiting their dual nature as producers and consumers. Borrowing from domain theory and topology, we define them as a least fixpoint (producer view) and as a continuous extension (consumer view). Both constructions yield proof principles that allow elegant proofs. We expect that the approach extends to codatatypes with finite truncations.
  19. Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, and Dmitriy Traytel: Truly Modular (Co)datatypes for Isabelle/HOL. In: Gerwin Klein and Ruben Gamboa (Eds.), Interactive Theorem Proving (ITP 2014), LNCS (LNAI) 8558, pp. 93-110, Spriger, 2014.
    • Original article available at springerlink.com
    • Preprint
    • BibTeX
    • Abstract Abstract. We extended Isabelle/HOL with a pair of definitional commands for datatypes and codatatypes. They support mutual and nested (co)recursion through well-behaved type constructors, including mixed recursion-corecursion, and are complemented by syntaxes for introducing primitively (co)recursive functions and by a general proof method for reasoning coinductively. As a case study, we ported Isabelle's Coinductive library to use the new commands, eliminating the need for tedious ad hoc constructions.
  20. Andreas Lochbihler and Marc Züst: Programming TLS in Isabelle/HOL. In: Isabelle Workshop 2014.
    • PDF
    • BibTeX
    • Slides
    • Abstract Abstract. Isabelle/HOL is not just a theorem prover, it has become a functional programming language. Algebraic datatypes and (pure) recursive functions are defined with various packages and compiled to executable code with the code generator. In this work, we explore whether and how this programming language is suitable for developing applications, which are stateful, interact with the environment, and use external libraries. To that end, we have implemented a prototype of the TLS network protocol as a case study. We present a model of interaction in HOL and its compilation, and discuss on the challenges in application development that the theorem prover/HOL Isabelle poses.
  21. Florian Haftmann, Andreas Lochbihler, and Wolfgang Schreiner: Towards abstract and executable multivariate polynomials in Isabelle. In: Isabelle Workshop 2014.
    • PDF
    • BibTeX
    • Slides
    • Abstract Abstract. This work in progress report envisions a library for multivariate polynomials developed jointly by experts from computer theorem proving (CTP) and computer algebra (CA). The urgency of veri ed algorithms has been recognised in the field of CA, but the cultural gap to CTP is considerable; CA users expect high usability and effciency. This work collects the needs of CA experts and reports on the design of a proof-of-concept prototype in Isabelle/HOL. The CA requirements have not yet been fully settled, and its development is still at an early stage. The authors hope for lively discussions at the Isabelle Workshop.
  22. Andreas Lochbihler: Light-weight containers for Isabelle: efficient, extensible, nestable. In: Sandrine Blazy and Christine Paulin-Mohring and David Pichardie (Eds.), Interactive Theorem Proving (ITP 2013), LNCS 7998, pp. 116--132, Springer, 2013.
    • Original article available at springerlink.com
    • Preprint
    • BibTeX
    • Slides
    • Abstract Abstract. In Isabelle/HOL, we develop an approach to efficiently implement container types such as sets and maps in generated code. Thanks to type classes and refinement during code generation, our light-weight framework is exible, extensible, and easy to use. To support arbitrary nesting of containers, we devise an efficient linear order on sets that can even compare complements and non-complements. Our evaluation shows that it is both efficient and usable.
  23. Andreas Lochbihler: Java and the Java Memory Model -- a Unified, Machine-Checked Formalisation. In: Helmut Seidl (Ed.), Programming Languages and Systems (ESOP 2012), LNCS 7211, pp. 497--517, Springer, March 2012.
    • Original article available at springerlink.com
    • Preprint
    • BibTeX
    • Slides
    • Abstract Abstract. We present a machine-checked formalisation of the Java memory model and connect it to an operational semantics for Java source code and bytecode. This provides the link between sequential semantics and the memory model that has been missing in the literature. Our model extends previous formalisations by dynamic memory allocation, thread spawns and joins, in nite executions, the wait-notify mechanism and thread interruption. We prove the Java data race freedom guarantee for the complete formalisation in a modular way. This work makes the assumptions about the sequential semantics explicit and shows how to discharge them.
    a preliminary version appeard as Karlsruhe Reports in Informatics 2011-34
  24. Andreas Lochbihler and Lukas Bulwahn: Animating the Formalised Semantics of a Java-like Language. In: Marko van Eekelen and Herman Geuvers and Julien Schmalz and Freek Wiedijk (Eds.), Interactive Theorem Proving (ITP 2011), LNCS 6898, pp. 216--232, Springer, 2011.
    • Original article available at springerlink.com
    • Preprint
    • BibTeX
    • Slides
    • Abstract Abstract. Considerable effort has gone into the techniques of extracting executable code from formal specifications and animating them. We show how to apply these techniques to the large JinjaThreads formalisation. It models a substantial subset of multithreaded Java source and bytecode in Isabelle/HOL and focuses on proofs and modularity whereas code generation was of little concern in its design. Employing Isabelle's code generation facilities, we obtain a verified Java interpreter that is sufficiently efficient for running small Java programs. To this end, we present refined implementations for common notions such as the reflexive transitive closure and Russell's definite description operator. From our experience, we distill simple guidelines on how to develop future formalisations with executability in mind.
  25. Peter Lammich and Andreas Lochbihler: The Isabelle Collections Framework. In: Matt Kaufmann and Lawrence C. Paulson (Eds.), Interactive Theorem Proving (ITP 2010), LNCS 6172, pp. 339--354, Springer, July 2010.
    • Original article available at springerlink.com
    • Preprint
    • BibTeX
    • Abstract Abstract. The Isabelle Collections Framework (ICF) provides a unified framework for using verified collection data structures in Isabelle/HOL formalizations and generating efficient functional code in ML, Haskell, and OCaml. Thanks to its modularity, it is easily extensible and supports switching to di erent data structures any time. For good integration with applications, a data refinement approach separates the correctness proofs from implementation details. The generated code based on the ICF lies in better complexity classes than the one that uses Isabelle's default setup (logarithmic vs. linear time). In a case study with tree automata, we demonstrate that the ICF is easy to use and efficient: An ICF based, verified tree automata library outperforms the unverified Timbuk/Taml library by a factor of 14.
  26. Bastian Katz, Marcus Krug, Andreas Lochbihler, Ignaz Rutter, Gregor Snelting, and Dorothea Wagner: Gateway Decompositions for Constrained Reachability Problems. Symposium on Experimental Algorithms (SEA 2010), LNCS 6049, pp. 449--461, Springer, May 2010.
    • Link
    • BibTeX
    • Abstract Abstract. Given a directed graph whose vertices are labeled with propositional constraints, is there a variable assignment that connects two given vertices by a path of vertices that evaluate to true? Constrained reachability is a powerful generalization of reachability and satisfiability problems and a cornerstone problem in program analysis. The key ingredient to tackle these computationally hard problems in large graphs is the efficient construction of a short path condition: A formula whose satisfiability is equivalent to constrained reachability and which can be fed into a state-of-the-art constraint solver.
      In this work, we introduce a new paradigm of decompositions of digraphs with a source and a target, called gateway decompositions. Based on this paradigm, we provide a framework for the modular generation of path conditions and an efficient algorithm to compute a fine-grained gateway decomposition. In benchmarks, we show that especially the combination of our decomposition and a novel arc filtering technique considerably reduces the size of path conditions and the runtime of a standard SAT solver on real-world program dependency graphs.
  27. Andreas Lochbihler: Verifying a Compiler for Java Threads. In: A. D. Gordon (Ed.), European Symposium on Programming (ESOP 2010), LNCS 6012, pp. 427--447, Springer, March 2010.
    • Original article available at springerlink.com
    • Preprint
    • BibTeX
    • Slides
    • Abstract Abstract. A verified compiler is an integral part of every security infrastructure. Previous work has come up with formal semantics for sequential and concurrent variants of Java and has proven the correctness of compilers for the sequential part. This paper presents a rigorous formalisation (in the proof assistant Isabelle/HOL) of concurrent Java source and byte code together with an executable compiler and its correctness proof. It guarantees that the generated byte code shows exactly the same observable behaviour as the semantics for the multithreaded source code.
  28. Andreas Lochbihler: Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL. In: Stefan Berghofer and Tobias Nipkow and Chrsitian Urban and Makarius Wenzel (Eds.), Proceedings of the 22nd International Conference of Theorem Proving in Higher Order Logics (TPHOLs 2009), LNCS 5674, pp. 310--326, Springer, August 2009.
    • Original article available at springerlink.com
    • Preprint
    • BibTeX
    • Slides
    • Abstract Abstract. FinFuns are total functions that are constant except for a finite set of points, i.e. a generalisation of finite maps. We formalise them in Isabelle/HOL and present how to safely set up Isabelle's code generator such that operations like equality testing and quanti cation on FinFuns become executable. On the code output level, FinFuns are explicitly represented by constant functions and pointwise updates, similarly to associative lists. Inside the logic, they behave like ordinary functions with extensionality. Via the update/constant pattern, a recursion combinator and an induction rule for FinFuns allow for de ning and reasoning about operators on FinFuns that directly become executable. We apply the approach to an executable formalisation of sets and use it for the semantics for a subset of concurrent Java.
  29. Daniel Wasserrab and Andreas Lochbihler: Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL. In: Outmane Ait Mohamed and César Muñoz and Sofiène Tahar (Eds.), Proceedings of the 21st International Conference of Theorem Proving in Higher Order Logics (TPHOLs 2008), LNCS 5170, pp. 294--309, Springer, August 2008.
    • Original article available on springerlink.com
    • Preprint
    • BibTeX
    • Slides
    • Abstract Abstract. Slicing is a widely-used technique with applications in e.g. compiler technology and software security. Thus verification of algorithms in these areas is often based on the correctness of slicing, which should ideally be proven independent of concrete programming languages and with the help of well-known verifying techniques such as proof assistants. As a first step in this direction, this contribution presents a framework for dynamic slicing based on control flow and program dependence graphs and machine checked in Isabelle/HOL. Abstracting from concrete syntax we base the framework on a graph representation of the program fulfilling certain structural and well-formedness properties.
  30. Andreas Lochbihler: Type Safe Nondeterminism - A Formal Semantics of Java Threads. International Workshop on Foundations of Object-Oriented Languages (FOOL 2008), January 2008.
    • PDF
    • BibTeX
    • Slides
    • Abstract Abstract. We present a generic framework to transform a single-threaded operational semantics into a semantics with interleaved execution of threads. Threads can be dynamically created and use locks for synchronisation. They can suspend themselves, be notied by other threads again, and interact via shared memory. We formalised this in the proof assistant Isabelle/HOL along with theorems to carry type safety proofs for the instantiating semantics (progress and preservation in the style of Wright and Felleisen) over to the multithreaded case, thereby investigating the role of deadlocks and giving an explicit formalisation for them. We apply this framework to the Java thread model using an extension of the Jinja source code semantics to have type safety for multithreaded Java machinechecked. The Java Memory Model is not included.
  31. Andreas Lochbihler and Gregor Snelting: On Temporal Path Conditions in Dependence Graphs. In: 7th IEEE Working Conference on Source Code Analysis and Manipulation (SCAM 2007), pp. 49--58, IEEE, September 2007.
    • Link
    • Preprint
    • BibTeX
    • Slides
    • Abstract Abstract. Program dependence graphs are a well-established device to represent possible information flow in a program. Path conditions in dependence graphs have been proposed to express more detailed circumstances of a particular flow; they provide precise necessary conditions for information flow along a path or chop in a dependence graph. Ordinary boolean path conditions however cannot express temporal properties, e.g. that for a specific flow it is necessary that some condition holds, and later another specific condition holds.
      In this contribution, we introduce temporal path conditions, which extend ordinary path conditions by temporal operators in order to express temporal dependencies between conditions for a flow. We present motivating examples, generation and simplication rules, application of model checking to generate witnesses for a specific flow, and a case study. We prove the following soundness property: if a temporal path condition for a path is satisfiable, then the ordinary boolean path condition for the path is satisfiable. The converse does not hold, indicating that temporal path conditions are more precise.

Further Technical Reports ↥

  1. Andreas Lochbihler and S. Reza Sefidgar: A tutorial introduction to CryptHOL. Cryptology ePrint Archive, Report 2018/941, 2018.
    • Link
    • BibTeX
    • Abstract Abstract. This tutorial demonstrates how cryptographic security notions, constructions, and game-based security proofs can be formalized using the CryptHOL framework. As a running example, we formalize a variant of the hash-based ElGamal encryption scheme and its IND-CPA security in the random oracle model. This tutorial assumes familiarity with Isabelle/HOL basics and standard cryptographic terminology.

Theses ↥

Archive of Formal Proofs ↥

  1. Andreas Lochbihler and S. Reza Sefidgar Constructive Cryptography in HOL: the Communication Modeling Aspect. Archive of Formal Proofs, March 2021.
  2. Andreas Lochbihler and Ognjen Maric Authenticated Data Structures As Functors. Archive of Formal Proofs, April 2020.
  3. David Butler and Andreas Lochbihler Sigma Protocols and Commitment Schemes. Archive of Formal Proofs, October 2019.
  4. Andreas Lochbihler and S. Reza Sefidgar Constructive Cryptography in HOL. Archive of Formal Proofs, December 2018.
  5. Andreas Lochbihler and Joshua Schneider Bounded Natural Functors with Covariance and Contravariance. Archive of Formal Proofs, April 2018.
  6. Andreas Lochbihler: Probabilistic while loop. Archive of Formal Proofs, May 2017.
  7. Joshua Schneider, Manuel Eberl, and Andreas Lochbihler: Monad normalisation. Archive of Formal Proofs, May 2017.
  8. Andreas Lochbihler: Effect polymorphism in higher-order logic. Archive of Formal Proofs, May 2017.
  9. Andreas Lochbihler: CryptHOL. Archive of Formal Proofs, May 2017.
  10. Andreas Lochbihler, S. Reza Sefidgar, and Bhargav Bhatt: Game-based cryptography in HOL. Archive of Formal Proofs, May 2017.
  11. Andreas Lochbihler: A formal proof of the max-flow min-cut theorem for countable networks. Archive of Formal Proofs, May 2016.
  12. Johannes Hölzl, Andreas Lochbihler, and Dmitriy Traytel: A Zoo of Probabilistic Systems. Archive of Formal Proofs, May 2015.
  13. Andreas Lochbihler and Joshua Schneider: Applicative Lifting. Archive of Formal Proofs, December 2015.
  14. Peter Gammie and Andreas Lochbihler: The Stern-Brocot Tree. Archive of Formal Proofs, December 2015.
  15. Andreas Lochbihler and Tobias Nipkow: Trie. Archive of Formal Proofs, March 2015.
  16. Andreas Lochbihler and Alexandra Maximova: Stream Fusion in HOL with Code Generation. Archive of Formal Proofs, October 2014.
  17. Andreas Lochbihler: Light-weight Containers. Archive of Formal Proofs, April 2013.
  18. Andreas Lochbihler: Native Word. Archive of Formal Proofs, September 2013.
  19. Andreas Lochbihler: Coinductive. Archive of Formal Proofs, February 2010.
  20. Andreas Lochbihler: Code Generation for Functions as Data. Archive of Formal Proofs, May 2009.
  21. Andreas Lochbihler: Jinja With Threads. Archive of Formal Proofs, December 2007.

Posters, tutorials, blog posts, and further talks ↥

  1. A semantic domain for privacy-aware smart contracts and interoperable sharded ledgers. CPP Lightning talk, January 2021.
  2. DAML and Canton: Enterprise Haskell on Distributed Ledger Technology. PLFM guest lecture, May 2020, HSR Rapperswil, Rapperswil, Switzerland.
  3. A structured semantic domain for smart contracts. CSF poster session, June 2019, Hoboken, NJ, USA.
  4. Isabelle meets compilers. LLVM meetup Zurich, September 2018, Zurich, Switzerland.
  5. How difficult is it to write correct smart contracts? Depends on your tools!. Blog post, August 2018.
  6. Mechanising a type-safe model of multithreaded Java with a veri ed compiler. Festkolloquium in honour of Tobias Nipkow, July 2018, TU Munich, Germany.
  7. Programming and Reasoning with Infinite Data in Isabelle/HOL. POPL tutorial, January 2018, Los Angeles, CA, USA.
  8. Conditional Parametricity in Isabelle/HOL. TABLEAUX/FroCoS/ITP poster session, September 2017, Brasila, Brazil.
  9. CryptHOL - Game-Based Cryptographic Proofs in Higher-Order Logic. Proof Assistants and Related Tools, September 2017, Kopenhagen, Denmark.
  10. Certified Functional (Co)programming with Isabelle/HOL. ICFP tutorial, September 2017, Oxford, UK.
  11. Functional programming and proving in Isabelle/HOL. HaskellerZ meetup, April 2017, Zurich, Switzerland.
  12. Certified Functional (Co)programming with Isabelle/HOL. CADE tutorial, August 2016, Gothenburg, Sweden.
  13. Making the Java Memory Model Safe. Dagstuhl seminar 16201, May 2016, Dagstuhl.
  14. Quis custodiet ipsos custodes: The Java memory model. RS3 annual meeting, October 2012, Munich.
  15. Animating the Formalised Semantics of a Java-Like Language. GI FG Deduction annual meeting, October 2011, Karlsruhe.
  16. Quis custodiet ipsos custodes. RS3 annual meeting, October 2011, Karlsruhe.
  17. A unified machine-checked model for multithreaded Java. Multi-Core Memory Models and Concurrency Theory, January 2011, Schloss Dagstuhl.
  18. KESS - Die Komplexität evolutionär stabiler Strategien. Institute for Statistics and Decision Support Systems, University of Vienna, November 2008.

Software ↥

Canton
An interoperability protocol for DAML-based distributed ledgers
Isabelle formalisations
My Isabelle formalisations are published in the Archive of Formal Proofs
Java2Jinja
An Eclipse plugin, converts Java programs to JinjaThreads syntax and provides a front-end to the JinjaThreads compiler, interpreter, and VM.

Teaching ↥

Lectures and Exercise Classes

Theses

I have (co-)supervised the following Bachelor's and Master's theses.

Supervised PhD students

Contact

Dr. Andreas Lochbihler
Neunbrunnenstrasse 31
8050 Zürich
mail@andreas-lochbihler.de