Journals

  1. Model-driven Privacy.
    To appear in Proceedings on Privacy Enhancing Technologies, 2024.

  2. User-controlled privacy: taint, track, and control.
    To appear in Proceedings on Privacy Enhancing Technologies, 2024.

  3. Efficient Evaluation of Arbitrary Relational Calculus Queries.
    Logical Methods in Computer Science, 19(4):1-40, 2023.

  4. IsaNet: A Framework for Verifying Secure Data Plane Protocols.
    Journal of Computer Security, 2023.

  5. Checking Websites' GDPR Consent Compliance for Marketing Emails.
    Proceedings on Privacy Enhancing Technologies, 2022.

  6. Scalable Online First-Order Monitoring.
    International Journal on Software Tools for Technology Transfer, 2021.

  7. Natural Projection as Partial Model Checking.
    Journal of Automated Reasoning, 2020.

  8. Decentralized Privacy-Preserving Proximity Tracing.
    IEEE Data Engineering Bulletin, 2020.

  9. Internet Backbones in Space.
    SIGCOMM Computer Communication Review, 2020.

  10. CryptHOL: Game-based Proofs in Higher-order Logic.
    Journal of Cryptology, 2020.

  11. Almost Event-rate Independent Monitoring.
    Formal Methods in System Design, 2019.

  12. Runtime Verification over Out-of-order Streams.
    ACM Transactions on Computational Logic, 2019.

  13. Cardinality Estimators do not Preserve Privacy.
    Proceedings on Privacy Enhancing Technology, 2 019.

  14. Refining Security Protocols.
    Journal of Computer Security, 2018.

  15. Algorithms for Monitoring Real-time Properties.
    Acta Informatica, 2017.

  16. Large-scale System Development using Abstract Data Types and Refinement.
    Science of Computer Programming, 2016.

  17. Scalable Offline Monitoring of Temporal Specifications.
    Formal Methods in System Design, 2016.

  18. Design, Analysis, and Implementation of ARPKI: an Attack-Resilient Public Key Infrastructure.
    IEEE Transactions on Dependable and Secure Computing, 2016.

  19. Monitoring of Temporal First-order Properties with Aggregations.
    Formal Methods in System Design, 2015.

  20. Monitoring Metric First-order Temporal Properties.
    Journal of the ACM, 2015.

  21. Greedily Computing Associative Aggregations on Sliding Windows.
    Information Processing Letters, 2015.

  22. Know your Enemy: Compromising Adversaries in Protocol Analysis.
    ACM Transactions on Information and System Security, 2014.

  23. Deciding Safety and Liveness in TPTL.
    Information Processing Letters, 2014.

  24. A Model-Driven Methodology for Developing Secure Data-Management Applications.
    IEEE Transactions on Software Engineering, 2014.

  25. LTL is Closed Under Topological Closure.
    Information Processing Letters, 2014.

  26. Obstruction-free Authorization Enforcement: Aligning Security and Business Objectives.
    Journal of Computer Security, 2014.

  27. Monitoring Data Usage in Distributed Systems.
    IEEE Transactions on Software Engineering, 2013.

  28. Provably Repairing the ISO/IEC 9798 Standard for Entity Authentication.
    Journal of Computer Security, 2013.

  29. Predictable Mobile Routing for Spacecraft Networks.
    IEEE Transactions on Mobile Computing, 2013.

  30. Role Mining with Probabilistic Models.
    ACM Transactions on Information and System Security, 2013.

  31. Efficient Construction of Machine-Checked Symbolic Protocol Security Proofs.
    Journal of Computer Security, 2013.

  32. Enforceable Security Policies Revisited.
    ACM Transactions on Information and System Security. 2013.

  33. Dyanmic Enforcement of Abstract Separation of Duty Constraints.
    ACM Transactions on Information and System Security, 2012.

  34. Multi-Assignment Clustering for Boolean Data.
    Journal of Machine Learning Research, 2012.

  35. Formal Reasoning about Physical Properties of Security Protocols.
    ACM Transactions on Information and System Security, 2011.

  36. Distributed Temporal Logic for the Analysis of Security Protocol Models.
    Theoretical Computer Science, 2011.

  37. Automatically Deriving Information-theoretic Bounds for Adaptive Side-channel Attacks.
    Journal of Computer Security, 2011.

  38. Constraint Differentiation: Search-Space Reduction for the Constraint-Based Analysis of Security Protocols.
    Journal of Computer Security, 2010.

  39. Efficient Analysis of Pattern-Based Constraint Specifications.
    Software and Systems Modeling, 2010.

  40. Labelled Tableaux for Distributed Temporal Logic.
    Journal of Logic and Computation, 2009.

  41. Developing Topology Discovery in Event-B.
    Science of Computer Programming, 2009.

  42. Automated Analysis of Security Design Models.
    Information and Software Technology, 2009.

  43. SSL/TLS Session-aware User Authentication Revisited.
    Computers & Security, 2008.

  44. Verifying a Signature Architecture --- A Comparative Case Study.
    Formal Aspects of Computing, 2007.

  45. On the Semantics of Alice&Bob Specifications of Security Protocols.
    Theoretical Computer Science, 2006.

  46. SSL/TLS Session-Aware User Authentication --- Or How to Effectively Thwart the Man-in-the-Middle.
    Computer Communications, 2006.

  47. Model Driven Security: from UML Models to Access Control Infrastructures.
    ACM Transactions on Software Engineering and Methodology, 2006.

  48. Relating Strand Spaces and Distributed Temporal Logic for Security Protocol Analysis.
    Logic Journal of the IGPL, 2005.

  49. OFMC: A Symbolic Model-Checker for Security Protocols.
    International Journal of Information Security, 2005.

  50. Reflective Metalogical Frameworks.
    ACM Transactions on Computational Logic, 2004.

  51. Bytecode Verification by Model Checking.
    Journal of Automated Reasoning, 2003.

  52. Decision Procedures for Inductive Boolean Functions based on Alternating Automata.
    Theoretical Computer Science, 2003.

  53. A Higher-Order Interpretation of Deductive Tableau.
    Journal of Symbolic Computation, 2001.

  54. Automated Complexity Analysis Based on Ordered Resolution.
    Journal of the ACM, 2001.

  55. A Theoretical and Empirical Investigation of Search in Imperfect Information Games.
    Theoretical Computer Science, 2001.

  56. Structuring Metatheory on Inductive Definitions.
    Information and Computation, 2000.

  57. Program Development Schemata as Derived Rules.
    Journal of Symbolic Computation, 2000.

  58. Modeling a Hardware Synthesis Methodology in Isabelle.
    Formal Methods in Systems Design, 1999.

  59. Logical Framework Based Program Development.
    ACM Computing Surveys, 1998.

  60. Automata Based Symbolic Reasoning in Hardware Verification.
    Formal Methods in Systems Design, 1998.

  61. Search in Games with Incomplete Information: A Case Study using Bridge Card Play.
    Artificial Intelligence, 1998.

  62. Labelled Modal Logics: Quantifiers.
    The Journal of Logic, Language, and Information, 1998.

  63. Natural Deduction for Non-Classical Logics.
    Studia Logica, 1998.

  64. Labelled Propositional Modal Logics: Theory and Practice.
    Journal of Logic and Computation, 1997.

  65. Adding Metatheoretic Facilities to First-order Theories.
    Journal of Logic and Computation, 1996.

  66. A Calculus for and Termination of Rippling.
    Journal of Automated Reasoning, 1996.

  67. Middle-Out Reasoning for Logic Program Synthesis.
    Journal of Automated Reasoning, 1996.

  68. Generalized Rewriting in Type Theory.
    Journal of Information Processing and Cybernetics, 1995.

  69. A Term Equality Problem Equivalent to Graph Isomorphism.
    Information Processing Letters, 1994.

  70. A Recursion Planning Analysis of Inductive Completion.
    Annals of Artificial Intelligence and Mathematics, 1993.

  71. Formally Verified Synthesis of Combinational CMOS Circuits.
    Integration: The International Journal of VLSI Design, 1991.

