Security and Privacy in Communication Networks. 6th Iternational ICST Conference, SecureComm 2010, Singapore, September 7-9, 2010. Proceedings

Research Article

Epistemic Model Checking for Knowledge-Based Program Implementation: An Application to Anonymous Broadcast

Download194 downloads
  • @INPROCEEDINGS{10.1007/978-3-642-16161-2_25,
        author={Omar Al-Bataineh and Ron Meyden},
        title={Epistemic Model Checking for Knowledge-Based Program Implementation: An Application to Anonymous Broadcast},
        proceedings={Security and Privacy in Communication Networks. 6th Iternational ICST Conference, SecureComm 2010, Singapore, September 7-9, 2010. Proceedings},
        proceedings_a={SECURECOMM},
        year={2012},
        month={5},
        keywords={Formal methods anonymity model checking},
        doi={10.1007/978-3-642-16161-2_25}
    }
    
  • Omar Al-Bataineh
    Ron Meyden
    Year: 2012
    Epistemic Model Checking for Knowledge-Based Program Implementation: An Application to Anonymous Broadcast
    SECURECOMM
    Springer
    DOI: 10.1007/978-3-642-16161-2_25
Omar Al-Bataineh1, Ron Meyden1
  • 1: University of New South Wales

Abstract

Knowledge-based programs provide an abstract level of description of protocols in which agent actions are related to their states of knowledge. The paper describes how epistemic model checking technology may be applied to discover and verify concrete implementations based on this abstract level of description. The details of the implementations depend on the specific context of use of the protocol. The knowledge-based approach enables the implementations to be optimized relative to these conditions of use. The approach is illustrated using extensions of the Dining Cryptographers protocol, a security protocol for anonymous broadcast.