David A. Basin

Jorge Toro-Pozo

Proceedings of the 30th USENIX Security Symposium, 2021

The EMV Standard: Break, Fix, Verify.

[BibT_eX]

[DOI]

Jorge Toro-Pozo

Proceedings of the 42nd IEEE Symposium on Security and Privacy, 2021

Formal Verification of Secure Forwarding Protocols.

[BibT_eX]

[DOI]

Tobias Klenze

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

Abstract Modeling of System Communication in Constructive Cryptography using CryptHOL.

[BibT_eX]

[DOI]

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

Verifying Table-Based Elections.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2020

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

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2020

CryptHOL: Game-Based Proofs in Higher-Order Logic.

[BibT_eX]

[DOI]

Andreas Lochbihler

S. Reza Sefidgar

J. Cryptol., 2020

Natural Projection as Partial Model Checking.

[BibT_eX]

[DOI]

J. Autom. Reason., 2020

Fixing the Achilles Heel of E-Voting: The Bulletin Board.

[BibT_eX]

[DOI]

Lucca Hirschi

IACR Cryptol. ePrint Arch., 2020

Decentralized Privacy-Preserving Proximity Tracing.

[BibT_eX]

[DOI]

IEEE Data Eng. Bull., 2020

A Theory of Black-Box Tests.

[BibT_eX]

[DOI]

CoRR, 2020

Decentralized Privacy-Preserving Proximity Tracing.

[BibT_eX]

[DOI]

CoRR, 2020

Internet backbones in space.

[BibT_eX]

[DOI]

Comput. Commun. Rev., 2020

Scalable Online Monitoring of Distributed Systems.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification - 20th International Conference, 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

Dispute Resolution in Voting.

[BibT_eX]

[DOI]

Proceedings of the 33rd IEEE Computer Security Foundations Symposium, 2020

Privacy-Preserving OpenID Connect.

[BibT_eX]

[DOI]

Sven Hammann

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.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

Multi-head Monitoring of Metric Dynamic Logic.

[BibT_eX]

[DOI]

Martin Raszyk

Proceedings of the Automated Technology for Verification and Analysis, 2020

2019

Cardinality Estimators do not Preserve Privacy.

[BibT_eX]

[DOI]

Damien Desfontaines

Andreas Lochbihler

Proc. Priv. Enhancing Technol., 2019

Almost event-rate independent monitoring.

[BibT_eX]

[DOI]

Bhargav Nagaraja Bhatt

Srdan Krstic

Formal Methods Syst. Des., 2019

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

[BibT_eX]

[DOI]

CoRR, 2019

A Formally Verified Monitor for Metric First-Order Temporal Logic.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification - 19th International Conference, 2019

From Nondeterministic to Multi-Head Deterministic Finite-State Transducers.

[BibT_eX]

[DOI]

Martin Raszyk

Proceedings of the 46th International Colloquium on Automata, Languages, and Programming, 2019

Information-Flow Control for Database-Backed Applications.

[BibT_eX]

[DOI]

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

Monitoring the GDPR.

[BibT_eX]

[DOI]

Emma Arfelt

Søren Debois

Proceedings of the Computer Security - ESORICS 2019, 2019

Formalizing Constructive Cryptography using CryptHOL.

[BibT_eX]

[DOI]

Proceedings of the 32nd IEEE Computer Security Foundations Symposium, 2019

User Account Access Graphs.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, 2019

Symbolic Analysis of Identity-Based Protocols.

[BibT_eX]

[DOI]

Lucca Hirschi

Proceedings of the Foundations of Security, Protocols, and Equational Reasoning, 2019

Multi-head Monitoring of Metric Temporal Logic.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2019

Adaptive Online First-Order Monitoring.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2019

2018

Model Checking Security Protocols.

[BibT_eX]

[DOI]

Catherine Meadows

Proceedings of the Handbook of Model Checking., 2018

Design, Analysis, and Implementation of ARPKI: An Attack-Resilient Public-Key Infrastructure.

[BibT_eX]

[DOI]

IEEE Trans. Dependable Secur. Comput., 2018

Refining security protocols.

[BibT_eX]

[DOI]

J. Comput. Secur., 2018

Algorithms for monitoring real-time properties.

[BibT_eX]

[DOI]

Acta Informatica, 2018

From Natural Projection to Partial Model Checking and Back.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

Networking in Heaven as on Earth.

[BibT_eX]

[DOI]

Proceedings of the 17th ACM Workshop on Hot Topics in Networks, 2018

On Purpose and by Necessity: Compliance Under the GDPR.

[BibT_eX]

[DOI]

Søren Debois

Thomas T. Hildebrandt

Proceedings of the Financial Cryptography and Data Security, 2018

Mining ABAC Rules from Sparse Logs.

