Formal Analysis of Security in Interactive Systems

Formal Analysis of Security in Interactive Systems

Antonio Cerone (United Nations University, China)
DOI: 10.4018/978-1-60566-132-2.ch025
OnDemand PDF Download:


Reducing the likelihood of human error in the use of interactive systems is increasingly important. Human errors could not only hinder the correct use and operation, they can also compromise the safety and security of such systems. Hence the need for formal methods to analyze and verify the correctness of interactive systems, particularly with regards to human interaction. This chapter examines the use of formal modeling and analysis of security properties of interactive systems. The reader is introduced to some basic concepts in security and human-computer interaction, followed by formal modeling of human cognitive behavior and analysis of such systems. Authors highlight the use of model-checking to drive the system development to design secure user actions and sequences of actions. Authors also analyze the patterns of user behavior that may lead to security violation. Finally, particular areas of security protocol design where human interaction plays a key role are discussed.
Chapter Preview


Reducing the likelihood of human error in the use of interactive systems is increasingly important: the use of such systems is becoming widespread in applications that demand high reliability due to safety, security, financial or similar considerations. Consequently, the use of formal methods in verifying the correctness of interactive systems should also include analysis of human behaviour in interacting with the interface.

The study of human behaviour in operating machines has emerged in the 1980’s, when Human Reliability Assessment (HRA) techniques have been used in the analysis of safety-critical systems (Kirwan, 1990). These techniques appeared soon to lack objectivity (Svenson, 1989) and failed to cope with the complex behaviours emerging in the human-machine interaction (Kirwan, 1992).

In the 1990s formal methods have started to be introduced aiming at a more objective analysis (Dix, 1991). However, the gain in objectivity was offset by an oversimplified model of the human behaviour, which was actually often modelled as defined by the interface requirements. In reality, the user interacting with the system does not necessarily behave as it was expected while designing the interface, and errors are actually the very result of an unexpected user behaviour that emerges through the interaction.

To best capture such an emergent behaviour, a model of the user must specify the cognitively plausible behaviour, which is all the possible behaviours that can occur, and that involve different cognitive processes (Butterworth et al, 2000). The model must take into account all relationship between user’s actions, user’s goals and the environment. Following this approach, a number of researchers have explored the use of formal models to understand how cognitive errors can affect user performance. Mode confusion is often blamed for human errors in interactive systems, whereby the user’s mental model of how the system works gets out of step with how the system is actually working. This phenomenon has been analysed by developing a plausible (but simplified) mental model such as might represent the user’s understanding of the system and comparing it with a user interface model, to look for sources of cognitive dissonance (Butler et al, 1998; Rushby, 2002). Rushby (2002) models the behaviour of a forgetful user who follows a warning display light or a non-forgetful user without warning lights and checks for emergent mode confusion. Curzon and Blandford (2004) focus on goal-based interactions and model the behaviour of a user who assumes all tasks completed when the goal is achieved, but forgets to complete some important subsidiary tasks (post-completion error). Cerone et al (2005) investigate the application of formal methods to the classification and analysis of task failure caused by systematic recurrence of human errors. This recurrence produces complex patterns of human behaviours, which are the result of bad habits, poor training, deficient mental models, or are associated with cognitive processes such as habituation. The error is modeled by the behavioural pattern itself, rather than by specific error states as for mode confusion and post-completion error. In particular, different categories of behavioural patterns are formally verified to be a sound and complete decomposition of an air traffic control task failure.

These formal approaches all address safety-critical aspects of interactive systems and cognitive behaviour. Only at the beginning of the new millenium, security aspects of interactive systems have been started to be systematically analysed (Cerone and Curzon, 2007; Yee, 2002; Zurko, 2005). In fact, security violations in human-computer interaction may be due to systematic causes such as cognitive overload, lack of security knowledge, and mismatches between the behaviour of the computer system and the user’s mental model (Yee, 2002). The user who causes the violation may or may not be the attacker: the user may either become aware of the violation and exploit it or unwillingly allow a malicious user to exploit it. The latter situation is more complex due to two reasons. First, the violation often emerges as a consequence of a complex behavioral pattern (Cerone et al, 2005). Secondly, the security properties need to capture the conditions which enable a malicious user to exploit the violation (Cerone and Elbegbayan, 2007).

Key Terms in this Chapter

Human Error: A class of errors that (in the context of interactive systems) refer to any undesired user action or user-system interaction that leads to the violation of a system goal. Such an interaction may also violate some security goal of the system, that is leakage of confidential information or facilitate unauthorised access to the system.

