Top

International Journal of Information Security

Published in:

01-06-2015 | Regular Contribution

Analysis of two authorization protocols using Colored Petri Nets

Authors: Younes Seifi, Suriadi Suriadi, Ernest Foo, Colin Boyd

Published in: International Journal of Information Security | Issue 3/2015

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

To prevent unauthorized access to protected trusted platform module (TPM) objects, authorization protocols, such as the object-specific authorization protocol (OSAP), have been introduced by the trusted computing group (TCG). By using OSAP, processes trying to gain access to the protected TPM objects need to prove their knowledge of relevant authorization data before access to the objects can be granted. Chen and Ryan’s 2009 analysis has demonstrated OSAP’s authentication vulnerability in sessions with shared authorization data. They also proposed the Session Key Authorization Protocol (SKAP) with fewer stages as an alternative to OSAP. Chen and Ryan’s analysis of SKAP using ProVerif proves the authentication property. The purpose of this paper was to examine the usefulness of Colored Petri Nets (CPN) and CPN Tools for security analysis. Using OSAP and SKAP as case studies, we construct intruder and authentication property models in CPN. CPN Tools is used to verify the authentication property using a Dolev–Yao-based model. Verification of the authentication property in both models using the state space tool produces results consistent with those of Chen and Ryan.

previous article Detection and analysis of eavesdropping in anonymous communication networks

next article Automated inference of past action instances in digital investigations

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Available only for authorised users

For other parts of the Fig. 9, the reference will be shown only by writing the ‘object’ word \(+\) coordinate. Other details will be eliminated.

This assumption is consistent with the formal model shown previously in [10].

Abadi, M., Blanchet, B.: Computer-assisted verification of a protocol for certified email. Sci. Comput. Program. 58(1–2), 3–27 (2005)CrossRefMATHMathSciNet

Al-Azzoni, I.: The verification of cryptographic protocols using Coloured Petri Nets. Master’s thesis, Department of Software Engineering (2004)

Al-Azzoni, Issam, Down, Douglas G., Khédri, Ridha: Modeling and verification of cryptographic protocols using Coloured Petri Nets and Design/CPN. Nord. J. Comput. 12(3), 200–228 (2005)

Aly, S., Mustafa, K.: Protocol verification and analysis using Colored Petri Nets. Depaul University (2003)

Bellare, M., Canetti, R., Krawczyk. H.: A modular approach to the design and analysis of authentication and key exchange protocols. In: Proceedings of the Thirtieth Annual ACM Symposium on Theory of Computing, pp. 419–428. ACM (1998)

Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In CSFW, number 0–7695-1146-5, pp. 82–96. IEEE Computer Society (2001)

Bozga, L., Lakhnech, Y., Périn, M.: Hermes: An automatic tool for verification of secrecy in security protocols. In: Computer Aided Verification, pp. 219–222. Springer (2003)

Brackin, S.H.: A HOL extension of GNY for automatically analyzing cryptographic protocols. In: Computer Security Foundations Workshop, 1996. Proceedings., 9th IEEE, pp. 62–76. IEEE (1996)

Burrows, M., Abadi, M., Needham, R.: A logic of authentication. ACM Trans. Comput. Syst. 8(1), 18–36 (1990)CrossRef

10.

Chen, L., Ryan, M.: Attack, solution and verification for shared authorisation data in TCG TPM. In: Formal Aspects in Security and Trust, pp. 201–216 (2010)

11.

Chen, L., Ryan, M.: Offline dictionary attack on TCG TPM weak authorisation data, and solution. In: Gawrock, D., Reimer, H., Sadeghi, A.-R., Vishik, C. (eds.) Future of Trust in Computing, pp. 193–196 . Vieweg+Teubner (2009)

12.

Cheng, A., Christensen, S., Mortensen, K.H.: Model checking Coloured Petri Nets exploiting strongly connected components. Citeseer (1997)

13.

Christensen, S., Mortensen, K.H.: Design/CPN ASK-CTL Manual (1996)

14.

Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244–263 (1986)

15.

Cremers, C.J.F.: The Scyther Tool: verification, falsification, and analysis of security protocols. In: Computer Aided Verification, pp. 414–418. Springer (2008)

16.

Doyle, E.M.: Automated security analysis of cryptographic protocols using Coloured Petri Net specifications (1997)

17.

Dutertre, B., Schneider, S.: Using a PVS embedding of CSP to verify authentication protocols. In: Theorem Proving in Higher Order Logics, pp. 121–136 (1997)

18.

Fontan, B., Mota, S., Villemur, T., Saqui-Sannes, P., Courtiat, J.P.: UML-based modeling and formal verification of authentication protocols (2006)

19.

Gong, L., Needham, R., Yahalom, R.: Reasoning about belief in cryptographic protocols. In: Research in Security and Privacy, 1990. Proceedings., 1990 IEEE Computer Society Symposium on, pp. 234–248. IEEE (1990)

20.

Hollestelle, G., Mauw, S., Cremers, C. J. F.: Systematic analysis of attacks on security protocols. Master’s Thesis, Technical University of Eindhover, Department of Mathematics and Computer Science (2005)

21.

ISO/IEC 18033–2.: Information technology—Security techni- ques—Encryption algorithms—part 2: Asymetric ciphers (2006) http://www.iso.org/iso/home/store/catalogue_tc/catalogue_detail.htm?csnumber=37971

22.