[BibT_eX]

[DOI]

Carlos Cotrini

Thilo Weghorn

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

Alethea: A Provably Secure Random Sample Voting Protocol.

[BibT_eX]

[DOI]

Proceedings of the 31st IEEE Computer Security Foundations Symposium, 2018

A Formal Analysis of 5G Authentication.

[BibT_eX]

[DOI]

Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, 2018

Optimal Proofs for Linear Temporal Logic on Lasso Words.

[BibT_eX]

[DOI]

Bhargav Nagaraja Bhatt

Proceedings of the Automated Technology for Verification and Analysis, 2018

2017

Symbolically analyzing security protocols using tamarin.

[BibT_eX]

[DOI]

ACM SIGLOG News, 2017

Election Security and Economics: It's All About Eve.

[BibT_eX]

[DOI]

Proceedings of the Electronic Voting - Second International Joint Conference, 2017

Almost Event-Rate Independent Monitoring of Metric Temporal Logic.

[BibT_eX]

[DOI]

Bhargav Nagaraja Bhatt

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

The MonPoly Monitoring Tool.

[BibT_eX]

[DOI]

Proceedings of the RV-CuBES 2017. An International Workshop on Competitions, 2017

AERIAL: Almost Event-Rate Independent Algorithms for Monitoring Metric Regular Properties.

[BibT_eX]

[DOI]

Srdjan Krstic

Proceedings of the RV-CuBES 2017. An International Workshop on Competitions, 2017

Almost Event-Rate Independent Monitoring of Metric Dynamic Logic.

[BibT_eX]

[DOI]

Srdan Krstic

Proceedings of the Runtime Verification - 17th International Conference, 2017

Test execution checkpointing for web applications.

[BibT_eX]

[DOI]

Tristan Buchs

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.

[BibT_eX]

[DOI]

Joseph Lallemand

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

Securing Databases from Probabilistic Inference.

[BibT_eX]

[DOI]

Proceedings of the 30th IEEE Computer Security Foundations Symposium, 2017

Cutoff Bounds for Consensus Algorithms.

[BibT_eX]

[DOI]

Ognjen Maric

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

Runtime Verification of Temporal Properties over Out-of-Order Data Streams.

[BibT_eX]

[DOI]

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

Tests and Refutation.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2017

2016

Large-scale system development using Abstract Data Types and refinement.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2016

Scalable offline monitoring of temporal specifications.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2016

Exploring Website Location as a Security Indicator.

[BibT_eX]

[DOI]

CoRR, 2016

Strong and Provably Secure Database Access Control.

[BibT_eX]

[DOI]

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

Security Testing Beyond Functional Tests.

[BibT_eX]

[DOI]

Proceedings of the Engineering Secure Software and Systems - 8th International Symposium, 2016

Access Control Synthesis for Physical Spaces.

[BibT_eX]

[DOI]

Proceedings of the IEEE 29th Computer Security Foundations Symposium, 2016

Modeling Human Errors in Security Protocols.

[BibT_eX]

[DOI]

Proceedings of the IEEE 29th Computer Security Foundations Symposium, 2016

In the Nick of Time: Proactive Prevention of Obligation Violations.

[BibT_eX]

[DOI]

Søren Debois

Thomas T. Hildebrandt

Proceedings of the IEEE 29th Computer Security Foundations Symposium, 2016

2015

Monitoring Metric First-Order Temporal Properties.

[BibT_eX]

[DOI]

J. ACM, 2015

Greedily computing associative aggregations on sliding windows.

[BibT_eX]

[DOI]

Inf. Process. Lett., 2015

Improving the Security of Cryptographic Protocol Standards.

[BibT_eX]

[DOI]

IEEE Secur. Priv., 2015

Monitoring of temporal first-order properties with aggregations.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2015

Semantic Vacuity.

[BibT_eX]

[DOI]

Grgur Petric Maretic

Muhammad Torabi Dashti

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

Failure-aware Runtime Verification of Distributed Systems.

[BibT_eX]

[DOI]

Proceedings of the 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, 2015

Consensus Refined.

[BibT_eX]

[DOI]

Ognjen Maric

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

Analyzing First-Order Role Based Access Control.

[BibT_eX]

[DOI]

Carlos Cotrini Jiménez

Thilo Weghorn

Proceedings of the IEEE 28th Computer Security Foundations Symposium, 2015

A Complete Characterization of Secure Human-Server Communication.

[BibT_eX]

[DOI]

Michael Schläpfer

Proceedings of the IEEE 28th Computer Security Foundations Symposium, 2015

Automated Symbolic Proofs of Observational Equivalence.

[BibT_eX]

[DOI]

Jannik Dreier

Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, 2015

Alice and Bob Meet Equational Theories.

