David A. Basin

Orcid: 0000-0003-2952-939X

Affiliations:
  • ETH Zurich, Switzerland


According to our database1, David A. Basin authored at least 313 papers between 1988 and 2024.

Collaborative distances:

Awards

ACM Fellow

ACM Fellow 2018, "For contributions to Information Security and Formal Methods".

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Model-driven Privacy.
Proc. Priv. Enhancing Technol., January, 2024

User-Controlled Privacy: Taint, Track, and Control.
Proc. Priv. Enhancing Technol., January, 2024

SOAP: A Social Authentication Protocol.
CoRR, 2024

2023
Locality-Sensitive Hashing Does Not Guarantee Privacy! Attacks on Google's FLoC and the MinHash Hierarchy System.
Proc. Priv. Enhancing Technol., October, 2023

Efficient Black-box Checking of Snapshot Isolation in Databases.
Proc. VLDB Endow., 2023

Efficient Evaluation of Arbitrary Relational Calculus Queries.
Log. Methods Comput. Sci., 2023

IsaNet: A framework for verifying secure data plane protocols.
J. Comput. Secur., 2023

FABRID: Flexible Attestation-Based Routing for Inter-Domain Networks.
Proceedings of the 32nd USENIX Security Symposium, 2023

Inducing Authentication Failures to Bypass Credit Card PINs.
Proceedings of the 32nd USENIX Security Symposium, 2023

Determining an Economic Value of High Assurance for Commodity Software Security.
Proceedings of the Security Protocols XXVIII, 2023

Sound Verification of Security Protocols: From Design to Interoperable Implementations.
Proceedings of the 44th IEEE Symposium on Security and Privacy, 2023

A Formal Framework for End-to-End DNS Resolution.
Proceedings of the ACM SIGCOMM 2023 Conference, 2023

RHINE: Robust and High-performance Internet Naming with E2E Authenticity.
Proceedings of the 20th USENIX Symposium on Networked Systems Design and Implementation, 2023

Monitoring the Internet Computer.
Proceedings of the Formal Methods - 25th International Symposium, 2023

Enforcing the GDPR.
Proceedings of the Computer Security - ESORICS 2023, 2023

ADEM: An Authentic Digital EMblem.
Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security, 2023

Is Modeling Access Control Worth It?
Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security, 2023

Correct and Efficient Policy Monitoring, a Retrospective.
Proceedings of the Automated Technology for Verification and Analysis, 2023

Formal Methods for Payment Protocols.
Proceedings of the 2023 ACM Asia Conference on Computer and Communications Security, 2023

SealClub: Computer-aided Paper Document Authentication.
Proceedings of the Annual Computer Security Applications Conference, 2023

2022
The Complete Guide to SCION - From Design Principles to Formal Verification
Information Security and Cryptography, Springer, ISBN: 978-3-031-05288-0, 2022

Checking Websites' GDPR Consent Compliance for Marketing Emails.
Proc. Priv. Enhancing Technol., 2022

Bridging the semantic gap between qualitative and quantitative models of distributed systems.
Proc. ACM Program. Lang., 2022

Tamarin: Verification of Large-Scale, Real-World, Cryptographic Protocols.
IEEE Secur. Priv., 2022

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

SealClub: Computer-aided Paper Document Authentication.
CoRR, 2022

IFCIL: An Information Flow Configuration Language for SELinux (Extended Version).
CoRR, 2022

Automating Cookie Consent and GDPR Violation Detection.
Proceedings of the 31st USENIX Security Symposium, 2022


Practical Relational Calculus Query Evaluation.
Proceedings of the 25th International Conference on Database Theory, 2022

Real-Time Policy Enforcement with Metric First-Order Temporal Logic.
Proceedings of the Computer Security - ESORICS 2022, 2022

N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures.
Proceedings of the 35th IEEE Computer Security Foundations Symposium, 2022

DPL: A Language for GDPR Enforcement.
Proceedings of the 35th IEEE Computer Security Foundations Symposium, 2022

IFCIL: An Information Flow Configuration Language for SELinux.
Proceedings of the 35th IEEE Computer Security Foundations Symposium, 2022

"I'm Surprised So Much Is Connected".
Proceedings of the CHI '22: CHI Conference on Human Factors in Computing Systems, New Orleans, LA, USA, 29 April 2022, 2022

2021
Scalable online first-order monitoring.
Int. J. Softw. Tools Technol. Transf., 2021

