# Convectively-coupled High-frequency Atmospheric waves triggered Kerala
floods in 2018 and 2019

Kiran S. R  Department of Civil Engineering
Central Polytechnic College
Thiruvananthapuram, Kerala
Email<EMAIL_ADDRESS>
ORCID Id: 0000-0003-3200-8624

###### Abstract

Floods have repeatedly battered the South Indian state, Kerala, as a result of
the unprecedented heavy rainfall during Boreal Summers, in recent years. The
state witnessed large departures from normal rainfall in 2018 and 2019.
Previous studies have seldom adopted a systematic approach to understand the
phenomenon responsible for the recurrent extreme events. Hence, this study,
based on spectral methods, identifies a characteristic propagation of high-
frequency equatorial waves in the atmosphere, which travelled from near
tropical west Pacific to the east coast of Africa. These waves stimulated
intense convection and ensured sufficient availability of moisture over the
state, and are hence responsible for Kerala Floods.

###### Index Terms:

Kerala Floods, Indian Monsoon, Mid-tropospheric convection, Moisture
convergence, High-frequency Equatorial waves

##  I Introduction

Kerala, the south-west coastal state of India, experienced heavy rainfall and
consequent floods in 2018 and 2019 during Summer. The state received extremely
heavy rainfall during the South-West Monsoon in the two years – from $8^{th}$
to $17^{th}$ August 2018 and from $3^{rd}$ to $10^{th}$ August 2019, which
caused unprecedented floods resulting in massive loss of life and property.
These recurrent extreme events in the state have raised questions of changing
climate in the southern part of Peninsular India. Hence, there arose a
necessity to identify the physical phenomenon which derailed the hydrology of
the State in recent years.

Vimal and Harsh (2019) observed no increase in mean and extreme precipitation
in Kerala over the past six decades and identified that the extreme rainfall
event in August 2018 was driven by anomalous atmospheric conditions due to
climate variability rather than anthropogenic factors [1]. Hunt and Menon
(2020) concluded that the precipitation in Kerala may be 18% heavier for the
pre-industrial period and 36% heavier for a prospective climate in 2100 [2].
According to Ref. [3], the presence of a strong westerly jet along with the
formation of the offshore vortex trough and the transport of mid-tropospheric
moisture from various sources under the presence of conducive vertical shear
of horizontal wind may have contributed to the extreme rainfall over Kerala in
2018. Further, there are theories that the strong westerly flow, which is a
part of the cross equatorial Monsoon flow, was constantly propelled by a
couple of cyclonic systems over Bay of Bengal, South China Sea and West
Pacific [4]. Similarly, Ref.[5] deduced that the Kerala floods of 2018 was
triggered by the formation of an intense and long-duration atmospheric river
with more than 60% of moisture supply from the Central-Eastern Indian Ocean.

Although, the above studies attempted to investigate the extreme precipitation
in 2018 from the general wind field conditions existed then, no conclusive
evidences to support their theories exist hitherto, even after the extreme
events repeated in 2019 and 2020 during the same season. This incited the
necessity to investigate the climate dynamics responsible for the recurrent
disaster.

##  II Data & Methodology

Tropical Rainfall Measuring Mission (TRMM) gives daily rainfall data at a
spatial resolution of $0.25^{o}$ $\times$ $0.25^{o}$ over the Indian Ocean
region. In addition, the daily gridded rainfall data from raingauge
observations over Kerala is obtained from Indian Meteorological Department
(IMD) from 2011 to 2019. Further, the ERA5 Reanalysis of the European Centre
for Medium-Range Weather Forecasts (ECMWF) gives the specific humidity (kg/kg)
and winds (zonal & meridional winds in m/s and vertical velocity (or omega) in
Pa/s) for different vertical pressure levels from 1000 to 100hPa.

Figure 1: (first & third figure) TRMM rainfall on the days of peak rainfall in
2018 and 2019 respectively. (second & fourth figure) Corresponding values of
ERA5 Vertical velocity at 600hPa and 350hPa respectively. Figure 2: IMD daily
rainfall anomalies (in millimetres) of 2018 over North, Central and South
Kerala, measured with respect to the 7 year mean precipitation. Figure 3: IMD
daily rainfall anomalies (in millimetres) of 2019 over North, Central and
South Kerala, measured with respect to 7 year mean precipitation.

In this study, the daily departures from the mean of atmospheric variables
during 2018 and 2019 by deducting the average of daily data of the atmospheric
variables from 2011 to 2017 from the daily data for the years 2018 and 2019
separately. Since, the two-day maximum precipitation of 2018 was abnormally
high (220mm) and surpassed even the $95^{th}$ percentile of 70 years (150mm),
a 7-year mean would suffice to capture the anomaly [1]. Hovmöller diagrams,
which depict the temporal variation of atmospheric variables along
zonal/meridional direction, are used to identify the propagation of waves and
its characteristics. Fast Fourier Transform (FFT) is performed on time series
of atmospheric variables or its anomalies for the ease of representation in
frequency domain. The dominant harmonics, thus identified, are filtered out
using Band-Pass Filters (BPF) for further analysis.

##  III Results & Discussions

###  III-A Rainfall over Kerala in 2018 $\&$ 2019