[BibT_eX]

[DOI]

Proceedings of the Logic, Rewriting, and Concurrency, 2015

2014

Model-Driven Development of a Secure eHealth Application.

[BibT_eX]

[DOI]

Carolina Dania

Proceedings of the Engineering Secure Future Internet Services and Systems, 2014

A Model-Driven Methodology for Developing Secure Data-Management Applications.

[BibT_eX]

[DOI]

Marina Egea

Carolina Dania

IEEE Trans. Software Eng., 2014

Know Your Enemy: Compromising Adversaries in Protocol Analysis.

[BibT_eX]

[DOI]

ACM Trans. Inf. Syst. Secur., 2014

Optimal Security-Aware Query Processing.

[BibT_eX]

[DOI]

Proc. VLDB Endow., 2014

Obstruction-free authorization enforcement: Aligning security and business objectives.

[BibT_eX]

[DOI]

J. Comput. Secur., 2014

LTL is closed under topological closure.

[BibT_eX]

[DOI]

Grgur Petric Maretic

Inf. Process. Lett., 2014

Deciding safety and liveness in TPTL.

[BibT_eX]

[DOI]

Carlos Cotrini Jiménez

Inf. Process. Lett., 2014

On Secure Data Deletion.

[BibT_eX]

[DOI]

Joel Reardon

IEEE Secur. Priv., 2014

Short paper: detection of GPS spoofing attacks in power grids.

[BibT_eX]

[DOI]

Proceedings of the 7th ACM Conference on Security & Privacy in Wireless and Mobile Networks, 2014

Automated Verification of Group Key Agreement Protocols.

[BibT_eX]

[DOI]

Proceedings of the 2014 IEEE Symposium on Security and Privacy, 2014

On Real-Time Monitoring with Imprecise Timestamps.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification - 5th International Conference, 2014

Scalable Offline Monitoring.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification - 5th International Conference, 2014

Decentralized Composite Access Control.

[BibT_eX]

[DOI]

Proceedings of the Principles of Security and Trust - Third International Conference, 2014

Code Generation for Event-B.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods - 11th International Conference, 2014

Anchored LTL separation.

[BibT_eX]

[DOI]

Grgur Petric Maretic

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.

[BibT_eX]

[DOI]

Marko Horvat

Proceedings of the IEEE 27th Computer Security Foundations Symposium, 2014

Fail-Secure Access Control.

[BibT_eX]

[DOI]

Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, 2014

ARPKI: Attack Resilient Public-Key Infrastructure.

[BibT_eX]

[DOI]

Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, 2014

Formal System Modelling Using Abstract Data Types in Event-B.

[BibT_eX]

[DOI]

Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2014

2013

Monitoring Data Usage in Distributed Systems.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 2013

Predictable Mobile Routing for Spacecraft Networks.

[BibT_eX]

[DOI]

IEEE Trans. Mob. Comput., 2013

Role Mining with Probabilistic Models.

[BibT_eX]

[DOI]

Mario Frank

Joachim M. Buhmann

ACM Trans. Inf. Syst. Secur., 2013

Enforceable Security Policies Revisited.

[BibT_eX]

[DOI]

ACM Trans. Inf. Syst. Secur., 2013

Efficient construction of machine-checked symbolic protocol security proofs.

[BibT_eX]

[DOI]

Simon Meier

J. Comput. Secur., 2013

Provably repairing the ISO/IEC 9798 standard for entity authentication.

[BibT_eX]

[DOI]

Simon Meier

J. Comput. Secur., 2013

SoK: Secure Data Deletion.

[BibT_eX]

[DOI]

Joel Reardon

Proceedings of the 2013 IEEE Symposium on Security and Privacy, 2013

Semi-valid input coverage for fuzz testing.

[BibT_eX]

[DOI]

Proceedings of the International Symposium on Software Testing and Analysis, 2013

Symbolic Probabilistic Analysis of Off-Line Guessing.

[BibT_eX]

[DOI]

Bruno Conchinha

Proceedings of the Computer Security - ESORICS 2013, 2013

Secure data deletion from persistent media.

[BibT_eX]

[DOI]

Proceedings of the 2013 ACM SIGSAC Conference on Computer and Communications Security, 2013

The TAMARIN Prover for the Symbolic Analysis of Security Protocols.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

Technology Transfer.

[BibT_eX]

[DOI]

Thai Son Hoang

Proceedings of the Industrial Deployment of System Engineering Methods, 2013

2012

Dynamic enforcement of abstract separation of duty constraints.

[BibT_eX]

[DOI]

ACM Trans. Inf. Syst. Secur., 2012

Multi-Assignment Clustering for Boolean Data.

[BibT_eX]

[DOI]

J. Mach. Learn. Res., 2012

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

