EasyChair Publications
Search
Paper Information
Paper:Takahiro Kubota, Yoshihiko Kakutani, Go Kato, Yasuhito Kawano and Hideki Sakurada
Automated Verification of Equivalence on Quantum Cryptographic Protocols
Title:Automated Verification of Equivalence on Quantum Cryptographic Protocols
Authors:Takahiro Kubota, Yoshihiko Kakutani, Go Kato, Yasuhito Kawano and Hideki Sakurada
Keyphrases:automated verification, bb84, quantum cryptography, process calculi, formal methods
Paper:
Abstract:t is recognized that security verification of cryptographic protocols tends to be difficult and in fact, some flaws on protocol designs or security proofs were found after they had been presented. The use of formal methods is a way to deal with such complexity. Especially, process calculi are suitable to describe parallel systems. Bisimilarity, which denotes that two processes behave indistinguishably from the outside, is a key notion in process calculi. However, by-hand verification of bisimilarity is often tedious when the processes have many long branches in their transitions. We developed a software tool to automatically verify bisimulation relation in a quantum process calculus qCCS and applied it to Shor and Preskill's security proof of BB84. The tool succeeds to verify the equivalence of BB84 and an EDP-based protocol, which are discussed in their proof.
Volume:Laura Kovacs and Temur Kutsia (editors). SCSS 2013. 5th International Symposium on Symbolic Computation in Software Science
Series:EPiC Series in Computing
Volume number:15
Pages:64-69
Editors:Laura Kovacs and Temur Kutsia
Page views:2
Downloads:16
BibTeX entry:
@inproceedings{SCSS2013:Automated_Verification_of_Equivalence_on_Quantum_Cryptographic_Protocols,
  author    = {Takahiro Kubota and Yoshihiko Kakutani and Go Kato and Yasuhito Kawano and Hideki Sakurada},
  title     = {Automated Verification of Equivalence on Quantum Cryptographic Protocols},
  booktitle = {SCSS 2013. 5th International Symposium on Symbolic Computation in Software Science},
  editor    = {Laura Kovacs and Temur Kutsia},
  series    = {EPiC Series in Computing},
  volume    = {15},
  pages     = {64-69},
  year      = {2013},
  publisher = {EasyChair},
  bibsource = {EasyChair, http://www.easychair.org},
  issn      = {2398-7340}}