Kerala experienced anomalous rainfall events in 2018 and 2019, with peak daily
precipitation on $15^{th}$ August and $8^{th}$ August respectively [3, 6].
Figure 1 (first & third figure) shows the spatial distribution of TRMM
rainfall over Peninsular India on these days. One observes heavy precipitation
confined only to the windward side of Western Ghats, especially its southern
region. Any propensities of localized convection over the state may be
determined from ERA5 omega distribution. At a geographical location in Kerala
($76.5^{o}$E, $10^{o}$N), unusually high negative values of omega (rising air)
were observed at 600hPa in 2018 and at 350hPa in 2019 (Fig. 1 (second & fourth
figure), and are hence juxtaposed with rainfall for comparison. It is
interesting to conclude very high spatial correlation of precipitation with
mid-tropospheric convection in 2018 and with upper-tropospheric convection in
2019, on the days of extreme events.

Figure 4: Amplitude spectrum of IMD rainfall anomalies of 2018 averaged over
the state of Kerala, in comparison to that of the 7 year mean precipitation.
Figure 5: Amplitude spectrum of IMD rainfall anomalies of 2019 averaged over
the state of Kerala, in comparison to that of the 7 year mean precipitation.

From IMD gridded rainfall point data, precipitation anomalies were determined
for the North, Central and South Kerala, for the years 2018 and 2019 (Fig. 2
and Fig. 3). In 2018, Kerala witnessed two distinct extreme events – on
$8^{th}$ August (over 50mm) and on $15^{th}$ August (over 150mm). Similarly,
two extreme events were observed in 2019 too – on $8^{th}$ August (over 150mm)
and on $15^{th}$ August (over 50mm).

Figure 6: 5-8days, 12-20days and 20-60days bandpass-filtered IMD rainfall
anomalies of 2018 averaged over the state of Kerala. Figure 7: 5-8days,
12-20days and 20-60days bandpass-filtered IMD rainfall anomalies of 2019
averaged over the state of Kerala.

###  III-B Dominant modes of variability

Identification of the constituent harmonics, which contributed to the
precipitation anomalies of 2018 and 2019, shall expose the real phenomenon
responsible for the extreme event. Hence, Fast Fourier Transforms (FFT) of the
spatially-averaged rainfall anomalies were performed for both the years, and
the resultant amplitude spectrum are shown in Fig. 4 and Fig. 5. The spectrum
corresponding to the 7 year mean daily rainfall is superimposed for
comparison. In 2018 and 2019, the rainfall spectra are dominated by
frequencies in the bands of period 5-8 days, 12-20 days and 20-60 days. The
semi-annual variability (180 days), a characteristic response of the
equatorial Indian Ocean region during Spring and Fall [7], can be neglected
for this study.

Figure 8: 5-8days, 12-20days and 20-60days bandpass-filtered ERA5 Meridional
velocities of 2018 averaged over the state of Kerala with altitude. Figure 9:
5-8days, 12-20days and 20-60days bandpass-filtered ERA5 Meridional velocities
of 2019 averaged over the state of Kerala with altitude. Figure 10: (first
$\&$ second figure) 5-8 days bandpass-filtered ERA5 Meridional velocities of
August 2018 meridionally averaged over the state of Kerala at pressure levels
200hPa and 700hPa respectively. (third figure) 12-20 days bandpass-filtered
Meridional velocities at 200hPa in 2018. (fourth figure) 20-60 days bandpass-
filtered Meridional velocities at 200hPa in 2018.

For further analysis, the time series of precipitation anomalies for the
concerned years were filtered separately for the bands 5-8 days, 12-20 days
and 20-60 days. Fig. 6 shows the bandpass-filtered rainfall anomalies for the
year 2018. The 5-8 days high frequency mode made an exceptional contribution
to the extreme event in August, compared to the other two modes. The high
frequency mode rightly captured the two prominent peaks in rainfall departures
during the month. In 2019, the extreme precipitation which peaked on $8^{th}$
August was the unambiguous consequence of superposition of all the three modes
in-phase (Fig. 7). Yet, the 5-8 days periodicity leads to capture the second
extreme event of the year. Hence, it is important to investigate the
phenomenon which is responsible for these dominant modes of variability,
especially the high frequency mode, which has assumed great significance to
the extreme rainfall events of 2018 and 2019.

Figure 11: (first figure) 5-8 days bandpass-filtered ERA5 Meridional
velocities of August 2019 averaged meridionally over the state of Kerala at
200hPa pressure level. (second figure) 12-20 days bandpass-filtered Meridional
velocities at 200hPa in 2019. (third figure) 20-60 days bandpass-filtered
Meridional velocities at 200hPa in 2019. Figure 12: 5-8days bandpass-filtered
Specific humidity vertically integrated from surface (1000 hPa) to 600 hPa
overlaid with 5-8days bandpass-filtered ERA5 winds at 700 hPa from $14^{th}$
to $17^{th}$ August 2018.

ERA5 Reanalysis meridional winds over the state of Kerala, for different
pressure levels in 2018 and 2019, are bandpass-filtered for the dominant modes
of variabilty (Fig. 8 and Fig. 9). In 2018, the 5-8 days mode is associated
with the intensification of meridional winds at mid-troposphere (800hPa -
500hPa). Similar anomalous wind patterns are seldom observed for the other
modes at mid-troposphere; although these had modulated the upper troposphere,
but not exclusive to period of extreme rainfall. Hence, the role of the high
frequency mode in causing the Kerala floods of 2018 stands substantiated, as
it conforms to the anomalous precipitation and convection observed in Fig. 1.

On the other hand, during the extreme event in August 2019, a stark
variability in meridional winds at upper atmosphere (400hPa - 200hPa) is
observed for the 5-8 days periodicity (Fig. 9). Other modes possessed
relatively lower magnitudes at any levels during this period, although all the
three modes contributed comparably to the precipitation anomalies as per Fig.
7. But, these modes can be observed to constitute the zonal winds over Kerala
(Figure not shown), which are long deemed classical Intra-seasonal Oscillation
(ISO) modes associated with the zonal component of the Monsoon Jet [11, 13].
As a consequence, it can be inferred that the Quasi-biweekly Oscillations
(QBO) of 12-20 days period and the Madden-Julian Oscillations (MJO) of 20-60
days period might have exacerbated the extreme event in August 2019 [12], but
cannot drive the anomalous event by itself. Therefore, the strong connection
between the high-frequency mode with the convective tendencies at mid-
troposphere in 2018 and at upper-troposphere in 2019 stands established.

###  III-C Westward-propagating High-frequency Waves

In order to study the temporal evolution of the filtered meridional winds at
any pressure levels, Hovemöller diagrams are prepared for the month of August
by meridional averaging over the latitudinal extend of the state of Kerala. As
per the above discussion, the middle and higher levels of troposphere
resonated to the 5-8 days mode during the extreme event of 2018, while only
the upper atmosphere resonated to 12-20 days and 20-60 days periodicity during
the same event. Therefore, Hovemöller diagram corresponding to 700hPa is
prepared only for the most dominant high frequency mode, while it is prepared
at 200 hPa for all the three modes of variability (Fig. 10). The 5-8 days mode
at 700hPa exposes a interesting dynamical phenomenon, vide Fig. 10(second
figure). During the extreme event of 2018, signals of strong anomalous
meridional winds propagated from the West equatorial Pacific ($100^{o}$E -
$120^{o}$E) to the east coast of Africa, with the phase speed ($C_{p}$) of
about 12 m/s. These westward propagating signals possess wave characteristics
which resemble the equatorially trapped atmospheric waves of synoptic time
scales [8, 9, 10]. The variability associated with meridional winds
corresponding to 12-20 days and 20-60 days at 200hPa, in Fig. 10(third figure)
and Fig. 10(fourth figure) respectively, do not reveal any wave
characteristics in the wind field.

Similarly, Hovemöller diagrams are prepared from meridional winds at 200hPa
pressure level in 2019 for the three variability modes (Fig. 11). As observed
in 2018, westward propagating waves of 5-8 days period, resonated the upper
troposphere for the second consecutive year (Fig. 11(first figure)). The high-
frequency waves originated near the east Indian Ocean ($100^{o}$E) crossed
over Kerala and finally reached Africa, with the same phase speed as in 2018.
As anticipated, the other modes had not assumed significance during the
extreme event (Fig. 11(second figure) and Fig. 11(third figure)). Therefore,
the westward-propagating high frequency waves were simultaneously excited in
the atmosphere with the anomalous convection over Kerala.

The ERA5 specific humidity in the atmosphere is vertically integrated from
near surface (1000 hPa) to the mid-troposphere (600 hPa) and bandpass-filtered
for the high-frequency mode for the year 2018, with the objective of
identifying the source of moisture (Fig. 12). The figure is overlaid with the
winds (5-8 days bandpassed) at 700 hPa. Alternate cyclonic and anti-cyclonic
circulations were observed to travel westward at mid-troposphere from
Equatorial Pacific to Arabian Sea, which is nothing but the manifestation of
the westward-propagating high-frequency wave train. The waves appear to
possess zonal wave length of about 6000 km as they propagate with a phase
speed of 12m/s and are trapped to the equator. One observes the transport of
moisture along the wave trajectory, especially with the cyclonic vortices,
which infers that the mid-tropospheric convection in 2018 was the response to
a low pressure region created by the circulations in the field induced by
waves. As a consequence, the waves dilated the wind field to stimulate
convection and further conveyed additional moisture to cause extreme
precipitation on the windward side of Kerala in consecutive years.

##  IV Summary & Conclusions

Kerala experienced a spate of flood events in 2018 and 2019 during Summer
Monsoon. This study resolves to understand the dynamics of anomalous rainfall
events in the state and gives better insights from the available observations.
The summary of analysis and the conclusions thus drawn are discussed here.

  1. 1.

Extreme precipitation events recurred in Kerala in 2018 and 2019, which peaked
on $15^{th}$ and $8^{th}$ August respectively. The convective activity at mid-
troposphere and upper-troposphere were strongly correlated with the spatial
distribution of precipitation.

  2. 2.

Fourier Transforms performed on the precipitation anomalies exposed the
prominent modes of variability – 5 to 8 days, 12 to 16 days and 20 to 60 days.
Out of these, the high frequency mode (5 to 8 days) is observed to dominate
over the other two in 2018 during the extreme event, although all the three
seemed to possess comparable magnitudes as they fell in-phase in 2019.

  3. 3.

The high frequency mode of period 5-8 days dominated mid-troposphere in 2018
as well as at the upper-troposphere in 2019, all particular to the period of
extreme events in the state. The 12-20 days mode (Quasi-biweekly Oscillation)
and 20-60 days mode (Madden-Julian Oscillation) have characterized the zonal
winds in 2019, thereby justifying their contribution to the extreme event of
the year, but not exclusively. Hence, the 5-8 days high frequency mode is
solely responsible for the extreme precipitation in Kerala.

  4. 4.

The high-frequency mode manifested as westward-propagating high frequency
tropical atmospheric waves of characteristic phase speed of nearly 12m/s,
which originated near east equatorial Indian Ocean or tropical West Pacific
and travelled to the east coast of Africa, and coincide with the same period
of extreme rainfall events over Kerala. Moreover, the waves appeared as
cyclonic and anti-cyclonic circulations trapped to the equator, which dilated
the wind field and transported moisture as it propagated. The waves not only
stimulated convection along its trajectory, but also ensured sufficient
moisture availability. Therefore, the convective activities which intensified
in the mid-troposphere and upper-atmosphere in 2018 and 2019 respectively,
were the direct consequence of the equatorially-trapped high frequency waves,
which played a significant role in driving the recurrent anomalous
precipitation in the South Indian state.

## Acknowledgment

The author thanks Indian Meteorological Department (IMD) and Asia-Pacific Data
Research Center (APDRC) services for granting free online access to the
observations and Reanalysis data for all users.

## Author Contributions

K.S.R. performed the analysis, drawn conclusions and prepared the manuscript.

## Competing Interests

The author declares that there exist no competing interest with any person or
agency in matters related to this research, and has not received any funds or
grants in any form for the same.

## References

  * [1] Vimal Mishra and Harsh L. Shah, “Hydroclimatological perspective of the Kerala flood of 2018,” J. Geo. Soc. India, Vol. 92, 2019, pp. 645–650.
  * [2] M. R. Hunt and Arathy Menon. “The 2018 kerala floods: a climate change perspective,” Cli. Dyn., Vol. 54, 2020, pp. 2433–2446.
  * [3] V. Yesubabu, C.V. Srinivas, G. Basha, D. Hari Prasad, S. Langodan, M. V. Ratnam, and I. Hoteit, “A diagnostic study of extreme precipitation over Kerala during August 2018,” Atm. Sci. Lett., 2019, pp. 1–26.
  * [4] Saji Mohandas, Timmy Francis, Vivek Singh, A. Jayakumar, John P. George, A. Sandeep, Prince Xavier, E.N. Rajagopal, “NWP perspective of the extreme precipitation and flood event in Kerala (India) during August 2018,” Dyn. Atm Oce., Vol. 91, 2020, pp. 1–21.
  * [5] Rosa Vellosa Lyngwa and Munir Ahmad Nayak, “Atmospheric river linked to extreme rainfall events over Kerala in August 2018,” Atm. Res., Vol. 253, 2021, pp. 1–13.
  * [6] P. Vijaykumar, S. Abhilash, A.V. Sreenath, U.N. Athira, K. Mohanakumar, B.E. Mapes, B. Chakrapani, A.K. Sahai, T.N. Niyas, O.P. Sreejith, “Kerala floods in consecutive years - Its association with mesoscale cloudburst and structural changes in monsoon clouds over the west coast of India,” Weather and Climate Extremes, Vol. 33, 100339, 2021.
  * [7] K. Wyrtki, “An equatorial jet in the indian ocean. Science, vol. 181, 1973, pp. 262–264.
  * [8] C. F. M. Raupp and P. L. Silva Dias, “Excitation mechanism of mixed Rossby-Gravity waves in the equatorial atmosphere: Role of the non linear interactions among equatorial waves,” J. Atm. Sci., Vol. 62, 2005.
  * [9] Michael Dickinson and John Molinari, “Mixed Rossby–Gravity waves and western pacific tropical cyclogenesis. part i: Synoptic evolution,” J. of Atm. Sci., Vol. 59, 2002.
  * [10] S. R. Kiran, “High-Frequency Mixed Rossby-Gravity Waves in the Mid-Troposphere Triggered Kerala Floods of 2018,” J. Extreme Events, Vol. 7, 2021, pp. 1–17.
  * [11] Xin Yan, Song Yang, Teng Wang, Eric D. Maloney, Shaorou Dong, Wei Wei and Shan He, “Quasi-biweekly oscillation of the Asian monsoon rainfall in late summer and autumn: different types of structure and propagation,” Cli. Dyn., vol. 53, 2019, pp. 6611–6628.
  * [12] Raghu Murtugudde, Richard Seager, and Prasad Thoppil, “Arabian sea response to monsoon variation,” Paleoceanography, Vol. 22, 2007.
  * [13] Sulochana Gadgil, “The monsoon system: Land–sea breeze or the ITCZ?,” J. Earth Syst. Sci., Vol. 127, 2018, pp. 1–29.


11institutetext: SnT, University of Luxembourg 22institutetext: Institute of
Computer Science, Polish Academy of Sciences, Warsaw, Poland 33institutetext:
Université d’Évry, France

# Natural Strategic Abilities in Voting Protocols

Wojciech Jamroga 1122 Damian Kurpiewski 22 Vadim Malvone 33

###### Abstract

Security properties are often focused on the technological side of the system.
One implicitly assumes that the users will behave in the right way to preserve
the property at hand. In real life, this cannot be taken for granted. In
particular, security mechanisms that are difficult and costly to use are often
ignored by the users, and do not really defend the system against possible
attacks.

Here, we propose a graded notion of security based on the complexity of the
user’s strategic behavior. More precisely, we suggest that the level to which
a security property $\varphi$ is satisfied can be defined in terms of (a) the
complexity of the strategy that the voter needs to execute to make $\varphi$
true, and (b) the resources that the user must employ on the way. The simpler
and cheaper to obtain $\varphi$, the higher the degree of security.

We demonstrate how the idea works in a case study based on an electronic
voting scenario. To this end, we model the vVote implementation of the Prêt à
Voter voting protocol for coercion-resistant and voter-verifiable elections.
Then, we identify “natural” strategies for the voter to obtain receipt-
freeness, and measure the voter’s effort that they require. We also look at
how hard it is for the coercer to compromise the election through a
randomization attack.

Keywords: electronic voting, coercion resistance, natural strategies, multi-
agent models, graded security

##  1 Introduction

Security analysis often focuses on the technological side of the system. It
implicitly assumes that the users will duly follow the sequence of steps that
the designer of the protocol prescribed for them. However, such behavior of
human participants seldom happens in real life. In particular, mechanisms that
are difficult and costly to use are often ignored by the users, even if they
are there to defend those very users from possible attacks.

For example, protocols for electronic voting are usually expected to satisfy
_receipt-freeness_ (the voter should be given no certificate that can be used
to break the anonymity of her vote) and the related property of _coercion-
resistance_ (the voter should be able to deceive the potential coercer and
cast her vote in accordance with her preferences) [7, 26, 17, 27]. More
recently, significant progress has been made in the development of voting
systems that would be coercion-resistant and at the same time _voter-
verifiable_ , i.e., would allow the voter to verify her part of the election
outcome [31, 12]. The idea is to partly “crowdsource” an audit of the election
to the voters, and see if they detect any irregularities. Examples include the
Prêt à Voter protocol [32] and its implementation vVote [13] that was used in
the 2014 election in the Australian state of Victoria.

However, the fact that a voting system includes a mechanism for voter-
verifiability does not immediately imply that it is more secure and
trustworthy. This crucially depends on how many voters will actually verify
their ballots [37], which in turn depends on how understandable and easy to
use the mechanism is. The same applies to mechanisms for coercion-resistance
and receipt-freeness, and in fact to any optional security mechanism. If the
users find the mechanism complicated and tiresome, and they can avoid it, they
will avoid it.

Thus, the right question is often not _if_ but _how much_ security is obtained
by the given mechanism. In this paper, we propose a graded notion of
_practical security_ based on the complexity of the strategic behavior,
expected from the user if a given security property is to be achieved. More
precisely, we suggest that the level to which property $\varphi$ is
“practically” satisfied can be defined in terms of (a) the complexity of the
strategy that the user needs to execute to make $\varphi$ true, and (b) the
resources that the user must employ on the way. The simpler and cheaper to
obtain $\varphi$, the higher the degree of security.

Obviously, the devil is in the detail. It often works best when a general idea
is developed with concrete examples in mind. Here, we do the first step, and
look how the level of coercion-resistance and voter-verifiability can be
assessed in vVote and Prêt à Voter. To this end, we come up with a multi-agent
model of vVote, inspired by interpreted systems [18]. We consider three main
types of agents participating in the voting process: the election system, a
voter, and a potential coercer. Then, we identify strategies for the voter to
use the voter-verifiability mechanism, and estimate the voter’s effort that
they require. We also look at how difficult it is for the coercer to
compromise the election through a randomization attack [26]. The strategic
reasoning and its complexity is formalized by means of so called _natural
strategies_ , proposed in [24, 25] and consistent with psychological evidence
on how humans use symbolic concepts [8, 19].

To create the models, we use the Uppaal model checker for distributed and
multi-agent systems [4], with its flexible modeling language and intuitive
GUI. This additionally allows to use the Uppaal verification functionality and
check that our natural strategies indeed obtain the goals for which they are
proposed.

Related work. Formal analysis of security that takes a more human-centered
approach has been done in a number of papers, for example with respect to
insider threats [21]. A more systematic approach, based on the idea of
_security ceremonies_ , was proposed and used in [10, 5, 6, 29], and applied
to formal analysis of voting protocols [28]. Here, we build on different
modeling tradition, namely on the framework of _multi-agent systems_. This
modeling approach was only used in [22] where a preliminary verification of
the Selene voting protocol was conducted. Moreover, to our best knowledge, the
idea of measuring the security level by the complexity of strategies needed to
preserve a given security requirement is entirely new.

Other (somewhat) related works include social-technical modeling of attacks
with timed automata [15] and especially game-theoretic analysis of voting
procedures [9, 14, 2, 23]. Also, strategies for human users to obtain simple
security requirements were investigated in [3]. Finally, specification of
coercion-resistance and receipt-freeness in logics of strategic ability was
attempted in [36].

##  2 Methodology

The main goal of this paper is to propose a framework for analyzing security
and usability of voting protocols, based on how easy it is for the
participants to use the functionality of the protocol and avoid a breach of
security. Dually, we can also look at how difficult it is for the attacker to
compromise the system. In this section we explain the methodology.

Figure 1:  Voter model

###  2.1 Modeling the Voting Process

The first step is to divide the description of the protocol into loosely
coupled components, called agents. The partition is often straightforward: in
our case, it will include the voter, the election infrastructure, the teller
etc.

For each agent we define its local model, which consists of locations (i.e.,
the local states of the agent) and labeled edges between locations (i.e.,
local transitions). A transition corresponds to an action performed by the
agent. An example model of the voter can be seen in Figure 1. When the voter
has scanned her ballot and is in the state $scanning$ she can perform action
$enter\\_vote$, thus moving to the state $voted$. This model, as well as the
others, has been created using the modeling interface of the Uppaal model
checker [4]. The locations in Uppaal are graphically represented as circles,
with initial locations marked by a double circle. The edges are annotated by
colored labels: guards (green), synchronizations (teal) and updates (blue).
The syntax of expressions is like that of C/C++. Guards enable the transition
if and only if the guard condition evaluates to true. Synchronizations allow
processes to synchronize over a common channel. Update expressions are
evaluated when the transition is taken.

The global model of the whole system consists of a set of concurrent
processes, i.e., local models of the agents. The combination of the local
models unfolds into a global model, where each global state represents a
possible configuration of the local states of the agents.

###  2.2 Natural Strategic Ability

Many relevant properties of multi-agent systems refer to _strategic abilities_
of agents and their groups. For example, voter-verifiability can be understood
as the ability of the voter to check if her vote was registered and tallied
correctly. Similarly, receipt-freeness can be understood as the inability of
the coercer, typically with help from the voter, to obtain evidence of how the
voter has voted [36].

Logics of strategic reasoning, such as ATL and Strategy Logic, provide neat
languages to express properties of agents’ behavior and its dynamics, driven
by individual and collective goals of the agents [1, 11, 30]. For example, the
ATL formula
$\langle\\!\langle{cust}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathsf{F}\,\mathsf{{ticket}}$
may be used to express that the customer $cust$ can ensure that he will
eventually obtain a ticket, regardless of the actions of the other agents.
Semantically, the specification holds if $cust$ has a strategy whose every
execution path satisfies $\mathsf{{ticket}}$ at some point in the future.
Strategies in a multi-agent system are understood as conditional plans, and
play central role in reasoning about purposeful agents [1, 35]. Formally,
strategies are defined as functions from states to actions. However, real-life
processes often have millions or even billions of possible states, which
allows for terribly complicated strategies – and humans are notoriously bad at
handling combinatorially complex objects.

To better model the way human agents strategize, the authors of [24, 25]
proposed to use a more human-friendly representation of strategies, based on
lists of condition-action rules. The conditions are given by Boolean formulas.
Moreover, it was postulated that only those strategies should be considered
whose complexity does not exceed a given bound. This is consistent with
classical approaches to commonsense reasoning [16] and planning [20], as well
as the empirical results on how humans learn and use concepts [8, 19].

Natural strategies. Let $\mathcal{B}(Prop_{a})$ be the set of Boolean formulas
over atomic propositions $Prop_{a}$ observable by agent $a$. In our case,
$Prop_{a}$ consists of all the references to the local variables of agent $a$,
as well as the global variables in the model. We represent natural strategies
of agent $a$ by _lists of guarded actions_ , i.e., sequences of pairs
${\phi_{i}}\leadsto{\alpha_{i}}$ such that: (1)
$\phi_{i}\in\mathcal{B}(Prop_{a})$, and (2) $\alpha_{i}$ is an action
available to agent $a$ in every state where $\phi_{i}$ holds. Moreover, we
assume that the last pair on the list is ${\top}\leadsto{\alpha}$ for some
action $\alpha$, i.e., the last rule is guarded by a condition that will
always be satisfied. A _collective natural strategy_ for a group of agents
$A=\\{{a_{1},\ldots,a_{|A|}}\\}$ is a tuple of individual natural strategies
$s_{A}=(s_{a_{1}},\ldots,s_{a_{|A|}})$. The set of such strategies is denoted
by $\Sigma_{A}$.

The “outcome” function $out(q,s_{A})$ returns the set of all paths (i.e., all
maximal traces) that occur when coalition $A$ executes strategy $s_{A}$ from
state $q$ onward, and the agents outside $A$ are free to act in an arbitrary
way.

Complexity of strategies. We will use the following complexity metric for
strategies: $\mathit{compl}(s_{A})=\sum_{(\phi,\alpha)\in s_{A}}|\phi|$, with
$|\phi|$ being the number of symbols in $\phi$, without parentheses. That is,
$\mathit{compl}(s_{A})$ simply counts the total length of guards in $s_{A}$.
Intuitively, the complexity of a strategy is understood as its level of
sophistication. It corresponds to the mental effort needed to come up with the
strategy, memorize it, and execute it.

###  2.3 Specification of Properties Based on Natural Strategies

To reason about natural strategic ability, the logic NatATL was introduced in
[24, 25] with the following syntax:

$\varphi::=\mathsf{{p}}\mid\lnot\varphi\mid\varphi\land\varphi\mid\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}^{\leq
k}\mathsf{X}\,\varphi\mid\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}^{\leq
k}\mathsf{F}\,\varphi\mid\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}^{\leq
k}\mathsf{G}\,\varphi\mid\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}^{\leq
k}\varphi\,\mathsf{U}\,\varphi.$