[BibT_eX]

[DOI]

CoRR, 2012

The research value of publishing attacks.

[BibT_eX]

[DOI]

Commun. ACM, 2012

Data Node Encrypted File System: Efficient Secure Deletion for Flash Memory.

[BibT_eX]

[DOI]

Joel Reardon

Proceedings of the 21th USENIX Security Symposium, Bellevue, WA, USA, August 8-10, 2012, 2012

Optimal workflow-aware authorizations.

[BibT_eX]

[DOI]

Proceedings of the 17th ACM Symposium on Access Control Models and Technologies, 2012

Monitoring Compliance Policies over Incomplete and Disagreeing Logs.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification, Third International Conference, 2012

SECFUZZ: Fuzz-testing security protocols.

[BibT_eX]

[DOI]

Proceedings of the 7th International Workshop on Automation of Software Test, 2012

Refining Key Establishment.

[BibT_eX]

[DOI]

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

Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties.

[BibT_eX]

[DOI]

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

User-level secure deletion on log-structured file systems.

[BibT_eX]

[DOI]

Proceedings of the 7th ACM Symposium on Information, Compuer and Communications Security, 2012

2011

Formal Reasoning about Physical Properties of Security Protocols.

[BibT_eX]

[DOI]

ACM Trans. Inf. Syst. Secur., 2011

Distributed temporal logic for the analysis of security protocol models.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2011

Automatically deriving information-theoretic bounds for adaptive side-channel attacks.

[BibT_eX]

[DOI]

Boris Köpf

J. Comput. Secur., 2011

Secure Deletion on Log-structured File Systems

[BibT_eX]

[DOI]

CoRR, 2011

Monitoring Usage-Control Policies in Distributed Systems.

[BibT_eX]

[DOI]

Proceedings of the Eighteenth International Symposium on Temporal Representation and Reasoning, 2011

A decade of model-driven security.

[BibT_eX]

[DOI]

Marina Egea

Proceedings of the 16th ACM Symposium on Access Control Models and Technologies, 2011

MONPOLY: Monitoring Usage-Control Policies.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification - Second International Conference, 2011

FAST: An Efficient Decision Procedure for Deduction and Static Equivalence.

[BibT_eX]

[DOI]

Bruno Conchinha

Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, 2011

Constructing Mid-Points for Two-Party Asynchronous Protocols.

[BibT_eX]

[DOI]

Proceedings of the Principles of Distributed Systems - 15th International Conference, 2011

Model-Driven Development of Security-Aware GUIs for Data-Centric Applications.

[BibT_eX]

[DOI]

Marina Egea

Carolina Dania

Gonzalo Ortiz

Javier Valdazo

Proceedings of the Foundations of Security Analysis and Design VI, 2011

Obstruction-Free Authorization Enforcement: Aligning Security with Business Objectives.

[BibT_eX]

[DOI]

Proceedings of the 24th IEEE Computer Security Foundations Symposium, 2011

Separation of duties as a service.

[BibT_eX]

[DOI]

Proceedings of the 6th ACM Symposium on Information, Computer and Communications Security, 2011

Applied Information Security - a Hands-on Approach.

[BibT_eX]

[DOI]

Patrick Schaller

Michael Schläpfer

Springer, ISBN: 978-3-642-24473-5, 2011

2010

Efficient analysis of pattern-based constraint specifications.

[BibT_eX]

[DOI]

Softw. Syst. Model., 2010

Constraint differentiation: Search-space reduction for the constraint-based analysis of security protocols.

[BibT_eX]

[DOI]

J. Comput. Secur., 2010

On the definition of role mining.

[BibT_eX]

[DOI]

Mario Frank

Joachim M. Buhmann

Proceedings of the 15th ACM Symposium on Access Control Models and Technologies, 2010

Monitoring security policies with metric first-order temporal logic.

[BibT_eX]

[DOI]

Samuel Müller

Proceedings of the 15th ACM Symposium on Access Control Models and Technologies, 2010

Efficient Decision Procedures for Message Deducibility and Static Equivalence.

[BibT_eX]

[DOI]

Bruno Conchinha

Proceedings of the Formal Aspects of Security and Trust - 7th International Workshop, 2010

SSG: a model-based development environment for smart, security-aware GUIs.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the Financial Cryptography and Data Security, 2010

Automatic Generation of Smart, Security-Aware GUI Models.

[BibT_eX]

[DOI]

Proceedings of the Engineering Secure Software and Systems, Second International Symposium, 2010

Modeling and Analyzing Security in the Presence of Compromising Adversaries.

[BibT_eX]

[DOI]

Proceedings of the Computer Security, 2010

Degrees of Security: Protocol Guarantees in the Face of Compromising Adversaries.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 24th International Workshop, 2010

