Skip to main content
SpringerLink
Log in

Mapping Requirements Specifications into a Formalized Blockchain-Enabled Authentication Protocol for Secured Personal Identity Assurance

  • Conference paper
  • First Online:
Future Data and Security Engineering (FDSE 2017)

Part of the book series: Lecture Notes in Computer Science ((LNISA,volume 10646))

Included in the following conference series:

Abstract

The design and development of novel security and authentication protocols is a challenging task. Design flaws, security and privacy issues as well as incomplete specifications pose risks for its users. Authcoin is a blockchain-based validation and authentication protocol for secure identity assurance. Formal methods, such as Colored Petri Nets (CPNs), are suitable to design, develop and analyze such new protocols in order to detect flaws and mitigate identified security risks. In this work, the Authcoin protocol is formalized using Colored Petri Nets resulting in a verifiable CPN model. An Agent-Oriented Modeling (AOM) methodology is used to create goal models and corresponding behavior models. Next, these models are used to derive the Authcoin CPN models. The modeling strategy as well as the required protocol semantics are explained in detail. Furthermore, we conduct a state-space analysis on the resulting CPN model and derive specific model properties. The result is a complete and correct formal specification that is used to guide future implementations of Authcoin.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    https://whispersystems.org/.

  2. 2.

    http://cpntools.org/.

  3. 3.

    https://www.agrello.org/.

References

  1. Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: the spi calculus. In: Proceedings of the 4th ACM Conference on Computer and Communications Security, pp. 36–47. ACM (1997)

    Google Scholar 

  2. Ahmed, N., Matulevičius, R.: Securing business processes using security risk-oriented patterns. Comput. Stand. Interfaces 36(4), 723–733 (2014)

    Article  Google Scholar 

  3. Aly, S., Mustafa, K.: Protocol Verification and Analysis Using Colored Petri Nets (2004)

    Google Scholar 

  4. Brook, C.: Nuclear power plant disrupted by cyber attack (2016). https://threatpost.com/nuclear-power-plant-disrupted-by-cyber-attack/121216/. Accessed 26 Apr 2017

  5. Buterin, V.: Ethereum: A Next-Generation Smart Contract and Decentralized Application Platform (2014). https://github.com/ethereum/wiki/wiki/White-Paper. Accessed 13 Mar 2017

  6. Cam-Winget, N., Housley, R., Wagner, D., Walker, J.: Security flaws in 802.11 data link protocols. Commun. ACM 46(5), 35–39 (2003)

    Article  Google Scholar 

  7. Carlsen, U.: Cryptographic protocol flaws: know your enemy. In: Computer Security Foundations Workshop VII, CSFW 7, Proceedings, pp. 192–200. IEEE (1994)

    Google Scholar 

  8. Cohn-Gordon, K., Cremers, C., Dowling, B., Garratt, L., Stebila, D.: A formal security analysis of the signal messaging protocol. https://eprint.iacr.org/2016/1013.pdf. Accessed 26 Apr 2017

  9. Crazzolara, F., Winskel, G.: Events in security protocols. In: Proceedings of the 8th ACM Conference on Computer and Communications Security, pp. 96–105. ACM (2001)

    Google Scholar 

  10. Dai, P., Mahi, N., Earls, J., Norta, A.: Smart-contract value-transfer protocols on a distributed mobile application platform (2017). https://qtum.org/uploads/files/cf6d69348ca50dd985b60425ccf282f3.pdf. Accessed 13 Mar 2017

  11. DeLoach, S.A.: Analysis and Design using MaSE and agentTool. Technical report, DTIC Document (2001)

    Google Scholar 

  12. Dresp, W.: Security analysis of the secure authentication protocol by means of coloured petri nets. In: Dittmann, J., Katzenbeisser, S., Uhl, A. (eds.) CMS 2005. LNCS, vol. 3677, pp. 230–239. Springer, Heidelberg (2005). https://doi.org/10.1007/11552055_23

    Chapter  Google Scholar 

  13. Edwards, K.: Cryptographic protocol specification and analysis using Coloured Petri Nets and Java. Ph.D. thesis, Queen’s University Kingston (1999)

    Google Scholar 

  14. Fábrega, F.J.T., Herzog, J.C., Guttman, J.D.: Strand spaces: why is a security protocol correct? In: 1998 IEEE Symposium on Security and Privacy, Proceedings, pp. 160–171. IEEE (1998)

    Google Scholar 

  15. Giorgini, P., Mylopoulos, J., Sebastiani, R.: Goal-oriented requirements analysis and reasoning in the tropos methodology. Eng. Appl. Artif. Intell. 18(2), 159–171 (2005)

    Article  Google Scholar 

  16. Hoare, C.A.R.: Communicating sequential processes. In: Hansen, P.B. (ed.) The Origin of Concurrent Programming, pp. 413–443. Springer, New York (1978). https://doi.org/10.1007/978-1-4757-3472-0_16

    Chapter  Google Scholar 

  17. Jensen, K.: Coloured petri nets. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) ACPN 1986. LNCS, vol. 254, pp. 248–299. Springer, Heidelberg (1987). https://doi.org/10.1007/978-3-540-47919-2_10

    Chapter  Google Scholar 

  18. 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. Transfer 9(3–4), 213–254 (2007)

    Article  Google Scholar 

  19. Leiding, B.: Securing the Authcoin Protocol using security risk-oriented patterns. Master’s thesis, University of Göttingen, Germany, DE (2017)

    Google Scholar 

  20. Leiding, B., Cap, C.H., Mundt, T., Rashidibajgan, S.: Authcoin: validation and authentication in decentralized networks. In: The 10th Mediterranean Conference on Information Systems - MCIS 2016, Cyprus, CY, September 2016

    Google Scholar 

  21. Mahunnah, M., Norta, A., Ma, L., Taveter, K.: Heuristics for designing and evaluating socio-technical agent-oriented behaviour models with Coloured Petri Nets. In: 2014 IEEE 38th International Computer Software and Applications Conference Workshops (COMPSACW), pp. 438–443. IEEE (2014)

    Google Scholar 

  22. Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, I. Inform. Comput. 100(1), 1–40 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  23. Moulin, B., Cloutier, L.: Collaborative work based on multiagent architectures: a methodological perspective. In: Soft Computing, pp. 261–296. Prentice-Hall Inc., Upper Saddle River (1994)

    Google Scholar 

  24. Moulin, B., Brassard, M.: A scenario-based design method and an environment for the development of multiagent systems. In: Zhang, C., Lukose, D. (eds.) DAI 1995. LNCS, vol. 1087, pp. 216–232. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61314-5_32

    Chapter  Google Scholar 

  25. Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008). https://bitcoin.org/bitcoin.pdf. Accessed 26 Apr 2017

  26. Norta, A., CINCO, Collaborative and Interoperable Computing: Safeguarding trusted eBusiness transactions of lifecycles for cross-enterprise collaboration. University of Helsinki, Department of Computer Science, Helsinki, Finland, Technical report C-2012-1 (2012)

    Google Scholar 

  27. Padgham, L., Winikoff, M.: Prometheus: a methodology for developing intelligent agents. In: Giunchiglia, F., Odell, J., Weiß, G. (eds.) AOSE 2002. LNCS, vol. 2585, pp. 174–185. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36540-0_14

    Chapter  Google Scholar 

  28. Petri, C.A.: Kommunikation mit Automaten. Ph.D. thesis, Technical University of Darmstadt (1962)

    Google Scholar 

  29. Sornkhom, P., Permpoontanalarp, Y.: Security analysis of Micali’s fair contract signing protocol by using Coloured Petri Nets. In: 2008 Ninth ACIS International Conference on Software Engineering, Artificial Intelligence, Networking, and Parallel/Distributed Computing (2008)

    Google Scholar 

  30. Sterling, L., Taveter, K.: The Art of Agent-Oriented Modeling. MIT Press, Cambridge (2009)

    Google Scholar 

  31. Stubblefield, A., Ioannidis, J., Rubin, A.D.: A key recovery attack on the 802.11b Wired Equivalent Privacy Protocol (WEP). ACM Trans. Inform. Syst. Secur. (TISSEC) 7(2), 319–332 (2004)

    Article  Google Scholar 

  32. Vanek, T., Rohlik, M.: Model of DoS resistant broadcast authentication protocol in Colored Petri Net environment. In: Proceedings of 17th International Conference Systems, Signals and Image Processing, (IWSSIP 2010), pp. 264–267 (2010)

    Google Scholar 

  33. Vaudenay, S.: Security flaws induced by CBC padding — applications to SSL, IPSEC, WTLS. In: Knudsen, L.R. (ed.) EUROCRYPT 2002. LNCS, vol. 2332, pp. 534–545. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-46035-7_35

    Chapter  Google Scholar 

  34. Wood, G.: Ethereum: A Secure Decrentralized Generalised Transaction Ledger (2014). http://gavwood.com/paper.pdf. Accessed 13 Mar 2017

  35. Wooldridge, M., Jennings, N.R., Kinny, D.: The Gaia methodology for agent-oriented analysis and design. Auton. Agent. Multi-Agent Syst. 3(3), 285–312 (2000)

    Article  Google Scholar 

  36. Xu, Y., Xie, X.: Modeling and analysis of security protocols using Colored Petri Nets. JCP 6(1), 19–27 (2011)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Science, University of Göttingen, Göttingen, Germany

    Benjamin Leiding

  2. Department of Software Systems, Tallinn University of Technology, Tallinn, Estonia

    Alex Norta