Model-Checking: An approach to verifying whether a model (of a software or hardware system) satisfies a set of formal assertions and constraints. This usually involves the use of a tool, which allows a model to be specified using a particular formal language (such as CSP), along with the property that it needs to be checked against, and then check whether the model would always satisfy the property for all its executions. The check involves the use of a state exploration technique to ensure that all possible states of the system are explored as desired. In case if the model fails to satisfy the stated property, the tool returns an execution path demonstrating the failure.

Empirical Channel: A formalisation of a medium of communication which results from human-to-human or human-to-device interaction. Some information communicated verbally from one person to another, read from a device display panel or input into a keyboard of a computer are all examples of communication over empirical channels. They are considered low bandwidth and reliable.

CSP: Communicating Sequential Processes, or CSP, is a formal language for describing patterns of interaction for concurrent systems (in computer science). First described by Sir Professor Tony Hoare at Oxford in 1978, it is a member of the family of mathematical theories of concurrency known as process algebras. It is traditionally written in a fairly mathematical notation, with special symbols representing its operators, and is typeset more like mathematics than a typical programming language.

Electronic-Voting: A voting infrastructure that uses electronic means to support and provide the casting and counting of votes. This usually involves an underlying computer system which allows the voters to cast their vote and output the result of the election.

Coercion-Resistance: A property of electronic voting systems where a voter is not able to prove to a coercer what way he/she voted. This is an important property as it prevents voters being bought or blackmailed by those who intend to unlawfully influence the results of the election.

Security Protocol: A security protocol is essentially a communication protocol – an agreed sequence of actions performed by two or more communicating entities in order to accomplish some mutually desirable goal – that makes use of cryptographic techniques, allowing the communicating entities to achieve a security goal. A particular protocol, however, may enable the communicating parties to establish one or more such goals. Some common security goals include (data and entity) authentication, confidentiality and integrity.

Complete Chapter List