Magazine Articles

  1. Tamarin: Verification of Large-Scale, Real-World, Cryptographic Protocols
    IEEE S\&P, 2022.

  2. Symbolically Analyzing Security Protocols using Tamarin
    ACM SIGLOG Newsletter, October 2017.

  3. Improving the Security of Cryptographic Protocol Standards (IEEE Preprint).
    IEEE Security & Privacy, 2015.

  4. On Secure Data Deletion.
    IEEE Security & Privacy, 2014.

  5. Verification for Monitoring Requirements of Train Monitoring Systems in Event-B.
    Information Processing Society of Japan, 2013.

  6. The Research Value of Publishing Attacks.
    Communications of the ACM, 2012.

  7. Conflict or Review --- Two Approaches to an Information Security Laboratory.
    Communications of the ACM, 2008.

  8. SSL/TLS Session-Aware User Authentication: A Lightweight Alternative to Client-Side Certificates.
    IEEE Computer, 2008.

  9. Secure Neighborhood Discovery: A Fundamental Element for Mobile Ad Hoc Networking.
    IEEE Communications, 2008.

  10. The Z Specification Language and the Proof Environment Isabelle/HOL-Z. (In Japanese)
    Computer Software --- Journal of the Japanese Society for Software Science and Technology, 2007.

  11. Distributed Usage Control.
    Communications of the ACM, 2006.
    See also the German version, which appeared in Digma, 2007.

  12. A Formal Analysis of a Digital Signature System. (In Japanese)
    Computer Software --- Journal of the Japanese Society for Software Science and Technology, 2005.

  13. Konflikt oder Review --- zwei Ansätze für Labors in angewandter Informationssicherheit. (In German)
    Informatik Spektrum, 2005.

Books

  1. The Complete Guide to SCION: From Design Principles to Formal Verification.
    Springer Verlag, 2022.

  2. Applied Information Security --- A Hands-on Approach.
    Springer Verlag, 2011.

  3. Rippling: Meta-level Guidance for Mathematical Reasoning.
    Cambridge Tracts in Theoretical Computer Science, No. 56, June 2005.