A comprehensive formal analysis of 5G handover.
Proceedings of the WiSec '21: 14th ACM Conference on Security and Privacy in Wireless and Mobile Networks, Abu Dhabi, United Arab Emirates, 28 June, 2021

Card Brand Mixup Attack: Bypassing the PIN in non-Visa Cards by Using Them for Visa Transactions.
Proceedings of the 30th USENIX Security Symposium, 2021

The EMV Standard: Break, Fix, Verify.
Proceedings of the 42nd IEEE Symposium on Security and Privacy, 2021

Formal Verification of Secure Forwarding Protocols.
Proceedings of the 34th IEEE Computer Security Foundations Symposium, 2021

Abstract Modeling of System Communication in Constructive Cryptography using CryptHOL.
Proceedings of the 34th IEEE Computer Security Foundations Symposium, 2021

Verifying Table-Based Elections.
Proceedings of the CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security, Virtual Event, Republic of Korea, November 15, 2021

2020
Runtime Verification over Out-of-order Streams.
ACM Trans. Comput. Log., 2020

Igloo: soundly linking compositional refinement and separation logic for distributed system verification.
Proc. ACM Program. Lang., 2020

CryptHOL: Game-Based Proofs in Higher-Order Logic.
J. Cryptol., 2020

Natural Projection as Partial Model Checking.
J. Autom. Reason., 2020

Fixing the Achilles Heel of E-Voting: The Bulletin Board.
IACR Cryptol. ePrint Arch., 2020

Decentralized Privacy-Preserving Proximity Tracing.
IEEE Data Eng. Bull., 2020

A Theory of Black-Box Tests.
CoRR, 2020

Decentralized Privacy-Preserving Proximity Tracing.
CoRR, 2020

Internet backbones in space.
Comput. Commun. Rev., 2020

A Spectral Analysis of Noise: A Comprehensive, Automated, Formal Analysis of Diffie-Hellman Protocols.
Proceedings of the 29th USENIX Security Symposium, 2020

Scalable Online Monitoring of Distributed Systems.
Proceedings of the Runtime Verification - 20th International Conference, 2020

SoK: Delegation and Revocation, the Missing Links in the Web's Chain of Trust.
Proceedings of the IEEE European Symposium on Security and Privacy, 2020

Dispute Resolution in Voting.
Proceedings of the 33rd IEEE Computer Security Foundations Symposium, 2020

Privacy-Preserving OpenID Connect.
Proceedings of the ASIA CCS '20: The 15th ACM Asia Conference on Computer and Communications Security, 2020

A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic.
Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

Multi-head Monitoring of Metric Dynamic Logic.
Proceedings of the Automated Technology for Verification and Analysis, 2020

2019
Cardinality Estimators do not Preserve Privacy.
Proc. Priv. Enhancing Technol., 2019

Almost event-rate independent monitoring.
Formal Methods Syst. Des., 2019

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

A Formally Verified Monitor for Metric First-Order Temporal Logic.
Proceedings of the Runtime Verification - 19th International Conference, 2019

From Nondeterministic to Multi-Head Deterministic Finite-State Transducers.
Proceedings of the 46th International Colloquium on Automata, Languages, and Programming, 2019

Information-Flow Control for Database-Backed Applications.
Proceedings of the IEEE European Symposium on Security and Privacy, 2019

Monitoring the GDPR.
Proceedings of the Computer Security - ESORICS 2019, 2019

Formalizing Constructive Cryptography using CryptHOL.
Proceedings of the 32nd IEEE Computer Security Foundations Symposium, 2019

User Account Access Graphs.
Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, 2019

The Next 700 Policy Miners: A Universal Method for Building Policy Miners.
Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, 2019

Symbolic Analysis of Identity-Based Protocols.
Proceedings of the Foundations of Security, Protocols, and Equational Reasoning, 2019

Multi-head Monitoring of Metric Temporal Logic.
Proceedings of the Automated Technology for Verification and Analysis, 2019

Adaptive Online First-Order Monitoring.
Proceedings of the Automated Technology for Verification and Analysis, 2019

2018
Model Checking Security Protocols.
Proceedings of the Handbook of Model Checking., 2018

Design, Analysis, and Implementation of ARPKI: An Attack-Resilient Public-Key Infrastructure.
IEEE Trans. Dependable Secur. Comput., 2018

Refining security protocols.
J. Comput. Secur., 2018

Algorithms for monitoring real-time properties.
Acta Informatica, 2018

From Natural Projection to Partial Model Checking and Back.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