Search this Book:
Editorial Advisory Board
Table of Contents
John Walp
Manish Gupta, Raj Sharman
Chapter 1
C. Warren Axelrod
This chapter examines the impact of catastrophes on information security and suggests who might have responsibility for maintaining an appropriate... Sample PDF
Responsibilities and Liabilities with Respect to Catastrophes
Chapter 2
David Porter
This chapter discusses the latest developments in the shifting threat landscape and their impact on the world of information security. It describes... Sample PDF
The Complex New World of Information Security
Chapter 3
Ahmed Awad E. Ahmed
In recent years, many studies have highlighted the unprecedented growth in security threats from multiple and varied sources faced by corporate, as... Sample PDF
Employee Surveillance Based on Free Text Detection of Keystroke Dynamics
Chapter 4
Arunabha Mukhopadhyay, Samir Chatterjee, Debashis Saha, Ambuj Mahanti, Samir K. Sadhukhan
An online business organization spends millions of dollars on firewalls, anti-virus, intrusion detection systems, digital signature, and encryption... Sample PDF
E-Risk Insurance Product Design: A Copula Based Bayesian Belief Network Model
Chapter 5
Guoling Lao
E-commerce mode aggravates information asymmetry so that honesty-credit problems become more serious. This chapter discusses the honesty-credit... Sample PDF
E-Commerce Security and Honesty-Credit
Chapter 6
Zhixiong Zhang, Xinwen Zhang, Ravi Sandhu
This chapter addresses the problem that traditional role-base access control (RBAC) models do not scale up well for modeling security policies... Sample PDF
Towards a Scalable Role and Organization Based Access Control Model with Decentralized Security Administration
Chapter 7
Chandan Mazumdar
There has been an unprecedented thrust in employing Computers and Communication technologies in all walks of life. The systems enabled by... Sample PDF
Enterprise Information System Security: A Life-Cycle Approach
Chapter 8
Peter O. Orondo
Most companies would agree that securing their information assets is worth some investment. It is thus plausible to assume that low levels of IT... Sample PDF
An Alternative Model of Information Security Investment
Chapter 9
George O.M. Yee
The growth of the Internet is increasing the deployment of e-services in such areas as e-commerce, e-learning, and e-health. In parallel, the... Sample PDF
Avoiding Pitfalls in Policy-Based Privacy Management
Chapter 10
Supriya Singh
Enabling customers to influence the way they are represented in the bank’s databases, is one of the major personalization, responsiveness, and... Sample PDF
Privacy and Banking in Australia
Chapter 11
Madhusudhanan Chandrasekaran, Shambhu Upadhyaya
Phishing scams pose a serious threat to end-users and commercial institutions alike. E-mail continues to be the favorite vehicle to perpetrate such... Sample PDF
A Multistage Framework to Defend Against Phishing Attacks
Chapter 12
Ghita Kouadri Mostefaoui, Patrick Brézillon
In recent years, the security research community has been very active in proposing different techniques and algorithms to face the proliferating... Sample PDF
A New Approach to Reducing Social Engineering Impact
Chapter 13
Yang Wang
Privacy-enhancing technologies (PETs), which constitute a wide array of technical means for protecting users’ privacy, have gained considerable... Sample PDF
Privacy-Enhancing Technologies
Chapter 14
Douglas P. Twitchell
This chapter introduces and defines social engineering, a recognized threat to the security of information systems. It also introduces a taxonomy... Sample PDF
Social Engineering and its Countermeasures
Chapter 15
Tom S. Chan
Social networking has become one of the most popular applications on the Internet since the burst of the dot-com bubble. Apart from being a haven... Sample PDF
Social Networking Site: Opportunities and Security Challenges
Chapter 16
James W. Ragucci, Stefan A. Robila
Fraudulent e-mails, known as phishing attacks, have brought chaos across the digital world causing billions of dollars of damage. These attacks are... Sample PDF
Designing Antiphishing Education
Chapter 17
Serkan Ada
This chapter discusses the recent theories used in information security research studies. The chapter initially introduces the importance of the... Sample PDF
Theories Used in Information Security Research: Survey and Agenda
Chapter 18
Samuel Liles
Information assurance education is an interdisciplinary endeavor that only when taken as a holistic and inclusive educational activity can be... Sample PDF
Information Assurance and Security Curriculum Meeting the SIGITE Guidelines
Chapter 19
Gary Hinson
This chapter highlights the broad range of factors that are relevant to the design of information security awareness programs, primarily by... Sample PDF
Information Security Awareness
Chapter 20
Nick Pullman, Kevin Streff
Security training and awareness is often overlooked or not given sufficient focus in many organizations despite being a critical component of a... Sample PDF
Creating a Security Education, Training, and Awareness Program
Chapter 21
E. Kritzinger, S.H von Solms
This chapter introduces information security within the educational environments that utilize electronic resources. The education environment... Sample PDF
Information Security Within an E-Learning Environment
Chapter 22
Donald Murphy, Manish Gupta, H.R. Rao
We present five emerging areas in information security that are poised to bring the radical benefits to the information security practice and... Sample PDF
Research Notes on Emerging Areas of Conflict in Security
Chapter 23
C. Orhan Orgun
This chapter develops a linguistically robust encryption system, LunabeL, which converts a message into syntactically and semantically innocuous... Sample PDF
The Human Attack in Linguistic Steganography
Chapter 24
Sérgio Tenreiro de Magalhães, Kenneth Revett, Henrique M.D. Santos, Leonel Duarte dos Santos, André Oliveira, César Ariza
The traditional approach to security has been the use of passwords. They provide the system with a barrier to access what was quite safe in the... Sample PDF
Using Technology to Overcome the Password's Contradiction
Chapter 25
Antonio Cerone
Reducing the likelihood of human error in the use of interactive systems is increasingly important. Human errors could not only hinder the correct... Sample PDF
Formal Analysis of Security in Interactive Systems
Chapter 26
Tejaswini Herath
It is estimated that over 1 billion people now have access to the Internet. This unprecedented access and use of Internet by individuals around the... Sample PDF
Internet Crime: How Vulnerable Are You? Do Gender, Social Influence and Education play a Role in Vulnerability?
Chapter 27
Jarrod Trevathan
Shill bidding is where spurious bids are introduced into an auction to drive up the final price for the seller, thereby defrauding legitimate... Sample PDF
Detecting Shill Bidding in Online English Auctions
Chapter 28
Carsten Röcker, Carsten Magerkurth, Steve Hinske
In this chapter we present a novel concept for personalized privacy support on large public displays. In the first step, two formative evaluations... Sample PDF
Information Security at Large Public Displays
Chapter 29
Yuko Murayama, Carl Hauser, Natsuko Hikage, Basabi Chakraborty
The sense of security, identified with the Japanese term, Anshin, is identified as an important contributor to emotional trust. This viewpoint... Sample PDF
The Sense of Security and Trust
About the Contributors