where $A$ is a group of agents and $k\in\mathbb{N}$ is a complexity bound.
Intuitively, $\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}^{\leq
k}\gamma$ reads as “coalition $A$ has a collective strategy of size less or
equal than $k$ to enforce the property $\gamma$.” The formulas of NatATL make
use of classical temporal operators: “$\mathsf{X}\,$” (“in the next state”),
“$\mathsf{G}\,$” (“always from now on”), “$\mathsf{F}\,$” (“now or sometime in
the future”), and $\,\mathsf{U}\,$ (strong “until”). For example, the formula
$\langle\\!\langle{cust}\rangle\\!\rangle_{{}_{\\!\mathit{}}}^{\leq
10}\mathsf{F}\,\mathsf{{ticket}}$ expresses that the customer can obtain a
ticket by a strategy of complexity at most $10$. This seems more appropriate
as a functionality requirement than to require the existence of _any_ function
from states to actions. The path quantifier “for all paths” can be defined as
$\mathsf{A}\gamma\equiv\langle\\!\langle{\emptyset}\rangle\\!\rangle_{{}_{\\!\mathit{}}}^{\leq
0}\gamma$.

We will use NatATL to specify requirements on the voting system. For example,
voter-verifiability captures the ability of the voter to verify her vote after
the election. In our case, this is represented by the $check4$ phase, hence we
can specify voter-verifiability with the formula
$\langle\\!\langle{voter}\rangle\\!\rangle_{{}_{\\!\mathit{}}}^{\leq
k}\mathsf{F}\,(\mathsf{{check4\\_ok}}\vee\mathsf{{error}})$. The intuition is
simple: the voter has a strategy of size at most $k$ to successfully perform
$check4$ or else signal an error. A careful reader can spot one problem with
the formalization: it holds if the voter can signal an error regardless of the
outcome of the check (and it shouldn’t!). A better specification is given by
$\langle\\!\langle{voter}\rangle\\!\rangle_{{}_{\\!\mathit{}}}^{\leq
k}\mathsf{F}\,(\mathsf{{check4\\_ok}}\vee\mathsf{{check4\\_fail}})$. Moreover,
we can use the formula
$\mathsf{A}\mathsf{G}\,(\mathsf{{check4\\_fail}}\rightarrow\langle\\!\langle{voter}\rangle\\!\rangle_{{}_{\\!\mathit{}}}^{\leq
k}\mathsf{F}\,\mathsf{{error}})$ to capture _dispute resolution_.

The conceptual structure of receipt-freeness is different. In that case, we
want to say that the voter has no way of proving how she has voted, and that
the coercer (or a potential vote-buyer) does not have a strategy that allows
him to learn the value of the vote. Crucially, this refers to the _knowledge_
of the coercer. To capture the requirement, we need to extend NatATL with
knowledge operators $K_{a}$, with $K_{a}\varphi$ expressing that agent $a$
knows that $\varphi$ holds. For instance, $K_{coerc}\mathsf{{voted_{i}}}$ says
that the coercer knows that the voter has voted for the candidate $i$. Then,
receipt-freeness can be formalized as

$\bigwedge_{i\in\mathit{Cand}}\lnot\langle\\!\langle{coerc,voter}\rangle\\!\rangle_{{}_{\\!\mathit{}}}^{\leq
k}\mathsf{G}\,(\mathsf{{end}}\rightarrow(K_{coerc}\mathsf{{voted_{i}}}\lor
K_{coerc}\lnot\mathsf{{voted_{i}}}))$.

That means that the coercer and the voter have no strategy with complexity at
most $k$ to learn, after the election is finished, whether the voter has voted
for $i$ or not. Note that this is only one of the possible formalization of
the requirement. For example, one may argue that, to violate receipt-freeness,
it suffices that the coercer can detect _whenever the voter has not obeyed_ ;
he does not have to learn the exact value of her vote. This can be captured by
the following formula:
$\bigwedge_{i\in\mathit{Cand}}\lnot\langle\\!\langle{coerc,voter}\rangle\\!\rangle_{{}_{\\!\mathit{}}}^{\leq
k}\mathsf{G}\,((\mathsf{{end}}\land\lnot\mathsf{{voted_{i}}})\rightarrow
K_{coerc}\lnot\mathsf{{voted_{i}}})$.

###  2.4 Using Verification Tools to Facilitate Analysis

The focus of this work is on modeling and specification; the formal analysis
is done mainly by hand. However, having the models specified in Uppaal
suggests that we can also benefit from its model checking functionality.
Unfortunately, the requirement specification language of Uppaal is very
limited, and allows for neither strategic operators nor knowledge modalities.
Still, we can use it to verify concrete strategies if we carefully modify the
input formula and the model. We will show how to do it in Section 6.

##  3 Use Case Scenario: vVote

Secure and verifiable voting is becoming more and more important for the
democracy to function correctly. In this paper, we analyze the vVote
implementation of Prêt à Voter which was used for remote voting and voting of
handicapped persons in the Victorian elections in November 2014 [13]. The main
idea of the Prêt à Voter protocol focuses on encoding the vote using a
randomized candidate list. In this protocol the ballot consists of two parts:
the randomized order of candidates (left part) and the list of empty
checkboxes along with the number encoding the order of the candidates (right
part). The voter cast her vote in an usual way, by placing a cross in the
right hand column against the candidate of her choice. After that she tears
the ballot in two parts, destroys the left part, cast the right one and takes
the copy of it as her receipt. After the election her vote appears on the Web
Bulletin Board as the pair of the encoding number and the marked box, which
can be compared with the receipt for verification. We look at the whole
process, from the voter entering the polling station, to the verification of
her vote on the public Web Bulletin Board (WBB).