Networking in Heaven as on Earth.
Proceedings of the 17th ACM Workshop on Hot Topics in Networks, 2018

On Purpose and by Necessity: Compliance Under the GDPR.
Proceedings of the Financial Cryptography and Data Security, 2018

Mining ABAC Rules from Sparse Logs.
Proceedings of the 2018 IEEE European Symposium on Security and Privacy, 2018

Alethea: A Provably Secure Random Sample Voting Protocol.
Proceedings of the 31st IEEE Computer Security Foundations Symposium, 2018

A Formal Analysis of 5G Authentication.
Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, 2018

Optimal Proofs for Linear Temporal Logic on Lasso Words.
Proceedings of the Automated Technology for Verification and Analysis, 2018

2017
Symbolically analyzing security protocols using tamarin.
ACM SIGLOG News, 2017

Election Security and Economics: It's All About Eve.
Proceedings of the Electronic Voting - Second International Joint Conference, 2017

Almost Event-Rate Independent Monitoring of Metric Temporal Logic.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

The MonPoly Monitoring Tool.
Proceedings of the RV-CuBES 2017. An International Workshop on Competitions, 2017

AERIAL: Almost Event-Rate Independent Algorithms for Monitoring Metric Regular Properties.
Proceedings of the RV-CuBES 2017. An International Workshop on Competitions, 2017

Almost Event-Rate Independent Monitoring of Metric Dynamic Logic.
Proceedings of the Runtime Verification - 17th International Conference, 2017

Test execution checkpointing for web applications.
Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, Santa Barbara, CA, USA, July 10, 2017

Refining Authenticated Key Agreement with Strong Adversaries.
Proceedings of the 2017 IEEE European Symposium on Security and Privacy, 2017

Securing Databases from Probabilistic Inference.
Proceedings of the 30th IEEE Computer Security Foundations Symposium, 2017

Cutoff Bounds for Consensus Algorithms.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017

Runtime Verification of Temporal Properties over Out-of-Order Data Streams.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017

Tests and Refutation.
Proceedings of the Automated Technology for Verification and Analysis, 2017

2016
Large-scale system development using Abstract Data Types and refinement.
Sci. Comput. Program., 2016

Scalable offline monitoring of temporal specifications.
Formal Methods Syst. Des., 2016

Exploring Website Location as a Security Indicator.
CoRR, 2016

Strong and Provably Secure Database Access Control.
Proceedings of the IEEE European Symposium on Security and Privacy, 2016

Security Testing Beyond Functional Tests.
Proceedings of the Engineering Secure Software and Systems - 8th International Symposium, 2016

Access Control Synthesis for Physical Spaces.
Proceedings of the IEEE 29th Computer Security Foundations Symposium, 2016

Modeling Human Errors in Security Protocols.
Proceedings of the IEEE 29th Computer Security Foundations Symposium, 2016

In the Nick of Time: Proactive Prevention of Obligation Violations.
Proceedings of the IEEE 29th Computer Security Foundations Symposium, 2016

2015
Monitoring Metric First-Order Temporal Properties.
J. ACM, 2015

Greedily computing associative aggregations on sliding windows.
Inf. Process. Lett., 2015

Improving the Security of Cryptographic Protocol Standards.
IEEE Secur. Priv., 2015

Monitoring of temporal first-order properties with aggregations.
Formal Methods Syst. Des., 2015

Semantic Vacuity.
Proceedings of the 22nd International Symposium on Temporal Representation and Reasoning, 2015

Failure-aware Runtime Verification of Distributed Systems.
Proceedings of the 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, 2015

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

Analyzing First-Order Role Based Access Control.
Proceedings of the IEEE 28th Computer Security Foundations Symposium, 2015

A Complete Characterization of Secure Human-Server Communication.
Proceedings of the IEEE 28th Computer Security Foundations Symposium, 2015

Automated Symbolic Proofs of Observational Equivalence.
Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, 2015

Alice and Bob Meet Equational Theories.
Proceedings of the Logic, Rewriting, and Concurrency, 2015

2014
Model-Driven Development of a Secure eHealth Application.
Proceedings of the Engineering Secure Future Internet Services and Systems, 2014

A Model-Driven Methodology for Developing Secure Data-Management Applications.
IEEE Trans. Software Eng., 2014

Know Your Enemy: Compromising Adversaries in Protocol Analysis.
ACM Trans. Inf. Syst. Secur., 2014

Optimal Security-Aware Query Processing.
Proc. VLDB Endow., 2014

