Computer Science/Security

Logging-independent Message Anonymity in the Relational Method
by Pasquale Noce

CoSMeDis: A confidentiality-verified distributed social media platform
by Thomas Bauereiss and Andrei Popescu

CoSMed: A confidentiality-verified social media platform
by Thomas Bauereiss and Andrei Popescu

Compositional BD Security
by Thomas Bauereiss and Andrei Popescu

CoCon: A Confidentiality-Verified Conference Management System
by Andrei Popescu, Peter Lammich and Thomas Bauereiss

Information Flow Control via Dependency Tracking
by Benedikt Nordhoff

Constructive Cryptography in HOL: the Communication Modeling Aspect
by Andreas Lochbihler and S. Reza Sefidgar

The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols
by Pasquale Noce

Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems
by Florian Kammüller

Stateful Protocol Composition and Typing
by Andreas V. Hess, Sebastian Mödersheim and Achim D. Brucker

Automated Stateful Protocol Verification
by Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker and Anders Schlichtkrull

An Under-Approximate Relational Logic
by Toby Murray

Sigma Protocols and Commitment Schemes
by David Butler and Andreas Lochbihler

Formalization of Generic Authenticated Data Structures
by Matthias Brun and Dmitriy Traytel

Multi-Party Computation
by David Aspinall and David Butler

Constructive Cryptography in HOL
by Andreas Lochbihler and S. Reza Sefidgar

An Isabelle/HOL Formalization of the Modular Assembly Kit for Security Properties
by Oliver Bračevac, Richard Gay, Sylvia Grewe, Heiko Mantel, Henning Sudbrock and Markus Tasch

Developing Security Protocols by Refinement
by Christoph Sprenger and Ivano Somaini

Game-based cryptography in HOL
by Andreas Lochbihler, S. Reza Sefidgar and Bhargav Bhatt

CryptHOL
by Andreas Lochbihler

The Group Law for Elliptic Curves
by Stefan Berghofer

Refining Authenticated Key Agreement with Strong Adversaries
by Joseph Lallemand and Christoph Sprenger

Formal Network Models and Their Application to Firewall Policies
by Achim D. Brucker, Lukas Brügger and Burkhart Wolff

Verification of a Diffie-Hellman Password-based Authentication Protocol by Extending the Inductive Method
by Pasquale Noce

A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor
by Zhe Hou, David Sanan, Alwen Tiu and Yang Liu

Compositional Security-Preserving Refinement for Concurrent Imperative Programs
by Toby Murray, Robert Sison, Edward Pierzchalski and Christine Rizkallah

A Dependent Security Type System for Concurrent Imperative Programs
by Toby Murray, Robert Sison, Edward Pierzchalski and Christine Rizkallah

Conservation of CSP Noninterference Security under Concurrent Composition
by Pasquale Noce

Conservation of CSP Noninterference Security under Sequential Composition
by Pasquale Noce

The Inductive Unwinding Theorem for CSP Noninterference Security
by Pasquale Noce

The Ipurge Unwinding Theorem for CSP Noninterference Security
by Pasquale Noce

The Generic Unwinding Theorem for CSP Noninterference Security
by Pasquale Noce

The Unified Policy Framework (UPF)
by Achim D. Brucker, Lukas Brügger and Burkhart Wolff

Formal Specification of a Generic Separation Kernel
by Freek Verbeek, Sergey Tverdyshev, Oto Havle, Holger Blasum, Bruno Langenstein, Werner Stephan, Yakoub Nemouchi, Abderrahmane Feliachi, Burkhart Wolff and Julien Schmaltz

Network Security Policy Verification
by Cornelius Diekmann

Noninterference Security in Communicating Sequential Processes
by Pasquale Noce

A Formalization of Strong Security
by Sylvia Grewe, Alexander Lux, Heiko Mantel and Jens Sauer

A Formalization of Declassification with WHAT-and-WHERE-Security
by Sylvia Grewe, Alexander Lux, Heiko Mantel and Jens Sauer

A Formalization of Assumptions and Guarantees for Compositional Noninterference
by Sylvia Grewe, Heiko Mantel and Daniel Schoepe

Bounded-Deducibility Security
by Andrei Popescu, Peter Lammich and Thomas Bauereiss

A shallow embedding of HyperCTL*
by Markus N. Rabe, Peter Lammich and Andrei Popescu

Probabilistic Noninterference
by Andrei Popescu and Johannes Hölzl

Compositional Properties of Crypto-Based Components
by Maria Spichkova

Possibilistic Noninterference
by Andrei Popescu and Johannes Hölzl

Inductive Study of Confidentiality
by Giampaolo Bella

Inter-Procedural Information Flow Noninterference via Slicing
by Daniel Wasserrab

Information Flow Noninterference via Slicing
by Daniel Wasserrab

Secure information flow and program logics
by Lennart Beringer and Martin Hofmann

A Correctness Proof for the Volpano/Smith Security Typing System
by Gregor Snelting and Daniel Wasserrab

Hotel Key Card System
by Tobias Nipkow

SHA1, RSA, PSS and more
by Christina Lindenberg and Kai Wirt