A declarative model for reasoning about form security

Hunter, Aaron (author)
(editor)
(translator)

Copyright © 2015 SciTePress (Science and Technology Publications, Lda.)

Proceedings of the International Conference on Agents and Artificial Intelligence in Lisbon, Portugal 2015. We introduce a formal methodology for analysing the security of digital forms, by representing form signing procedures in a declarative action formalism. In practice, digital forms are represented as XML documents and the security of information is guaranteed through the use of digital signatures. However, the security of a form can be compromised in many different ways. For example, an honest agent might be convinced to make a commitment that they do not wish to make or they may be fooled into believing that another agent has committed to something when they have not. In many cases, these attacks do not require an intruder to break any form of encryption or digital signature; instead, the intruder simply needs to manipulate the way signatures are applied and forms are passed between agents. In this paper, we demonstrate that form signing procedures can actually be seen as a variation of the message passing systems used in connection with cryptographic protocols. We start with an exis ting declarative model for reasoning about cryptographic protocols in the Situation Calculus, and we show how it can be extended to identify security issues related to digital signatures, and form signing procedures. We suggest that our results could be used to help users create secure digital forms, using tools such as IBM’s Lotus Forms software.

http://www.scitepress.org/DigitalLibrary/Link.aspx?doi=10.5220%2f0005213...