Obstruction-free authorization enforcement: Aligning security and business objectives.
J. Comput. Secur., 2014

LTL is closed under topological closure.
Inf. Process. Lett., 2014

Deciding safety and liveness in TPTL.
Inf. Process. Lett., 2014

On Secure Data Deletion.
IEEE Secur. Priv., 2014

Short paper: detection of GPS spoofing attacks in power grids.
Proceedings of the 7th ACM Conference on Security & Privacy in Wireless and Mobile Networks, 2014

Automated Verification of Group Key Agreement Protocols.
Proceedings of the 2014 IEEE Symposium on Security and Privacy, 2014

On Real-Time Monitoring with Imprecise Timestamps.
Proceedings of the Runtime Verification - 5th International Conference, 2014

Scalable Offline Monitoring.
Proceedings of the Runtime Verification - 5th International Conference, 2014

Decentralized Composite Access Control.
Proceedings of the Principles of Security and Trust - Third International Conference, 2014

Code Generation for Event-B.
Proceedings of the Integrated Formal Methods - 11th International Conference, 2014

Anchored LTL separation.
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2014

Actor Key Compromise: Consequences and Countermeasures.
Proceedings of the IEEE 27th Computer Security Foundations Symposium, 2014

Fail-Secure Access Control.
Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, 2014

ARPKI: Attack Resilient Public-Key Infrastructure.
Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, 2014

Formal System Modelling Using Abstract Data Types in Event-B.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2014

2013
Monitoring Data Usage in Distributed Systems.
IEEE Trans. Software Eng., 2013

Predictable Mobile Routing for Spacecraft Networks.
IEEE Trans. Mob. Comput., 2013

Role Mining with Probabilistic Models.
ACM Trans. Inf. Syst. Secur., 2013

Enforceable Security Policies Revisited.
ACM Trans. Inf. Syst. Secur., 2013

Efficient construction of machine-checked symbolic protocol security proofs.
J. Comput. Secur., 2013

Provably repairing the ISO/IEC 9798 standard for entity authentication.
J. Comput. Secur., 2013

SoK: Secure Data Deletion.
Proceedings of the 2013 IEEE Symposium on Security and Privacy, 2013

Semi-valid input coverage for fuzz testing.
Proceedings of the International Symposium on Software Testing and Analysis, 2013

Symbolic Probabilistic Analysis of Off-Line Guessing.
Proceedings of the Computer Security - ESORICS 2013, 2013

Secure data deletion from persistent media.
Proceedings of the 2013 ACM SIGSAC Conference on Computer and Communications Security, 2013

The TAMARIN Prover for the Symbolic Analysis of Security Protocols.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013

Technology Transfer.
Proceedings of the Industrial Deployment of System Engineering Methods, 2013

2012
Dynamic enforcement of abstract separation of duty constraints.
ACM Trans. Inf. Syst. Secur., 2012

Multi-Assignment Clustering for Boolean Data.
J. Mach. Learn. Res., 2012

Abstract Data Types in Event-B - An Application of Generic Instantiation
CoRR, 2012

The research value of publishing attacks.
Commun. ACM, 2012

Data Node Encrypted File System: Efficient Secure Deletion for Flash Memory.
Proceedings of the 21th USENIX Security Symposium, Bellevue, WA, USA, August 8-10, 2012, 2012

Optimal workflow-aware authorizations.
Proceedings of the 17th ACM Symposium on Access Control Models and Technologies, 2012

Monitoring Compliance Policies over Incomplete and Disagreeing Logs.
Proceedings of the Runtime Verification, Third International Conference, 2012

SECFUZZ: Fuzz-testing security protocols.
Proceedings of the 7th International Workshop on Automation of Software Test, 2012

Refining Key Establishment.
Proceedings of the 25th IEEE Computer Security Foundations Symposium, 2012

Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties.
Proceedings of the 25th IEEE Computer Security Foundations Symposium, 2012

User-level secure deletion on log-structured file systems.
Proceedings of the 7th ACM Symposium on Information, Compuer and Communications Security, 2012

2011
Formal Reasoning about Physical Properties of Security Protocols.
ACM Trans. Inf. Syst. Secur., 2011

Distributed temporal logic for the analysis of security protocol models.
Theor. Comput. Sci., 2011

Automatically deriving information-theoretic bounds for adaptive side-channel attacks.
J. Comput. Secur., 2011

Secure Deletion on Log-structured File Systems
CoRR, 2011

