• DocumentCode
    3332543
  • Title

    Towards Model-Checking Quantum Security Protocols

  • Author

    Baltazar, P. ; Chadha, R. ; Mateus, P. ; Sernadas, A.

  • Author_Institution
    SQIG-IT, Lisbon
  • fYear
    2007
  • fDate
    2-6 Jan. 2007
  • Firstpage
    14
  • Lastpage
    14
  • Abstract
    Logics for reasoning about quantum states have been given in the literature. In this paper, we extend one such logic with temporal constructs mimicking the standard computational tree logic used to reason about classical transition systems. We investigate the model-checking problem for this temporal quantum logic and illustrate its use by reasoning about the BB84 key distribution protocol.
  • Keywords
    cryptographic protocols; quantum cryptography; BB84 key distribution protocol; classical transition systems; computational tree logics; model-checking quantum security protocols; quantum logics; Cost accounting; Hilbert space; Information processing; Information security; Logic design; Measurement standards; Protocols; Quantum computing; Quantum mechanics; Tensile stress;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Quantum, Nano, and Micro Technologies, 2007. ICQNM '07. First International Conference on
  • Conference_Location
    Guadeloupe City
  • Electronic_ISBN
    0-7695-2759-0
  • Type

    conf

  • DOI
    10.1109/ICQNM.2007.21
  • Filename
    4077007