Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Buchtitelbild

2020 | OriginalPaper | Buchkapitel

Modeling and Verification of the Nervos CKB Block Synchronization Protocol in UPPAAL

verfasst von : Qi Zhang, Yuteng Lu, Meng Sun

Erschienen in: Blockchain and Trustworthy Systems

Verlag: Springer Singapore

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

The Nervos CKB (Common Knowledge Base) is a public permission-less blockchain designed for a peer-to-peer crypto- economy network. The CKB block synchronization protocol is an important part of the Nervos CKB, which provides a set of rules that participating nodes must obey while synchronizing their blocks. The protocol contains three stages: Connecting Header, Downloading Block and Accepting Block. In this paper, we develop the formal model of the CKB block synchronization protocol and verify some important properties of the protocol using the UPPAAL model checker. Based on the formal model, the reliability of CKB can be guaranteed.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel Correction to: Scalable and Communication-Efficient Decentralized Federated Edge Learning with Multi-blockchain Framework
Nächstes Kapitel A Blockchain Consensus Mechanism for Marine Data Management System
Literatur
1.
Abdellatif, T., Brousmiche, K.-L.: Formal verification of smart contracts based on users and blockchain behaviors models. In: 2018 9th IFIP International Conference on New Technologies, Mobility and Security (NTMS), pp. 1–5. IEEE (2018)
2.
3.
Bai, X., Cheng, Z., Duan, Z., Hu, K.: Formal modeling and verification of smart contracts. In: Proceedings of ICSCA 2018, pp. 322–326. ACM (2018)
4.
5.
Bhargavan, K., Blanchet, B., Kobeissi, N.: Verified models and reference implementations for the TLS 1.3 standard candidate. In: 2017 IEEE Symposium on Security and Privacy, pp. 483–502. IEEE (2017)
6.
Bigi, G., Bracciali, A., Meacci, G., Tuosto, E.: Validation of decentralised smart contracts through game theory and formal methods. In: Bodei, C., Ferrari, G.-L., Priami, C. (eds.) Programming Languages with Applications to Biology and Security. LNCS, vol. 9465, pp. 142–161. Springer, Cham (2015). https://​doi.​org/​10.​1007/​978-3-319-25527-9_​11CrossRefMATH
7.
Chaudhary, K., Fehnker, A., van de Pol, J., Stoelinga, M.: Modeling and verification of the bitcoin protocol. In: Proceedings of MARS 2015, EPTCS, pp. 46–60. Open Publishing Association, November 2015
8.
9.
David, A., Larsen, K.G., Legay, A., Mikuǎionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transfer 17(4), 397–415 (2015)CrossRef
10.
Ellul, J., Pace, G.J.: Runtime verification of ethereum smart contracts. In: Proceedings of EDCC 2018, pp. 158–163. IEEE Computer Society (2018)
11.
12.
Lu, Y., Sun, M.: Modeling and verification of IEEE 802.11i security protocol in UPPAAL for internet of things. Int. J. Softw. Eng. Knowl. Eng. 28(11–12), 1619–1636 (2018)CrossRef
13.
Madl, G., Bathen, L.A.D., Flores, G.H., Jadav, D.: Formal verification of smart contracts using interface automata. In: Proceedings of Blockchain 2019, pp. 556–563. IEEE (2019)
14.
15.
16.
Zheng, Z., Xie, S., Dai, H., Chen, X., Wang, H.: Blockchain challenges and opportunities: a survey. Int. J. Web Grid Serv. 14(4), 352–375 (2018)CrossRef
Metadaten
Titel
Modeling and Verification of the Nervos CKB Block Synchronization Protocol in UPPAAL
verfasst von
Qi Zhang
Yuteng Lu
Meng Sun
Copyright-Jahr
2020
Verlag
Springer Singapore
Buch
Blockchain and Trustworthy Systems

Print ISBN: 978-981-15-9212-6

Electronic ISBN: 978-981-15-9213-3

Copyright-Jahr: 2020

DOI
https://doi.org/10.1007/978-981-15-9213-3_1

Premium Partner

    Bildnachweise