Monitoring Usage-Control Policies in Distributed Systems.
Proceedings of the Eighteenth International Symposium on Temporal Representation and Reasoning, 2011

A decade of model-driven security.
Proceedings of the 16th ACM Symposium on Access Control Models and Technologies, 2011

MONPOLY: Monitoring Usage-Control Policies.
Proceedings of the Runtime Verification - Second International Conference, 2011

FAST: An Efficient Decision Procedure for Deduction and Static Equivalence.
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, 2011

Constructing Mid-Points for Two-Party Asynchronous Protocols.
Proceedings of the Principles of Distributed Systems - 15th International Conference, 2011

Model-Driven Development of Security-Aware GUIs for Data-Centric Applications.
Proceedings of the Foundations of Security Analysis and Design VI, 2011

Obstruction-Free Authorization Enforcement: Aligning Security with Business Objectives.
Proceedings of the 24th IEEE Computer Security Foundations Symposium, 2011

Separation of duties as a service.
Proceedings of the 6th ACM Symposium on Information, Computer and Communications Security, 2011

Applied Information Security - a Hands-on Approach.
Springer, ISBN: 978-3-642-24473-5, 2011

2010
Efficient analysis of pattern-based constraint specifications.
Softw. Syst. Model., 2010

Constraint differentiation: Search-space reduction for the constraint-based analysis of security protocols.
J. Comput. Secur., 2010

On the definition of role mining.
Proceedings of the 15th ACM Symposium on Access Control Models and Technologies, 2010

Monitoring security policies with metric first-order temporal logic.
Proceedings of the 15th ACM Symposium on Access Control Models and Technologies, 2010

Efficient Decision Procedures for Message Deducibility and Static Equivalence.
Proceedings of the Formal Aspects of Security and Trust - 7th International Workshop, 2010

SSG: a model-based development environment for smart, security-aware GUIs.
Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, 2010

How to Evaluate the Security of Real-Life Cryptographic Protocols? - The Cases of ISO/IEC 29128 and CRYPTREC.
Proceedings of the Financial Cryptography and Data Security, 2010

Automatic Generation of Smart, Security-Aware GUI Models.
Proceedings of the Engineering Secure Software and Systems, Second International Symposium, 2010

Modeling and Analyzing Security in the Presence of Compromising Adversaries.
Proceedings of the Computer Security, 2010

Degrees of Security: Protocol Guarantees in the Face of Compromising Adversaries.
Proceedings of the Computer Science Logic, 24th International Workshop, 2010

Impossibility Results for Secret Establishment.
Proceedings of the 23rd IEEE Computer Security Foundations Symposium, 2010

Strong Invariants for the Efficient Construction of Machine-Checked Protocol Security Proofs.
Proceedings of the 23rd IEEE Computer Security Foundations Symposium, 2010

Developing security protocols by refinement.
Proceedings of the 17th ACM Conference on Computer and Communications Security, 2010

Policy Monitoring in First-Order Temporal Logic.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

Keeping data secret under full compromise using porter devices.
Proceedings of the Twenty-Sixth Annual Computer Security Applications Conference, 2010

2009
Developing topology discovery in Event-B.
Sci. Comput. Program., 2009

Labelled Tableaux for Distributed Temporal Logic.
J. Log. Comput., 2009

Automated analysis of security-design models.
Inf. Softw. Technol., 2009

From Dolev-Yao to Strong Adaptive Corruption: Analyzing Security in the Presence of Compromising Adversaries.
IACR Cryptol. ePrint Arch., 2009

Let's Get Physical: Models and Methods for Real-World Security Protocols.
Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

Modeling and Verifying Physical Properties of Security Protocols for Wireless Networks.
Proceedings of the 22nd IEEE Computer Security Foundations Symposium, 2009

A probabilistic approach to hybrid role mining.
Proceedings of the 2009 ACM Conference on Computer and Communications Security, 2009

2008
SSL/TLS Session-Aware User Authentication.
Computer, 2008

SSL/TLS session-aware user authentication revisited.
Comput. Secur., 2008

Secure neighborhood discovery: a fundamental element for mobile ad hoc networking.
IEEE Commun. Mag., 2008

Two approaches to an information security laboratory.
Commun. ACM, 2008

A Labeled Tableaux Systemfor the Distributed Temporal Logic DTL.
Proceedings of the 15th International Symposium on Temporal Representation and Reasoning, 2008

Topology dynamics and routing for predictable mobile networks.
Proceedings of the 16th annual IEEE International Conference on Network Protocols, 2008

Runtime Monitoring of Metric First-order Temporal Properties.
Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2008

Cryptographically-Sound Protocol-Model Abstractions.
Proceedings of the 21st IEEE Computer Security Foundations Symposium, 2008

Mechanisms for usage control.
Proceedings of the 2008 ACM Symposium on Information, Computer and Communications Security, 2008

A class of probabilistic models for role engineering.
Proceedings of the 2008 ACM Conference on Computer and Communications Security, 2008

2007
Preface.
J. Comput. Secur., 2007

Verifying a signature architecture: a comparative case study.
Formal Aspects Comput., 2007

Securing the Distribution and Storage of Secrets with Trusted Platform Modules.
Proceedings of the Information Security Theory and Practices. Smart Cards, 2007

A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols.
Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

A Metamodel-Based Approach for Analyzing Security-Design Models.
Proceedings of the Model Driven Engineering Languages and Systems, 2007

A Proof of Concept Implementation of SSL/TLS Session-Aware User Authentication (TLS-SA).
Proceedings of the Kommunikation in Verteilten Systemen (KiVS), 2007

Monitors for Usage Control.
Proceedings of the Trust Management, 2007

A Policy Language for Distributed Usage Control.
Proceedings of the Computer Security, 2007

An information-theoretic model for adaptive side-channel attacks.
Proceedings of the 2007 ACM Conference on Computer and Communications Security, 2007

Specifying and analyzing security automata using CSP-OZ.
Proceedings of the 2007 ACM Symposium on Information, Computer and Communications Security, 2007

BAP: Broadcast Authentication Using Cryptographic Puzzles.
Proceedings of the Applied Cryptography and Network Security, 5th International Conference, 2007

Midpoints Versus Endpoints: From Protocols to Firewalls.
Proceedings of the Applied Cryptography and Network Security, 5th International Conference, 2007

2006
Model driven security: From UML models to access control infrastructures.
ACM Trans. Softw. Eng. Methodol., 2006

On the semantics of Alice&Bob specifications of security protocols.
Theor. Comput. Sci., 2006

Automated Reasoning for Security Protocol Analysis.
J. Autom. Reason., 2006

Cryptographically Sound Theorem Proving.
IACR Cryptol. ePrint Arch., 2006

SSL/TLS session-aware user authentication - Or how to effectively thwart the man-in-the-middle.
Comput. Commun., 2006

Distributed usage control.
Commun. ACM, 2006

Formalizing and Analyzing Sender Invariance.
Proceedings of the Formal Aspects in Security and Trust, Fourth International Workshop, 2006

Controlling Access to Documents: A Formal Access Control Model.
Proceedings of the Emerging Trends in Information and Communication Security, 2006

Timing-Sensitive Information Flow Analysis for Synchronous Systems.
Proceedings of the Computer Security, 2006

Model Driven Security.
Proceedings of the The First International Conference on Availability, 2006

2005
Konflikt oder Review zwei Ansätze für Labors in angewandter Informationssicherheit.
Inform. Spektrum, 2005

OFMC: A symbolic model checker for security protocols.
Int. J. Inf. Sec., 2005

Relating Strand Spaces and Distributed Temporal Logic for Security Protocol Analysis.
Log. J. IGPL, 2005

Deconstructing Alice and Bob.
Proceedings of the Second Workshop on Automated Reasoning for Security Protocol Analysis, 2005

Firewall Conformance Testing.
Proceedings of the Testing of Communicating Systems, 2005

Algebraic Intruder Deductions.
Proceedings of the Logic for Programming, 2005

Verification of a Signature Architecture with HOL-Z.
Proceedings of the FM 2005: Formal Methods, 2005

On Obligations.
Proceedings of the Computer Security, 2005

The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

Rippling - meta-level guidance for mathematical reasoning.
Cambridge tracts in theoretical computer science 56, Cambridge University Press, ISBN: 978-0-521-83449-0, 2005

2004
Reflective metalogical frameworks.
ACM Trans. Comput. Log., 2004

Editorial.
High. Order Symb. Comput., 2004

Metareasoning about Security Protocols using Distributed Temporal Logic.
Proceedings of the Workshop on Automated Reasoning for Security Protocol Analysis, 2004

Synthesis of Programs in Computational Logic.
Proceedings of the Program Development in Computational Logic: A Decade of Research Advances in Logic-Based Program Development, 2004

