Skip to main content
Kent Academic Repository

Tests for Establishing Security Properties

Cheval, Vincent, Delaune, Stéphanie, Ryan, Mark (2014) Tests for Establishing Security Properties. In: 9th International Symposium on Trustworthy Global Computing (TGC'14), September 2014, Roma, Italy. (doi:10.1007/978-3-662-45917-1_6) (KAR id:46879)


Ensuring strong security properties in some cases requires participants to carry out tests during the execution of a protocol. A classical example is electronic voting: participants are required to verify the presence of their ballots on a bulletin board, and to verify the computation of the election outcome. The notion of certificate transparency is another example, in which participants in the protocol are required to perform tests to verify the integrity of a certificate log.

We present a framework for modelling systems with such `testable properties', using the applied pi calculus. We model the tests that are made by participants in order to obtain the security properties. Underlying our work is an attacker model called ``malicious but cautious'', which lies in between the Dolev-Yao model and the ``honest but curious'' model. The malicious-but-cautious model is appropriate for cloud computing providers that are potentially malicious but are assumed to be cautious about launching attacks that might cause user tests to fail.

Item Type: Conference or workshop item (Paper)
DOI/Identification number: 10.1007/978-3-662-45917-1_6
Uncontrolled keywords: Cryptographic protocols, Formal verification, Symbolic model, Testable properties, Invisible attacks
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science
Q Science > QA Mathematics (inc Computing science) > QA 9 Formal systems, logics
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Vincent Cheval
Date Deposited: 23 Jan 2015 11:54 UTC
Last Modified: 08 Dec 2022 22:26 UTC
Resource URI: (The current URI for this page, for reference purposes)

University of Kent Author Information

Cheval, Vincent.

Creator's ORCID:
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.