Impossibility Results for Secret Establishment.

[BibT_eX]

[DOI]

Benedikt Schmidt

Patrick Schaller

Proceedings of the 23rd IEEE Computer Security Foundations Symposium, 2010

Strong Invariants for the Efficient Construction of Machine-Checked Protocol Security Proofs.

[BibT_eX]

[DOI]

Simon Meier

Proceedings of the 23rd IEEE Computer Security Foundations Symposium, 2010

Developing security protocols by refinement.

[BibT_eX]

[DOI]

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

Policy Monitoring in First-Order Temporal Logic.

[BibT_eX]

[DOI]

Samuel Müller

Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

Keeping data secret under full compromise using porter devices.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Sixth Annual Computer Security Applications Conference, 2010

2009

Developing topology discovery in Event-B.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2009

Labelled Tableaux for Distributed Temporal Logic.

[BibT_eX]

[DOI]

J. Log. Comput., 2009

Automated analysis of security-design models.

[BibT_eX]

[DOI]

Inf. Softw. Technol., 2009

From Dolev-Yao to Strong Adaptive Corruption: Analyzing Security in the Presence of Compromising Adversaries.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2009

Let's Get Physical: Models and Methods for Real-World Security Protocols.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

Modeling and Verifying Physical Properties of Security Protocols for Wireless Networks.

[BibT_eX]

[DOI]

Proceedings of the 22nd IEEE Computer Security Foundations Symposium, 2009

A probabilistic approach to hybrid role mining.

[BibT_eX]

[DOI]

Proceedings of the 2009 ACM Conference on Computer and Communications Security, 2009

2008

SSL/TLS Session-Aware User Authentication.

[BibT_eX]

[DOI]

Rolf Oppliger

Ralf Hauser

Computer, 2008

SSL/TLS session-aware user authentication revisited.

[BibT_eX]

[DOI]

Rolf Oppliger

Ralf Hauser

Comput. Secur., 2008

Secure neighborhood discovery: a fundamental element for mobile ad hoc networking.

[BibT_eX]

[DOI]

IEEE Commun. Mag., 2008

Two approaches to an information security laboratory.

[BibT_eX]

[DOI]

Michael Näf

Commun. ACM, 2008

A Labeled Tableaux Systemfor the Distributed Temporal Logic DTL.

[BibT_eX]

[DOI]

Proceedings of the 15th International Symposium on Temporal Representation and Reasoning, 2008

Topology dynamics and routing for predictable mobile networks.

[BibT_eX]

[DOI]

Daniel Fischer

Thomas Engel

Proceedings of the 16th annual IEEE International Conference on Network Protocols, 2008

Runtime Monitoring of Metric First-order Temporal Properties.

[BibT_eX]

[DOI]

Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2008

Cryptographically-Sound Protocol-Model Abstractions.

[BibT_eX]

[DOI]

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

Mechanisms for usage control.

[BibT_eX]

[DOI]

Proceedings of the 2008 ACM Symposium on Information, Computer and Communications Security, 2008

A class of probabilistic models for role engineering.

[BibT_eX]

[DOI]

Mario Frank

Joachim M. Buhmann

Proceedings of the 2008 ACM Conference on Computer and Communications Security, 2008

2007

Preface.

[BibT_eX]

[DOI]

Michael Backes

Michael Waidner

J. Comput. Secur., 2007

Verifying a signature architecture: a comparative case study.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2007

Securing the Distribution and Storage of Secrets with Trusted Platform Modules.

[BibT_eX]

[DOI]

Paul E. Sevinç

Mario Strasser

Proceedings of the Information Security Theory and Practices. Smart Cards, 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

A Metamodel-Based Approach for Analyzing Security-Design Models.

[BibT_eX]

[DOI]

Proceedings of the Model Driven Engineering Languages and Systems, 2007

A Proof of Concept Implementation of SSL/TLS Session-Aware User Authentication (TLS-SA).

[BibT_eX]

[DOI]

Proceedings of the Kommunikation in Verteilten Systemen (KiVS), 2007

Monitors for Usage Control.

[BibT_eX]

[DOI]

Proceedings of the Trust Management, 2007

A Policy Language for Distributed Usage Control.

[BibT_eX]

[DOI]

Proceedings of the Computer Security, 2007

An information-theoretic model for adaptive side-channel attacks.

[BibT_eX]

[DOI]

Boris Köpf

Proceedings of the 2007 ACM Conference on Computer and Communications Security, 2007

Specifying and analyzing security automata using CSP-OZ.

[BibT_eX]

[DOI]

Ernst-Rüdiger Olderog

Paul E. Sevinç

Proceedings of the 2007 ACM Symposium on Information, Computer and Communications Security, 2007

BAP: Broadcast Authentication Using Cryptographic Puzzles.

