Christoph Sprenger

CoRR, 2024

The Sumcheck Protocol.

[BibT_eX]

[DOI]

Azucena Garvía Bosshard

Jonathan Bootle

Arch. Formal Proofs, 2024

2023

IsaNet: A framework for verifying secure data plane protocols.

[BibT_eX]

[DOI]

Tobias Klenze

J. Comput. Secur., 2023

Sound Verification of Security Protocols: From Design to Interoperable Implementations.

[BibT_eX]

[DOI]

Proceedings of the 44th IEEE Symposium on Security and Privacy, 2023

2022

Sound Verification of Security Protocols: From Design to Interoperable Implementations (extended version).

[BibT_eX]

[DOI]

CoRR, 2022

IsaNet: Formalization of a Verification Framework for Secure Data Plane Protocols.

[BibT_eX]

[DOI]

Tobias Klenze

Arch. Formal Proofs, 2022

N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures.

[BibT_eX]

[DOI]

Proceedings of the 35th IEEE Computer Security Foundations Symposium, 2022

2021

Formal Verification of Secure Forwarding Protocols.

[BibT_eX]

[DOI]

Tobias Klenze

Proceedings of the 34th IEEE Computer Security Foundations Symposium, 2021

2020

Igloo: soundly linking compositional refinement and separation logic for distributed system verification.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2020

EPIC: Every Packet Is Checked in the Data Plane of a Path-Aware Internet.

[BibT_eX]

[DOI]

Proceedings of the 29th USENIX Security Symposium, 2020

SoK: Delegation and Revocation, the Missing Links in the Web's Chain of Trust.

[BibT_eX]

[DOI]

Proceedings of the IEEE European Symposium on Security and Privacy, 2020

2019

Proxy Certificates: The Missing Link in the Web's Chain of Trust.

[BibT_eX]

[DOI]

CoRR, 2019

2018

Refining security protocols.

[BibT_eX]

[DOI]

J. Comput. Secur., 2018

Abstractions for security protocol verification.

[BibT_eX]

[DOI]

Thanh Binh Nguyen

Cas Cremers

J. Comput. Secur., 2018

2017

Developing Security Protocols by Refinement.

[BibT_eX]

[DOI]

Ivano Somaini

Arch. Formal Proofs, 2017

Refining Authenticated Key Agreement with Strong Adversaries.

[BibT_eX]

[DOI]

Joseph Lallemand

Arch. Formal Proofs, 2017

Refining Authenticated Key Agreement with Strong Adversaries.

[BibT_eX]

[DOI]

Joseph Lallemand

Proceedings of the 2017 IEEE European Symposium on Security and Privacy, 2017

Cutoff Bounds for Consensus Algorithms.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 29th International Conference, 2017

2015

Consensus Refined.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2015

Abstractions for Security Protocol Verification.

[BibT_eX]

[DOI]

Thanh Binh Nguyen

Proceedings of the Principles of Security and Trust - 4th International Conference, 2015

Consensus Refined.

[BibT_eX]

[DOI]

Proceedings of the 45th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, 2015

2014

Verification of a Transactional Memory Manager under Hardware Failures and Restarts.

[BibT_eX]

[DOI]

Proceedings of the FM 2014: Formal Methods, 2014

2013

Sound Security Protocol Transformations.

[BibT_eX]

[DOI]

Thanh Binh Nguyen

Proceedings of the Principles of Security and Trust - Second International Conference, 2013

2012

Refining Key Establishment.

[BibT_eX]

[DOI]

Proceedings of the 25th IEEE Computer Security Foundations Symposium, 2012

2010

Developing security protocols by refinement.

[BibT_eX]

[DOI]

Proceedings of the 17th ACM Conference on Computer and Communications Security, 2010

2008

Compositional verification of sequential programs with procedures.

[BibT_eX]

[DOI]

Dilian Gurov

Marieke Huisman

Inf. Comput., 2008

Cryptographically-Sound Protocol-Model Abstractions.

[BibT_eX]

[DOI]

Proceedings of the 21st IEEE Computer Security Foundations Symposium, 2008

2007

A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

2006

Cryptographically Sound Theorem Proving.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2006

2004

Compositional verification for secure loading of smart card applets.

[BibT_eX]

[DOI]

Dilian Gurov

Marieke Huisman

Proceedings of the 2nd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2004), 2004

Checking Absence of Illicit Applet Interactions: A Case Study.

[BibT_eX]

[DOI]

Proceedings of the Fundamental Approaches to Software Engineering, 2004

2003

On global induction mechanisms in a µ-calculus with explicit approximations.

[BibT_eX]

[DOI]

Mads Dam

RAIRO Theor. Informatics Appl., 2003

A Verification Methodology for Infinite-State Message Passing Systems.

[BibT_eX]

[DOI]

Krzysztof Worytkiewicz

Proceedings of the 1st ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2003), 2003

On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the µ-Calculus.

[BibT_eX]

[DOI]

Mads Dam

Proceedings of the Foundations of Software Science and Computational Structures, 2003

2002

A note on global induction in a mu-calculus with explicit approximations.

[BibT_eX]

Mads Dam

Proceedings of the Fixed Points in Computer Science, 2002

1998

A Verified Model Checker for the Modal µ-calculus in Coq.

[BibT_eX]

[DOI]