ISO/IEC 18033–3.: Information technology—Security techni- ques—Encryption algorithms—part 3: Block ciphers (2005)http://www.iso.org/iso/home/store/catalogue_ics/catalogue_detail_ics.htm?csnumber=37972

23.

ISO/IEC 19772.: Information technology—Security techniques— Authenticated encryption (2009)http://www.iso.org/iso/catalogue_detail?csnumber=46345

24.

ISO/IEC 9797–2.: Information technology—security techniques—Message Authentication Codes (MACs)—part 2: Mechanisms using a dedicated hash-function (2002)

25.

Jensen, K.: A brief introduction to Coloured Petri Nets. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 203–208. Springer, Berlin, Heidelberg (1997)

26.

Jensen, K.: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use, volume 1, Basic Concepts. Monographs in Theoretical Computer Science. Springer, New York, 2nd corrected printing 1997, ISBN: 3-540-60943-1 (1997)

27.

Jensen, K.: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use., volume 2, Analysis Methods. Monographs in Theoretical Computer Science. Springer, New York, 2nd corrected printing 1997, ISBN: 3-540-58276-2 (1997)

28.

Jensen, K.: Special section on Coloured Petri Nets. Int. J. Softw. Tools Technol. Transf. (STTT) 9(3), 209–212 (2007)

29.

Jensen, K., Kristensen, L.M., Wells, L.: Coloured Petri Nets and CPN tools for modelling and validation of concurrent systems. Int. J. Softw. Tools Technol. Transf. (STTT) 9(3), 213–254 (2007)CrossRef

30.

Jensen, K., Kristensen, L.M.: Coloured Petri Nets—Modelling and Validation of Concurrent Systems. Springer, Berlin (2009)CrossRef

31.

Lowe, G.: An attack on the Needham-Schroeder public-key authentication protocol. Inf. Process. Lett. 56(3), 131–133 (1995)CrossRefMATH

32.

Meadows, C.A.: Formal verification of cryptographic protocols: A survey. Advances in Cryptology—ASIACRYPT’94, pp. 133–150 (1995)

33.

Millen, J.K., Clark, S.C., Freedman, S.B.: The interrogator: Protocol security analysis. IEEE Trans. Softw. Eng. SE–13(2), 274–288 (1987)CrossRef

34.

Mitchell, C.: Trusted computing, volume 6. Iet (2005)

35.

Rubin, A.D., Honeyman, P.: Formal Methods for the Analysis of Authentication Protocols. Technical report, Citeseer (1993)

36.

Schneider, S.: Verifying authentication protocols in CSP. IEEE Trans. Softw. Eng. 24(9), 741–758 (1998)CrossRef

37.

Seifi, Y., Suriadi, S., Foo, E., Boyd, C.: Analysis of Object-Specific Authorization Protocol (OSAP) using Coloured Petri Net. In: AISC2012 Proceedings (2012)

38.

Seifi, Y., Suriadi, S., Foo, E., Boyd, C.: Analysis of Object-Specific Authorization Protocol (OSAP) using Coloured Petri Nets—version 1.0. Technical report, Queensland University of Technology (2011)

39.

Tarigan, A. et al.: Survey in Formal Analysis of Security Properties of Cryptographic Protocol. Universität Bielefeld (2002)

40.

TCG.: TCG Specification Architecture Overview Revision 1.4 (2007)

41.

TCG.: TCG TPM specification 1.2, http://www.trustedcomputinggroup.org (2003)

42.

TCG.: TCG TPM specification 2.0, http://www.trustedcomputinggroup.org/resources/-trusted_platform_module_specifications_in_public_review (2013)

43.

Viganò, Luca: Automated security protocol analysis with the AVISPA tool. Electron. Notes Theor. Comput. Sci. 155, 61–86 (2006)CrossRef

44.

Westergaard, M., Evangelista, S., Kristensen, L.: ASAP: An extensible platform for state space analysis. Applications and theory of petri nets, pp. 303–312 (2009)

45.

Westergaard, M., Maggi, F.M.: Modeling and verification of a protocol for operational support using coloured petri nets. Applications and Theory of Petri Nets. volume 6709 of Lecture Notes in Computer Science, pp. 169–188. Springer, Berlin/Heidelberg (2011)

46.

Woo, T.Y.C., Lam, S.S.: A semantic model for authentication protocols. In: Research in Security and Privacy, 1993. Proceedings., 1993 IEEE Computer Society Symposium on, pp. 178–194. IEEE (1993)

47.

Woo, T.Y.C., Lam, S.S.: Verifying authentication protocols: Methodology and example. In Network Protocols, 1993. Proceedings., 1993 International Conference on, pp. 36–45. IEEE (1993)

48.

Yao, A.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198–208 (1983)CrossRefMATH

Title: Analysis of two authorization protocols using Colored Petri Nets
Authors: Younes Seifi
Suriadi Suriadi
Ernest Foo
Colin Boyd
Publication date: 01-06-2015
Publisher: Springer Berlin Heidelberg
Published in: International Journal of Information Security / Issue 3/2015
Print ISSN: 1615-5262
Electronic ISSN: 1615-5270
DOI: https://doi.org/10.1007/s10207-014-0243-z

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Technik"

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Other articles of this Issue 3/2015

A new algorithm for low-deterministic security

Detection and analysis of eavesdropping in anonymous communication networks

GPU-assisted malware

Automated inference of past action instances in digital investigations

Premium Partner