Chapters in Books

  1. Formal Methods for Security.
    The Cyber Security Body of Knowledge, 2021.

  2. Model Checking Security Protocols.
    Handbook of Model Checking, 2018.

  3. Model-Driven Development of a Secure eHealth Application.
    Engineering Secure Future Inernet Services and Systems, 2014.

  4. Technology Transfer.
    Industrial Deployment of System Engineering Methods, 2013.

  5. Model-Driven Develoment of Security-Aware GUIs for Data-Centric Applications.
    Foundations of Security Analysis and Design VI (FOSAD Tutorial Lectures), 2011.

  6. Model Driven Security.
    Engineering Theories of Software Intensive Systems, 2004.

  7. A Formal Analysis of a Digital Signature Architecture.
    6th Conference on Integrity and Internal Control in Information Systems, 2004.

  8. Synthesis of Programs in Computational Logic.
    Program Development in Computational Logic, 2004.

  9. Logical Frameworks.
    Handbook of Philosophical Logic, 2002.

  10. Combining WS1S with HOL.
    Frontiers of Combining Systems 2, 2000.

  11. A Recipe for the Complexity Analysis of Non-Classical Logics.
    Frontiers of Combining Systems 2, 2000.

  12. Formalization of the Development Process.
    Algebraic Foundations of System Specification, 1988.

  13. A Modular Presentation of Modal Logics in a Logical Framework.
    The Tbilisi Symposium on Logic, Language, and Computation, 1998.

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

  15. Logic Program Synthesis via Proof Planning.
    Logic Programming Synthesis and Transformation, 1993.

  16. Metalogical Frameworks.
    Logical Environments, 1993.

  17. Experience with FS0 as a Framework Theory.
    Logical Environments, 1993.

  18. The Boyer-Moore Prover and Nuprl: An Experimental Comparison.
    Logical Frameworks, 1991.