Authors
  1. Benjamin Leiding
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alex Norta
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Benjamin Leiding .

Editor information

Editors and Affiliations

  1. HCMC University of Technology, Ho Chi Minh City, Vietnam

    Tran Khanh Dang

  2. Johannes Kepler University Linz, Linz, Austria

    Roland Wagner

  3. Johannes Kepler University Linz, Linz, Austria

    Josef Küng

  4. Ho Chi Minh City University of Technolog , Ho Chi Minh City, Vietnam

    Nam Thoai

  5. Hosei University, Koganei, Tokyo, Japan

    Makoto Takizawa

  6. University of Vienna, Vienna, Austria

    Erich J. Neuhold

A Appendix

A Appendix

1.1 A.1 CPN Model

https://owncloud.gwdg.de/index.php/s/tfCNiFQtdNJKESG

1.2 A.2 Goal Model

https://owncloud.gwdg.de/index.php/s/yUHx8DFN57TqTIn

1.3 A.3 Behavior Interfaces of Activities

https://owncloud.gwdg.de/index.php/s/JCMD0ft3tQUbeSp

1.4 A.4 Protocol Semantics

https://owncloud.gwdg.de/index.php/s/OS7WcjrUEklSH0T

1.5 A.5 State-Space Analysis

https://owncloud.gwdg.de/index.php/s/nQwMLr7mK78z8wk

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Leiding, B., Norta, A. (2017). Mapping Requirements Specifications into a Formalized Blockchain-Enabled Authentication Protocol for Secured Personal Identity Assurance. In: Dang, T., Wagner, R., Küng, J., Thoai, N., Takizawa, M., Neuhold, E. (eds) Future Data and Security Engineering. FDSE 2017. Lecture Notes in Computer Science(), vol 10646. Springer, Cham. https://doi.org/10.1007/978-3-319-70004-5_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-70004-5_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-70003-8

  • Online ISBN: 978-3-319-70004-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation