Theory Propaedeutics
section "Propaedeutic definitions and lemmas"
theory Propaedeutics
imports Complex_Main "HOL-Library.Countable"
begin
declare [[goals_limit = 20]]
text ‹
\null
\emph{This paper is an achievement of the whole OS Development and Certification team of the Arjo
Systems site at Arzano, Italy, because it would have never been born without the contributions of my
colleagues, the discussions we had, the ideas they shared with me. Particularly, the intuition that
the use of Chip Authentication Mapping makes the secrecy of the PACE authentication key unnecessary
is not mine. I am very grateful to all the team members for these essential contributions, and even
more for these unforgettable years of work together.}
›
subsection "Introduction"
text ‹
Password-based authentication in an insecure environment -- such as password-based authentication
between a user and a smart card, which is the subject of this paper -- requires that the password be
exchanged on a secure channel, so as to prevent it from falling into the hands of an eavesdropper.
A possible method to establish such a channel is Password Authenticated Connection Establishment
(PACE), which itself is a password-based Diffie-Hellman key agreement protocol, specified in the
form of a smart card protocol in \<^cite>‹"R4"›. Thus, in addition to the user's password, another
password is needed if PACE is used, namely the one from which the PACE authentication key is
derived.
A simple choice allowing to reduce the number of the passwords that the user has to manage would be
to employ the same password both as key derivation password, verified implicitly by means of the
PACE protocol, and as direct use password, verified explicitly by comparison. However, this approach
has the following shortcomings:
\begin{itemize}
\item
A usual countermeasure against trial-and-error attacks aimed at disclosing the user's password
consists of blocking its use after a number of consecutive verification failures exceeding a given
threshold. If the PACE authentication key is derived from the user's password, such key has to be
blocked as well. Thus, an additional PACE authentication key would be needed for any user's
operation not requiring to be preceded by the verification of the user's password, but only to be
performed on a secure channel, such as the verification of a Personal Unblocking Code (PUC) by means
of command RESET RETRY COUNTER \<^cite>‹"R5"› to unblock the password. On the contrary, a single PACE
authentication key is sufficient for all user's operations provided it is independent of the user's
password, which leads to a simpler system.
\item
The user is typically allowed to change her password, e.g. by means of command CHANGE REFERENCE DATA
\<^cite>‹"R5"›. If the PACE authentication key is derived from the user's password, such key has to be
changed as well. This gives rise to additional functional requirements which can be nontrivial to
meet, particularly in the case of a preexisting implementation having to be adapted. For instance,
if the key itself is stored on the smart card rather than being derived at run time from the user's
password, which improves performance and prevents side channel attacks, the update of the password
and the key must be performed as an atomic operation to ensure their consistency. On the contrary,
the PACE authentication key can remain unchanged provided it is independent of the user's password,
which leads to a simpler system.
\end{itemize}
Therefore, a PACE password distinct from the user's password seems to be preferable. As the user's
password is a secret known by the user only, the derivation of the PACE authentication key from the
user's password would guarantee the secrecy of the key as well. If the PACE authentication key is
rather derived from an independent password, then a new question arises: is this key required to be
secret?
In order to find the answer, it is useful to schematize the protocol applying the informal notation
used in \<^cite>‹"R1"›. If Generic Mapping is employed as mapping method (cf. \<^cite>‹"R4"›), the protocol
takes the following form, where agents $U$ and $C$ stand for a given user and her own smart card,
step C$n$ for the $n$th command APDU, and step R$n$ for the $n$th response APDU (for further
information, cf. \<^cite>‹"R4"› and \<^cite>‹"R5"›).
\null
\qquad R1. $C \rightarrow U : \{s\}_K$
\qquad C2. $U \rightarrow C : PK_{Map,PCD}$
\qquad R2. $C \rightarrow U : PK_{Map,IC}$
\qquad C3. $U \rightarrow C : PK_{DH,PCD}$
\qquad R3. $C \rightarrow U : PK_{DH,IC}$
\qquad C4. $U \rightarrow C : \{PK_{DH,IC}\}_{KS}$
\qquad R4. $C \rightarrow U : \{PK_{DH,PCD}\}_{KS}$
\qquad C5. $U \rightarrow C : \{$\emph{User's password}$\}_{KS}$
\qquad R5. $C \rightarrow U : \{$\emph{Success code}$\}_{KS}$
\null
Being irrelevant for the security analysis of the protocol, the initial MANAGE SECURITY ENVIRONMENT:
SET AT command/response pair, as well as the first GENERAL AUTHENTICATE command requesting nonce
$s$, are not included in the scheme.
In the response to the first GENERAL AUTHENTICATE command (step R1), the card returns nonce $s$
encrypted with the PACE authentication key $K$.
In the second GENERAL AUTHENTICATE command/response pair (steps C2 and R2), the user and the card
exchange the respective ephemeral public keys $PK_{Map,PCD} = [SK_{Map,PCD}]G$ and $PK_{Map,IC} =
[SK_{Map,IC}]G$, where $G$ is the static cryptographic group generator (the notation used in
\<^cite>‹"R6"› is applied). Then, both parties compute the ephemeral generator $G' = [s + SK_{Map,PCD}
\times SK_{Map,IC}]G$.
In the third GENERAL AUTHENTICATE command/response pair (steps C3 and R3), the user and the card
exchange another pair of ephemeral public keys $PK_{DH,PCD} = [SK_{DH,PCD}]G'$ and $PK_{DH,IC} =
[SK_{DH,IC}]G'$, and then compute the shared secret $[SK_{DH,PCD} \times SK_{DH,IC}]G'$, from which
session keys $KS_{Enc}$ and $KS_{MAC}$ are derived. In order to abstract from unnecessary details,
the above scheme considers a single session key $KS$.
In the last GENERAL AUTHENTICATE command/response pair (steps C4 and R4), the user and the card
exchange the respective authentication tokens, obtained by computing a Message Authentication Code
(MAC) of the ephemeral public keys $PK_{DH,IC}$ and $PK_{DH,PCD}$ with session key $KS_{MAC}$. In
order to abstract from unnecessary details, the above scheme represents these MACs as cryptograms
generated using the single session key $KS$.
Finally, in steps C5 and R5, the user sends her password to the card on the secure messaging channel
established by session keys $KS_{Enc}$ and $KS_{MAC}$, e.g. via command VERIFY \<^cite>‹"R5"›, and the
card returns the success status word 0x9000 \<^cite>‹"R5"› over the same channel. In order to abstract
from unnecessary details, the above scheme represents both messages as cryptograms generated using
the single session key $KS$.
So, what if the PACE authentication key $K$ were stolen by an attacker -- henceforth called
\emph{spy} as done in \<^cite>‹"R1"›? In this case, even if the user's terminal were protected from
attacks, the spy could get hold of the user's password by replacing the user's smart card with a
fake one capable of performing a remote data transmission, so as to pull off a \emph{grandmaster
chess attack} \<^cite>‹"R2"›. In this way, the following scenario would occur, where agents $F$ and $S$
stand for the fake card and the spy.
\null
\qquad R1. $F \rightarrow U : \{s\}_K$
\qquad C2. $U \rightarrow F : PK_{Map,PCD}$
\qquad R2. $F \rightarrow U : PK_{Map,IC}$
\qquad C3. $U \rightarrow F : PK_{DH,PCD}$
\qquad R3. $F \rightarrow U : PK_{DH,IC}$
\qquad C4. $U \rightarrow F : \{PK_{DH,IC}\}_{KS}$
\qquad R4. $F \rightarrow U : \{PK_{DH,PCD}\}_{KS}$
\qquad C5. $U \rightarrow F : \{$\emph{User's password}$\}_{KS}$
\qquad C5'. $F \rightarrow S : $ \emph{User's password}
\null
Since the spy has stored key $K$ in its memory, the fake card can encrypt nonce $s$ with $K$, so
that it computes the same session keys as the user in step R3. As a result, the user receives a
correct authentication token in step R4, and then agrees to send her password to the fake card in
step C5. At this point, in order to accomplish the attack, the fake card has to do nothing but
decrypt the user's password and send it to the spy on a remote communication channel, which is what
happens in the final step C5'.
This argument demonstrates that the answer to the pending question is affirmative, namely the PACE
authentication key is indeed required to be secret, if Generic Mapping is used. Moreover, the same
conclusion can be drawn on the basis of a similar argument in case the mapping method being used is
Integrated Mapping (cf. \<^cite>‹"R4"›). Therefore, the PACE password from which the key is derived must
be secret as well.
This requirement has a significant impact on both the security and the usability of the system. In
fact, the only way to prevent the user from having to input the PACE password in addition to the
direct use one is providing such password to the user's terminal by other means. In the case of a
stand-alone application, this implies that either the PACE password itself or data allowing its
computation must be stored somewhere in the user's terminal, which gives rise to a risk of leakage.
The alternative is to have the PACE password typed in by the user, which renders longer the overall
credentials that the user is in charge of managing securely. Furthermore, any operation having to be
performed on a secure messaging channel before the user types in her password -- such as identifying
the user in case the smart card is endowed with an identity application compliant with \<^cite>‹"R3"› and
\<^cite>‹"R4"› -- would require an additional PACE password independent of the user's one. Hence, such
preliminary operations and the subsequent user's password verification would have to be performed on
distinct secure messaging channels, which would cause a deterioration in the system performance.
In case Chip Authentication Mapping is used as mapping method instead (cf. \<^cite>‹"R4"›), the resulting
protocol can be schematized as follows.
\null
\qquad R1. $C \rightarrow U : \{s\}_K$
\qquad C2. $U \rightarrow C : PK_{Map,PCD}$
\qquad R2. $C \rightarrow U : PK_{Map,IC}$
\qquad C3. $U \rightarrow C : PK_{DH,PCD}$
\qquad R3. $C \rightarrow U : PK_{DH,IC}$
\qquad C4. $U \rightarrow C : \{PK_{DH,IC}\}_{KS}$
\qquad R4. $C \rightarrow U : \{PK_{DH,PCD}$, $(SK_{IC})^{-1} \times SK_{Map,IC}$ \emph{mod n},
\qquad \qquad $PK_{IC}$, $PK_{IC}$ \emph{signature}$\}_{KS}$
\qquad C5. $U \rightarrow C : \{$\emph{User's password}$\}_{KS}$
\qquad R5. $C \rightarrow U : \{$\emph{Success code}$\}_{KS}$
\null
In the response to the last GENERAL AUTHENTICATE command (step R4), in addition to the MAC of
$PK_{DH,PCD}$ computed with session key $KS_{MAC}$, the smart card returns also the \emph{Encrypted
Chip Authentication Data} ($A_{IC}$) if Chip Authentication Mapping is used. These data result from
the encryption with session key $KS_{Enc}$ of the \emph{Chip Authentication Data} ($CA_{IC}$), which
consist of the product modulo $n$, where $n$ is the group order, of the inverse modulo $n$ of the
static private key $SK_{IC}$ with the ephemeral private key $SK_{Map,IC}$.
The user can then verify the authenticity of the chip applying the following procedure.
\begin{enumerate}
\item
Read the static public key $PK_{IC} = [SK_{IC}]G$ from a dedicated file of the smart card, named
\emph{EF.CardSecurity}.
\\Because of the read access conditions to be enforced by this file, it must be read over the secure
messaging channel established by session keys $KS_{Enc}$ and $KS_{MAC}$ (cf. \<^cite>‹"R3"›).
\item
Verify the signature contained in file EF.CardSecurity, generated over the contents of the file by a
trusted Certification Authority (CA).
\\To perform this operation, the user's terminal is supposed to be provided by secure means with the
public key corresponding to the private key used by the CA for signature generation.
\item
Decrypt the received $A_{IC}$ to recover $CA_{IC}$ and verify that $[CA_{IC}]PK_{IC} = PK_{Map,IC}$.
\\Since this happens just in case $CA_{IC} = (SK_{IC})^{-1} \times SK_{Map,IC}$ \emph{mod n}, the
success of such verification proves that the chip knows the private key $SK_{IC}$ corresponding to
the certified public key $PK_{IC}$, and thus is authentic.
\end{enumerate}
The reading of file EF.CardSecurity is performed next to the last GENERAL AUTHENTICATE command as a
separate operation, by sending one or more READ BINARY commands on the secure messaging channel
established by session keys $KS_{Enc}$ and $KS_{MAC}$ (cf. \<^cite>‹"R3"›, \<^cite>‹"R4"›, and \<^cite>‹"R5"›). The
above scheme represents this operation by inserting the public key $PK_{IC}$ and its signature into
the cryptogram returned by the last GENERAL AUTHENTICATE command, so as to abstract from unnecessary
details once again.
A successful verification of Chip Authentication Data provides the user with a proof of the fact
that the party knowing private key $SK_{Map,IC}$, and then sharing the same session keys $KS_{Enc}$
and $KS_{MAC}$, is an authentic chip. Thus, the protocol ensures that the user accepts to send her
password to an authentic chip only. As a result, the grandmaster chess attack described previously
is not applicable, so that the user's password cannot be stolen by the spy any longer. What is more,
this is true independently of the secrecy of the PACE authentication key. Therefore, this key is no
longer required to be secret, which solves all the problems ensuing from such requirement.
The purpose of this paper is indeed to construct a formal model of the above protocol in the Chip
Authentication Mapping case and prove its security, applying Paulson's Inductive Method as described
in \<^cite>‹"R1"›. In more detail, the formal development is aimed at proving that such protocol enforces
the following security properties.
\begin{itemize}
\item
Secrecy theorem ‹pr_key_secrecy›: if a user other than the spy sends her password to some
smart card (not necessarily her own one), then the spy cannot disclose the session key used to
encrypt the password. This property ensures that the protocol is successful in establishing
trustworthy secure messaging channels between users and smart cards.
\item
Secrecy theorem ‹pr_passwd_secrecy›: the spy cannot disclose the passwords of other users.
This property ensures that the protocol is successful in preserving the secrecy of users' passwords.
\item
Authenticity theorem ‹pr_user_authenticity›: if a smart card receives the password of a user
(not necessarily the cardholder), then the message must have been originally sent by that user. This
property ensures that the protocol enables users to authenticate themselves to their smart cards,
viz. provides an \emph{external authentication} service (cf. \<^cite>‹"R5"›).
\item
Authenticity theorem ‹pr_card_authenticity›: if a user sends her password to a smart card and
receives a success code as response, then the card is her own one and the response must have been
originally sent by that card. This property ensures that the protocol enables smart cards to
authenticate themselves to their cardholders, viz. provides an \emph{internal authentication}
service (cf. \<^cite>‹"R5"›).
\end{itemize}
Remarkably, none of these theorems turns out to require the secrecy of the PACE authentication key
as an assumption, so that all of them are valid independently of whether this key is secret or not.
The main technical difficulties arising from this formal development are the following ones.
\begin{itemize}
\item
Data such as private keys for Diffie-Hellman key agreement and session keys do not necessarily occur
as components of exchanged messages, viz. they may be computed by some agent without being ever sent
to any other agent. In this case, whichever protocol trace ‹evs› is given, any such key
‹x› will not be contained in either set ‹analz (spies evs)› or ‹used evs›, so
that statements such as ‹x ∈ analz (spies evs)› or ‹x ∈ used evs› will be vacuously
false. Thus, some way must be found to formalize a state of affairs where ‹x› is known by the
spy or has already been used in some protocol run.
\item
As private keys for Diffie-Hellman key agreement do not necessarily occur as components of exchanged
messages, some way must be found to record the private keys that each agent has either generated or
accepted from some other agent (possibly implicitly, in the form of the corresponding public keys)
in each protocol run.
\item
The public keys for Diffie-Hellman key agreement being used are comprised of the elements of a
cryptographic cyclic group of prime order $n$, and the private keys are the elements of the finite
field comprised of the integers from 0 to $n$ - 1 (cf. \<^cite>‹"R4"›, \<^cite>‹"R6"›). Hence, the operations
defined in these algebraic structures, as well as the generation of public keys from known private
keys, correspond to additional ways in which the spy can generate fake messages starting from known
ones. A possible option to reflect this in the formal model would be to extend the inductive
definition of set ‹synth H› with rules enabling to obtain new Diffie-Hellman private and
public keys from those contained in set ‹H›, but the result would be an overly complex
definition. Thus, an alternative formalization ought to be found.
\end{itemize}
These difficulties are solved by extending the Inductive Method, with respect to the form specified
in \<^cite>‹"R1"›, as follows.
\begin{itemize}
\item
The protocol is no longer defined as a set of event lists, but rather as a set of 4-tuples
@{term "(evs, S, A, U)"} where ‹evs› is an event list, ‹S› is the current protocol
\emph{state} -- viz. a function that maps each agent to the private keys for Diffie-Hellman key
agreement generated or accepted in each protocol run --, ‹A› is the set of the Diffie-Hellman
private keys and session keys currently known by the spy, and ‹U› is the set of the
Diffie-Hellman private keys and session keys which have already been used in some protocol run.
\\In this way, the first two difficulties are solved. Particularly, the full set of the messages
currently known by the spy can be formalized as the set ‹analz (A ∪ spies evs)›.
\item
The inductive definition of the protocol does not contain a single \emph{fake} rule any longer, but
rather one \emph{fake} rule for each protocol step. Each \emph{fake} rule is denoted by adding
letter "F" to the identifier of the corresponding protocol step, e.g. the \emph{fake} rules
associated to steps C2 and R5 are given the names \emph{FC2} and \emph{FR5}, respectively.
\\In this way, the third difficulty is solved, too. In fact, for each protocol step, the related
\emph{fake} rule extends the spy's capabilities to generate fake messages with the operations on
known Diffie-Hellman private and public keys relevant for that step, which makes an augmentation of
set ‹synth H› with such operations unnecessary.
\end{itemize}
Throughout this paper, the salient points of definitions and proofs are commented; for additional
information, cf. Isabelle documentation, particularly \<^cite>‹"R7"›, \<^cite>‹"R8"›, \<^cite>‹"R9"›, and
\<^cite>‹"R10"›.
Paulson's Inductive Method is described in \<^cite>‹"R1"›, and further information is provided in
\<^cite>‹"R7"› as a case study. The formal developments described in \<^cite>‹"R1"› and \<^cite>‹"R7"› are included
in the Isabelle distribution.
Additional information on the involved cryptography can be found in \<^cite>‹"R4"› and \<^cite>‹"R6"›.
›
subsection "Propaedeutic definitions"
text ‹
First of all, the data types of encryption/signature keys, Diffie-Hellman private keys, and
Diffie-Hellman public keys are defined. Following \<^cite>‹"R7"›, encryption/signature keys are
identified with natural numbers, whereas Diffie-Hellman private keys and public keys are represented
as rational and integer numbers in order to model the algebraic structures that they form (a field
and a group, respectively; cf. above).
\null
›
type_synonym key = nat
type_synonym pri_agrk = rat
type_synonym pub_agrk = int
text ‹
\null
Agents are comprised of an infinite quantity of users and smart cards, plus the Certification
Authority (CA) signing public key $PK_{IC}$. For each ‹n›, ‹User n› is the cardholder
of smart card ‹Card n›.
\null
›