After entering the polling station, the Poll Worker (PW) authenticates the
voter (using the method prescribed by the appropriate regulations), and sends
a print request to the Print On Demand (PON) device specifying the
district/region of the voter. If the authentication is valid (state
$printing$) then the PON retrieves and prints an appropriate ballot for the
voter, including a Serial Number (SN) and the district, with a signature from
the Private Web Bulletin Board (PWBB). The PWBB is a robust secure database
which receives messages, performs basic validity checks, and returns
signatures. After that, the voter may choose to check and confirm the ballot.
This involves demanding a proof that the ballot is properly formed, i.e., that
the permuted candidate list corresponds correctly to the cipher-texts on the
public WBB for that serial number. The WBB is an authenticated public
broadcast channel with memory. If the ballot has a confirmation check, the
voter returns to the printing step for a new ballot (transition from state
$check1$ to $printing$).

Having obtained and possibly checked her ballot (state $has\\_ballot$), the
voter can scan it by showing the ballot bar code to the Electronic Ballot
Marker (EBM). Then, she enters her vote (state $scanning$) via the EBM
interface. The EBM prints on a separate sheet the voter’s receipt with the
following information: (i) the electoral district, (ii) the Serial Number,
(iii) the voter’s vote permuted appropriately to match the Prêt à Voter
ballot, and (iv) a QR code with this data and the PWBB signature.

Further, the voter must check the printed vote against the printed candidate
list. In particular, she checks that the district is correct and the Serial
Number matches the one on the ballot form. If all is well done, she can
optionally check the PWBB signature, which covers only the data visible to the
voter. Note that, if either $check2$ or $check3$ fails, the vote is canceled
using the cancellation protocol. If everything is OK, the voter validates the
vote, shreds the candidate list, and leaves the polling station. Finally, the
voter can check her vote on the WBB after the election closes. She only needs
to check the SR and the order of her preference numbers.

##  4 Models

In this section we present models of a simplified version of vVote, focusing
on the steps that are important from the voter’s perspective. We use Uppaal as
the modeling tool because of its flexible modeling language and user-friendly
GUI.

Figure 2:  Voter refinement: phase check4

###  4.1 Voter Model

The model already presented in Figure 1 captures the voter actions from
entering the polling station to casting her vote, going back home and
verifying her receipt on the web bulletin board. As shown in the model, some
actions, i.e. additional checks, are optional for the voter. Furthermore, to
simulate the human behavior we added some additional actions, not described in
the protocol itself. For example the voter can skip even obligatory steps,
like $check2$. This is especially important, as $check2$ may be the most time-
consuming action for the voter and many voters may skip it in the real life.
After every check, the voter can signal an error, thus ending up in the
$error$ state. The state represents communication with the election authority,
signaling that the voter could not cast her vote or a machine malfunction was
detected.

###  4.2 Refinements of the Voter Model

The model shown in Figure 1 is relatively abstract. For example, $check4$ is
shown as an atomic action, but in fact it requires that the voter compares
data from the receipt and the WBB. In order to properly measure the complexity
of the voter strategies, it is crucial to consider different levels of
granularity.

Figure 3:  Serial number check

Figure 4:  Preferences order check

Check4 phase. Recall that this is the last phase in the protocol and it is
optional. Here, the voter can check that the printed receipt matches her
intended vote on the WBB. This includes checking that the serial numbers match
(action $check\\_serial$), and that the printed preferences order match the
one displayed on the WBB (action $check\\_preferences$). So, if both steps
succeed, then the voter reach state $check4\\_ok$. The whole model for this
phase is presented in Figure 2. Other phases, like $check2$ can be presented
in a similar way.

Serial number phase. In some cases the model shown in Figure 2 may still be
too general. Depending on the length of the serial number we can have
different levels of difficulty. For example comparing two alphanumeric
sequences of length 2 is easier then comparing such sequences of length 10. To
express this concept, we split this step into atomic actions:
$check\\_serial1(i)$ for checking the $i$th symbol on the WBB, and
$check\\_serial2(i)$ for checking the $i$th symbol on the receipt. The
resulting model is shown in Figure 4, where $n$ is the length of the serial
number.

Preferences order phase. Similarly to comparing the two serial numbers,
verifying the printed preferences can also be troublesome for the voter. In
order to make sure that her receipt matches the entry on the WBB, the voter
must check each number showing her preference. Actions $check\\_number1(i)$
and $check\\_number2(i)$ mean checking number on the WBB and on the receipt,
respectively. This is shown on the model in Figure 4, where $m$ is the number
of candidates in the ballot.

Figure 5:  Public WBB

Figure 6:  Private WBB

Figure 7:  Cancel station

###  4.3 Voting Infrastructure

The voter is not the only entity taking part in the election procedure. The
election infrastructure and the electronic devices associated with it
constitute a significant part of the procedure. Since there are several
components involved in the voting process, we decided to model each component
as a separate agent. The models of the Public WBB, Private WBB, the cancel
station, the print-on-demand printer, and the EBM are shown in Figures 7–9.

Figure 8:  Print-on-demand printer

Figure 9:  Electronic Ballot Marker (EBM)

###  4.4 Coercer Model

To model the coercer, we first need to determine his exact capabilities. Is he
able to interact with the voter, or only with the system? Should he have full
control over the network, like the Dolev-Yao attacker, or do we want the agent
to represent implicit coercion, where the relatives or subordinates are forced
to vote for the specified candidate. There are many possibilities, and to this
end we have decided that one model for the Coercer agent is not enough.
Because of that and due to lack of space, we omit the details, and only
describe the possible actions of the coercer:

  * $\bullet$

$Coerce(v,ca)$: the coercer coerces the voter $v$ to vote for his candidate
$ca$;

  * $\bullet$

$ModifyBallot(v,ca)$: the coercer modifies the ballot for $v$ by setting $ca$;

  * $\bullet$

$RequestVote(v)$: the coercer requests a vote from $v$;

  * $\bullet$

$Punish(v)$: the coercer punishes $v$;

  * $\bullet$

$Infect$: the coercer infects the voting machine with malicious code;

  * $\bullet$

$Listen(v)$: the coercer listens to the vote of $v$ from the voting machine;

  * $\bullet$

$Replace(v,ca)$: the coercer replaces the vote of $v$ with $ca$.

Some of the actions may depend on each other. For example, $Listen$ and
$Replace$ actions should be executed only after the $Infect$ action has
succeed, as the Coercer needs some kind of access to the voting machine.

##  5 Strategies and Their Complexity

There are many possible objectives for the participants of a voting procedure.
A voter’s goal could be to just cast her vote, another one could be to make
sure that her vote was correctly counted, and yet another one to verify the
election results. The same goes for the coercer: he may just want to make his
family vote in the “correct,” or to change the outcome of the election. In
order to define different objectives, we can use formulas of NatATL and look
for appropriate natural strategies, as described in Section 2. More precisely,
we can fix a subset of the participants and their objective with a formula of
NatATL, find the smallest strategy that achieves the objective, and compute
its size. The size of the strategy will be an indication of how hard it is to
make sure that the objective is achieved.

An example of specification that the voter wants to achieve is the
verifiability of her vote. Given the model in Figure 1, we can use the formula
$\langle\\!\langle{v}\rangle\\!\rangle_{{}_{\\!\mathit{}}}^{\leq k}{\rm
F}check4\\_ok$ to check whether the voter has a natural strategy of size less
or equal than $k$ to verify that her receipt has the same information
displayed in the public WBB. If we want to check only if the voter has a
natural strategy to verify her receipt, i.e. we want also consider the case in
which the voter’s receipt and the information in the public WBB are different,
we can consider the formula
$\langle\\!\langle{v}\rangle\\!\rangle_{{}_{\\!\mathit{}}}^{\leq k}{\rm
F}(check4\\_ok\vee check4\\_fail)$ as we discussed in Section 2.3.

Note that it is essential to fix the granularity level of the modeling right.
When shifting the level of abstraction, we obtain significantly different
“measurements” of strategic complexity. This is why we proposed several
variants of the voter model in Section 4. In this section, we will show how it
affects the outcome of the analysis.

In the following we take another look at the previously defined models and try
to list possible strategies for the participants.

###  5.1 Strategies for the Voter

In this section we focus on natural strategies for voter-verifiability. Given
the model in Figure 1, we can analyze an example of natural strategy that can
be used by the voter to achieve the end of the voting procedure, i.e., to
satisfy the NatATL formula
$\varphi_{1}=\langle\\!\langle{v}\rangle\\!\rangle_{{}_{\\!\mathit{}}}^{\leq
k}{\rm F}\mathsf{{end}}$. Clearly, $\varphi_{1}$ specifies the fact that the
voter has a natural strategy of size less or equal than $k$ (captured by
$\langle\\!\langle{v}\rangle\\!\rangle_{{}_{\\!\mathit{}}}^{\leq k}$) to reach
sooner or later (captured by the eventually operator ${\rm F}$) the end of
procedure (i.e. the state labeled with atom $\mathsf{{end}}$).

###### Natural Strategy 1

A strategy for the voter is:

  1. 1.

$\mathsf{{has\\_ballot}}\leadsto scan\\_ballot$

  2. 2.

$\mathsf{{scanning}}\leadsto enter\\_vote$

  3. 3.

$\mathsf{{voted}}\leadsto check2$

  4. 4.

$\mathsf{{check2\\_ok}}\vee\mathsf{{check2\\_fail}}\vee\mathsf{{out}}\leadsto
move\\_next$

  5. 5.

$\mathsf{{vote\\_ok}}\leadsto shred\\_ballot$

  6. 6.

$\mathsf{{shred}}\leadsto leave$

  7. 7.

$\mathsf{{check4}}\leadsto check4$

  8. 8.

