2025
SoK: Attacks on Modern Card Payments.
CoRR, April, 2025
2024
A Formal Analysis of Apple's iMessage PQ3 Protocol.
IACR Cryptol. ePrint Arch., 2024
A Spectral Analysis of Noise: A Comprehensive, Automated, Formal Analysis of Diffie-Hellman Protocols.
IACR Cryptol. ePrint Arch., 2024
Getting Chip Card Payments Right.
Proceedings of the Formal Methods - 26th International Symposium, 2024
2023
Sound Verification of Security Protocols: From Design to Interoperable Implementations.
Proceedings of the 44th IEEE Symposium on Security and Privacy, 2023
2022
Sound Verification of Security Protocols: From Design to Interoperable Implementations.
Dataset, August, 2022
Sound Verification of Security Protocols: From Design to Interoperable Implementations.
Dataset, August, 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
"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
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
2020
Verification of stateful cryptographic protocols with exclusive OR.
J. Comput. Secur., 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
Formal Analysis and Implementation of a TPM 2.0-based Direct Anonymous Attestation Scheme.
Proceedings of the ASIA CCS '20: The 15th ACM Asia Conference on Computer and Communications Security, 2020
Privacy-Preserving OpenID Connect.
Proceedings of the ASIA CCS '20: The 15th ACM Asia Conference on Computer and Communications Security, 2020
2019
Seems Legit: Automated Analysis of Subtle Attacks on Protocols that Use Signatures.
IACR Cryptol. ePrint Arch., 2019
Security Issues in the 5G Standard and How Formal Methods Come to the Rescue.
ERCIM News, 2019
Proxy Certificates: The Missing Link in the Web's Chain of Trust.
CoRR, 2019
A Symbolic Analysis of ECC-Based Direct Anonymous Attestation.
Proceedings of the IEEE European Symposium on Security and Privacy, 2019
User Account Access Graphs.
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
2018
Design, Analysis, and Implementation of ARPKI: An Attack-Resilient Public-Key Infrastructure.
IEEE Trans. Dependable Secur. Comput., 2018
Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR.
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
2017
Symbolically analyzing security protocols using tamarin.
ACM SIGLOG News, 2017
Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols.
Proceedings of the Principles of Security and Trust - 6th International Conference, 2017
2016
Automated Symbolic Proofs of Security Protocols.
Proceedings of the 30th International Workshop on Unification, 2016
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
Automated Verification of Group Key Agreement Protocols.
Proceedings of the 2014 IEEE Symposium on Security and Privacy, 2014
ARPKI: Attack Resilient Public-Key Infrastructure.
Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, 2014
2013
Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis.
Proceedings of the Automated Deduction - CADE-24, 2013
2012
Security models in rewriting logic for cryptographic protocols and browsers
PhD thesis, 2012
Folding variant narrowing and optimal variant termination.
J. Log. Algebraic Methods Program., 2012
IBOS: A Correct-By-Construction Modular Browser.
Proceedings of the Formal Aspects of Component Software, 9th International Symposium, 2012
Effective Symbolic Protocol Analysis via Equational Irreducibility Conditions.
Proceedings of the Computer Security - ESORICS 2012, 2012
2011
Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis.
Proceedings of the 25th International Workshop on Unification, 2011
Protocol analysis in Maude-NPA using unification modulo homomorphic encryption.
Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2011
2010
Protocol Analysis Modulo Combination of Theories: A Case Study in Maude-NPA.
Proceedings of the Security and Trust Management - 6th International Workshop, 2010
2009
Model-Checking DoS Amplification for VoIP Session Initiation.
Proceedings of the Computer Security, 2009
2008
Variant Narrowing and Equational Unification.
Proceedings of the Seventh International Workshop on Rewriting Logic and its Applications, 2008
Equational Unification by Variant Narrowing (Extended Abstract).
Proceedings of the 22nd International Workshop on Unification, 2008
Effectively Checking the Finite Variant Property.
Proceedings of the Rewriting Techniques and Applications, 19th International Conference, 2008
2007
A Systematic Approach to Uncover Security Flaws in GUI Logic.
Proceedings of the 2007 IEEE Symposium on Security and Privacy (S&P 2007), 2007
,
,
,
,
,
,
,
,
,
,
,
,
,
,
Proceedings of the All About Maude, 2007
2006
Java+ITP: A Verification Tool Based on Hoare Logic and Algebraic Semantics.
Proceedings of the 6th International Workshop on Rewriting Logic and its Applications, 2006
2005
Automatic Validation of Transformation Rules for Java Verification Against a Rewriting Semantics.
Proceedings of the Logic for Programming, 2005