• DocumentCode
    1844875
  • Title

    Computational Semantics of a Verification Logic of Local Sessions

  • Author

    Yinyin Xiao

  • Author_Institution
    Dept. of Comput. Sci., Guangdong Polytech. Normal Univ., Guangzhou, China
  • fYear
    2013
  • fDate
    21-23 June 2013
  • Firstpage
    835
  • Lastpage
    838
  • Abstract
    We propose a computational semantics for a previously developed protocol security logic, Logic of Local Sessions (LLS), replacing its earlier symbolic semantics based on the Dolev-Yao model. With the new semantics, the protocol verification of LLS is more close to the real execution, while the proofs can still be carried out at a symbolic level using the original proof system and the automatic verification tool. Our results hold under standard cryptographic assumptions.
  • Keywords
    cryptographic protocols; formal verification; theorem proving; Dolev-Yao model; LLS; automatic verification tool; computational semantics; cryptographic assumptions; proof system; protocol security logic; protocol verification; symbolic semantics; verification logic of local sessions; Computational model; Computational semantics; Indistinguishability; Logic of Local Sessions;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Computational and Information Sciences (ICCIS), 2013 Fifth International Conference on
  • Conference_Location
    Shiyang
  • Type

    conf

  • DOI
    10.1109/ICCIS.2013.224
  • Filename
    6643140
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=1844875