2003
Decision procedures for inductive Boolean functions based on alternating automata.
Theor. Comput. Sci., 2003

Bytecode Verification by Model Checking.
J. Autom. Reason., 2003

A Formal Analysis of a Digital Signature Architecture.
Proceedings of the Integrity and Internal Control in Information Systems VI, 2003

Model driven security for process-oriented systems.
Proceedings of the 8th ACM Symposium on Access Control Models and Technologies, 2003

An On-the-Fly Model-Checker for Security Protocol Analysis.
Proceedings of the Computer Security, 2003

CDiff: a new reduction technique for constraint-based analysis of security protocols.
Proceedings of the 10th ACM Conference on Computer and Communications Security, 2003

2002
A Formal Analysis of the CORBA Security Service.
Proceedings of the ZB 2002: Formal Specification and Development in Z and B, 2002

SecureUML: A UML-Based Modeling Language for Model-Driven Security.
Proceedings of the UML 2002 - The Unified Modeling Language, 5th International Conference, Dresden, Germany, September 30, 2002

Verified Bytecode Model Checkers.
Proceedings of the Theorem Proving in Higher Order Logics, 15th International Conference, 2002

Bytecode Model Checking: An Experimental Analysis.
Proceedings of the Model Checking of Software, 2002

QUBOS: Deciding Quantified Boolean Logic Using Propositional Satisfiability Solvers.
Proceedings of the Formal Methods in Computer-Aided Design, 4th International Conference, 2002

The Next 700 Synthesis Calculi.
Proceedings of the FME 2002: Formal Methods, 2002

The AVISS Security Protocol Analysis Tool.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002

2001
A theoretical and empirical investigation of search in imperfect information games.
Theor. Comput. Sci., 2001

A Higher-order Interpretation of Deductive Tableau.
J. Symb. Comput., 2001

Current Trends in Logical Frameworks and Metalanguages.
J. Autom. Reason., 2001

Automated complexity analysis based on ordered resolution.
J. ACM, 2001

Towards an awareness-based semantics for security protocol analysis.
Proceedings of the Logical Aspects of Cryptographic Protocol Verification, 2001

A formal data-model of the CORBA security service.
Proceedings of the 8th European Software Engineering Conference held jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering 2001, 2001

2000
Program Development Schemata as Derived Rules.
J. Symb. Comput., 2000

Structuring Metatheory on Inductive Definitions.
Inf. Comput., 2000

Maude versus Haskell: an Experimental Comparison in Security Protocol Analysis.
Proceedings of the 3rd International Workshop on Rewriting Logic and its Applications, 2000

Rewriting Logic as a Metalogical Framework.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 2000

B2M: A Semantic Based Tool for BLIF Hardware Descriptions.
Proceedings of the Formal Methods in Computer-Aided Design, Third International Conference, 2000

Bounded Model Construction for Monadic Second-Order Logics.
Proceedings of the Computer Aided Verification, 12th International Conference, 2000

Combining Knowledge and Search to Solve Single-Suit Bridge.
Proceedings of the Seventeenth National Conference on Artificial Intelligence and Twelfth Conference on on Innovative Applications of Artificial Intelligence, July 30, 2000

1999
Formalization of the Development Process.
Proceedings of the Algebraic Foundations of Systems Specification, 1999

Modeling a Hardware Synthesis Methodology in Isabelle.
Formal Methods Syst. Des., 1999

Structural and Behavioral Modeling with Monadic Logics.
Proceedings of the 29th IEEE International Symposium on Multiple-Valued Logic, 1999

Lazy Infinite-State Analysis of Security Protocols.
Proceedings of the Secure Networking - CQRE (Secure) '99, International Exhibition and Congress Düsseldorf, Germany, November 30, 1999

Java Bytecode Verification by Model Checking.
Proceedings of the Computer Aided Verification, 11th International Conference, 1999

1998
Natural Deduction for Non-Classical Logics.
Stud Logica, 1998

Labelled Modal Logics: Quantifiers.
J. Log. Lang. Inf., 1998

Search in Games with Incomplete Information: A Case Study Using Bridge Card Play.
J. Int. Comput. Games Assoc., 1998

Scoped metatheorems.
Proceedings of the 1998 International Workshop on Rewriting Logic and its Applications, 1998

Logical-Framework-Based Program Development.
ACM Comput. Surv., 1998

A Recipe for the Complexity Analysis of Non-Classical Logics.
Proceedings of the Frontiers of Combining Systems, Second International Workshop, 1998