$\mathsf{{check4\\_ok}}\vee\mathsf{{check4\\_fail}}\leadsto finish$

  9. 9.

$\top\leadsto\star$

Recall that the above is an ordered sequence of guarded commands. The first
condition (guard) that evaluates to _true_ determines the action of the voter.
Thus, if the voter has the ballot and she has not scanned it (proposition
$\mathsf{{has\\_ballot}}$), she scans the ballot. If $\mathsf{{has\\_ballot}}$
is false and $\mathsf{{scanning}}$ is true then she enters her vote, and so
on. If all the preconditions except $\top$ are false, then she executes an
arbitrary available action (represented by the wildcard $\star$). For example,
the voter will do $print\\_ballot$ at the state $printing$, where the voter
needs to wait while the Pool Walker identifies her and generates a new ballot.

In Natural Strategy 1, we have $9$ guarded commands in which the command (4)
costs $5$ since in its condition there are five symbols (three atoms plus two
disjunctions), the command (7) costs $3$ since in its condition there are
three symbols (two atoms plus the disjunction), while the other guarded
commands cost $1$, so the total complexity is $1\cdot 7+3\cdot 1+5\cdot 1=15$.
So, the formula $\varphi_{1}$ is true with any $k$ of $15$ or more. Further,
by Natural Strategy 1, starting from the state $\mathsf{{has\\_ballot}}$, the
voter needs of $9$ steps to achieve the state $\mathsf{{end}}$.

Note that Natural Strategy 1 can be also used to demonstrate that the formula
$\psi=\langle\\!\langle{v}\rangle\\!\rangle_{{}_{\\!\mathit{}}}^{\leq k}{\rm
F}(\allowbreak\mathsf{{check4\\_ok}}\vee\mathsf{{check4\\_fail}})$ holds. In
that case, we can reduce the size of the strategy by removing the guarded
command (8). Thus, $\psi$ is satisfied even for $k\geq 12$.

For completeness, in what follows, we show a natural strategy with the
additional guarded commands in case the voter wants to do the optional phases
$check1$ and $check3$, i.e., we want to satisfy the formula
$\varphi_{2}=\langle\\!\langle{v}\rangle\\!\rangle_{{}_{\\!\mathit{}}}^{\leq
k}{\rm F}(\mathsf{{checked1}}\land\mathsf{{checked3}}\land\mathsf{{end}})$. In
particular, $\varphi_{2}$ checks whether there exist a natural strategy for
the voter such that sooner or later she does $check1$, $check3$, and ends the
whole voting process. Note that, apart from the standard propositions like
$check1$, we also add their persistent version like $checked1$, i.e., once it
gets true, it remains always true.

###### Natural Strategy 2

A strategy for the voter that considers the optional phases $check1$ and
$check3$ is:

  1. 1.

$\mathsf{{has\\_ballot}}\land\mathsf{{counter==0}}\leadsto check1$

  2. 2.

$\mathsf{{has\\_ballot}}\leadsto scan\\_ballot$

  3. 3.

$\mathsf{{scanning}}\leadsto enter\\_vote$

  4. 4.

$\mathsf{{voted}}\leadsto check2$

  5. 5.

$\mathsf{{check2\\_ok}}\vee\mathsf{{check2\\_fail}}\leadsto check3$

  6. 6.

$\mathsf{{check1}}\vee\mathsf{{check3}}\vee\mathsf{{out}}\leadsto move\\_next$

  7. 7.

$\mathsf{{vote\\_ok}}\leadsto shred\\_ballot$

  8. 8.

$\mathsf{{shred}}\leadsto leave$

  9. 9.

$\mathsf{{check4}}\leadsto check4$

  10. 10.

$\mathsf{{check4\\_ok}}\vee\mathsf{{check4\\_fail}}\leadsto finish$

  11. 11.

$\top\leadsto\star$

In Natural Strategy 2, we introduce the verification of $check1$ and $check3$.
To do this we add two new guarded commands (5) and (6), and we update (1) by
adding a control on a counter to determine if $check1$ is done or not. Here,
we have a total complexity of $1\cdot 7+3\cdot 3+5\cdot 1=21$. So, the formula
$\varphi_{2}$ is true for any $k\geq 21$. Further, by Natural Strategy 2,
starting from the state $\mathsf{{has\\_ballot}}$, the voter needs of $13$
steps to achieve the state $\mathsf{{end}}$.

An important aspect to evaluate in this subject concerns the detailed analysis
of $check4$. Some interesting questions on this analysis could be: how does
the voter perform $check4$? How does she compare the printed preferences with
the information in the public WWB? These questions open up several scenarios
both from a strategic point of view and from the model to be used. From a
strategic point of view, we could consider a refinement of Natural Strategy 1,
in which the action $check4$ is evaluated as something of atomic. If we
consider that the $check4$ includes: comparing preferences with the
information in the public WWB and checking the serial number, we can already
divide the single action into two different actions for each of the checks to
be performed. So, given the model in Figure 2, we can refine the natural
strategy for the voter, as follows.

###### Natural Strategy 3

A strategy for the voter that refines $check4$ is:

  1. 1.

$\mathsf{{has\\_ballot}}\leadsto scan\\_ballot$

  2. 2.

$\mathsf{{scanning}}\leadsto enter\\_vote$

  3. 3.

$\mathsf{{voted}}\leadsto check2$

  4. 4.

$\mathsf{{check2\\_ok}}\vee\mathsf{{check2\\_fail}}\vee\mathsf{{out}}\leadsto
move\\_next$

  5. 5.

$\mathsf{{vote\\_ok}}\leadsto shred\\_ballot$

  6. 6.

$\mathsf{{shred}}\leadsto leave$

  7. 7.

$\mathsf{{check4}}\leadsto check\\_serial$

  8. 8.

$\mathsf{{check4\\_1}}\leadsto check\\_preferences$

  9. 9.

$\mathsf{{check4\\_2}}\leadsto check4$

  10. 10.

$\mathsf{{check4\\_ok}}\vee\mathsf{{check4\\_fail}}\leadsto finish$

  11. 11.

$\top\leadsto\star$

In Natural Strategy 3, we have $11$ guarded commands in which all the
conditions are defined with a single atom but (4) in which there is a
disjunction of three atoms and (10) in which there is a disjunction of two
atoms. So, the total complexity is $1\cdot 9+3\cdot 1+5\cdot 1=17$.

To verify that the voter does each step of $check4$, we need to provide a
formula that verifies atoms $\mathsf{{check4}}$, $\mathsf{{check4\\_1}}$, and
$\mathsf{{check4\\_2}}$. To do this in NatATL, we use the formula
$\varphi_{3}=\langle\\!\langle{v}\rangle\\!\rangle_{{}_{\\!\mathit{}}}^{\leq
k}{\rm
F}(\mathsf{{checked4}}\land\mathsf{{checked4\\_1}}\land\mathsf{{checked4\\_2}})$.
Note that $\varphi_{3}$ is true for any $k\geq 17$; one can use Natural
Strategy 3 to demonstrate that.

In addition, to increase the level of detail, one could consider that the
voter checks the preferences and the serial number one by one in an ordered
fashion. So, given the models in Figures 4 and 4, we can consider a formula
that checks whether the voter has a strategy that satisfies the following
properties:

  1. 1.

sooner or later she enters in the $check4$ phase;

  2. 2.

she verifies a symbols of the SN in the public WBB and in her receipt;

  3. 3.

she does (2) until the last symbol of the serial number is verified;

  4. 4.

she does a similar approach as in (2)-(3) for the verification of preferences;

  5. 5.

she finishes the whole procedure.

This can be captured by the formula
$\varphi_{4}=\langle\\!\langle{v}\rangle\\!\rangle_{{}_{\\!\mathit{}}}^{\leq
k}{\rm
F}(\mathsf{{checked4}}\land\mathsf{{wbb\\_checked\\_sn}}\land\mathsf{{receipt\\_checked\\_sn}}\land\mathsf{{checked4\\_1}}\land\mathsf{{wbb\\_checked\\_pr}}\land\mathsf{{receipt\\_checked\\_pr}}\land\mathsf{{checked4\\_2}})$.
So, we can define a natural strategy that satisfies $\varphi_{4}$, as follows.

###### Natural Strategy 4

A strategy for the voter that still refines $check4$ is:

  1. 1.

$\mathsf{{has\\_ballot}}\leadsto scan\\_ballot$

  2. 2.

$\mathsf{{scanning}}\leadsto enter\\_vote$

  3. 3.

$\mathsf{{voted}}\leadsto check2$

  4. 4.

$\mathsf{{vote\\_ok}}\leadsto shred\\_ballot$

  5. 5.

$\mathsf{{shred}}\leadsto leave$

  6. 6.

$\mathsf{{out}}\vee\mathsf{{check2\\_ok}}\vee\mathsf{{check2\\_fail}}\vee\mathsf{{receipt\\_check\\_sn}}\vee\mathsf{{receipt\\_check\\_pr}}\leadsto
move\\_next$

  7. 7.

$\mathsf{{check4}}\leadsto check\\_serial1$

  8. 8.

$\mathsf{{wbb\\_check\\_sn}}\leadsto check\\_serial2$

  9. 9.

$\mathsf{{receipt\\_check\\_sn}}\land\mathsf{{i==n}}\leadsto end\\_first$

  10. 10.

$\mathsf{{check4\\_1}}\leadsto check\\_number1$

  11. 11.