[BibT_eX]

[DOI]

Patrick Schaller

Proceedings of the Applied Cryptography and Network Security, 5th International Conference, 2007

Midpoints Versus Endpoints: From Protocols to Firewalls.

[BibT_eX]

[DOI]

Diana von Bidder

Germano Caronni

Proceedings of the Applied Cryptography and Network Security, 5th International Conference, 2007

2006

Model driven security: From UML models to access control infrastructures.

[BibT_eX]

[DOI]

Jürgen Doser

Torsten Lodderstedt

ACM Trans. Softw. Eng. Methodol., 2006

On the semantics of Alice&Bob specifications of security protocols.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2006

Automated Reasoning for Security Protocol Analysis.

[BibT_eX]

[DOI]

J. Autom. Reason., 2006

Cryptographically Sound Theorem Proving.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2006

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

[BibT_eX]

[DOI]

Rolf Oppliger

Ralf Hauser

Comput. Commun., 2006

Distributed usage control.

[BibT_eX]

[DOI]

Alexander Pretschner

Manuel Hilty

Commun. ACM, 2006

Formalizing and Analyzing Sender Invariance.

[BibT_eX]

[DOI]

Proceedings of the Formal Aspects in Security and Trust, Fourth International Workshop, 2006

Controlling Access to Documents: A Formal Access Control Model.

[BibT_eX]

[DOI]

Paul E. Sevinç

Ernst-Rüdiger Olderog

Proceedings of the Emerging Trends in Information and Communication Security, 2006

Timing-Sensitive Information Flow Analysis for Synchronous Systems.

[BibT_eX]

[DOI]

Boris Köpf

Proceedings of the Computer Security, 2006

Model Driven Security.

[BibT_eX]

[DOI]

Proceedings of the The First International Conference on Availability, 2006

2005

Konflikt oder Review zwei Ansätze für Labors in angewandter Informationssicherheit.

[BibT_eX]

[DOI]

Michael Näf

Inform. Spektrum, 2005

OFMC: A symbolic model checker for security protocols.

[BibT_eX]

[DOI]

Int. J. Inf. Sec., 2005

Relating Strand Spaces and Distributed Temporal Logic for Security Protocol Analysis.

[BibT_eX]

[DOI]

Log. J. IGPL, 2005

Deconstructing Alice and Bob.

[BibT_eX]

[DOI]

Proceedings of the Second Workshop on Automated Reasoning for Security Protocol Analysis, 2005

Firewall Conformance Testing.

[BibT_eX]

[DOI]

Diana Senn

Germano Caronni

Proceedings of the Testing of Communicating Systems, 2005

Algebraic Intruder Deductions.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2005

Verification of a Signature Architecture with HOL-Z.

[BibT_eX]

[DOI]

Proceedings of the FM 2005: Formal Methods, 2005

On Obligations.

[BibT_eX]

[DOI]

Manuel Hilty

Alexander Pretschner

Proceedings of the Computer Security, 2005

The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

Rippling - meta-level guidance for mathematical reasoning.

[BibT_eX]

Cambridge tracts in theoretical computer science 56, Cambridge University Press, ISBN: 978-0-521-83449-0, 2005

2004

Reflective metalogical frameworks.

[BibT_eX]

[DOI]

José Meseguer

ACM Trans. Comput. Log., 2004

Editorial.

[BibT_eX]

[DOI]

Olivier Danvy

Robert Harper

High. Order Symb. Comput., 2004

Metareasoning about Security Protocols using Distributed Temporal Logic.

[BibT_eX]

[DOI]

Proceedings of the Workshop on Automated Reasoning for Security Protocol Analysis, 2004

Synthesis of Programs in Computational Logic.

[BibT_eX]

[DOI]

Jørgen Fischer Nilsson

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.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2003

Bytecode Verification by Model Checking.

[BibT_eX]

[DOI]

Marek Gawkowski

J. Autom. Reason., 2003

A Formal Analysis of a Digital Signature Architecture.

[BibT_eX]

[DOI]

Kunihiko Miyazaki

Kazuo Takaragi

Proceedings of the Integrity and Internal Control in Information Systems VI, 2003

Model driven security for process-oriented systems.

[BibT_eX]

[DOI]

Jürgen Doser

Torsten Lodderstedt

Proceedings of the 8th ACM Symposium on Access Control Models and Technologies, 2003

An On-the-Fly Model-Checker for Security Protocol Analysis.

[BibT_eX]

[DOI]

Proceedings of the Computer Security, 2003

CDiff: a new reduction technique for constraint-based analysis of security protocols.

[BibT_eX]

[DOI]

Proceedings of the 10th ACM Conference on Computer and Communications Security, 2003

2002

A Formal Analysis of the CORBA Security Service.