Conference and Workshop Proceedings

  1. Determining an Economic Value of High Assurance for Commodity Software Security.
    To appear in: Twenty-eighth International Workshop on Security Protocols, 2023.

  2. Correct and Efficient Policy Monitoring, a Retrospective.
    Proceedings of the 21st International Symposium on Automated Technology for Verification and Analysis (ATVA), 2023.

  3. SealClub: Computer-aided Paper Document Authentication.
    Annual Computer Security Applications Conference (ACSAC), 2023.

  4. ADEM: An Authentic Digital EMblem.
    30th ACM Conference on Computer and Communications Security (CCS), 2023.

  5. Is Modeling Access Control Worth It?
    30th ACM Conference on Computer and Communications Security (CCS), 2023.

  6. Monitoring the Internet Computer.
    Proceedings of the 25th International Symposium on Formal Methods (FM), 2023.

  7. Locality-Sensitive Hashing Does Not Guarantee Privacy! Attacks on Google's FLoC and the MinHash Hierarchy System.
    Privacy Enhancing Technologies Symposium (PETS), 2023.

  8. A Formal Framework for End-to-End DNS Resolution.
    ACM SIGCOMM, 2023.

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

  10. Efficient Black-box Checking of Snapshot Isolation in Databases.
    49th International Conference on Very Large Data Bases (VLDB), 2023.

  11. RHINE: Robust and High-performance Internet Naming ith E2E Authenticity.
    20th USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2023.

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

  13. Bridging the Semantic Gap between Qualitative and Quantitative Models of Distributed Systems.
    OOPSLA:The ACM Conference on Systems, Programming, Languages, and Applications: Software for Humanity, 2022.

  14. Real-Time Policy Enforcement with Metric First-Order Temporal Logic.
    27th European Symposium on Research in Computer Security (ESORICS) 2022.

  15. I'm Surprised So Much Is Connected.
    Conference on Human Factors in Computing Systems (CHI), 2022.

  16. Automating Cookie Consent and GDPR Violation Detection.
    31st USENIX Security Symposium, 2022.

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

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

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

  20. Practical Relational Calculus Query Evaluation.
    25th International Conference on Database Theory (ICDT), 2022.

  21. Verifying Table-Based Elections.
    28th ACM Conference on Computer and Communications Security (CCS), 2021.

  22. A Comprehensive Formal Analysis of 5G Handover.
    4th ACM Conference on Security and Privacy in Wireless and Mobile Networks (WiSec), 2021.

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

  24. Abstract Modeling of System Communication in Constructive Cryptography using CryptHOL.
    34th IEEE Computer Security Foundations Symposium (CSF), 2021.

  25. Fixing the Achilles Heel of E-Voting: The Bulletin Board. (Full Version)
    34nd IEEE Computer Security Foundations Symposium (CSF), 2021.

  26. Formal Verification of Secure Forwarding Protocols.
    34nd IEEE Computer Security Foundations Symposium (CSF), 2021.

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

  28. Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification.
    OOPSLA, 2020.

  29. Multi-head Monitoring of Metric Dynamic Logic.
    ATVA, 2020.

  30. Dispute Resolution in Voting.
    33rd IEEE Computer Security Foundations Symposium (CSF), 2020.

  31. A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic.
    10th International Joint Conference on Automated Reasoning (IJCAR), 2020.

  32. Scalable Online Monitoring of Distributed Systems.
    20th International Conference on Runtime Verification (RV20), 2020.

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

  34. SoK: Delegation and Revocation, the Missing Links in the Web’s Chain of Trust.
    5th IEEE European Symposium on Security and Privacy (EuroS&P), 2020.

  35. Privacy-Preserving OpenID Connect.
    15th ACM Asia Conference on Computer and Communications Security (Asia CCS) , 2020.

  36. Formalizing Constructive Cryptography using CryptHOL.
    IEEE 32nd Computer Security Foundations Symposium (CSF), 2019.

  37. A Formally Verified Monitor for Metric First-​Order Temporal Logic.
    19th International Conference on Runtime Verification (RV), 2019.

  38. The Next 700 Policy Miners: A Universal Method for Building Policy Miners.
    26th ACM Conference on Computer and Communications Security (CCS), 2019.

  39. User Account Access Graphs.
    6th ACM Conference on Computer and Communications Security (CCS), 2019.

  40. Monitoring the GDPR.
    4th European Symposium on Research in Computer Security (ESORICS), 2019.

  41. Adaptive Online First-Order Monitoring.
    17th International Symposium on Automated Technology for Verification and Analysis (ATVA), 2019.

  42. Multi-Head Monitoring of Metric Temporal Logic.
    17th International Symposium on Automated Technology for Verification and Analysis (ATVA), 2019.

  43. From Nondeterministic to Multi-Head Deterministic Finite-State Transducers.
    46th International Colloquium on Automata, Languages and Programming (ICALP), 2019.

  44. Information-Flow Control for Database-backed Applications.
    4th IEEE European Symposium on Security and Privacy (Euro S&P), 2019.

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

  46. Scalable Online First-Order Monitoring.
    18th International Conference on Runtime Verification (RV), 2018.

  47. Networking in Heaven as on Earth.
    17th ACM Workshop on Hot Topics in Networks (HotNets), 2018.

  48. A Formal Analysis of 5G Authentication.
    25th ACM Conference on Computer and Communications Security, 2018.

  49. Optimal Proofs for Linear Temporal Logic on Lasso Words.
    16th International Symposium on Automated Technology for Verification and Analysis (ATVA), 2018.

  50. Alethea: A Provably Secure Random Sample Voting Protocol.
    31st IEEE Computer Security Foundations Symposium (CSF), 2018.

  51. On Purpose and by Necessity: Compliance under the GDPR.
    Twenty-Second International Conference on Financial Cryptography and Data Security, 2018.

  52. Mining ABAC Rules from Sparse Logs.
    3rd IEEE European Symposium on Security and Privacy (Euro S&P), 2018.

  53. From Natural Projection to Partial Model Checking and Back.
    24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2018.

  54. Exploring Website Location as a Security Indicator.
    Proceedings of the NDSS Workshop on Usable Security (USEC), 2018.

  55. The MonPoly Monitoring Tool.
    RV-​CuBES 2017, 2017.

  56. Election Security and Economics: It's all about Eve.
    2nd International Joint Conference on Electronic Voting (evoteID), 2017.

  57. Tests and Refutation.
    15th International Symposium on Automated Technology for Verification and Analysis (ATVA), 2017.

  58. Securing Databases from Probabilistic Inference.(full version)
    30th IEEE Computer Security Foundations Symposium (CSF), 2017.

  59. Almost Event-Rate Independent Monitoring of Metric Dynamic Logic.
    17th International Conference on Runtime Verification (RV), 2017.

  60. Test Execution Checkpointing for Web Applications.
    26th International Symposium on Software Testing and Analysis (ISSTA), 2017.

  61. Runtime Verification of Temporal Properties over Out-of-order Data Streams.
    29th International Conference on Computer-Aided Verification (CAV), 2017.

  62. Cutoff Bounds for Consensus Algorithms.
    29th International Conference on Computer-Aided Verification (CAV), 2017.

  63. Almost Event-Rate Independent Monitoring of Metric Temporal Logic.
    23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2017.

  64. Refining Authenticated Key Agreement with Strong Adversaries.
    2nd IEEE European Symposium on Security and Privacy (Euro S&P), 2017.

  65. Modeling Human Errors in Security Protocols.
    29th IEEE Computer Security Foundations Symposium, 2016.

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

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

  68. Strong and Provably Secure Database Access Control.
    1st IEEE European Symposium on Security and Privacy (Euro S&P), 2016.

  69. Security Testing Beyond Functional Tests.
    Eight International Symposium on Engineering Secure Software and Systems (ESSOS), 2016.

  70. Failure-aware Runtime Verification of Distributed Systems.
    35th Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTCCS), 2015.

  71. Automated Symbolic Proofs of Observational Equivalence.
    22nd ACM Conference on Computer and Communications Security (CCS), 2015.

  72. Alice and Bob Meet Equational Theories.
    Logic, Rewriting, and Concurrency, 2015.

  73. Semantic Vacuity.
    22nd International Symposium on Temporal Representation and Reasoning (TIME), 2015.

  74. Analyzing First-order Role Based Access Control.
    28th Computer Security Foundations (CSF), 2015.

  75. A Complete Characterization of Secure Human-Server Communication.
    28th Computer Security Foundations (CSF), 2015.

  76. Consensus Refined.
    45th IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), 2015.

  77. Fail-Secure Access Control.
    21st ACM Conference on Computer and Communications Security (CCS), 2014.

  78. ARPKI: Attack Resilient Public-key Infrastructure.
    21st ACM Conference on Computer and Communications Security (CCS), 2014.

  79. Scalable Offline Monitoring.
    5th International Conference on Runtime Verification (RV), 2014.

  80. On Real-time Monitoring with Imprecise Timestamps.
    5th International Conference on Runtime Verification (RV), 2014.

  81. Optimal Security-Aware Query Processing.
    40th International Conference on Very Large Data Bases (VLDB), 2014.

  82. Code Generation for Event-B.
    11th International Conference on Integrated Formal Methods (IFM), 2014.

  83. Detection of GPS Spoofing Attacks in Power Grids.
    7th ACM Conference on Security and Privacy in Wireless and Mobile Networks (WiSec), 2014.

  84. Anchored LTL Separation.
    Twenty-Third Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2014.

  85. Actor Key Compromise: Consequences and Countermeasures.
    Computer Security Foundations (CSF), 2014.

  86. Formal System Modelling Using Abstract Data Types in Event-B.
    4th International ABZ Conference, 2014.

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

  88. Decentralized Composite Access Control.
    3rd Conference on Principles of Security and Trust (POST), 2014.

  89. Secure Data Deletion from Persistent Media.
    20th ACM Conference on Computer and Communications Security (CCS), 2013.

  90. Symbolic Probabilistic Analysis of Off-line Guessing.
    18th European Symposium on Research in Computer Security (ESORICS), 2013.

  91. Monitoring of Temporal First-Order Properties with Aggregations.
    4th International Conference on Runtime Verification (RV), 2013.

  92. The TAMARIN Prover for the Symbolic Analysis of Security Protocols.
    25th International Conference on Computer Aided Verification (CAV), 2013.

  93. Semi-valid Input Coverage for Fuzz Testing.
    International Symposium on Software Testing and Analysis (ISSTA), 2013.

  94. Secure Data Deletion
    IEEE Symposium on Security and Privacy, 2013.

  95. Monitoring Compliance Policies over Incomplete and Disagreeing Logs (full version).
    3rd International Conferene on Runtime Verification (RV), 2012.

  96. Automated Analysis of Diffie- Hellman Protocols and Advanced Security Properties.
    25th IEEE Computer Security Foundations Symposium (CSF), 2012.

  97. Refining Key Establishment.
    25th IEEE Computer Security Foundations Symposium (CSF), 2012.

  98. Data Node Encrypted File System: Efficient Secure Deletion for Flash Memory.
    21st USENIX Security Symposium, 2012.

  99. SecFuzz: Fuzz-testing Security Protocols.
    7th International Workshop on Automation of Software Test, 2012.

  100. Optimal Workflow-aware Authorizations.
    17th ACM Symposium on Access Control Models and Technologies (SACMAT), 2012.

  101. User-Level Secure Deletion on Log-structured File Systems.
    7th ACM Symposium on Information, Computer and Communications Security (ASIACCS), 2012.

  102. Enforceable Security Policies Revisited.
    1st Conference on Principles of Security and Trust (POST), 2012.

  103. Provably Repairing the ISO/IEC 9798 Standard for Entity Authentication.
    1st Conference on Principles of Security and Trust (POST), 2012.

  104. Constructing Mid-Points for Two-Party Asynchronous Protocols.
    15th International Conference On Principles Of Distributed Systems (OPODIS), 2011.

  105. MONPOLY: Monitoring Usage-control Policies.
    2nd International Conference on Runtime Verification (RV), 2011.

  106. Algorithms for Monitoring Real-time Properties. (full version).
    2nd International Conference on Runtime Verification (RV), 2011.

  107. Monitoring Usage-control Policies in Distributed Systems (full version).
    8th International Symposium on Temporal Representation and Reasoning (TIME), 2011.

  108. Separation of Duties as a Service.
    6th ACM Symposium on Information, Computer and Communications Security (ASIACCS), 2011.

  109. Obstruction-free Authorization Enforcement: Aligning Security With Business Objectives.
    24th IEEE Computer Security Foundations Symposium (CSF), 2011.

  110. A Decade of Model-Driven Security.
    16th ACM Symposium on Access Control Models and Technologies (SACMAT), 2011.

  111. FAST: An Efficient Decision Procedure for Deduction and Static Equivalence.
    22nd International Conference on Rewriting Techniques and Applications (RTA), 2011.

  112. Keeping Data Secret under Full Compromise using Porter Devices.
    Proceedings of the Annual Computer Security Applications Conference (ACSAC), 2010.

  113. Developing Security Protocols by Refinement.
    17th ACM Conference on Computer and Communications Security (CCS), 2010.

  114. Efficient Decision Procedures for Message Deducibility and Static Equivalence.
    Formal Aspects in Security and Trust (FAST), 2010.

  115. Modeling and Analyzing Security in the Presence of Compromising Adversaries.
    The 15th European Symposium on Research in Computer Security (ESORICS), 2010.

  116. Degrees of Security: Protocol Guarantees in the Face of Compromising Adversaries.
    19th EACSL Annual Conference on Computer Science Logic (CSL), 2010.

  117. Policy Monitoring in First-order Temporal Logic.
    22nd International Conference on Computer-Aided Verification (CAV), 2010.

  118. Impossibility Results for Secret Establishment.
    23rd IEEE Computer Security Foundations Symposium (CSF), 2010.

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

  120. On the Definition of Role Mining.
    15th ACM Symposium on Access Control Models and Technologies (SACMAT), 2010.

  121. SSG: A Model-Based Development Environment for Smart, Security-Aware GUIs.
    32nd ACM/IEEE Conference on Software Engineering (ICSE), 2010.

  122. Monitoring Security Policies with Metric First-order Temporal Logic.
    15th ACM Symposium on Access Control Models and Technologies (SACMAT), 2010.

  123. Automatic Generation of Smart, Security-Aware GUI Models.
    International Symposium on Engineering Secure Software and Systems (ESSOS), 2010.

  124. How to Evaluate the Security of Real-life Cryptographic Protocols? The cases of ISO/IEC 29128 and CRYPTREC.
    1st Workshop on Real-life Cryptographic Protocols and Standardization, 2010.

  125. A Probabilistic Approach to Hybrid Role Mining.
    16th ACM Conference on Computer and Communications Security, 2009.

  126. Dynamic Enforcement of Abstract Separation of Duty Constraints.
    14th European Symposium on Research in Computer Security (ESORICS), 2009.

  127. Let's Get Physical: Models and Methods for Real-World Security Protocols.
    22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs), 2009.

  128. Modeling and Verifying Physical Properties of Security Protocols for Wireless Networks.
    22nd IEEE Computer Security Foundations Symposium (CSF), 2009.

  129. Automatic Generation of Security-Aware GUI Models.
    Security in Model Driven Architecture (Sec-MDA), 2009.

  130. Multi-Assignment Clustering for Boolean Data.
    26th International Conference on Machine Learning (ICML), 2009.

  131. Developing Topology Discovery in Event-B.
    7th International Conference on Integrated Formal Methods (IFM), 2009.

  132. Runtime Monitoring of Metric First-order Temporal Properties.
    Foundations of Software Technology and Theoretical Computer Science (FSTTCS), 2008.

  133. Topology Dynamics and Routing for Predictable Mobile Networks.
    16th IEEE International Conference on Network Protocols (ICNP), 2008

  134. Cryptographically-sound Protocol-model Abstractions.
    Logic in Computer Science (LICS), 2008.

  135. Cryptographically-sound Protocol-model Abstractions.
    Compuer Security Foundations (CSF), 2008.

  136. A Class of Probabilistic Models for Role Engineering.
    15th ACM Conference on Computer and Communications Security (CCS), 2008.

  137. A Labeled Tableaux System for the Distributed Temporal Logic DTL.
    15th International Symposium on Temporal Representationand Reasoning (TIME), 2008.

  138. Mechanisms for Usage Control.
    ACM Symposium on Information, Computer and Communications Security (ASIACCS), 2008.

  139. An Information-Theoretic Model for Adaptive Side-Channel Attacks.
    14th ACM Conference on Computer and Communications Security (CCS), 2007.
  140. A Policy Language for Distributed Usage Control.
    12th European Symposium on Research in Computer Security (ESORICS), 2007.
  141. A Metamodel-Based Approach for Analyzing Security-Design Models.
    ACM/IEEE 10th International Conference on Model Driven Engineering Languages and Systems (MODELS), 2007.

  142. A Monad-based Modeling and Verification Toolbox with Application to Security Protocols.
    20th International Conference on Theorem Proving in Higher Order Logics (TPHOLs), 2007.

  143. BAP: Broadcast Authentication Using Cryptographic Puzzles.
    International Conference on Applied Cryptography and Network Security (ACNS), 2007.
  144. Midpoints versus Endpoints: From Protocols to Firewalls.
    5th International Conference on Applied Cryptography and Network Security (ACNS), 2007.

  145. Securing the Distribution and Storage of Secrets with Trusted Platform Modules.
    Workshop on Information Security Theory and Practice (WISTP), 2007.

  146. Specifying and Analyzing Security Automata using CSP-OZ.
    2nd ACM Symposium on Information, Computer and Communications Security (ASIACCS), 2007.

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

  148. Formalizing and Analyzing Sender Invariance.
    Formal Aspects of Security and Trust (FAST), 2007.

  149. Timing-Sensitive Information Flow Analysis for Synchronous Systems.
    11th European Symposium on Research in Computer Security (ESORICS), 2006.

  150. Cryptographically Sound Theorem Proving.
    19th IEEE Computer Security Foundations Workshop (CSFW), 2006.

  151. Controlling Access to Documents: A Formal Access Control Model.
    International Conference on Emerging Trends in Information and Communication Security (ETRICS), 2006.

  152. Algebraic Intruder Deductions.
    12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), 2005.

  153. On Obligations.
    10th European Symposium on Research in Computer Security (ESORICS), 2005.

  154. Verification of a Signature Architecture with HOL-Z.
    Formal Methods (FM), 2005.

  155. The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications.
    17th International Conference on Computer Aided Verification (CAV), 2005.

  156. Deconstructing Alice and Bob.
    Workshop on Automated Reasoning for Security Protocol Analysis, 2005.

  157. Firewall Conformance Testing.
    Testing of Communicating Systems (TestCom), 2005.

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

  159. Towards a Metalogic for Security Protocol Analysis.
    Proceedings of the Workshop on the Combination of Logics: Theory and Applications, 2004.

  160. Constraint Differentiation: A New Reduction Technique for Constraint-Based Analysis of Security Protocols.
    10th ACM Conference on Computer and Communications Security (CCS), 2003.

  161. An On-The-Fly Model-Checker for Security Protocol Analysis.
    8th European Symposium on Research in Computer Security (ESORICS), 2003.

  162. Model Driven Security for Process-Oriented Systems.
    8th ACM Symposium on Access Control Models and Technologies (SACMAT), 2003.

  163. QUBOS: Deciding Quantified Boolean Logic using Propositional Satisfiability Solvers.
    4th International Conference on Formal Methods in Computer-Aided Design (CAV), 2002.

  164. SecureUML: A UML-Based Modeling Language for Model-Driven Security.
    5th International Conference on the Unified Modeling Language (UML), 2002.

  165. Modal Specifications of Trace-based Security Properties.
    2nd International Workshop on Security of Mobile Multiagent Systems, 2002.

  166. The AVISS Security Protocol Analysis Tool.
    14th International Conference on Computer-Aided Verification (CAV), 2002.

  167. Verified Bytecode Model Checkers.
    15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs), 2002.

  168. Bytecode Model Checking: An Experimental Analysis.
    9th International SPIN Workshop on Model Checking of Software, 2002.

  169. A Formal Analysis of the CORBA Security Service.
    The 2nd International Z and B Conference, 2002.

  170. A Formal Data-Model of the CORBA Security Service.
    8th European Software Engineering Conference (ESEC), 2001.

  171. Towards an Awareness-based Semantics for the Analysis of Security Protocols.
    Workshop on Logical Aspects of Cryptographic Protocol Verification, 2001.

  172. Maude versus Haskell: an Experimental Comparison in Security Protocol Analysis.
    International Workshop on Rewriting Logic and its Applications, 2001.

  173. Rewriting Logic as a Metalogical Framework.
    Foundations of Software Technology and Theoretical Computer Science (FSTTCS), 2000.

  174. B2M: A Semantic Based Tool for BLIF Hardware Descriptions.
    3rd International Conference on Formal Methods in Computer Aided Design (FMCAD), 2000.

  175. Decision Procedures for Inductive Boolean Functions based on Alternating Automata.
    12th International Conference on Computer-Aided Verification (CAV), 2000.

  176. Bounded Model Construction for Monadic Second-Order Logics.
    12th International Conference on Computer-Aided Verification (CAV), 2000.

  177. Combining Knowledge and Search to Solve Single-suit Bridge.
    Seventeenth National Conference on Artificial Intelligence (AAAI), 2000.

  178. Lazy Infinite-State Analysis of Security Protocols.
    Secure Networking -- CQRE [Secure] '99, 1999.

  179. Strategies Explained.
    Proceedings of the Fifth Game Programming Workshop in Japan (GPW), 1999.

  180. Java Byte Code Verification by Model Checking.
    11th International Conference on Computer-Aided Verification (CAV), 1999.

  181. Structural and Behavioral Modeling with Monadic Logics.
    IEEE International Symposium on Multiple-Valued Logic, 1999

  182. Scoped Metatheorems.
    International Workshop on Rewriting Logic and its Applications, 1998.

  183. Finding Optimal Strategies for Imperfect Information Games.
    Fifteenth National Conference on Artificial Intelligence (AAAI), 1998.

  184. Optimal Play Against Best Defence: Complexity and Heuristics.
    The First International Conference on Computers and Games (CG), 1998.

  185. LISA: A Specification Language Based on WS2S.
    Annual Conference of the European Association for Computer Science Logic (CSL), 1997.

  186. Monte-Carlo Sampling in Games with Incomplete Information: empirical investigation and analysis.
    Game-Tree Search in the Past, Present, and Future, 1997.

  187. Labelled Quantified Modal Logics.
    21st German Annual Conference on Artificial Intelligence, 1997.

  188. A New Method for Bounding the Complexity of Modal Logics.
    5th Kurt Goedel Colloquium (KGC) on Computational Logic and Proof Theory, 1997.

  189. Implementing Modal and Relevance Logics in a Logical Framework.
    Fifth International Conference On Principles of Knowledge Representation and Reasoning (KR), 1996.

  190. Modeling a Hardware Synthesis Methodology in Isabelle.
    1996 International Conference on Theorem Proving in Higher Order Logics (TPHOLs), 1996.

  191. Experiments in Automating Hardware Verification using Inductive Proof Planning.
    Formal Methods in Computer-Aided Design (FMCAD), 1996.

  192. Complexity Analysis Based on Ordered Resolution.
    11th Annual IEEE Symposium on Logic in Computer Science (LICS), 1996.

  193. Structuring Metatheory on Inductive Definitions.
    Thirteenth International Conference on Automated Deduction (CADE), 1996.

  194. Generic System Support for Deductive Program Development.
    Second International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 1996.

  195. Deriving and Applying Logic Program Transformers.
    Asian Computer Science Conference, 1995.

  196. Hardware Verification using Monadic Second-Order Logic.
    7th International Conference on Computer-Aided Verification (CAV), 1995.

  197. A Calculus for Rippling.
    Workshop on Conditional (and Typed) Term Rewriting Systems (CTRS), 1994.

  198. Coloured Rippling: An Extension of a Theorem P roving Heuristic.
    12th European Conference on Artificial Intelligence (ECAI), 1994.

  199. Logic Frameworks for Logic Programs.
    4th International Workshop on Logic Program Synthesis and Transformation, (LOPSTR), 1994.

  200. IsaWhelk: Whelk Interpreted in Isabelle.
    11th International Conference on Logic Programming (ICLP), 1994.

  201. Termination Orderings for Rippling.
    12th International Conference on Automated Deduction (CADE), 1994.

  202. A Conservative Extension of First Order Logic and its Applications to Theorem Proving.
    13th Conference of the Foundations of Software Technology and Theoretical Computer Science (FSTTCS), 1993.

  203. A Framework for Program Development Based on Schematic Proof.
    7th International Workshop on Software Specification and Design (IWSSD), 1993.

  204. Difference Unification.
    Thirteenth International Joint Conference on Artificial Intelligence (IJCAI), 1993.

  205. Middle-Out Reasoning for Logic Program Synthesis.
    10th International Conference on Logic Programming (ICLP), 1993.

  206. Finesse: An Adaptation of Proof-Planning to Declarer Play in Bridge.
    10th European Conference on Artificial Intelligence (ECAI), 1992.

  207. Difference Matching.
    11th International Conference On Automated Deduction (CADE), 1992.

  208. Some Normalization Properties of Martin-Lof's Type Theory, and Applications.
    Theoretical Aspects of Computer Software (TACS), 1991.

  209. Automating Meta-theory Creation and System Extension.
    Italian Association for Artificial Intelligence (AI*IA), 1991.

  210. Extracting Circuits from Constructive Proofs.
    IFIP-IEEE International Workshop on: Formal Methods in VLSI Design, 1991.

  211. Equality of Terms Containing Associative-Commutative Functions and Commutative Binding Operators is Isomorphism Complete.
    10th International Conference On Automated Deduction (CADE), 1990.

  212. Formally Verified Synthesis of CMOS.
    IMEC-IFIP International Workshop on Applied Formal Methods For Correct VLSI Design, 1989.

  213. Verification of Combinational Logic in Nuprl.
    Workshop on Hardware Specification, Verification and Synthesis: Mathematical Aspects, 1989.

  214. Building Theories in Nuprl.
    Logic At Botik, 1989.

  215. An Environment for Automated Reasoning about Partial Functions.
    9th International Conference On Automated Deduction (CADE), 1988.

