Formalizing and Analyzing Security Ceremonies with Heterogeneous Devices in ANP and PDL

  • Antonio González-BurgueñoEmail author
  • Peter Csaba Ölveczky
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11761)


Security ceremonies extend cryptographic protocols with models of human users to allow us to take human behaviors into account when reasoning about security. Actor-network procedures (ANPs) are a well-known formal model of security ceremonies, and procedure derivation logic (PDL) allows us to reason logically about ANPs. In a security ceremony, different nodes may have different capabilities: computers can encrypt and decrypt messages, whereas humans cannot; a biometric device can capture biometric information, whereas a random number generator used in e-banking cannot; and so on. Furthermore, even if a node has the decryption capability, it must also know the encryption key to decrypt a message. ANPs do not support explicitly specifying node capabilities. In this paper, we extend ANPs to deal with heterogeneous devices by explicitly specifying the nodes’ capabilities. We also modify PDL to take into account the knowledge of participants at different points in time. All this allows us to reason about secrecy and authentication in ceremonies with different kinds of devices and human users.


  1. 1.
    Anlauff, M., Pavlovic, D., Waldinger, R., Westfold, S.: Proving authentication properties in the Protocol Derivation Assistant. In: FCS-ARSPA 2006. ACM (2006)Google Scholar
  2. 2.
    Balfanz, D., Smetters, D.K., Stewart, P., Wong, H.C.: Talking to strangers: authentication in ad-hoc wireless networks. In: NDSS 2002. The Internet Society (2002)Google Scholar
  3. 3.
    Basin, D.A., Radomirovic, S., Schläpfer, M.: A complete characterization of secure human-server communication. In: CSF 2015. IEEE Computer Society (2015)Google Scholar
  4. 4.
    Bella, G., Coles-Kemp, L.: Layered analysis of security ceremonies. In: Gritzalis, D., Furnell, S., Theoharidou, M. (eds.) SEC 2012. IAICT, vol. 376, pp. 273–286. Springer, Heidelberg (2012). Scholar
  5. 5.
    Cervesato, I., Meadows, C.A., Pavlovic, D.: An encapsulated authentication logic for reasoning about key distribution protocols. In: CSFW 2005, vol. 1. IEEE (2005)Google Scholar
  6. 6.
    Chen, S., Sasse, R., Meseguer, J., Wang, H., Wang, Y.M.: A systematic approach to uncover security flaws in GUI logic. In: IEEE SSP 2007. IEEE (2007)Google Scholar
  7. 7.
    Clavel, M., et al.: All About Maude - A High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic. LNCS, vol. 4350. Springer, Heidelberg (2007). Scholar
  8. 8.
    Ellison, C.: Ceremony design and analysis. IACR Cryptology ePrint Archive (2007)Google Scholar
  9. 9.
    Fiadeiro, J., Ţuţu, I., Lopes, A., Pavlovic, D.: Logics for actor networks: a case study in constrained hybridization. In: Madeira, A., Benevides, M. (eds.) DALI 2017. LNCS, vol. 10669, pp. 98–114. Springer, Cham (2018). Scholar
  10. 10.
    Gonzalez-Burgueño, A., Ölveczky, P.C.: Formalizing and analyzing security ceremonies with heterogeneous devices in ANP and PDL (2018).
  11. 11.
    Meadows, C., Pavlovic, D.: Deriving, attacking and defending the GDOI protocol. In: Samarati, P., Ryan, P., Gollmann, D., Molva, R. (eds.) ESORICS 2004. LNCS, vol. 3193, pp. 53–72. Springer, Heidelberg (2004). Scholar
  12. 12.
    Meadows, C., Pavlovic, D.: Formalizing physical security procedures. In: Jøsang, A., Samarati, P., Petrocchi, M. (eds.) STM 2012. LNCS, vol. 7783, pp. 193–208. Springer, Heidelberg (2013). Scholar
  13. 13.
    Pavlovic, D., Meadows, C.: Actor-network procedures. In: Ramanujam, R., Ramaswamy, S. (eds.) ICDCIT 2012. LNCS, vol. 7154, pp. 7–26. Springer, Heidelberg (2012). Scholar
  14. 14.
    Pavlovic, D., Meadows, C.: Deriving secrecy in key establishment protocols. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol. 4189, pp. 384–403. Springer, Heidelberg (2006). CrossRefGoogle Scholar
  15. 15.
    Pavlovic, D., Meadows, C.: Actor-network procedures: modeling multi-factor authentication, device pairing, social interactions. CoRR abs/1106.0706 (2011)Google Scholar
  16. 16.
    Pavlovic, D., Meadows, C.: Deriving ephemeral authentication using channel axioms. In: Christianson, B., Malcolm, J.A., Matyáš, V., Roe, M. (eds.) Security Protocols 2009. LNCS, vol. 7028, pp. 240–261. Springer, Heidelberg (2013). Scholar
  17. 17.
    Radke, K., Boyd, C., Nieto, J.G., Manulis, M., Stebila, D.: Formalising human recognition: a fundamental building block for security proofs. In: AISC 2014. CRPIT, vol. 149. Australian Computer Society (2014)Google Scholar
  18. 18.
    Roscoe, A.W., Goldsmith, M., Creese, S.J., Zakiuddin, I.: The attacker in ubiquitous computing environments: formalising the threat model. In: FAST 2003 (2003)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2019

Authors and Affiliations

  • Antonio González-Burgueño
    • 1
    Email author
  • Peter Csaba Ölveczky
    • 1
  1. 1.University of OsloOsloNorway

Personalised recommendations