[BibT_eX]

[DOI]

Frank Rittinger

Proceedings of the ZB 2002: Formal Specification and Development in Z and B, 2002

SecureUML: A UML-Based Modeling Language for Model-Driven Security.

[BibT_eX]

[DOI]

Torsten Lodderstedt

Jürgen Doser

Proceedings of the UML 2002 - The Unified Modeling Language, 5th International Conference, Dresden, Germany, September 30, 2002

Verified Bytecode Model Checkers.

[BibT_eX]

[DOI]

Marek Gawkowski

Proceedings of the Theorem Proving in Higher Order Logics, 15th International Conference, 2002

Bytecode Model Checking: An Experimental Analysis.

[BibT_eX]

[DOI]

Proceedings of the Model Checking of Software, 2002

QUBOS: Deciding Quantified Boolean Logic Using Propositional Satisfiability Solvers.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 4th International Conference, 2002

The Next 700 Synthesis Calculi.

[BibT_eX]

[DOI]

Proceedings of the FME 2002: Formal Methods, 2002

The AVISS Security Protocol Analysis Tool.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 14th International Conference, 2002

2001

A theoretical and empirical investigation of search in imperfect information games.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2001

A Higher-order Interpretation of Deductive Tableau.

[BibT_eX]

[DOI]

J. Symb. Comput., 2001

Current Trends in Logical Frameworks and Metalanguages.

[BibT_eX]

[DOI]

Amy P. Felty

J. Autom. Reason., 2001

Automated complexity analysis based on ordered resolution.

[BibT_eX]

[DOI]

Harald Ganzinger

J. ACM, 2001

Towards an awareness-based semantics for security protocol analysis.

[BibT_eX]

[DOI]

Rafael Accorsi

Proceedings of the Logical Aspects of Cryptographic Protocol Verification, 2001

A formal data-model of the CORBA security service.

[BibT_eX]

[DOI]

Frank Rittinger

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.

[BibT_eX]

[DOI]

Penny Anderson

J. Symb. Comput., 2000

Structuring Metatheory on Inductive Definitions.

[BibT_eX]

[DOI]

Inf. Comput., 2000

Maude versus Haskell: an Experimental Comparison in Security Protocol Analysis.

[BibT_eX]

[DOI]

Grit Denker

Proceedings of the 3rd International Workshop on Rewriting Logic and its Applications, 2000

Rewriting Logic as a Metalogical Framework.

[BibT_eX]

[DOI]

José Meseguer

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 2000

B2M: A Semantic Based Tool for BLIF Hardware Descriptions.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, Third International Conference, 2000

Bounded Model Construction for Monadic Second-Order Logics.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 12th International Conference, 2000

Combining Knowledge and Search to Solve Single-Suit Bridge.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Bernd Krieg-Brückner

Proceedings of the Algebraic Foundations of Systems Specification, 1999

Modeling a Hardware Synthesis Methodology in Isabelle.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 1999

Structural and Behavioral Modeling with Monadic Logics.

[BibT_eX]

[DOI]

Proceedings of the 29th IEEE International Symposium on Multiple-Valued Logic, 1999

Lazy Infinite-State Analysis of Security Protocols.

[BibT_eX]

[DOI]

Proceedings of the Secure Networking - CQRE (Secure) '99, International Exhibition and Congress Düsseldorf, Germany, November 30, 1999

Java Bytecode Verification by Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 11th International Conference, 1999

1998

Natural Deduction for Non-Classical Logics.

[BibT_eX]

[DOI]

Stud Logica, 1998

Labelled Modal Logics: Quantifiers.

[BibT_eX]

[DOI]

J. Log. Lang. Inf., 1998

Scoped metatheorems.

[BibT_eX]

[DOI]

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

Logical-Framework-Based Program Development.

[BibT_eX]

[DOI]

ACM Comput. Surv., 1998

Search in Games with Incomplete Information: A Case Study Using Bridge Card Play.

[BibT_eX]

[DOI]

Artif. Intell., 1998

A Recipe for the Complexity Analysis of Non-Classical Logics.

[BibT_eX]

Proceedings of the Frontiers of Combining Systems, Second International Workshop, 1998

Combining WS1S and HOL.

[BibT_eX]

Proceedings of the Frontiers of Combining Systems, Second International Workshop, 1998

Optimal Play against Best Defence: Complexity and Heuristics.

[BibT_eX]

[DOI]

Proceedings of the Computers and Games, First International Conference, 1998

Finding Optimal Strategies for Imperfect Information Games.

[BibT_eX]

[DOI]

Hitoshi Matsubara

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.

[BibT_eX]

[DOI]

J. Log. Comput., 1997

Labelled Quantified Modal Logics.

[BibT_eX]

