Theory Definitions
section "The relational method and message anonymity"
theory Definitions
imports Main
begin
text ‹
\null
\emph{This paper is dedicated to my mother, my favourite chess opponent -- in addition to being many
other wonderful things!}
›
subsection "Introduction"
text ‹
As Bertrand Russell says in the last pages of \emph{A History of Western Philosophy}, a distinctive
feature of science is that "we can make successive approximations to the truth, in which each new
stage results from an improvement, not a rejection, of what has gone before". When dealing with a
formal verification method for information processing systems, such as Paulson's inductive method
for the verification of cryptographic protocols (cf. \<^cite>‹"Paulson98"›, \<^cite>‹"Paulson20"›), a
more modest goal for this iterative improvement process, yet of significant practical importance, is
to streamline the definitions and proofs needed to model such a system and verify its properties.
With this aim, specially when it comes to verifying protocols using public key cryptography, this
paper proposes an enhancement of the inductive method, named \emph{relational method} for reasons
clarified in what follows, and puts it into practice by verifying a sample protocol. This new method
is the result of some changes to the way how events, states, spy's capabilities, and the protocol
itself are formalized in the inductive method. Here below is a description of these changes, along
with a rationale for them.
➧[Events.] In the inductive method, the fundamental building blocks of cryptographic protocols are
events of the form @{text "Says A B X"}, where @{text X} is a message being exchanged, @{text A} is
the agent that sends it, and @{text B} is the agent to which it is addressed.
\\However, any exchanged message can be intercepted by the spy and forwarded to any other agent, so
its intended recipient is not relevant for the protocol \emph{security} correctness -- though of
course being relevant for the protocol \emph{functional} correctness. Moreover, a legitimate agent
may also generate messages, e.g. ephemeral private keys, that she will never exchange with any other
agent. To model such an event, a datatype constructor other than @{text Says} should be used. How to
make things simpler?
\\The solution adopted in the relational method is to model events just as ordered pairs of the form
@{text "(A, X)"}, where @{text A} is an agent and @{text X} is a message. If event @{text "(A, X)"}
stands for @{text A}'s sending of @{text X} to another agent, where @{text A} is a legitimate agent,
then this event will be accompanied by event @{text "(Spy, X)"}, representing the spy's interception
of @{text X}. If event @{text "(A, X)"} rather stands for @{text A}'s generation of private message
@{text X}, e.g. an ephemeral private key, for her own exclusive use -- and if the spy has not hacked
@{text A} so as to steal her private messages as well --, then no companion event @{text "(Spy, X)"}
will occur instead.
➧[States.] In the inductive method, the possible states of a cryptographic protocol are modeled as
event \emph{traces}, i.e. lists, and the protocol itself is formalized as a set of such traces.
Consequently, the protocol rules and security properties are expressed as formulae satisfied by any
event trace @{text evs} belonging to this set.
\\However, these formulae are such that their truth values depend only on the events contained in
@{text evs}, rather than on the actual order in which they occur -- in fact, robust protocol rules
and security properties cannot depend on the exact sequence of message exchanges in a scenario where
the spy can freely intercept and forward messages, or even generate and send her own ones. Thus, one
library function, @{const set}, and two custom recursive functions, @{text used} and @{text knows},
are needed to convert event traces into event sets and message sets, respectively.
\\In the relational method, protocol states are simply modeled as event sets, so that the occurrence
of event @{text "(A, X)"} in state @{text s} can be expressed as the transition to the augmented
state @{term "insert (A, X) s"}. Hence, states consist of relations between agents and messages. As
a result, function @{const set} need not be used any longer, whereas functions @{text used} and
@{text spied} -- the latter one being a replacement for @{text "knows Spy"} --, which take a state
@{text s} as input, are mere abbreviations for @{term "Range s"} and @{term "s `` {Spy}"}.
➧[Spy's capabilities.] In the inductive method, the spy's attack capabilities are formalized via
two inductively defined functions, @{text analz} and @{text synth}, used to construct the sets of
all the messages that the spy can learn -- @{text "analz (knows Spy evs)"} -- and send to legitimate
agents -- @{text "synth (analz (knows Spy evs))"} -- downstream of event trace @{text evs}.
\\Indeed, the introduction of these functions goes in the direction of decoupling the formalization
of the spy's capabilities from that of the protocol itself, consistently with the fact that what the
spy can do is independent of how the protocol works -- which only matters when it comes to verifying
protocol security.
\\In principle, this promises to provide a relevant benefit: these functions need to be defined, and
their properties to be proven, just once, whereupon such definitions and properties can be reused in
the formalization and verification of whatever protocol.
\\In practice, since both functions are of type @{text "msg set ⇒ msg set"}, where @{text msg} is
the datatype defining all possible message formats, this benefit only applies as long as message
formats remain unchanged. However, when it comes to verifying a protocol making use of public key
cryptography, some new message format, and consequently some new related spy's capability as well,
are likely to be required. An example of this will be provided right away by the protocol considered
in this paper.
\\In the relational method, the representation of events as agent-message pairs offers a simpler way
to model the spy's capabilities, namely as supplementary protocol rules, analogous to the inductive
method's @{text Fake} rule, augmenting a state by one or more events of the form @{text "(Spy, X)"}.
In addition to eliminating the need for functions @{text analz} and @{text synth} -- which, in light
of the above considerations, does not significantly harm reusability --, this choice also abolishes
any distinction between what the spy can learn and what she can send. In fact, a state containing
event @{text "(Spy, X)"} is interpreted as one where the spy both knows message @{text X} and may
have sent it to whatever legitimate agent. Actually, this formalizes the facts that a real-world
attacker is free to send any message she has learned to any other party, and conversely to use any
message she has generated to further augment her knowledge.
\\In the inductive method, the former fact is modeled by property @{term "H ⊆ synth H"} of function
@{text synth}, but the latter one has no formal counterpart, as in general @{term "H ⊂ synth H"}.
This limitation on the spy's capabilities is not significant as long as the protocol makes use of
static keys only, but it is if session keys or ephemeral key pairs are generated -- as happens in
key establishment protocols, even in those using symmetric cryptography alone. In any such case, a
realistic spy must also be able to learn from anything she herself has generated, such as a nonce or
an ephemeral private key -- a result achieved without effort in the relational method.
\\An additional, nontrivial problem for the inductive method is that many protocols, including key
establishment ones, require the spy to be able to generate \emph{fresh} ephemeral messages only, as
otherwise the spy could succeed in breaking the protocol by just guessing the ephemeral messages
already generated at random by some legitimate agent -- a quite unrealistic attack pattern, provided
that such messages vary in a sufficiently wide range. At first glance, this need could be addressed
by extending the inductive definition of function @{text synth} with introduction rules of the form
@{term "Nonce n ∉ H ⟹ Nonce n ∈ synth H"} or @{term "PriKey A ∉ H ⟹ PriKey A ∈ synth H"}.
However, private ephemeral messages are not in general included in @{text "analz (knows Spy evs)"},
since nonces may be encrypted with uncompromised keys when exchanged and private keys are usually
not exchanged at all, so this approach would not work. The only satisfactory alternative would be to
change the signature of function @{text synth}, e.g. by adding a second input message set @{text H'}
standing for @{text "used evs"}, or else by replacing @{text H} with event trace @{text evs} itself,
but this would render the function definition much more convoluted -- a problem easily bypassed in
the relational method.
➧[Protocol.] In the inductive method, a cryptographic protocol consists of an inductively defined
set of event traces. This enables to prove the protocol security properties by induction using the
induction rule automatically generated as a result of such an inductive definition, i.e. by means of
\emph{rule induction}. Actually, this feature is exactly what gives the method its very name. Hence,
a consistent way to name a protocol verification method using some other form of induction would be
to replace adjective "inductive" with another one referring to that form of induction.
\\The relational method owes its name to this consideration. In this method, the introduction rules
defining \emph{protocol rules}, i.e. the possible transitions between protocol states, are replaced
with \emph{relations} between states, henceforth named \emph{protocol relations}. That is, for any
two states @{text s} and @{text s'}, there exists a transition leading from @{text s} to @{text s'}
just in case the ordered pair @{term "(s, s')"} is contained in at least one protocol relation --
a state of affairs denoted using infix notation @{text "s ⊢ s'"}. Then, the inductively defined set
itself is replaced with the \emph{reflexive transitive closure} of the union of protocol relations.
Namely, any state @{text s} may be reached from \emph{initial state} @{text s⇩0}, viz. is a possible
protocol state, just in case pair @{term "(s⇩0, s)"} lies within this reflexive transitive closure --
a state of affairs denoted using infix notation @{text "s⇩0 ⊨ s"}. As a result, rule induction is
replaced with induction over reflexive transitive closures via rule @{thm [source] rtrancl_induct},
which is the circumstance that originates the method name.
\\These changes provide the following important benefits.
▪ Inserting and modifying the formal definition of a protocol is much more comfortable. In fact,
any change even to a single introduction rule within a monolithic inductive set definition entails a
re-evaluation of the whole definition, whereas each protocol relation will have its own stand-alone
definition, which also makes it easier to find errors. This advantage may go almost unnoticed for a
very simple protocol providing for just a few protocol rules, but gets evident in case of a complex
protocol. An example of this will be provided by the protocol considered in this paper: when looking
at the self-contained abbreviations used to define protocol relations, the reader will easily grasp
how much more convoluted an equivalent inductive set definition would have been.
▪ In addition to induction via rule @{thm [source] rtrancl_induct}, a further powerful reasoning
pattern turns out to be available. It is based on the following general rule applying to reflexive
transitive closures (indeed, a rule so general and useful that it could rightfully become part of
the standard library), later on proven and assigned the name @{text rtrancl_start}:
@{prop [display] "⟦(x, y) ∈ r⇧*; P y; ¬ P x⟧ ⟹
∃u v. (x, u) ∈ r⇧* ∧ (u, v) ∈ r ∧ (v, y) ∈ r⇧* ∧ ¬ P u ∧ P v"}
In natural language, this rule states that for any chain of elements linked by a relation, if some
predicate is false for the first element of the chain and true for the last one, there must exist a
link in the chain where the predicate becomes true.
\\This rule can be used to prove propositions of the form @{text "⟦s ⊨ s'; P s'[; Q]⟧ ⟹ R s'"} for
any state @{text s} and predicate @{text P} such that @{term "¬ P s"}, with an optional additional
assumption @{text Q}, without resorting to induction. Notably, \emph{regularity lemmas} have exactly
this form, where @{term "s = s⇩0"}, @{term "P = (λs. X ∈ parts (used s))"} for some term @{text X} of
type @{text msg}, and @{text Q}, if present, puts some constraint on @{text X} or its components.
\\Such a proof consists of two steps. First, lemma @{text "⟦s ⊢ s'; P s'; ¬ P s[; Q]⟧ ⟹ R s'"} is
proven by simplification, using the definitions of protocol relations. Then, the target proposition
is proven by applying rule @{text rtrancl_start} as a destruction rule (cf. \<^cite>‹"Paulson20"›) and
proving @{term "P s'"} by assumption, @{term "¬ P s"} by simplification, and the residual subgoal
by means of the previous lemma.
In addition to the relational method, this paper is aimed at introducing still another enhancement:
besides message confidentiality and authenticity, it takes into consideration a further important
security property, \emph{message anonymity}. Being legitimate agents identified via natural numbers,
the fact that in state @{text s} the spy ignores that message @{text X⇩n} is associated with agent
@{text n}, viz. @{text X⇩n}'s property of being \emph{anonymous} in state @{text s}, can be expressed
as @{text "⟨n, X⇩n⟩ ∉ spied s"}, where notation @{text "⟨n, X⇩n⟩"} refers to a new constructor added to
datatype @{text msg} precisely for this purpose.
A basic constraint upon any protocol relation augmenting the spy's knowledge with @{text "⟨n, X⟩"}
is that the spy must know message @{text X} in the current state, as it is impossible to identify
the agent associated with an unknown message. There is also an additional, more subtle constraint.
Any such protocol relation either augments a state in which the spy knows @{text "⟨n, C X⇩1 … X⇩m⟩"},
i.e. containing event @{text "(Spy, ⟨n, C X⇩1 … X⇩m⟩)"}, with event @{text "(Spy, ⟨n, X⇩i⟩)"}, where
$1 \leq i \leq m$ and @{text C} is some constructor of datatype @{text msg}, or conversely augments
a state containing event @{text "(Spy, ⟨n, X⇩i⟩)"} with @{text "(Spy, ⟨n, C X⇩1 … X⇩m⟩)"}. However, the
latter spy's inference is justified only if the compound message @{text "C X⇩1 … X⇩m"} is part of a
message generated or accepted by some legitimate agent according to the protocol rules. Otherwise,
that is, if @{text "C X⇩1 … X⇩m"} were just a message generated at random by the spy, her inference
would be as sound as those of most politicians and all advertisements: even if the conclusion were
true, it would be so by pure chance.
This problem can be solved as follows.
▪ A further constructor @{text Log}, taking a message as input, is added to datatype @{text msg},
and every protocol relation modeling the generation or acceptance of a message @{text X} by some
legitimate agent must augment the current state with event @{term "(Spy, Log X)"}.
\\In this way, the set of all the messages that have been generated or accepted by some legitimate
agent in state @{text s} matches @{term "Log -` spied s"}.
▪ A function @{text crypts} is defined inductively. It takes a message set @{text H} as input, and
returns the least message set @{text H'} such that @{term "H ⊆ H'"} and for any (even empty) list
of keys @{text KS}, if the encryption of @{text "⦃X, Y⦄"}, @{text "⦃Y, X⦄"}, or @{text "Hash X"}
with @{text KS} is contained in @{text H'}, then the encryption of @{text X} with @{text KS} is
contained in @{text H'} as well.
\\In this way, the set of all the messages that are part of messages exchanged by legitimate agents,
viz. that may be mapped to agents, in state @{text s} matches @{term "crypts (Log -` spied s)"}.
▪ Another function @{text key_sets} is defined, too. It takes two inputs, a message @{text X} and
a message set @{text H}, and returns the set of the sets of @{text KS}' inverse keys for any list of
keys @{text KS} such that the encryption of @{text X} with @{text KS} is included in @{text H}.
\\In this way, the fact that in state @{text s} the spy can map a compound message @{text X} to some
agent, provided that she knows all the keys in set @{text U}, can be expressed through conditions
@{term "U ∈ key_sets X (crypts (Log -` spied s))"} and @{term "U ⊆ spied s"}.
\\The choice to define @{text key_sets} so as to collect the inverse keys of encryption keys, viz.
decryption ones, depends on the fact that the sample protocol verified in this paper uses symmetric
keys alone -- which match their own inverse keys -- for encryption, whereas asymmetric key pairs are
used in cryptograms only for signature generation -- so that the inverse keys are public ones. In
case of a protocol (also) using public keys for encryption, encryption keys themselves should (also)
be collected, since the corresponding decryption keys, i.e. private keys, would be unknown to the
spy by default. This would formalize the fact that encrypted messages can be mapped to agents not
only by decrypting them, but also by recomputing the cryptograms (provided that the plaintexts are
known) and checking whether they match the exchanged ones.
›
subsection "A sample protocol"
text ‹
As previously mentioned, this paper tries the relational method, including message anonymity, by
applying it to the verification of a sample authentication protocol in which Password Authenticated
Connection Establishment (PACE) with Chip Authentication Mapping (cf. \<^cite>‹"ICAO15"›) is first
used by an \emph{owner} to establish a secure channel with her own \emph{asset} and authenticate it,
and then the owner sends a password (other than the PACE one) to the asset over that channel so as
to authenticate herself. This enables to achieve a reliable mutual authentication even if the PACE
key is shared by multiple owners or is weak, as happens in electronic passports. Although the PACE
mechanism is specified for use in electronic documents, nothing prevents it in principle from being
used in other kinds of smart cards or even outside of the smart card world, which is the reason why
this paper uses the generic names \emph{asset} and \emph{owner} for the card and the cardholder,
respectively.
In more detail, this protocol provides for the following steps. In this list, messages are specified
using the same syntax that will be adopted in the formal text (for further information about PACE
with Chip Authentication Mapping, cf. \<^cite>‹"ICAO15"›).
▸ \emph{Asset n} $\rightarrow$ \emph{Owner n}:
\\\hspace*{1em}@{text "Crypt (Auth_ShaKey n) (PriKey S)"}
▸ \emph{Owner n} $\rightarrow$ \emph{Asset n}:
\\\hspace*{1em}@{text "⦃Num 1, PubKey A⦄"}
▸ \emph{Asset n} $\rightarrow$ \emph{Owner n}:
\\\hspace*{1em}@{text "⦃Num 2, PubKey B⦄"}
▸ \emph{Owner n} $\rightarrow$ \emph{Asset n}:
\\\hspace*{1em}@{text "⦃Num 3, PubKey C⦄"}
▸ \emph{Asset n} $\rightarrow$ \emph{Owner n}:
\\\hspace*{1em}@{text "⦃Num 4, PubKey D⦄"}
▸ \emph{Owner n} $\rightarrow$ \emph{Asset n}:
\\\hspace*{1em}@{text "Crypt (SesK SK) (PubKey D)"}
▸ \emph{Asset n} $\rightarrow$ \emph{Owner n}:
\\\hspace*{1em}@{text "⦃Crypt (SesK SK) (PubKey C),"}
\\\hspace*{1.5em}@{text "Crypt (SesK SK) (Auth_PriK n ⊗ B),"}
\\\hspace*{1.5em}@{text "Crypt (SesK SK) (Crypt SigK"}
\\\hspace*{2em}@{text "⦃Hash (Agent n), Hash (Auth_PubKey n)⦄)⦄"}
▸ \emph{Owner n} $\rightarrow$ \emph{Asset n}:
\\\hspace*{1em}@{text "Crypt (SesK SK) (Pwd n)"}
▸ \emph{Asset n} $\rightarrow$ \emph{Owner n}:
\\\hspace*{1em}@{text "Crypt (SesK SK) (Num 0)"}
Legitimate agents consist of an infinite population of assets and owners. For each natural number
@{text n}, @{text "Owner n"} is an owner and @{text "Asset n"} is her own asset, and these agents
are assigned the following authentication data.
▪ @{text "Key (Auth_ShaKey n)"}: static symmetric PACE key shared by both agents.
▪ @{text "Auth_PriKey n"}, @{text "Auth_PubKey n"}: static private and public keys stored on
@{text "Asset n"} and used for @{text "Asset n"}'s authentication via Chip Authentication Mapping.
▪ @{text "Pwd n"}: unique password (other than the PACE one) shared by both agents and used for
@{text "Owner n"}'s authentication.
Function @{text Pwd} is defined as a constructor of datatype @{text msg} and then is injective,
which formalizes the assumption that each asset-owner pair has a distinct password, whereas no such
constraint is put on functions @{text Auth_ShaKey}, @{text Auth_PriKey}, and @{text Auth_PubKey},
which allows multiple asset-owner pairs to be assigned the same keys. On the other hand, function
@{text Auth_PriKey} is constrained to be such that the complement of its range is infinite. As each
protocol run requires the generation of fresh ephemeral private keys, this constraint ensures that
an unbounded number of protocol runs can be carried out. All assumptions are formalized by applying
the definitional approach, viz. without introducing any axiom, and so is this constraint, expressed
by defining function @{text Auth_PriKey} using the indefinite description operator @{text SOME}.
The protocol starts with @{text "Asset n"} sending an ephemeral private key encrypted with the PACE
key to @{text "Owner n"}. Actually, if @{text "Asset n"} is a smart card, the protocol should rather
start with @{text "Owner n"} sending a plain request for such encrypted nonce, but this preliminary
step is omitted here as it is irrelevant for protocol security. After that, @{text "Owner n"} and
@{text "Asset n"} generate two ephemeral key pairs each and send the respective public keys to the
other party.
Then, both parties agree on the same session key by deriving it from the ephemeral keys generated
previously (actually, two distinct session keys would be derived, one for encryption and the other
one for MAC computation, but such a level of detail is unnecessary for protocol verification). The
session key is modeled as @{text "Key (SesK SK)"}, where @{text SesK} is an apposite constructor
added to datatype @{text key} and @{term "SK = (Some S, {A, B}, {C, D})"}. The adoption of type
@{typ "nat option"} for the first component enables to represent as @{term "(None, {A, B}, {C, D})"}
the wrong session key derived from @{text "Owner n"} if @{text "PriKey S"} was encrypted using a key
other than @{text "Key (Auth_ShaKey n)"} -- which reflects the fact that the protocol goes on even
without the two parties sharing the same session key. The use of type @{typ "nat set"} for the other
two components enables the spy to compute @{text "Key (SesK SK)"} if she knows \emph{either} private
key and the other public key referenced by each set, as long as she also knows @{text "PriKey S"} --
which reflects the fact that given two key pairs, Diffie-Hellman key agreement generates the same
shared secret independently of which of the respective private keys is used for computation.
This session key is used by both parties to compute their authentication tokens. Both encrypt the
other party's second ephemeral public key, but @{text "Asset n"} appends two further fields: the
Encrypted Chip Authentication Data, as provided for by Chip Authentication Mapping, and an encrypted
signature of the hash values of @{text "Agent n"} and @{text "Auth_PubKey n"}. Infix notation
@{text "Auth_PriK n ⊗ B"} refers to a constructor of datatype @{text msg} standing for plain Chip
Authentication Data, and @{text Agent} is another such constructor standing for agent identification
data. @{text "Owner n"} is expected to validate this signature by also checking @{text "Agent n"}'s
hash value against reference identification data known by other means -- otherwise, the spy would
not be forced to know @{text "Auth_PriKey n"} to masquerade as @{text "Asset n"}, since she could do
that by just knowing @{text "Auth_PriKey m"} for some other @{text m}, even if @{term "Auth_PriKey m
≠ Auth_PriKey n"}. If @{text "Asset n"} is an electronic passport, the owner, i.e. the inspection
system, could get cardholder's identification data by reading her personal data on the booklet, and
such a signature could be retrieved from the chip (actually through a distinct message, but this is
irrelevant for protocol security as long as the password is sent after the signature's validation)
by reading the Document Security Object -- provided that @{text "Auth_PubKey n"} is included within
Data Group 14.
The protocol ends with @{text "Owner n"} sending her password, encrypted with the session key, to
@{text "Asset n"}, who validates it and replies with an encrypted acknowledgment.
Here below are some concluding remarks about the way how this sample protocol is formalized.
▪ A single signature private key, unknown to the spy, is assumed to be used for all legitimate
agents. Similarly, the spy might have hacked some legitimate agent so as to steal her ephemeral
private keys and session keys as soon as they are generated, but here all legitimate agents are
assumed to be out of the spy's reach in this respect. Of course, this is just the choice of one of
multiple possible modeling scenarios, and nothing prevents these assumptions from being dropped.
▪ In the real world, a legitimate agent would use any one of her ephemeral private keys just once,
after which the key would be destroyed. On the contrary, no such constraint is enforced here, since
it turns out to be unnecessary for protocol verification. There is a single exception, required for
the proof of a unicity lemma: after @{text "Asset n"} has used @{text "PriKey B"} to compute her
authentication token, she must discard @{text "PriKey B"} so as not to use this key any longer. The
way how this requirement is expressed emphasizes once more the flexibility of the modeling of events
in the relational method: @{text "Asset n"} may use @{text "PriKey B"} in this computation only if
event @{text "(Asset n, PubKey B)"} is not yet contained in the current state @{text s}, and then
@{text s} is augmented with that event. Namely, events can also be used to model garbage collection!
▪ The sets of the legitimate agents whose authentication data have been identified in advance (or
equivalently, by means other than attacking the protocol, e.g. by social engineering) by the spy are
defined consistently with the constraint that known data alone can be mapped to agents, as well as
with the definition of initial state @{text s⇩0}. For instance, the set @{text bad_id_prikey} of the
agents whose Chip Authentication private keys have been identified is defined as a subset of the set
@{text bad_prikey} of the agents whose Chip Authentication private keys have been stolen. Moreover,
all the signatures included in assets' authentication tokens are assumed to be already known to the
spy in state @{text s⇩0}, so that @{text bad_id_prikey} includes also any agent whose identification
data or Chip Authentication public key have been identified in advance.
▪ The protocol rules augmenting the spy's knowledge with some message of the form @{text "⟨n, X⟩"}
generally require the spy to already know some other message of the same form. There is just one
exception: the spy can infer @{text "⟨n, Agent n⟩"} from @{text "Agent n"}. This expresses the fact
that the detection of identification data within a message generated or accepted by some legitimate
agent is in itself sufficient to map any known component of that message to the identified agent,
regardless of whether any data were already mapped to that agent in advance.
▪ As opposed to what happens for constructors @{text "(⊗)"} and @{text "MPair"}, there do not
exist two protocol rules enabling the spy to infer @{text "⟨n, Crypt K X⟩"} from @{text "⟨n, X⟩"} or
@{text "⟨n, Key K⟩"} and vice versa. A single protocol rule is rather defined, which enables the spy
to infer @{text "⟨n, X⟩"} from @{text "⟨n, Key K⟩"} or vice versa, provided that @{text "Crypt K X"}
has been exchanged by some legitimate agent. In fact, the protocol provides for just one compound
message made up of cryptograms, i.e. the asset's authentication token, and all these cryptograms are
generated using the same encryption key @{text "Key (SesK SK)"}. Thus, if two such cryptograms have
plaintexts @{text X⇩1}, @{text X⇩2} and the spy knows @{text "⟨n, X⇩1⟩"}, she can infer @{text "⟨n, X⇩2⟩"}
by inferring @{text "⟨n, Key (SesK SK)⟩"}, viz. she need not know @{text "⟨n, Crypt (SesK SK) X⇩1⟩"}
to do that.
The formal content is split into the following sections.
▪ Section \ref{Definitions}, \emph{Definitions}, contains all the definitions needed to formalize
the sample protocol by means of the relational method, including message anonymity.
▪ Section \ref{Authentication}, \emph{Confidentiality and authenticity properties}, proves that
the following theorems hold under appropriate assumptions.
▸ Theorem @{text sigkey_secret}: the signature private key is secret.
▸ Theorem @{text auth_shakey_secret}: an asset-owner pair's PACE key is secret.
▸ Theorem @{text auth_prikey_secret}: an asset's Chip Authentication private key is secret.
▸ Theorem @{text owner_seskey_unique}: an owner's session key is unknown to other owners.
▸ Theorem @{text owner_seskey_secret}: an owner's session key is secret.
▸ Theorem @{text owner_num_genuine}: the encrypted acknowledgment received by an owner has been
sent by the respective asset.
▸ Theorem @{text owner_token_genuine}: the PACE authentication token received by an owner has
been generated by the respective asset, using her Chip Authentication private key and the same
ephemeral keys used to derive the session key.
▸ Theorem @{text pwd_secret}: an asset-owner pair's password is secret.
▸ Theorem @{text asset_seskey_unique}: an asset's session key is unknown to other assets, and
may be used by that asset to compute just one PACE authentication token.
▸ Theorem @{text asset_seskey_secret}: an asset's session key is secret.
▸ Theorem @{text asset_pwd_genuine}: the encrypted password received by an asset has been sent
by the respective owner.
▸ Theorem @{text asset_token_genuine}: the PACE authentication token received by an asset has
been generated by the respective owner, using the same ephemeral key used to derive the session key.
▸ Theorem @{text seskey_forward_secret}: a session key shared by an asset-owner pair is
endowed with \emph{forward secrecy}, viz. it is secret independently of the secrecy of static keys.
Particularly, these proofs confirm that the mutual authentication between an owner and her asset
is reliable even if their PACE key is compromised, unless either their Chip Authentication private
key or their password also is -- namely, the protocol succeeds in implementing a two-factor mutual
authentication --, with the forward secrecy of the generated session keys being ensured as well.
▪ Section \ref{Anonymity}, \emph{Anonymity properties}, proves that the following theorems hold
under appropriate assumptions.
▸ Theorem @{text pwd_anonymous}: an asset-owner pair's password is anonymous.
▸ Theorem @{text auth_prikey_anonymous}: an asset's Chip Authentication private key is
anonymous.
▸ Theorem @{text auth_shakey_anonymous}: an asset-owner pair's PACE key is anonymous.
▪ Section \ref{Possibility}, \emph{Possibility properties}, shows how possibility properties (cf.
\<^cite>‹"Paulson98"›) can be proven by constructing sample protocol runs, either ordinary or attack
ones. Two such properties are proven:
▸ Theorem @{text runs_unbounded}: for any possible protocol state @{text s} and any asset-owner
pair, there exists a state @{text s'} reachable from @{text s} in which a protocol run has been
completed by those agents using an ephemeral private key @{text "PriKey S"} not yet exchanged in
@{text s} -- namely, an unbounded number of protocol runs can be carried out by legitimate agents.
▸ Theorem @{text pwd_compromised}: in a scenario not satisfying the assumptions of theorem
@{text pwd_anonymous}, the spy can steal an asset-owner pair's password and even identify those
agents.
The latter is an example of a possibility property aimed at confirming that the assumptions of a
given confidentiality, authenticity, or anonymity property are necessary for it to hold.
For further information about the formal definitions and proofs contained in these sections, see
Isabelle documentation, particularly \<^cite>‹"Paulson20"›, \<^cite>‹"Nipkow20"›, \<^cite>‹"Krauss20"›,
and \<^cite>‹"Nipkow11"›.
\textbf{Important note.} This sample protocol was already considered in a former paper of mine (cf.
\<^cite>‹"Noce17"›). For any purpose, that paper should be regarded as being obsolete and superseded
by the present paper.
›
subsection "Definitions"
text ‹
\label{Definitions}
›
type_synonym agent_id = nat
type_synonym key_id = nat
type_synonym seskey_in = "key_id option × key_id set × key_id set"