Formalising human recognition: A fundamental building block for security proofs

Relationship between human perceptible authenticator acceptance and recognition spaces.


A fundamental part of many authentication protocols which authenticate a party to a human involves the human recognizing or otherwise processing a message received from the party. Examples include typical implementations of Verified by Visa in which a message, previously stored by the human at a bank, is sent by the bank to the human to authenticate the bank to the human; or the expectation that humans will recognize or verify an extended validation certificate in a HTTPS context. This paper presents general definitions and building blocks for the modelling and analysis of human recognition in authentication protocols, allowing the creation of proofs for protocols which include humans. We cover both generalized trawling and human-specific targeted attacks. As examples of the range of uses of our construction, we use the model presented in this paper to prove the security of a mutual authentication login protocol and a human-assisted device pairing protocol.

Keywords: ceremony, human, HTTPS, Transport Layer Security (TLS), provable security, authentication, human perceptible authenticator (HPA)


Kenneth Radke, Colin Boyd, Juan González Nieto, Mark Manulis, Douglas Stebila. Formalising human recognition: A fundamental building block for security proofs. In Udaya Parampalli, Ian Welch, editors, Proc. 12th Australasian Information Security Conference (AISC) 2014, Conferences in Research and Practice in Information Technology, vol. 149, pp. 37-45. Australian Computer Society, January 2014. © Australian Computer Society.




This research was supported by:
  • the Australian Technology Network–German Academic Exchange Service (ATN-DAAD) Joint Research Co-operation Scheme
  • Australian Research Council (ARC) Linkage Project grant LP120200246