Abstract
We consider the refinement-based process for the development of security protocols. Our approach is based on the Event B refinement, which makes proofs easier and which makes the design process faithfull to the structure of the protocol as the designer thinks of it. We introduce the notion of mechanism related to a given security property; a mechanism can be combined with another mechanism through the double refinement process ensuring the preservation of previous security properties of mechanisms. Mechanisms and combination of mechanisms are based on Event B models related to the security property of the current mechanism. Analysing cryptographic protocols requires precise modelling of the attacker’s knowledge and the attacker’s behaviour conforms to the Dolev-Yao model.
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
Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2009) (forthcoming book)
Abrial, J.-R., Hallerstede, S.: Refinement, decomposition, and instantiation of discrete models: Application to event-b. Fundam. Inform. 77(1-2), 1–28 (2007)
Benassa, N.: Modelling attacker’s knowledge for cascade cryptographic protocols. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 251–264. Springer, Heidelberg (2008)
Benaïssa, N., Méry, D.: Cryptologic protocols analysis using Event B. In: Marchuk, A. (réd.) Seventh International Andrei Ershov Memorial Conference Perspectives of System Informatics, Novosibirsk, Akademgorodok, Russia, June 15-19. LNCS. Springer, Heidelberg (2010)
Blake-Wilson, S., Menezes, A.: Entity authentication and authenticated key transport protocols employing asymmetric techniques. In: Christianson, B., Lomas, M. (eds.) Security Protocols 1997. LNCS, vol. 1361, pp. 137–158. Springer, Heidelberg (1998)
Cansell, D., Paul Gibson, J., Méry, D.: Refinement: A constructive approach to formal software design for a secure e-voting interface. Electr. Notes Theor. Comput. Sci. 183, 39–55 (2007)
Cansell, D., Méry, D.: The Event B Modelling Method: Concepts and Case Studies, pp. 33–140. Springer, Heidelberg (2007)
Mathuria, A., Boyd, C.: Protocols for Authentication and Key Establishment (2003)
Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)
Gamma, E., Helm, R., Johnson, R., Vlissides, R., Gamma, P.: Design Patterns: Elements of Reusable Object-Oriented Software Design Patterns. Addison-Wesley Professional Computing, Reading (1997)
Jerdonek, R., Honeyman, P., Coffman, K., Rees, J., Wheeler, K.: Implementation of a provably secure, smartcard-based key distribution protocol. In: Schneier, B., Quisquater, J.-J. (eds.) CARDIS 1998. LNCS, vol. 1820, pp. 229–235. Springer, Heidelberg (2000)
Lowe, G.: Breaking and fixing the needham-schroeder public-key protocol using fdr. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)
Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993–999 (1978)
Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6, 85–128 (1998)
Project RODIN. The rodin project: Rigorous open development environment for complex systems, http://rodin-b-sharp.sourceforge.net/
Syverson, P.F., Van Oorschot, P.C.: On unifying some cryptographic protocol logics. In: SP ’94: Proceedings of the 1994 IEEE Symposium on Security and Privacy, Washington, DC, USA, p. 14. IEEE Computer Society, Los Alamitos (1994)
ISO. Information technology - Security techniques - Key management - Part 2: Mechanisms Using Symmetric techniques ISO/IEC 11770-2, International Standard (1996)
ISO. Information technology - Security techniques - Entity authentication - Part 2: Mechanisms Using Symmetric Encipherment Algorithms ISO/IEC 9798-2, 2nd edn. International Standard (1999)
Clifford Neuman, B., Ts’o, T.: Kerberos: An authentication service for computer networks. IEEE Communications magazine 32(9), 33–38 (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Benaissa, N., Méry, D. (2010). Proof-Based Design of Security Protocols. In: Ablayev, F., Mayr, E.W. (eds) Computer Science – Theory and Applications. CSR 2010. Lecture Notes in Computer Science, vol 6072. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13182-0_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-13182-0_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-13181-3
Online ISBN: 978-3-642-13182-0
eBook Packages: Computer ScienceComputer Science (R0)