$\mathsf{{wbb\\_check\\_pr}}\leadsto check\\_number2$

  12. 12.

$\mathsf{{receipt\\_check\\_pr}}\land\mathsf{{j==m}}\leadsto end\\_second$

  13. 13.

$\mathsf{{check4\\_2}}\leadsto check4$

  14. 14.

$\mathsf{{check4\\_ok}}\vee\mathsf{{check4\\_fail}}\leadsto finish$

  15. 15.

$\top\leadsto\star$

To conclude, the above natural strategy has $15$ guarded commands in which the
conditions in (9), (12), and (14) are conjunctions of two atoms, the condition
in (6) is a disjunction of five atoms, and all the other conditions are
defined with a single atom. Therefore, the complexity of Natural Strategy 4 is
$1\cdot 11+3\cdot 3+9\cdot 1=29$. So, the formula $\varphi_{4}$ is true with
$k\geq 29$.

###  5.2 Counting Other Kinds of Resources

So far, we have measured the effort of the voter by how complex strategies she
must execute. This helps to estimate the mental difficulty related, e.g., to
voter-verifiability. However, this is not the only source of effort that the
voter has to invest. Verifying one’s vote might require money (for example, if
the voter needs to buy special software or a dedicated device), computational
power, and, most of all, time. Here, we briefly concentrate on the latter
factor.

For a voter’s task expressed by the NatATL formula
$\langle\\!\langle{v}\rangle\\!\rangle_{{}_{\\!\mathit{}}}^{\leq
k}\mathsf{F}\,\varphi$ and a natural strategy $s_{v}$ for the voter, we can
estimate the time spent on the task by the number of transitions necessary to
reach $\varphi$. That is, we take all the paths in $out(q,s_{v})$, where $q$
is the initial state of the procedure. On each path, $\varphi$ must occur at
some point. We look for the path where the first occurrence of $\varphi$
happens _latest_ , and count the number of steps to $\varphi$ on that path. We
will demonstrate how it works on the last two strategies from Section 5.1.

For Natural Strategy 3, starting from the starting state, the voter needs of
$9+2=11$ steps to achieve
$\mathsf{{check4}}\land\mathsf{{wbb\\_check\\_sn}}\land\mathsf{{receipt\\_check\\_sn}}\land\mathsf{{check4\\_1}}\land\mathsf{{wbb\\_check\\_pr}}\land\mathsf{{receipt\\_check\\_pr}}\land\mathsf{{check4\\_2}}$.
More precisely, $9$ steps are needed to achieve $check4$ in the local model
shown in Figure 1, and $2$ more steps to reach $check4\\_2$ in the refinement
of the final section of the procedure (see Figure 2).

For Natural Strategy 4, the calculation is slightly more complicated. Starting
from state $\mathsf{{start}}$, the voter needs of $9+((2\cdot n)+1)+((2\cdot
m)+1)$ steps to achieve her goals, where $n$ and $m$ are the sizes of the
serial number and the list of preferences, respectively. In particular, $9$
steps are needed to achieve $check4$ in Figure 1, then $((2\cdot n)+1)$ steps
to achieve $check4\\_1$ in Figure 4, and finally $((2\cdot m)+1)$ steps to
achieve $check4\\_2$ in Figure 4.

###  5.3 Strategies for the Coercer

For the coercer, we can start the analysis by considering the basic setting in
which he requests the vote and if the voter does not give him the ballot or
the vote is different with the one imposed by him, then he punish the voter.
This reasoning is captured by the following natural strategy.

  1. 1.

$\neg\mathsf{{coerced_{v}}}\leadsto Coerce(v,ca)$

  2. 2.

$\mathsf{{coerced_{v}}}\land\neg\mathsf{{requested_{v}}}\leadsto
RequestVote(v)$

  3. 3.

$\mathsf{{coerced_{v}}}\land\mathsf{{requested_{v}}}\land\neg\mathsf{{punished_{v}}}\land(\mathsf{{ca_{v}}}\neq\mathsf{{ca}}\lor\mathsf{{not\\_show_{v}}})\leadsto
Punish(v)$

The total complexity of the above natural strategy is $16$ since (1) has $2$
symbols (atom + negation), (2) has $4$ symbols (two atoms + conjunction +
negation), and (3) has $10$ symbols (five atoms + three conjunctions +
negation + disjunction).

Another intervention of the coercer regards the possibility to infect one or
more machines and to replace the vote of a voter.

  1. 1.

$\neg\mathsf{{infected}}\leadsto Infect$

  2. 2.

$\mathsf{{infected}}\land\neg\mathsf{{replaced_{v}}}\leadsto Replace(v,ca)$

In this case the complexity is $6$ since we have three atoms involved, two
negations, and a conjunction.

We can extend the above by considering that the coercer can infect the machine
and then can coerce the voter. So, if the coercer see a different vote on the
machine he can punish the voter. Note that this setting is interesting in the
case the coercer has infected a machine that only displays informations
without having the power to modify the vote.

  1. 1.

$\neg\mathsf{{infected}}\leadsto Infect$

  2. 2.

$\neg\mathsf{{coerced_{v}}}\leadsto Coerce(v,ca)$

  3. 3.

$\mathsf{{infected}}\land\mathsf{{listen_{v}}}\neq\mathsf{{ca}}\leadsto
Punish(v)$

In the above, the complexity is $7$, where (1) and (2) have complexity $2$ and
(3) has complexity $3$.

##  6 Automated Verification of Strategies

In this section we explain how the model checking functionality of Uppaal can
be used for an automated verification of the strategies presented in Section
5. To verify selected formulas and the corresponding natural strategies, we
need to modify several things: _(i)_ the formula, _(ii)_ the natural strategy
and finally, _(iii)_ the model. We start by explaining the required
modifications step by step.

Formula. To specify the required properties for the protocol, we have used a
variant of strategic logic, as it is one of the most suited logic to specify
properties for agents in an intuitive way. However, Uppaal does not support
NatATL, so the formula needs to be modified accordingly. In the formula we
replace the strategic operator
$\langle\\!\langle{A}\rangle\\!\rangle_{{}_{\\!\mathit{}}}^{\leq k}$ with an
universal path quantifier A. For example, we can consider the formula
$\varphi_{1}$ used in Section 5. In this context, we produce the CTL formula
$\varphi^{\prime}_{1}={\rm A}{\rm F}\mathsf{{end}}$.

Natural Strategy. The natural strategy needs to be modified so that all the
guard conditions are mutually exclusive. To this end, we go through the
preconditions from top to bottom, and refine them by adding the negated
preconditions from all the previous guarded commands. For example, Natural
Strategy 1 is modified as follows:

  1. 1.

$\mathsf{{has\\_ballot}}\leadsto scan\\_ballot$

  2. 2.

$\lnot\mathsf{{has\\_ballot}}\land\mathsf{{scanning}}\leadsto enter\\_vote$

  3. 3.

$\lnot\mathsf{{has\\_ballot}}\land\lnot\mathsf{{scanning}}\land\mathsf{{voted}}\leadsto
check2$

  4. 4.

$\lnot\mathsf{{has\\_ballot}}\land\lnot\mathsf{{scanning}}\land\lnot\mathsf{{voted}}\land(\mathsf{{check2\\_ok}}\vee\mathsf{{check2\\_fail}}\vee\mathsf{{out}})\leadsto
move\\_next$

  5. 5.

$\lnot\mathsf{{has\\_ballot}}\land\lnot\mathsf{{scanning}}\land\lnot\mathsf{{voted}}\land\lnot(\mathsf{{check2\\_ok}}\vee\mathsf{{check2\\_fail}}\vee\mathsf{{out}})\land\mathsf{{vote\\_ok}}\leadsto
shred\\_ballot$

  6. 6.

$\lnot\mathsf{{has\\_ballot}}\land\lnot\mathsf{{scanning}}\land\lnot\mathsf{{voted}}\land\lnot(\mathsf{{check2\\_ok}}\vee\mathsf{{check2\\_fail}}\vee\mathsf{{out}})\land\lnot\mathsf{{vote\\_ok}}\land\mathsf{{shred}}\leadsto
leave$

  7. 7.

$\lnot\mathsf{{has\\_ballot}}\land\lnot\mathsf{{scanning}}\land\lnot\mathsf{{voted}}\land\lnot(\mathsf{{check2\\_ok}}\vee\mathsf{{check2\\_fail}}\vee\mathsf{{out}})\land\lnot\mathsf{{vote\\_ok}}\land\lnot\mathsf{{shred}}\land(\mathsf{{check4\\_ok}}\vee\mathsf{{check4\\_fail}})\leadsto
finish$

  8. 8.

$\top\leadsto\star$

Model. To verify the selected strategy, we fix it in the model by adding the
preconditions of the guards to the preconditions of the corresponding local
transitions in the voter’s model. Thus, we effectively remove all transitions
that are not in accordance with the strategy. This way, only the paths that
are consistent with the strategy will be considered by the model-checker.

Levels of granularity. As we showed in Section 4, it is often important to
have variants of the model for different levels of abstraction. To handle
those in Uppaal, we have used synchronizations edges. For example, to have a
more detailed version of the phase $check4$, we added synchronization edges in
the voter model (Figure 1) and in the $check4$ model (Figure 2). Then, when
going through the $check4$ phase in the voter model, Uppaal will proceed to
the more detailed model and come back after getting to its final state.