Edited Volumes

  1. Second International Conference, Principles of Security and Trust.
    Springer, 2013.

  2. 5th ACM Symposium on Information, Computer and Communications Security.
    ACM Press, 2010.

  3. Second ACM Conference on Wireless Network Security.
    ACM Press, 2009.

  4. Automated Reasoning for Security Protocol Analysis.
    Special issue of the Journal of Automated Reasoning, 2006.

  5. ACM Workshop on Formal Methods in Security Engineering.
    ACM Press, 2004.

  6. International Joint Conference on Automated Reasoning.
    Springer-Verlag LNCS, 2004.

  7. Theorem Proving in Higher Order Logics.
    Springer-Verlag LNCS, 2003.

  8. ACM Workshop on Formal Methods in Security Engineering.
    ACM Press, 2003.

  9. Current Trends in Logical Frameworks and Metalanguages.
    Editorial for the Special Issue of the Journal of Automated Reasoning on Logical Frameworks and Meta-languages, 2001.

  10. Labelled Deduction.
    Kluwer Applied Logic Series, 2000

Miscellaneous

  1. A Theory of Black-Box Tests.
    Arxiv Technical Report, 2020.

  2. Fixing the Achilles Heel of E-Voting: The Bulletin Board.
    IACR Cryptology ePrint Archive, 2020.

  3. Solving Single-suit Bridge Play: Winning and Knowing Why. (Draft)

  4. Single-suit Bridge Play: computer outperforms human.
    The Bridge World, 2000.

  5. Building Problem Solving Environments in Constructive Type Theory.
    Ph.D. Dissertation, Cornell University, December 1989. Cornell Technical Report 89-1063.

Back to David Basin