Analysis of LYSA-calculus with explicit confidentiality annotations

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    176 Downloads (Pure)

    Abstract

    Recently there has been an increased research interest in applying process calculi in the verification of cryptographic protocols due to their ability to formally model protocols. This work presents LYSA with explicit confidentiality annotations for indicating the expected behavior of target protocols. A static analysis approach is developed for analyzing protocols specified in the extended LYSA. The proposed approach will over-approximate the possible executions of protocols while keeping track of all messages communicated over the network, and furthermore it will capture the potential malicious activities performed by attackers as specified by the confidentiality annotations. The proposed analysis approach is fully automatic without the need of human intervention and has been applied successfully to a number of protocols.
    Original languageEnglish
    Title of host publicationProceeding of 20th International Conference on Advanced Information Networking and Applications
    Volume2
    PublisherIEEE
    Publication date2006
    Pages39-43
    ISBN (Print)0-7695-2466-4
    DOIs
    Publication statusPublished - 2006
    Event20th International Conference on Advanced Information Networking and Applications -
    Duration: 1 Jan 2006 → …

    Conference

    Conference20th International Conference on Advanced Information Networking and Applications
    Period01/01/2006 → …

    Bibliographical note

    Copyright: 2006 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE

    Cite this

    Gao, H., & Nielson, H. R. (2006). Analysis of LYSA-calculus with explicit confidentiality annotations. In Proceeding of 20th International Conference on Advanced Information Networking and Applications (Vol. 2, pp. 39-43). IEEE. https://doi.org/10.1109/AINA.2006.100