Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proc. 28th ACM Symp. on Principles of Programming Lanes (POPL 2001) (2001)
Arapinis, M., Chothia, T., Ritter, E., Ryan, M.: Analysing unlinkability and anonymity using the applied pi calculus. In: Proc. 23rd IEEE Computer Security Foundations Symposium (CSF 2010) (2010)
Aumann, Y., Lindell, Y.: Security against covert adversaries: Efficient protocols for realistic adversaries. In: Vadhan, S.P. (ed.) TCC 2007. LNCS, vol. 4392, pp. 137–156. Springer, Heidelberg (2007)
Bruso, M., Chatzikokolakis, K., den Hartog, J.: Formal verification of privacy for RFID systems. In: Proc. 23rd IEEE Computer Security Foundations Symposium (CSF 2010). IEEE Computer Society Press (2010)
Bursuc, S., Grewal, G.S., Ryan, M.D.: Trivitas: Voters directly verifying votes. In: Kiayias, A., Lipmaa, H. (eds.) VoteID 2011. LNCS, vol. 7187, pp. 190–207. Springer, Heidelberg (2012)
Cheval, V.: APTE (Algorithm for Proving Trace Equivalence) (2013). http://projects.lsv.ens-cachan.fr/APTE/
Cheval, V., Comon-Lundh, H., Delaune, S.: Trace equivalence decision: Negative tests and non-determinism. In: Proc. 18th ACM Conference on Computer and Communications Security (CCS 2011) (2011)
Damgård, I., Keller, M., Larraia, E., Pastro, V., Scholl, P., Smart, N.P.: Practical covertly secure mpc for dishonest majority – or: Breaking the spdz limits. In: Crampton, J., Jajodia, S., Mayes, K. (eds.) ESORICS 2013. LNCS, vol. 8134, pp. 1–18. Springer, Heidelberg (2013)
Delaune, S., Kremer, S., Ryan, M.D.: Verifying privacy-type properties of electronic voting protocols. Journal of Computer Security 4, 435–487 (2008)
Grewal, G.S., Ryan, M.D., Bursuc, S., Ryan, P.Y.A.: Caveat coercitor: Coercion-evidence in electronic voting. In: IEEE Symposium on Security and Privacy, pp. 367–381 (2013)
Kremer, S., Ryan, M., Smyth, B.: Election verifiability in electronic voting protocols. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol. 6345, pp. 389–404. Springer, Heidelberg (2010)
Laurie, B., Langley, A., Kasper, E.: Certificate Transparency. RFC 6962 (Experimental) (2013)
Merkle, R.C.: A digital signature based on a conventional encryption function. In: Pomerance, C. (ed.) CRYPTO 1987. LNCS, vol. 293, pp. 369–378. Springer, Heidelberg (1988)
Nakamoto, S.: Bitcoin: A peer-to-peer electronic cash system (2008)
Roberts, P.: Phony SSL certificates issued for Google. Skype, others, Yahoo (March 2011)
Sterling, T.: Second firm warns of concern after Dutch hack (September 2011)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cheval, V., Delaune, S., Ryan, M. (2014). Tests for Establishing Security Properties. In: Maffei, M., Tuosto, E. (eds) Trustworthy Global Computing. TGC 2014. Lecture Notes in Computer Science(), vol 8902. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-45917-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-662-45917-1_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-45916-4
Online ISBN: 978-3-662-45917-1
eBook Packages: Computer ScienceComputer Science (R0)