(2016) Automated analysis of security protocols with global state.
Abstract
Security APIs, key servers and protocols that need to keep the status of transactions, require to maintain a global, non-monotonic state, e.g., in the form of a database or register. However, most existing automated verification tools do not support the analysis of such stateful security protocols -- sometimes because of fundamental reasons, such as the encoding of the protocol as Horn clauses, which are inherently monotonic. A notable exception is the recent tamarin prover which allows specifying protocols as multiset rewrite (msr) rules, a formalism expressive enough to encode state. As multiset rewriting is a ``low-level'' specification language with no direct support for concurrent message passing, encoding protocols correctly is a difficult and error-prone process. We propose a process calculus which is a variant of the applied pi calculus with constructs for manipulation of a global state by processes running in parallel. We show that this language can be translated to msr rules whilst preserving all security properties expressible in a dedicated first-order logic for security properties. The translation has been implemented in a prototype tool which uses the tamarin prover as a backend. We apply the tool to several case studies among which a simplified fragment of PKCS\\#11, the Yubikey security token, and an optimistic contract signing protocol.
| Item Type: | Article |
|---|---|
| Additional Information: | pub_id: 1062 Bibtex: KK-jcs16 URL date: None |
| Uncontrolled Keywords: | automated verification,security APIs,stateful security protocols |
| Divisions: | Michael Backes (InfSec) |
| Depositing User: | Sebastian Weisgerber |
| Date Deposited: | 26 Jul 2017 10:28 |
| Last Modified: | 18 Jul 2019 12:09 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/156 |
Actions
Actions (login required)
 |
View Item |