Visible to the public Biblio

Filters: Keyword is symbolic model  [Clear All Filters]
2019-11-12
Dreier, Jannik, Hirschi, Lucca, Radomirovic, Sasa, Sasse, Ralf.  2018.  Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR. 2018 IEEE 31st Computer Security Foundations Symposium (CSF). :359-373.

Exclusive-or (XOR) operations are common in cryptographic protocols, in particular in RFID protocols and electronic payment protocols. Although there are numerous applications, due to the inherent complexity of faithful models of XOR, there is only limited tool support for the verification of cryptographic protocols using XOR. The Tamarin prover is a state-of-the-art verification tool for cryptographic protocols in the symbolic model. In this paper, we improve the underlying theory and the tool to deal with an equational theory modeling XOR operations. The XOR theory can be freely combined with all equational theories previously supported, including user-defined equational theories. This makes Tamarin the first tool to support simultaneously this large set of equational theories, protocols with global mutable state, an unbounded number of sessions, and complex security properties including observational equivalence. We demonstrate the effectiveness of our approach by analyzing several protocols that rely on XOR, in particular multiple RFID-protocols, where we can identify attacks as well as provide proofs.

2018-02-28
Cheval, V., Cortier, V., Warinschi, B..  2017.  Secure Composition of PKIs with Public Key Protocols. 2017 IEEE 30th Computer Security Foundations Symposium (CSF). :144–158.

We use symbolic formal models to study the composition of public key-based protocols with public key infrastructures (PKIs). We put forth a minimal set of requirements which a PKI should satisfy and then identify several reasons why composition may fail. Our main results are positive and offer various trade-offs which align the guarantees provided by the PKI with those required by the analysis of protocol with which they are composed. We consider both the case of ideally distributed keys but also the case of more realistic PKIs.,,Our theorems are broadly applicable. Protocols are not limited to specific primitives and compositionality asks only for minimal requirements on shared ones. Secure composition holds with respect to arbitrary trace properties that can be specified within a reasonably powerful logic. For instance, secrecy and various forms of authentication can be expressed in this logic. Finally, our results alleviate the common yet demanding assumption that protocols are fully tagged.