Combining WS1S and HOL.
Proceedings of the Frontiers of Combining Systems, Second International Workshop, 1998

Optimal Play against Best Defence: Complexity and Heuristics.
Proceedings of the Computers and Games, First International Conference, 1998

Finding Optimal Strategies for Imperfect Information Games.
Proceedings of the Fifteenth National Conference on Artificial Intelligence and Tenth Innovative Applications of Artificial Intelligence Conference, 1998

1997
Labelled Propositional Modal Logics: Theory and Practice.
J. Log. Comput., 1997

Labelled Quantified Modal Logics.
Proceedings of the KI-97: Advances in Artificial Intelligence, 1997

A New Method for Bounding the Complexity of Modal Logics.
Proceedings of the Computational Logic and Proof Theory, 5th Kurt Gödel Colloquium, 1997

LISA: A Specification Language Based on WS2S.
Proceedings of the Computer Science Logic, 11th International Workshop, 1997

1996
Adding Metatheoretic Facilities to First-Order Theories.
J. Log. Comput., 1996

Middle-Out Reasoning for Synthesis and Induction.
J. Autom. Reason., 1996

A Calculus for and Termination of Rippling.
J. Autom. Reason., 1996

Generic System Support for Deductive Program Development.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1996

Complexity Analysis Based on Ordered Resolution.
Proceedings of the Proceedings, 1996

Implementing Modal and Relevance Logics in a Logical Framework.
Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning (KR'96), 1996

A Topography of Labelled Modal Logics.
Proceedings of the Frontiers of Combining Systems, 1996

Experiments in Automating Hardware Verification Using Inductive Proof Planning.
Proceedings of the Formal Methods in Computer-Aided Design, First International Conference, 1996

1995
Hardware Verification using Monadic Second-Order Logic.
Proceedings of the Computer Aided Verification, 1995

Deriving and Applying Logic Program Transformers.
Proceedings of the Algorithms, 1995

1994
A Term Equality Problem Equivalent to Graph Isomorphism.
Inf. Process. Lett., 1994

Generalized Rewriting in Type Theory.
J. Inf. Process. Cybern., 1994

Logic Frameworks for Logic Programs.
Proceedings of the Logic Programming Synthesis and Transformation, 1994

IsaWhelk Interpreted in Isabelle.
Proceedings of the Logic Programming, 1994

Coloured Rippling: An Extension of a Theorem Proving Heuristic.
Proceedings of the Eleventh European Conference on Artificial Intelligence, 1994

A Calculus for Rippling.
Proceedings of the Conditional and Typed Rewriting Systems, 4th International Workshop, 1994

Termination Orderings for Rippling.
Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

1993
A Recursion Planning Analysis of Inductive Completion.
Ann. Math. Artif. Intell., 1993

A Framework for Program Development Based on Schematic Proof.
Proceedings of the 7th International Workshop on Software Specification and Design, 1993

Difference Unification.
Proceedings of the 13th International Joint Conference on Artificial Intelligence. Chambéry, France, August 28, 1993

Middle-Out Reasoning for Logic Program Synthesis.
Proceedings of the Logic Programming, 1993

A Conservative Extension of First-order Logic and Its Application to Theorem Proving.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1993

1992
Logic Program Synthesis via Proof Planning.
Proceedings of the Logic Program Synthesis and Transformation, 1992

An Adaptation of Proof-Planning to Declarer Play in Bridge.
Proceedings of the 10th European Conference on Artificial Intelligence, 1992

Difference Matching.
Proceedings of the Automated Deduction, 1992

1991
Formally verified synthesis of combinational CMOS circuits.
Integr., 1991

Some Normalization Properties of Martin-Löf's Type Theory, and Applications.
Proceedings of the Theoretical Aspects of Computer Software, 1991

Automating Meta-Theory Creation and System Extension.
Proceedings of the Trends in Artificial Intelligence, 1991

1990
Building Problem Solving Environments in Constructive Type Theory.
PhD thesis, 1990

Equality of Terms Containing Associative-Commutative Functions and Commutative Binding Operators in Isomorphism Complete.
Proceedings of the 10th International Conference on Automated Deduction, 1990

1989
Verification Of Combinational Logic in Nuprl.
Proceedings of the Hardware Specification, 1989

Building Theories in Nuprl.
Proceedings of the Logic at Botik '89, 1989

1988
An Environment For Automated Reasoning About Partial Functions.
Proceedings of the 9th International Conference on Automated Deduction, 1988


  Loading...