[DOI]

Proceedings of the KI-97: Advances in Artificial Intelligence, 1997

A New Method for Bounding the Complexity of Modal Logics.

[BibT_eX]

[DOI]

Proceedings of the Computational Logic and Proof Theory, 5th Kurt Gödel Colloquium, 1997

LISA: A Specification Language Based on WS2S.

[BibT_eX]

[DOI]

Andreas Podelski

Proceedings of the Computer Science Logic, 11th International Workshop, 1997

1996

Adding Metatheoretic Facilities to First-Order Theories.

[BibT_eX]

[DOI]

J. Log. Comput., 1996

Middle-Out Reasoning for Synthesis and Induction.

[BibT_eX]

[DOI]

Ina Kraan

J. Autom. Reason., 1996

A Calculus for and Termination of Rippling.

[BibT_eX]

[DOI]

J. Autom. Reason., 1996

Generic System Support for Deductive Program Development.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1996

Complexity Analysis Based on Ordered Resolution.

[BibT_eX]

[DOI]

Harald Ganzinger

Proceedings of the Proceedings, 1996

Implementing Modal and Relevance Logics in a Logical Framework.

[BibT_eX]

Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning (KR'96), 1996

A Topography of Labelled Modal Logics.

[BibT_eX]

Proceedings of the Frontiers of Combining Systems, 1996

Experiments in Automating Hardware Verification Using Inductive Proof Planning.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, First International Conference, 1996

1995

Hardware Verification using Monadic Second-Order Logic.

[BibT_eX]

[DOI]

Nils Klarlund

Proceedings of the Computer Aided Verification, 1995

Deriving and Applying Logic Program Transformers.

[BibT_eX]

[DOI]

Penny Anderson

Proceedings of the Algorithms, 1995

1994

A Term Equality Problem Equivalent to Graph Isomorphism.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1994

Generalized Rewriting in Type Theory.

[BibT_eX]

J. Inf. Process. Cybern., 1994

Logic Frameworks for Logic Programs.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming Synthesis and Transformation, 1994

IsaWhelk Interpreted in Isabelle.

[BibT_eX]

Proceedings of the Logic Programming, 1994

Coloured Rippling: An Extension of a Theorem Proving Heuristic.

[BibT_eX]

Proceedings of the Eleventh European Conference on Artificial Intelligence, 1994

A Calculus for Rippling.

[BibT_eX]

[DOI]

Proceedings of the Conditional and Typed Rewriting Systems, 4th International Workshop, 1994

Termination Orderings for Rippling.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Richard Barnett

Jane Hesketh

Ann. Math. Artif. Intell., 1993

A Framework for Program Development Based on Schematic Proof.

[BibT_eX]

[DOI]

Proceedings of the 7th International Workshop on Software Specification and Design, 1993

Difference Unification.

[BibT_eX]

[DOI]

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

Middle-Out Reasoning for Logic Program Synthesis.

[BibT_eX]

Ina Kraan

Proceedings of the Logic Programming, 1993

A Conservative Extension of First-order Logic and Its Application to Theorem Proving.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1993

1992

Logic Program Synthesis via Proof Planning.

[BibT_eX]

[DOI]

Ina Kraan

Proceedings of the Logic Program Synthesis and Transformation, 1992

An Adaptation of Proof-Planning to Declarer Play in Bridge.

[BibT_eX]

Proceedings of the 10th European Conference on Artificial Intelligence, 1992

Difference Matching.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1992

1991

Formally verified synthesis of combinational CMOS circuits.

[BibT_eX]

[DOI]

Geoffrey M. Brown

Miriam Leeser

Integr., 1991

Some Normalization Properties of Martin-Löf's Type Theory, and Applications.

[BibT_eX]

[DOI]

Douglas J. Howe

Proceedings of the Theoretical Aspects of Computer Software, 1991

Automating Meta-Theory Creation and System Extension.

[BibT_eX]

[DOI]

Fausto Giunchiglia

Paolo Traverso

Proceedings of the Trends in Artificial Intelligence, 1991

1990

Building Problem Solving Environments in Constructive Type Theory.

[BibT_eX]

PhD thesis, 1990

Equality of Terms Containing Associative-Commutative Functions and Commutative Binding Operators in Isomorphism Complete.

[BibT_eX]

[DOI]

Proceedings of the 10th International Conference on Automated Deduction, 1990

1989

Verification Of Combinational Logic in Nuprl.

[BibT_eX]

[DOI]

Peter Del Vecchio

Proceedings of the Hardware Specification, 1989

Building Theories in Nuprl.

[BibT_eX]

[DOI]

Proceedings of the Logic at Botik '89, 1989

1988

An Environment For Automated Reasoning About Partial Functions.

[BibT_eX]

[DOI]