Running the verification. We have modified the models, formulas, and
strategies from Sections 4 and 5 following the above steps. Then, we used
Uppaal to verify that Natural Strategies 1–4 indeed enforce the prescribed
properties. The tool reported that each formula holds in the corresponding
model. The execution time was always at most a few seconds.

##  7 Conclusions

In the analysis of a voting protocols it is important to make sure that the
voter has a strategy to use the functionality of the protocol. That is, she
has a strategy to fill in and cast her ballot, verify her vote on the bulletin
board, etc. However, this is not enough: it is also essential to see how hard
that strategy is. In this paper, we propose a methodology that can be used to
this end. One can assume a natural representation of the voter’s strategy, and
to measure its complexity as the size of the representation.

We mainly focus on one aspect of the voter’s effort, namely the mental effort
needed to produce, memorize, and execute the required actions. We also
indicate that there are other important factors, like the time needed to
execute the strategy or the financial cost of the strategy. This may lead to
tradeoffs where optimizing the costs with respect to one resource leads to
higher costs in terms of another resource. Moreover, resources can vary in
their importance for different agents. For example, time may be more important
for the voter, while money more relevant when we analyze the strategy of the
coercer. We leave a closer study of such tradeoffs for future work.

Another interesting extension would be to further analyze the parts of the
protocol where the voter compares two numbers, tables, etc. As the voter is a
human being, it is natural for her to make a mistake. Furthermore, the
probability of making a mistake at each step can be added to the model to
analyze the overall probability of successfully comparing two data sets by the
voter.

Finally, we point out that the methodology proposed in this paper can be
applied outside the e-voting domain. For example, one can use it to study the
usability of policies for social distancing in the current epidemic situation,
and whether they are likely to obtain the expected results.

## References

  * [1] R. Alur, T. A. Henzinger, and O. Kupferman.  Alternating-time Temporal Logic.  Journal of the ACM, 49:672–713, 2002.
  * [2] David A. Basin, Hans Gersbach, Akaki Mamageishvili, Lara Schmid, and Oriol Tejada.  Election security and economics: It’s all about Eve.  In Proceedings of E-Vote-ID, pages 1–20, 2017.
  * [3] David A. Basin, Sasa Radomirovic, and Lara Schmid.  Modeling human errors in security protocols.  In Computer Security Foundations Symposium, CSF, pages 325–340. IEEE Computer Society, 2016.
  * [4] G. Behrmann, A. David, and K.G. Larsen.  A tutorial on uppaal.  In Formal Methods for the Design of Real-Time Systems: SFM-RT, number 3185 in LNCS, pages 200–236. Springer, 2004.
  * [5] Giampaolo Bella, Paul Curzon, Rosario Giustolisi, and Gabriele Lenzini.  A socio-technical methodology for the security and privacy analysis of services.  In COMPSAC Workshops, pages 401–406. IEEE Computer Society, 2014.
  * [6] Giampaolo Bella, Paul Curzon, and Gabriele Lenzini.  Service security and privacy as a socio-technical problem.  J. Comput. Secur., 23(5):563–585, 2015.
  * [7] J. Benaloh and D. Tuinstra.  Receipt-free secret-ballot elections.  In Proceedings of the twenty-sixth annual ACM symposium on Theory of Computing, pages 544–553. ACM, 1994.
  * [8] L. E. Bourne.  Knowing and using concepts.  Psychol. Rev., 77:546–556, 1970.
  * [9] Ahto Buldas and Triinu Mägi.  Practical security analysis of e-voting systems.  In Proceedings of IWSEC, volume 4752 of Lecture Notes in Computer Science, pages 320–335. Springer, 2007.
  * [10] Marcelo Carlomagno Carlos, Jean Everson Martina, Geraint Price, and Ricardo Felipe Custódio.  A proposed framework for analysing security ceremonies.  In SECRYPT, pages 440–445. SciTePress, 2012.
  * [11] K. Chatterjee, T.A. Henzinger, and N. Piterman.  Strategy Logic.  Information and Computation, 208(6):677–693, 2010.
  * [12] V. Cortier, D. Galindo, R. Küsters, J. Müller, and T. Truderung.  SoK: Verifiability notions for e-voting protocols.  In IEEE Symposium on Security and Privacy, pages 779–798, 2016\.
  * [13] C. Culnane, P.Y.A. Ryan, S.A. Schneider, and V. Teague.  vvote: A verifiable voting system.  ACM Trans. Inf. Syst. Secur., 18(1):3:1–3:30, 2015.
  * [14] Chris Culnane and Vanessa Teague.  Strategies for voter-initiated election audits.  In Decision and Game Theory for Security: Proceedings of GameSec, volume 9996 of Lecture Notes in Computer Science, pages 235–247. Springer, 2016.
  * [15] Nicolas David, Alexandre David, René Rydhof Hansen, Kim Guldstrand Larsen, Axel Legay, Mads Chr. Olesen, and Christian W. Probst.  Modelling social-technical attacks with timed automata.  In Proceedings of International Workshop on Managing Insider Security Threats, MIST, pages 21–28. ACM, 2015.
  * [16] E. Davis and G. Marcus.  Commonsense reasoning.  Communications of the ACM, 58(9):92–103, 2015.
  * [17] S. Delaune, S. Kremer, and M. Ryan.  Coercion-resistance and receipt-freeness in electronic voting.  In Computer Security Foundations Workshop, 2006. 19th IEEE, pages 12–pp. IEEE, 2006.
  * [18] R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi.  Reasoning about Knowledge.  MIT Press, 1995.
  * [19] J. Feldman.  Minimization of Boolean complexity in human concept learning.  Nature, 407:630–3, 11 2000.
  * [20] M. Ghallab, D. Nau, and P. Traverso.  Automated Planning: Theory and Practice.  Morgan Kaufmann, 2004.
  * [21] Jeffrey Hunker and Christian W. Probst.  Insiders and insider threats - an overview of definitions and mitigation techniques.  J. Wirel. Mob. Networks Ubiquitous Comput. Dependable Appl., 2(1):4–27, 2011.
  * [22] W. Jamroga, M. Knapik, and D. Kurpiewski.  Model checking the SELENE e-voting protocol in multi-agent logics.  In Proceedings of the 3rd International Joint Conference on Electronic Voting (E-VOTE-ID), volume 11143 of Lecture Notes in Computer Science, pages 100–116. Springer, 2018.
  * [23] W. Jamroga and M. Tabatabaei.  Preventing coercion in e-voting: Be open and commit.  In Electronic Voting: Proceedings of E-Vote-ID 2016, volume 10141 of Lecture Notes in Computer Science, pages 1–17. Springer, 2017\.
  * [24] Wojciech Jamroga, Vadim Malvone, and Aniello Murano.  Natural strategic ability.  Artificial Intelligence, 277, 2019.
  * [25] Wojciech Jamroga, Vadim Malvone, and Aniello Murano.  Natural strategic ability under imperfect information.  In Proceedings of the 18th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2019, pages 962–970. IFAAMAS, 2019.
  * [26] A. Juels, D. Catalano, and M. Jakobsson.  Coercion-resistant electronic elections.  In Proceedings of the 2005 ACM workshop on Privacy in the electronic society, pages 61–70. ACM, 2005.
  * [27] R. Küsters, T. Truderung, and A. Vogt.  A game-based definition of coercion-resistance and its applications.  In Proceedings of the 2010 23rd IEEE Computer Security Foundations Symposium, pages 122–136. IEEE Computer Society, 2010.
  * [28] T. Martimiano, E. Dos Santos, M. Olembo, and J.E. Martina.  Ceremony analysis meets verifiable voting: Individual verifiability in Helios.  In SECURWARE, 2015.
  * [29] Taciane Martimiano and Jean Everson Martina.  Threat modelling service security as a security ceremony.  In 11th International Conference on Availability, Reliability and Security, ARES, pages 195–204. IEEE Computer Society, 2016.
  * [30] F. Mogavero, A. Murano, G. Perelli, and M.Y. Vardi.  Reasoning about strategies: On the model-checking problem.  ACM Transactions on Computational Logic, 15(4):1–42, 2014.
  * [31] Peter Y. A. Ryan, Steve A. Schneider, and Vanessa Teague.  End-to-end verifiability in voting systems, from theory to practice.  IEEE Security & Privacy, 13(3):59–62, 2015.
  * [32] P.Y.A. Ryan.  The computer ate my vote.  In Formal Methods: State of the Art and New Directions, pages 147–184. Springer, 2010.
  * [33] F.P. Santos.  Dynamics of Reputation and the Self-organization of Cooperation.  PhD thesis, University of Lisbon, 2018.
  * [34] F.P. Santos, F.C. Santos, and J.M. Pacheco.  Social norm complexity and past reputations in the evolution of cooperation.  Nature, 555:242–245, 2018.
  * [35] Y. Shoham and K. Leyton-Brown.  Multiagent Systems - Algorithmic, Game-Theoretic, and Logical Foundations.  Cambridge University Press, 2009.
  * [36] M. Tabatabaei, W. Jamroga, and Peter Y. A. Ryan.  Expressing receipt-freeness and coercion-resistance in logics of strategic ability: Preliminary attempt.  In Proceedings of the 1st International Workshop on AI for Privacy and Security, PrAISe@ECAI 2016, pages 1:1–1:8. ACM, 2016.
  * [37] Verified Voting.  Policy on direct recording electronic voting machines and ballot marking devices.  2019\.