PAR
ingnieur informaticien diplm EPF
de nationalit suisse et originaire de Charmey (Lac) (FR)
accepte sur proposition du jury:
Lausanne, EPFL
2007
Prof. E. Telatar, prsident du jury
Prof. U. Nestmann, Prof. T. Henzinger, directeurs de thse
Prof. S. Artmov, rapporteur
Prof. R. Ksters, rapporteur
Prof. L. Moss, rapporteur
LOGICAL CONCEPTS IN CRYPTOGRAPHY
Simon KRAMER
THSE N
O
3845 (2007)
COLE POLYTECHNIQUE FDRALE DE LAUSANNE
PRSENTE LE 4 JUILLET 2007
LA FACULT INFORMATIQUE ET COMMUNICATIONS
Laboratoire de modles et thorie de calculs
SECTION D'INFORMATIQUE
To my teachers
Abstract
Subject This thesis is about a breadthrst exploration of logical concepts
in cryptography and their linguistic abstraction and modeltheoretic combina
tion in a comprehensive logical system, called CPL (for Cryptographic Proto
col Logic). We focus on two fundamental aspects of cryptography. Namely,
the security of communication (as opposed to security of storage) and crypto
graphic protocols (as opposed to cryptographic operators). The primary logical
concepts explored are the following: the modal concepts of belief, knowledge,
norms, provability, space, and time. The distinguishing feature of CPL is that
it unies and renes a variety of existing approaches. This feature is the result
of our wholistic conception of propertybased (modal logics) and modelbased
(process algebra) formalisms.
Keywords applied formal logic, information security.
URL http://library.epfl.ch/en/theses/?nr=3845
Resume
Sujet Cette th`ese a comme sujet une exploration en largeur de concepts lo
giques en cryptographie et leur abstraction et combinaison linguistique en un
syst`eme logique syncretique, appele CPL (pour Cryptographic Protocol Logic).
Nous nous interessons `a deux aspects fondamentaux de la cryptographie. Dune
part, `a la securite de la communication (par opposition `a la securite du stockage)
de donnees, et dautre part, aux protocoles cryptographiques (par opposition aux
operateurs cryptographiques). Les concepts logiques primaires explores sont les
suivants : les concepts modaux de la croyance, de la connaissance, des normes,
de la prouvabilite, de lespace, et du temps. Le trait distinctif de CPL est duni
er et de raner une variete dapproches existantes. Ce trait est le resultat de
notre conception holistique des formalismes bases sur les proprietes (logiques
modales) et de ceux bases sur les mod`eles (alg`ebres de processus).
Motsclefs logique formelle appliquee, securite dinformation.
URL http://library.epfl.ch/en/theses/?nr=3845
Synopsis
This thesis is about a breadthrst exploration of logical concepts in cryptog
raphy and their linguistic abstraction and modeltheoretic combination in a
comprehensive logical system, called CPL (for Cryptographic Protocol Logic).
We focus on two fundamental aspects of cryptography. Namely, the security
of communication (as opposed to security of storage) and cryptographic pro
tocols (as opposed to cryptographic operators). The logical concepts explored
are the following. Primary concepts: the modal concepts of belief, knowl
edge, norms, provability, space, and time. Secondary concepts: belief with
error control, individual and propositional knowledge, condentiality norms,
truthfunctional and relevant (in particular, intuitionistic) implication, multiple
and complex truth values, and program types. The distinguishing feature of
CPL is that it unies and renes a variety of existing approaches. This feature
is the result of our wholistic conception of propertybased (modal logics) and
modelbased (process algebra) formalisms. We illustrate the expressiveness of
CPL on representative requirements engineering case studies. Further, we ex
tend (core) CPL (qualitative time) with rationalvalued time, i.e., time stamps,
timed keys, and potentially drifting local clocks, to tCPL (quantitative time).
Our extension is conservative and provides further evidence for Lamports claim
that adding real time to an untimed formalism is really simple. Furthermore,
we sketch an extension of (core) CPL with a notion of probabilistic polynomial
time (PP) computation. We illustrate the expressiveness of this extended logic
(ppCPL) on tentative formalisation case studies of fundamental and applied con
cepts. Fundamental concepts: (1) oneway function, (2) hardcore predicate, (3)
computational indistinguishability, (4) (nparty) interactive proof, and (5) (n
prover) zeroknowledge. Applied concepts: (1) security of encryption schemes,
(2) unforgeability of signature schemes, (3) attacks on encryption schemes, (4)
attacks on signature schemes, and (5) breaks of signature schemes. In the light
of logic, adding PP to a formalism for cryptographic protocols is perhaps also
simple and can be achieved with an Ockhams razor extension of an existing
core logic, namely CPL.
Moreover, we dene: (1) message meaning; (2) message information content;
(3) protocol meaning; and, based on all that, (4) protocol information content.
From the meaning of a cryptographic message, we obtain (1) an equational
denition of its contextsensitivity, and (2) a formalisation of the rst of Abadi
and Needhams principles for prudent engineering practice for cryptographic
protocols. From the meaning of a cryptographic protocol, we obtain natural
denitions of the concepts of (1) a protocol invariant, (2) protocol safety, and
(3) protocol renement. Last but not least, we show that protocol agents can
be conceived as evolving Scott information systems.
Synth`ese
Cette th`ese a comme sujet une exploration en largeur de concepts logiques en
cryptographie et leur abstraction et combinaison linguistique en un syst`eme lo
gique syncretique, appele CPL (pour Cryptographic Protocol Logic). Nous nous
interessons `a deux aspects fondamentaux de la cryptographie. Dune part, `a
la securite de la communication (par opposition `a la securite du stockage) de
donnees, et dautre part, aux protocoles cryptographiques (par opposition aux
operateurs cryptographiques). Les concepts logiques explores sont les suivants.
Concepts primaires : les concepts modaux de la croyance, de la connais
sance, des normes, de la prouvabilite, de lespace, et du temps. Concepts se
condaires : la croyance avec controle derreur, la connaissance individuelle
et propositionnelle, les normes de condentialite, limplication verifonctionnelle
et pertinente (en particulier, intuitionniste), les valeurs de verite multiples et
complexes, et les types de programmes. Le trait distinctif de CPL est duni
er et de raner une variete dapproches existantes. Ce trait est le resultat de
notre conception holistique des formalismes bases sur les proprietes (logiques mo
dales) et de ceux bases sur les mod`eles (alg`ebres de processus). Nous illustrons
lexpressivite de CPL `a laide detudes de cas representatives de type require
ments engineering. Ensuite, nous etendons CPL (temporisee qualitativement)
avec du temps `a nombres rationnels, cest`adire, avec des etiquettes temporelles,
des clefs temporisees, et des horloges locales potentiellement derivantes dans le
temps, `a tCPL (temporisee quantitativement). Notre extension est conserva
trice et va dans le sens de la th`ese de Lamport qui arme quajouter du temps
reel `a un formalisme est vraiment simple. En outre, nous esquissons une exten
sion de CPL avec une notion de calcul probabiliste et polynomial. Nous illus
trons lexpressivite de cette logique etendue (ppCPL) `a laide detudes de cas
experimentales de concepts fondamentaux et appliques. Concepts fondamen
taux : (1) les fonctions `a sens unique, (2) les predicats de type hardcore, (3)
lindistinguabilite computationnelle, (4) les preuves interactives (`a n entites),
et (5) les preuves `a divulgation nulle de connaissance (`a n entites). Concepts
appliqu es : (1) la securite du et les attaques des algorithmes de chirage ; et (2)
la nonfalsiabilite, les attaques des algorithmes de creation, et les falsications
des signatures electroniques.
`
A la lumi`ere de la logique, le rajout dune notion
de calcul probabiliste et polynomial `a un formalisme pour protocoles cryptogra
phiques est peutetre aussi simple et peut etre realise avec une extension selon
le principe du rasoir dOckham dune logique existante, `a savoir CPL.
De plus, nous denissons : le sens dun message ; le contenu en information
dun tel message ; le sens dun protocole ; et sur base de tout cela, le contenu en
information dun tel protocole.
`
A partir du sens dun message cryptographique,
nous obtenons (1) une denition equationnelle de sa dependance du contexte, et
(2) une formalisation du premier des principes dingenierie prudente pour pro
tocoles cryptographiques dAbadi et Needham.
`
A partir dun protocole crypto
graphique, nous obtenons des denitions naturelles des concepts (1) dinvariant
de protocole, (2) de s urete de protocole, et (3) de ranement de protocole. En
n, nous montrons que les agents de protocole peuvent etre concus comme des
syst`emes dinformation de Scott.
Contents
Contents 13
List of Tables 17
List of Slogans 19
I Prologue 21
1 Preface 23
2 Introduction 27
2.1 Motivation: problem . . . . . . . . . . . . . . . . . . . . . . . . . 27
2.1.1 Symptom . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.1.2 Cause . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.1.3 Remedy . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.2 Goal: solution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.2.1 Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.2.2 Extent . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.2.2.1 Scope . . . . . . . . . . . . . . . . . . . . . . . . 29
2.2.2.2 Grain . . . . . . . . . . . . . . . . . . . . . . . . 30
2.3 Methodology . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
2.3.1 Approach . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
2.3.2 Formalism . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
2.3.2.1 Unifying modal logics for cryptography . . . . . 31
2.3.2.2 Integrating modal logic and program semantics . 31
2.4 Prerequisites . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
2.4.1 Logic and program semantics . . . . . . . . . . . . . . . . 32
2.4.2 Cryptography . . . . . . . . . . . . . . . . . . . . . . . . . 32
2.4.2.1 Prehistory . . . . . . . . . . . . . . . . . . . . . 32
2.4.2.2 Classical cryptography . . . . . . . . . . . . . . 33
2.4.2.3 Modern cryptography . . . . . . . . . . . . . . . 33
2.5 Preview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
2.5.1 Cryptographic states of aairs . . . . . . . . . . . . . . . 34
2.5.2 Cryptographic concepts . . . . . . . . . . . . . . . . . . . 34
2.5.3 Research highlight . . . . . . . . . . . . . . . . . . . . . . 35
2.5.4 Peerreview . . . . . . . . . . . . . . . . . . . . . . . . . . 35
13
14 CONTENTS
II Cryptographic Protocol Logic 37
3 DolevYao cryptography 39
3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
3.1.1 Historical context . . . . . . . . . . . . . . . . . . . . . . . 39
3.1.2 Topical context . . . . . . . . . . . . . . . . . . . . . . . . 40
3.1.2.1 Requirements engineeringideally . . . . . . . . 40
3.1.2.2 Requirements engineeringreally . . . . . . . . 41
3.1.2.3 Requirements engineeringCPL . . . . . . . . . 43
3.2 Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
3.2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
3.2.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
3.2.3 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
3.2.3.1 Expressiveness . . . . . . . . . . . . . . . . . . . 55
3.2.3.2 Relevant implication . . . . . . . . . . . . . . . . 55
3.2.3.3 Conicting obligations . . . . . . . . . . . . . . . 57
3.2.3.4 Logical omniscience . . . . . . . . . . . . . . . . 57
3.2.3.5 Other connections . . . . . . . . . . . . . . . . . 58
3.3 Application: formalisation case studies . . . . . . . . . . . . . . . 59
3.3.1 Trustrelated aairs . . . . . . . . . . . . . . . . . . . . . 59
3.3.2 Condentialityrelated aairs . . . . . . . . . . . . . . . . 59
3.3.3 Authenticationrelated aairs . . . . . . . . . . . . . . . . 60
3.3.4 Commitmentrelated aairs . . . . . . . . . . . . . . . . . 62
3.3.5 Compositionalityrelated aairs . . . . . . . . . . . . . . . 64
3.3.5.1 A popular attack scenario . . . . . . . . . . . . . 65
3.4 tCPL: an extension of CPL with real time . . . . . . . . . . . . . 68
3.4.1 Historical and topical context . . . . . . . . . . . . . . . . 69
3.4.2 Extension . . . . . . . . . . . . . . . . . . . . . . . . . . . 70
3.4.3 Expressiveness . . . . . . . . . . . . . . . . . . . . . . . . 72
3.4.4 Application: a timed attack scenario . . . . . . . . . . . . 73
4 Calculus of Cryptographic Communication 77
4.1 Core calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
4.1.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
4.1.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
4.1.3 Observational equivalence . . . . . . . . . . . . . . . . . . 82
4.1.4 Application: an algebraic attack scenario . . . . . . . . . 82
4.2 tC
3
: an extension of C
3
with real time . . . . . . . . . . . . . . . 83
4.2.1 Extension . . . . . . . . . . . . . . . . . . . . . . . . . . . 85
4.2.2 Application: a timed, algebraic attack scenario . . . . . . 86
4.3 Denotational semantics . . . . . . . . . . . . . . . . . . . . . . . . 87
4.3.1 Message meaning . . . . . . . . . . . . . . . . . . . . . . . 88
4.3.2 Protocol meaning . . . . . . . . . . . . . . . . . . . . . . . 90
5 Towards PPcryptography 93
5.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93
5.1.1 Symbolic logic . . . . . . . . . . . . . . . . . . . . . . . . 94
5.1.2 Probability theory . . . . . . . . . . . . . . . . . . . . . . 95
5.1.3 Probabilistic polynomialtime cryptography . . . . . . . . 95
5.2 ppCPL: an extension of CPL with PP . . . . . . . . . . . . . . . 96
CONTENTS 15
5.2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96
5.2.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
5.3 Application: formalisation case studies . . . . . . . . . . . . . . . 99
5.3.1 Fundamental concepts . . . . . . . . . . . . . . . . . . . . 99
5.3.2 Applied concepts . . . . . . . . . . . . . . . . . . . . . . . 103
III Epilogue 109
6 Conclusion 111
6.1 Review of achievements . . . . . . . . . . . . . . . . . . . . . . . 111
6.2 Future work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114
A Proofs 115
B Specication Library (Glossary) 123
C Bibliography 125
D Index 134
Curriculum Vit 145
16 CONTENTS
List of Tables
3.1 Message language . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
3.2 Predicate language . . . . . . . . . . . . . . . . . . . . . . . . . . 47
3.3 Derivation of individual knowledge . . . . . . . . . . . . . . . . . 50
3.4 Truth denotation . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
3.5 Parsing cryptographic messages . . . . . . . . . . . . . . . . . . . 52
3.6 Deriving a plaintext . . . . . . . . . . . . . . . . . . . . . . . . . 56
3.7 Protocol narration for core NSPuK . . . . . . . . . . . . . . . . . 65
3.8 Protocol template for core NSPuK . . . . . . . . . . . . . . . . . 66
3.9 Prehistory for core NSPuK . . . . . . . . . . . . . . . . . . . . . 67
3.10 Attack narration for NSPuK . . . . . . . . . . . . . . . . . . . . . 67
3.11 Denability of durations . . . . . . . . . . . . . . . . . . . . . . . 73
3.12 Protocol narration for WMF . . . . . . . . . . . . . . . . . . . . 73
3.13 Protocol template for WMF . . . . . . . . . . . . . . . . . . . . . 74
3.14 Prehistory for WMF . . . . . . . . . . . . . . . . . . . . . . . . . 75
3.15 Attack narration for WMF . . . . . . . . . . . . . . . . . . . . . 75
4.1 C
3
processes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
4.2 Pattern matching . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
4.3 Lookup predicate . . . . . . . . . . . . . . . . . . . . . . . . . . . 80
4.4 Process and thread execution . . . . . . . . . . . . . . . . . . . . 81
4.5 Attack trace for NSPuK . . . . . . . . . . . . . . . . . . . . . . . 83
4.6 Timed lookup predicate . . . . . . . . . . . . . . . . . . . . . . . 85
4.7 History template for WMF . . . . . . . . . . . . . . . . . . . . . 87
5.1 Syntactic representation of individual concepts . . . . . . . . . . 94
5.2 Probabilistic process reduction . . . . . . . . . . . . . . . . . . . 95
5.3 Probabilistic message denotation . . . . . . . . . . . . . . . . . . 96
5.4 PP derivation of individual knowledge . . . . . . . . . . . . . . . 98
5.5 Expressing properties of protocols, operators, and messages . . . 99
17
18 LIST OF TABLES
List of Slogans
1
Logic is . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
Proof of concept is . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
The subjectmatter of applied formal logic is . . . . . . . . . . . . . . . 24
The purpose of logic is . . . The purpose of machines is . . . . . . . . . . 27
Proving with Turing machines is . . . . . . . . . . . . . . . . . . . . . . 29
The subjectmatter of programming languages is . . . . . . . . . . . . . 31
Cryptography is . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
The purpose of a cryptographic protocol is . . . . . . . . . . . . . . . . 39
In theory, . . . In practice, . . . . . . . . . . . . . . . . . . . . . . . . . . 40
Cryptographic protocol correctness: . . . . . . . . . . . . . . . . . . . . 40
Belief can be used to show . . . . . . . . . . . . . . . . . . . . . . . . . 43
The formal method for any science is . . . . . . . . . . . . . . . . . . . . 43
Logic for engineering necessarily is . . . . . . . . . . . . . . . . . . . . . 44
Trustworthiness = . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
Meaning, when communicable, is . . . Semantics is . . . . . . . . . . . . . 49
Authenticity is . . . Secrecy is . . . . . . . . . . . . . . . . . . . . . . . . 62
Stating the possibly weakest exocondition . . . . . . . . . . . . . . . . 65
Debatable requirements entail . . . . . . . . . . . . . . . . . . . . . . . . 65
Actions are . . . Events are . . . . . . . . . . . . . . . . . . . . . . . . . . 80
In cryptography, individual knowledge is the key to . . . . . . . . . . . 90
Predicates speak of . . . Propositions talk about . . . . . . . . . . . . . . 99
Proves should be written like . . . . . . . . . . . . . . . . . . . . . . . . 122
1
meant
to connote (not to denote) scientic content
to denote (not to connote) scientic intent
19
20 LIST OF TABLES
Part I
Prologue
21
Chapter 1
Preface
Studies in the foundations of mathematics divide symmetrically
into two sorts, conceptual and doctrinal. The conceptual studies
are concerned with meaning, the doctrinal with truth. The concep
tual studies are concerned with clarifying concepts by dening them,
some in terms of others. The doctrinal studies are concerned with
establishing laws by proving them, some on the basis of others. Ide
ally the obscurer concepts would be dened in terms of the clearer
ones so as to maximize clarity, and the less obvious laws would be
proved from the more obvious ones so as to maximize certainty. Ide
ally the denitions would generate all the concepts from clear and
distinct ideas, and the proofs would generate all the theorems from
selfevident truths. The two ideals are linked.
1
Willard V. Quine
(cf. [Gib04, Page 259])
This thesis is the inception of a conceptual study in the logical foundations
of cryptography. Our perspective is metatheoretic; our concern applied; and
our approach formal, and based on the following conviction
2
, formulated as a
slogan:
Slogan 1 Logic is the interdisciplinary and unifying scientic discipline par
excellence.
Our perspective is metatheoretic because such a perspective is conducive to
the perception of pertinent connections between disciplines that the members
of their respective communities typically claim to perceive as safely unconnected.
Our concern is applied for the sake of practical relevance. And our approach is
formal for the sake of scientic rigour.
Our conceptual study is concerned with the clarication of the meaning
of cryptographic intuitions by reducing them to logical concepts and dening
them in terms of logical constructions. According to Quine: It is valuable to
1
the link is the duality between concept and doctrine, between knowing what a sentence
means and knowing whether it is true. [Gib04, Page 273]
2
The communitycentered reader uprooted by this individual declaration of faith can be
reassured that our conviction is socially wellfounded in another community, namely the
one of mathematical foundationalists (though not necessarily fundamentalists).
23
24 CHAPTER 1. PREFACE
show the reducibility of any principle to another through denition of erstwhile
primitives, for every such achievement reduces the number of our presupposi
tions and simplies and integrates the structure of theories. [Gib04, Page 30].
Our enterprise is clearly in the spirit of mathematical foundationalism and thus
consistent with the maxim of the rst quotation to dene the obscurer (i.e.,
cryptographic) concepts in terms of the clearer (i.e., logical) ones so as to max
imise clarity. Our ambition is concomitant with the maxim of the rst quotation
that ideally, the (logical) denitions would generate all the concepts (those rel
evant to cryptographic protocols) from clear and distinct ideas. Our study is
conceptual because (and that is the link in the rst quotation):
Slogan 2 Proof of concept
3
is necessary for the concept of proof.
And the concept of proof is wellunderstood, as opposed to cryptographic con
cepts, which according to Goldreich are not: To summarize, the basic concepts
of cryptography are indeed very natural, but they are not selfevident nor well
understood. Hence, we do not yet understand these concepts well enough to be
able to discuss them correctly without using precise denitions and rigorously
justifying every statement made. [Gol01]. This thesis is our humble contribu
tion to the discussion in the form of a logical conceptualisation of the security
of communication at the level of cryptographic protocols and its crystallisa
tion into a comprehensive logical theory. Logic is about correct (and hopefully,
intercommunal) discourse and conversation (and hopefully, dialogue). Our at
titude is curiosity in and service to cryptography. Our hope is to awake
awareness of the relevance of formal logic applied to cryptography.
Slogan 3 The subjectmatter of applied formal logic is pragmatics of cognition.
Its purpose is empowerment of the human mind in the formulation, validation,
and communication of statements.
Audience
Our target audience is the community of logically inclined engineers, computer
scientists, cryptographers, logicians, and philosophers. Our (meta)community
is the one of all those who believe that thinking in terms of closed scientic
communities is imprisonment of the mind and ultimately antiscientic. The
concept of a closed scientic community is a strong logical paradox, i.e., non
sense.
Acknowledgements
I would like to thank: Johannes Borgstrom for his contribution to our joint
work, and for teaching me through that work what I know about process al
gebra; Mika Cohen for our stimulating discussions about crypto logics and his
constructive criticism of my work; Marc De Falco for his exploratory (now super
seded) contribution to my work at an experimental stage; Christoph Frei for his
elderbrotherly advice on the practice of being a Ph.D. student; Henrik Imhof
for his abiding Upanishads on mathematical logic; Michael Mendler for our early
3
or at least, evidence for concept
25
discussions about crypto logics; and Jacques Zahnd for his nonpareil teachings
of elementary logic [Zah03], which have gained the status of true urelements in
my education.
Last but not least, I would like to thank the members of my thesis committee
for their appreciation of my thesis, and my supervisors for their logistic support
during my thesis. I am especially grateful to Johan van Benthem and Lawrence
Moss (this thesis is a tribute to his manifesto for applied logic [Mos05]) for their
valuable comments and encouraging opinion about my work.
The research documented in this thesis has been funded by the Swiss Na
tional Science Foundation.
Ecole Polytechnique Federale de Lausanne Simon Kramer
4
Lausanne, Switzerland July 2007
~ ~ ~ ~
Trancher
S pour K
Unifier
~ ~~~
Trancher
S pour K
Unifier
~~~ ~
Trancher
S pour K
Unifier
~~~~
Trancher
S pour K
Unifier
~~ ~~
Trancher
S pour K
Unifier
~ ~~~
Trancher
S pour K
Unifier
4
simon.kramer@a3.epfl.ch
26 CHAPTER 1. PREFACE
Chapter 2
Introduction
Mechanisms come and go, are improved upon, rarely become pop
ular, and are never really basic and compelling enough to bring satis
faction. Theorems are ignored or strengthened, forgotten, and hardly
anyone reads their proofs or cares. What lasts, at least for a little
while, are the notions of the eld and that which is associated to
making those notions precise: denitions.
Phillip Rogaway
(cf. [Rog04])
This thesis proposes denitions (and a few theorems with proofs) for crypto
graphic notions that are heretical w.r.t. the established canon of modern cryp
tography. Our denitions are heretical in the sense that we choose to formulate
them in terms of logical constructions, rather than in terms of the canonical Tur
ing machines. The benediction of our heresy is to provide linguistic abstractions
of cryptographic concepts. The benet of linguistic abstractions is to produce
diction (idioms) for intuitions. Additionally, our linguistic abstractions have
the benet of being declarative abstractions (i.e., they focus on the what) of
operational (focusing on the how) aspects.
1
The benet of logic is to enable
humans to think and communicate with each other as humans rather than as
machines. Humans, perhaps with the exception of computer geeks and nerds,
think and communicate in the language of the mind, i.e., logic, rather than in
the (programming) language of (Turing) machines.
Slogan 4 The purpose of logic is understanding. The purpose of machines is
control.
2
2.1 Motivation: problem
The motivation for our heresy is a certain dissatisfaction with the canonical
denitions of modern cryptography. Our diagnosis of the purported problem is
the following.
1
our intention is in the spirit of descriptive rather than computational complexity theory
2
no negative connotation intended
27
28 CHAPTER 2. INTRODUCTION
2.1.1 Symptom
Traditional denitions of modern cryptographic concepts yield proofs (that is
the link in the rst quotation of Chapter 1) that are obscure, in the sense
that they are mentally intractable. Even cryptographers themselves have come
to argue for taming the complexity of security proofs that might otherwise
become so messy, complicated, and subtle as to be nearly impossible to verify.
[Sho04]. In other words, the decision problem consisting in the question of
whether or not a traditional security proof is correct typically has no succinct
certicate. In particular, the candidate proof itself is then no such certicate.
This is an empirical fact and a dissatisfactory state of aairs. It means that
traditional security proofs, which aim at establishing certain (computational)
intractability results, are themselves (mentally) intractable. In other words,
(modern) cryptography disproves itself with its own (traditional) proofs. An
empirical corollary is the dominance of proofs (by example) of the presence of
attacks on cryptographic constructions and on proofs thereof, over proofs (by
argument) of the absence of such attacks.
2.1.2 Cause
The cause of this selfinicted obscurity of modern cryptography is deeprooted
in its denitions. Traditional security proofs are mentally intractable because
they rely on denitions that aim at capturing extremely highlevel declarative
concerns (e.g., trust, condentiality, identity, commitment) with extremely low
level operational linguistic abstractions (i.e., Turing machine instructions). The
generated gap between the what and the how is abysmal. A fortiori, formal
proofs relying on traditional denitions are mentally intractable because the
literal programming of Turing machines, on which such proofs would depend,
is. As a matter of fact, writing formal proofs is unpopular. This would involve
unpopular formal logic. An empirical corollary is the dominance of indirect
property statements about cryptographic constructions. That is, the statement
of properties in terms of how they are supposed to be established, rather than
just the statement of what they are supposed to establish. As a matter of fact,
direct property statements are unpopular. Again, this would involve unpopular
formal logic.
2.1.3 Remedy
A deeprooted problem (denitions) must be administered a radical remedy:
redenition at least at rst sight and stage. It is preconceived usage that
denes the concepts of modern cryptography in terms of Turing machines. This
need not be so. In Quines words: Preconceived usage may lead us to stack the
cards, but does not enter the rules of the game. [Gib04, Page 22]. And: There
are indenitely many ways of framing denitions [. . .] choice among these ways
is guided by convenience or chance. [Gib04, Page 13]. That is, denition is by
denition heretical; it requires the ability to choose (a priori), and is an act of
choice (a posteriori).
The heresy of modern cryptography was guided by chance because compu
tational complexity theory, which it is based on, happens to be dened in terms
of (probabilistic) Turing machines by the mainstream of computer scientists.
2.2. GOAL: SOLUTION 29
On account of the (proof)technical inconvenience that Turing machines entail
in cryptography, this is lamentably bad luck.
Slogan 5 Proving with Turing machines is like programming with calculus
3
.
That is, formal proofs with Turing machines are (doubly) inadequate because
they are mentally intractable (too lowlevel) and because they are inappro
priate (they use the wrong tool). Turing machines are appropriate as a model
of computation, not as a means to proofs. A fortiori, informal proofs with Tur
ing machines are inadequate because the are, besides being mentally intractable
and inappropriate, also inaccurate. In view of the theoretical subtleties and
practical pitfalls of cryptography, this is pitiful bad practice.
2.2 Goal: solution
The cure for prooftechnical inconvenience is, of course, logic, more precisely
proof theory. That is our ultimate goal. Our intermediate goal and the one of
this thesis must be the synthesis of the remedy, i.e., the synthesis of a logical
system powerful enough to allow for the meaningful redenition of cryptographic
concepts.
2.2.1 Logic
The logical solution to a problem of meaning is a relation of satisfaction (or
modelling relation). That is, a relation between a model (of a cryptographic
protocol in our case) and a formula (expressing a statement about that protocol)
asserting that the formula is a true statement about the considered model. Thus
this thesis is about model theory for cryptography, although we shall also address
provability but from a modeltheoretic point of view.
2.2.2 Extent
The redenition of the whole of modern cryptography is, of course, out of the
scope of a Ph.D. thesis.
2.2.2.1 Scope
We shall focus on logical constructions for the security of communication (as op
posed to security of storage) at the level of cryptographic protocols (as opposed
to cryptographic operators). A cryptographic operator is to a cryptographic
protocol what a brick is to a brickhouse. Good bricks are necessary but not
sucient for good brickhouses.
3
a powerful xpoint logic famous for its computational tractability and its mental tractabil
ity at the metalevel, but infamous for its mental intractability at the object level (frequently
referred to as the machinecodelevel language of program logics)
30 CHAPTER 2. INTRODUCTION
2.2.2.2 Grain
The focus on cryptographic protocols provides a macroscopic view on the secu
rity of communication. At this scale of sight, cryptographic operators are ideally
perceived as black boxes with perfect functionality (the socalled DolevYao ab
straction). Perfect operator functionality guarantees functionality of operators
in spite of ideal (i.e., informationtheoretic) adversaries and discharges the pro
tocol functionality from the assumed perfect functionality of the operators the
protocol employs. In contrast, imperfect operator functionality only guarantees
functionality of operators in spite of real (i.e., complexitytheoretic) adversaries.
In consequence, operator functionality might infringe on protocol functionality.
We shall construct two optics of dierent cryptographic grain for our logical
system. The rst optic will have a lens to accommodate the grain of perfect
cryptography, and the second a tentative lens to accommodate the grain of
probabilistic polynomialtime cryptography.
2.3 Methodology
We shall derive the synthesis of our logical system from a comprehensive analysis
of the cryptographic concepts that are relevant to the security of communica
tion. Preceding analysis is necessary for successful synthesis. For example, the
synthesis should respect conceptual orthogonality and hierarchy.
2.3.1 Approach
Our conceptual analysis resembles Leibnizs approach described in his magnus
opus, namely the Monadology. There, Leibniz describes the analysis of concepts
as a breaking down into their atomic constituents (the socalled monads) com
parable to the factorisation of natural numbers into their primes. Proceeding
this way, Leibniz ultimately arrives at primitive concepts.
Our approach is goaloriened in the sense that we discover logical concepts
in naturallanguage formulations of goals for cryptographic protocols. We then
cast these naturallanguage formulations (in mental stepwise renement of pre
cision) into formulae of an imaginary logical language and invent an adequate
semantics (the relation of satisfaction) for these formulae.
The challenge in this enterprise is to nd the right primitive linguistic ab
stractions and the right method of their logical combination. Metaphorically
speaking, our task is to nd the right cryptographic prime factors and the
right notion of and algorithm for their factorisation. This is a nontrivial
task.
2.3.2 Formalism
A distinguishing feature of our approach is that we use formal logic in a doubly
unifying sense. That is, in the sense of the unication of dierent (modal) logics
and in the sense of the integration of logic with (formal) program semantics.
Manifesto There is a ctive schism between the socalled formalmethods
community and the hardcore cryptography community on the subject of for
malism. The formalmethods community professes that formalism is good be
2.3. METHODOLOGY 31
cause formalism means abstraction from bitstrings and thus automation. The
hardcore cryptography community professes that formalism is bad because for
malism means abstraction from bitstrings and thus imprecision. The schism is
ctive because both professions proclaim a mirage, namely the one of imagining
that possibility be necessity. Formalism possibly, but not necessarily, means
abstraction. When it means abstraction, it eectively means automation and
possibly imprecision; otherwise it means neither of both. It is a misconception
to believe that bitstrings cannot be reasoned about formally. A bitstring can
be simply and faithfully modelled as a syntactic term, i.e., as a string of symbols
over the alphabet 0, 1. And that bit of syntax does not require big bites of
formalism. Both professions need confession: this schism is nonsense
4
.
5
2.3.2.1 Unifying modal logics for cryptography
As our imaginary logical language we shall use the language of modal logic as
an aid to precision [BvBW07, Page xvi]. Modal logics are logics with modal
operators (modalities), i.e., operators that are not truthfunctional. A non
truthfunctional operator is an operator that, when applied to operands, yields
a formula whose truth value cannot be established as a mere function of the
truth values of its operands. Many modal logics are relevant to the purpose
of our conceptual investigation. Thereof, we shall demonstrate the relevance of
the modal logics of knowledge, norms, provability, space, and time. Unifying
these logics in a single manydimensional modal logic for that purpose is clearly
desirable.
2.3.2.2 Integrating modal logic and program semantics
As a complement to our logical language, we shall introduce a programming
language, with adequate semantics, for cryptographic protocols. The programs
of this programming language are the models for our logical formulae.
Slogan 6 The subjectmatter of programming languages is pragmatics of control
(of action for eect). Their purpose is empowerment of the human mind in the
formulation of instructions for machines.
The complementary nature of our two languages is explained by ve nat
ural, but notwithstanding novel (except for Item 4 and 5), integrating design
decisions: (1) dene the meaning of a cryptographic protocol (its denotational
semantics) in terms of the meaning of the cryptographic messages it produces
during its execution, i.e., dene the what (denotation) in terms of the how (op
eration); (2) dene the meaning of a cryptographic message in terms of the
propositional knowledge a protocol agent would acquire from the (individual )
knowledge of that message; (3) dene dynamic observational equivalence (indis
tinguishability of execution paths) in terms of static observational equivalence
4
we mean scientic (as opposed to political ) nonsense
5
The executive reader might object that both sides have found a terrain dentente in
soundness (and incompleteness) results w.r.t. the formal view on cryptography in the sense
of DolevYao (so cryptographers still do the real stu). That reader is urged to consider that
that view is not necessarily a limit to the formal view in the sense of Godel. The question
thus is: Is cryptography completely axiomatisable at the level of cryptographic protocols?
(At the level of cryptographic operators it is not due to the involved number theory.)
32 CHAPTER 2. INTRODUCTION
(indistinguishability of execution states); (4) identify static observational equiv
alence with epistemic accessibility (the semantics of propositional knowledge);
and (5) identify the operational semantics (protocol execution) with temporal
accessibility (the semantics of temporal propositions).
2.4 Prerequisites
The prerequisites for this thesis are, by the very nature of our exposition, ba
sic knowledge of logic, program semantics, and cryptography. We shall not
restate that basic knowledge here, but rather conne ourselves to pointing the
needful reader to the relevant literature here and to introducing more advanced
knowledge on the y in our exposition ahead.
2.4.1 Logic and program semantics
A classical, comprehensive reference for general mathematical logic is [Bar99].
The relevant chapters for our exposition are: A.1 (rstorder logic, by J. Bar
wise), B.1 (set theory, by J. R. Shoeneld), and C.7 (inductive denitions, by
P. Aczel). A recent, comprehensive reference for modal logic is [BvBW07]. The
relevant chapters for our exposition are: 1 (semantics, by P. Blackburn and J.
van Benthem), 9 (rstorder modal logic, by T. Bra uner and S. Ghilardi), 11
(temporal logic, by I. Hodkinson and M. Reynolds), 16 (provability and spatial
logic, by S. Artemov), and 18 (deontic, doxastic, and epistemic logic, by J.J.
Meyer and F. Veltnam). A classical, comprehensive reference for program se
mantics is [vL90]. The relevant chapters for our exposition are: Denotational
Semantics by P. D. Mosses, and Operational and Algebraic Semantics of Con
current Processes by R. Milner.
2.4.2 Cryptography
Slogan 7 Cryptography is a technological means to information security.
A twovolume foundational reference for modern cryptography is [Gol01, Gol04].
A comprehensive reference for applied cryptography is [MvOV96] (where from
we shall often quote in this thesis). A comprehensive reference for cryptographic
protocols is [BM03]. And an encyclopaedic reference for the whole eld is [vT05].
2.4.2.1 Prehistory
The prehistory of cryptography (i.e., message obfuscation) is steganography (i.e.,
message hiding). In general, a steganographic message is hidden in another,
apparent, message, whereas a cryptographic message is apparent as such. It is
possible to combine steganography with cryptography, e.g., by encrypting the
steganographic message. With the advent of redundant, digital representation
of information, steganography has regained relevance in modern times. Data
compression on the contrary makes steganography more dicult.
2.4. PREREQUISITES 33
2.4.2.2 Classical cryptography
Classical cryptography is based on information theory
6
. Its rst published,
mathematical treatment appeared in 1949 under the title Communication The
ory of Secrecy Systems by C. Shannon. Classical cryptography guarantees
perfect secrecy of the encrypted plaintext [M[
k
under the assumptions of the
perfect secrecy of the encrypting key k required to be of the same length as
the plaintext M. A corollary of the equallength assumption is that the key be
used only once. That is, using the key a second time divides its entropy (i.e.,
information indeterminacy) by two. Whence the name onetime pad of this
(XORbased) encryption scheme. A property of classical encryption schemes is
that they are symmetric, i.e., the same key is used for en and decryption.
2.4.2.3 Modern cryptography
Modern cryptography is based on (computational) complexity theory. It does
not guarantee perfect secrecy, but, besides computational secrecy, aims at
guaranteeing many more desirable properties related to information security.
The assumptions of modern cryptography are the existence of oneway func
tions and of true randomness. Oneway functions are functions whose inversion
is computationally intractable. An important result of modern cryptography
is that true randomness can be arbitrarily well approximated by pseudo ran
domness, i.e., the randomness furnished by classical (as opposed to quantum)
computers. Security of cryptographic schemes is demonstrated by reduction to
computational problems whose hardness is an empirical fact. A property of
modern encryption schemes is that they are possibly asymmetric, i.e., dierent
keys are used for en and decryption. The rst published treatment of asymmet
ric schemes appeared in 1976 under the title New Directions in Cryptography
by W. Die and M. Hellman. The rst published implementation of an asym
metric scheme appeared in 1978 and is due to R. Rivest, A. Shamir, and L.
Adleman.
Cryptographic operators The traditional occupation of cryptographers is
the construction of operators for cryptographic tasks such as en and decryption,
electronic signature generation and verication, and irreversible obfuscation and
destructive compression of data (data hashing). The traditional occupation of
cryptanalysts is the destruction of those operators, i.e., the breaking of their
intended functionality.
Cryptographic protocols A more modern occupation of cryptographers is
the construction of protocols for cryptographic concerns (e.g., trust, conden
tiality, identity, and commitment) by employing cryptographic operators. Such
concerns arise in the context of communication in hostile environment. The oc
cupation of hostile communicators (socalled adversaries) is the destruction
of those protocols, i.e., the breaking of their intended functionality. Adver
saries can be passive and active. A passive adversary may eavesdrop, i.e., (1)
6
there is also a relation to coding theory: Cryptography distinguishes itself from coding
theory in the sense that the presence of random noise in the latter is replaced by malicious
adversaries in the former. [Vau05, Page 1]
34 CHAPTER 2. INTRODUCTION
read any message, (2) decompose a message into parts (analysis) and remem
ber them. An active adversary may also (3) block message transmission, (4)
generate fresh data as needed, and (5) compose new messages from known data
(synthesis) and send messages. That is, eavesdropping is unaltered (no tamper
ing) eventual forwarding (at most temporary blocking) of intercepted messages.
It is common, theoretical practice to assume the existence of one, archetypical
adversary, and to identify that adversary with the communication network. It
has been reasoned that this is reasonable practice [CLC04].
Our interest with cryptographic protocols is the declarative description (the
what) of their intended functionality. Such declarative statements have the
advantage of being mentally tractable (and hopefully, compelling to bring satis
faction eventually) as we will show. In contrast, cryptographic protocols them
selves, i.e., their operational descriptions (the how), despite their small size, are
mentally intractable, as experience has amply shown.
2.5 Preview
We produce the following declarative descriptions of cryptographic states of af
fairs and cryptographic concepts that are relevant to the functionality of cryp
tographic protocols.
2.5.1 Cryptographic states of aairs
Trustrelated aairs maliciousness, honesty, faultiness, prudency, and trust
worthiness of protocol agents (cf. Section 3.3.1).
Condentialityrelated aairs shared secret, secrecy, anonymity, data deri
vation, noninteraction, perfect forward secrecy, knownkey attack, and
agent corruption (cf. Section 3.3.2).
Authenticationrelated aairs key conrmation, key authentication (impli
cit and explicit), message integrity, message authorship, message authenti
cation (authenticity), key transport (unacknowledged and acknowledged),
key agreement (unacknowledged and acknowledged), entity authentica
tion (identication) (unilateral, weakly mutual, and strongly mutual) (cf.
Section 3.3.3).
Commitmentrelated aairs cryptographic proof, cryptographic evidence,
provability, nonrepudiation, contract signing, (optimism, completion, ac
countability, and abusefreeness) (cf. Section 3.3.4).
Compositionalityrelated aairs key separation, compositional correctness
(existential composability, conditional composability, and universal com
posability), and attack scenario (cf. Section 3.3.5).
2.5.2 Cryptographic concepts
Fundamental concepts oneway function, hardcore predicate, computatio
nal indistinguishability, (nparty) interactive proof, interactive provabil
ity, proof of knowledge, and (nprover) zeroknowledge (cf. Section 5.3.1).
2.5. PREVIEW 35
Applied concepts security of encryption schemes (standard, semantic, via in
distinguishability, and via nonmalleability), unforgeability of signature
schemes, attacks on encryption schemes (ciphertextonly attack, known
plaintext attack, chosenplaintext attack, adaptive chosenplaintext at
tack, chosenciphertext attack, and adaptive chosenciphertext attack),
attacks on signature schemes (keyonly attack, knownmessage attack,
chosenmessage attack, and adaptive chosenmessage attack), and breaks
of signature schemes (existential forgery, selective forgery, universal for
gery, and total break) (cf. Section 5.3.2).
2.5.3 Research highlight
Our research highlight is having demonstrated the macrodenability of a Godel
style provability modality within the spatioepistemic fragment of CPL (cf. The
orem 2). With this modality, CPL can capture the provability meaning of intu
itionistic implication, and provability is shown to be the key to the formalisation
of commitment and related cryptographic states of aairs (cf. Section 3.3.4).
2.5.4 Peerreview
The content of this thesis has been validated through the publication of three
peerreviewed short papers [Kra03], [Kra06a], and [Kra06b]; four workshop pa
pers [Kra04], [BKN06], [BGK06], and [Kra07a, Kra07b]; and one journal paper
[Kraar].
36 CHAPTER 2. INTRODUCTION
Part II
Cryptographic Protocol
Logic
37
Chapter 3
DolevYao cryptography
3.1 Introduction
We give a comprehensive motivation for our approach to the correctness of
cryptographic protocols by placing the approach in its historical and topical
context. The length of the introduction reects our desire to expose a wide and
deep perspective on the highly interdisciplinary eld of cryptographic protocols.
3.1.1 Historical context
A cryptographic protocol [. . .] is a distributed algorithm dened by a sequence
of steps precisely specifying the actions required of two or more entities to
achieve a specic security objective. [MvOV96, Page 33]. Principal security
objectives are secrecy of condential information, authenticity of received mes
sages w.r.t. their origin, and nonrepudiation of message authorship. Our slogan
is:
Slogan 8 The purpose of a cryptographic protocol is to interactively compute,
via message passing
1
, knowledge of the truth of desired and, dually, knowledge
of the falsehood of undesired cryptographic states of aairs.
In 1996, Anderson and Needham assert that cryptographic protocols typi
cally involve the exchange of about 25 messages, and one might think that a
program of this size would be fairly easy to get right. However, this is absolutely
not the case: bugs are routinely found in well known protocols, and years after
they were rst published. The problem is the presence of a hostile opponent, who
can alter messages at will. In eect, our task is to program a computer which
gives answers which are subtly and maliciously wrong at the most inconvenient
possible moment. [AN96b]. Indeed, designing a correct cryptographic proto
col (i.e., programming Satans computer [AN96b]), is extremely more dicult
than designing a correct, ordinary computer program (i.e., programming Mur
phys [computer] [AN96b]) of the same size. In fact, at the end of the 1980s,
i.e., 20 years after the surge of the software crisis in the softwareengineering
community, the communicationsecurity community was also shaken by a soft
ware crisis, though a dierent one. The rst software crisis was provoked by the
1
rather than shared memory
39
40 CHAPTER 3. DOLEVYAO CRYPTOGRAPHY
(increasing) size of computer programs [Dij72], whereas the second crisis was
triggered by the (sudden, e.g., [BAN90]) awareness about the complexity of the
structure of a certain class of such programs, namely cryptographic protocols.
Our slogan, especially applying to cryptographic protocols, is:
Slogan 9 In theory, it is possible to construct a correct computer program with
out knowing a theory of program correctness; in practice, it rarely is.
The answer to both software crises has really been the formalmethods move
ment. In 1999, McLean arms that [o]ne of the biggest success stories of formal
methods in the computer security community is the application of them to cryp
tographic protocols. Cryptographic protocols are small enough to be susceptible
to complete formal analysis, and such analyses have turned up aws that would
have, otherwise, gone undetected. [McL99]. However, McLean also points out
the need for more research in the specication arena. in the same paper. In
2003, Meadows rearms and strengthens the importance of that issue by ob
serving that [. . .] although it is dicult to get cryptographic protocols right,
what is really dicult is not the design of the protocol itself, but of the require
ments. Many problems with security protocols arise, not because the protocol
as designed did not satisfy its requirements, but because the requirements were
not well understood in the rst place. [Mea03] (consider also, more generally,
[Rog04]). Our slogan is:
Slogan 10 Cryptographic protocol correctness: a killer application for formal
methods.
3.1.2 Topical context
3.1.2.1 Requirements engineeringideally
Indeed, the construction of a cryptographic protocol begins (and ends if this
stage is not mastered) with requirements engineering, i.e., the denition of the
requirements (global properties) the protocol is supposed to meet. In particu
lar, understanding protocol requirements is necessary for understanding protocol
attacks, which can be looked at as falsications of necessary conditions for the
requirements to hold. Protocol specication (requirements engineering), design
(modelling), verication, and implementation (programming) are engineering
tasks (the spirit of [MvOV96]). In contrast, the construction of a cryptographic
operator (for encryption, signing, and hashing) is a scientic task (the spirit
of [Gol01, Gol04]) requiring profound expertise from dierent elds of discrete
mathematics.
2
Protocol engineers do (and should) not have (to have) this exper
tise. For example, it is legitimate for a protocol engineer to abstract negligible
probabilities and consider them as what they are negligible. Ideally, engi
neers should only have to master a single, common, and formal language for
requirements engineering that adequately abstracts hardcore mathematical
concepts.
2
consider also [Riv90]: The design of protocols and the design of operators are rather
independent [. . .]. The protocol designer creates protocols assuming the existence of operators
with certain security properties. The operator designer proposes implementations of those
operators, and tries to prove that the proposed operators have the desired properties.
3.1. INTRODUCTION 41
Since logic is what all sciences have in common, it is natural to stipulate
that such a lingua franca for requirementsengineering cryptographic protocols
be an appropriate logical language.
Program statement We argue that a good candidate language is a can
didate that is technically adequate and socially acceptable. By a technically
adequate candidate we mean a candidate that (1) is semantically and pragmat
ically suciently expressive, i.e., versatile and yielding intuitive specications,
respectively; (2) has a cryptographically intuitive semantics; (3) is completely
axiomatisable; and (4) has important decidable fragments (e.g., the temporal
fragment). By a versatile candidate we mean a candidate that allows all de
sirable specications to be directly expressed, or else dened, in terms of the
primitives of the candidate. By intuitive specications we mean that the con
ceptual dimensions of a specication are apparent in distinctive forms in the
formula that expresses the specication succinctly. By a socially acceptable
candidate we mean a candidate that unies and possibly transcends previous
specication languages.
Our task shall be to synthesise the relevant logical concepts in cryptogra
phy into a cryptographic protocol logic with a temporallogic skeleton. Our
preference of temporal logic over program logics such as Hoare and dynamic
logic is motivated by the success of temporal logic as a specication language
for (noncryptographic) interactive systems. We will validate our language, at
least at a rst stage, on specication (stress on dierent requirements) rather
than verication (stress on dierent protocols) case studies, since program spec
ication must in theory, and should in practicewhere it unfortunately rarely
doesprecede program verication. Nonetheless, the existence of verication
examples is guaranteed by subsumption under CPL of other logics from authors
with the opposite focus.
3.1.2.2 Requirements engineeringreally
We briey survey requirements engineering (the practice of the specication) of
cryptographic protocols. Protocol designers commonly dene a cryptographic
protocol jointly by a semiformal description of its behaviour (or local prop
erties) in terms of protocol narrations, and by an informal prescription of its
requirements (or global properties) in natural language [BM03]. Informal spec
ications present two major drawbacks: they do not have a welldened, and
thus a wellunderstood meaning, and, therefore, they do not allow for verica
tion of correctness. In formal specications of cryptographic protocols, local and
global properties are expressed either explicitly as such in a logical (or property
based) language, or implicitly as code, resp. as encodings in a programming (or
model based) language (e.g., applied Calculus [SP03]; process calculi: CSP
[RSG
+
00], applied Calculus [AF01], SpiCalculus [AG99], and [MRST06]).
Modelbased languages The most popular examples of such encodings are
equations between protocol instantiations [Aba00]. However, such encodings
present four major drawbacks: (1) they have to be found for each protocol anew;
worse, (2) they may not even exist; (3) they are neither directly comparable
with other encodings in the same or in other programming languages, nor with
properties expressed explicitly in logical languages; and (4) they are not easy to
42 CHAPTER 3. DOLEVYAO CRYPTOGRAPHY
understand because the intuition of the encoded property is not explicit in the
encoding; yet [r]obust security is about explicitness. [AN96b]! On the other
hand, process calculi are ideal design formalisms. That is, they oer due
to their minimalist, linguistic abstractions of modelling concepts (syntax) and
their mathematical, operational notion of execution (semantics) a winwin
situation between the (pedantic) rigour of (Turing) machine models and the
(practical) usability of mainstream programming languages.
Propertybased languages Still, informal language and programming (or
eect) languages are inadequate for expressing and comparing cryptographic
properties. It is our belief that only a logical (or truth) language equipped with
an appropriate notion of truth, i.e., a cryptographic logic, will produce the nec
essary adequacy. A number of logics have been proposed in this aim so far,
ranging from specialpurpose, cryptographic logics: the pioneering BANlogic
[BAN90], a unication of several variants of BANlogic [SvO96], and a recent
reworking of BANlogic [KS06]; over generalpurpose propositional, modal, pro
gram, and rst and higherorder logics used for the special purpose of crypto
graphic protocol analysis: propositional (logic programming) [AM01, AB05];
modal : deontic [BC93], doxastic [ABV01, ZV01], epistemic [SS99, HO02], lin
ear [BD04], temporal [GM95]; program: dynamic [FHJ02, ADM03], Hoare
style [DMP03, LA05]; rstorder [CJM98, Sel01, Coh03]; higherorder [Pau98,
IK06]; to combinations thereof: doxasticepistemic [CS97], doxastictemporal
[BGPS00], distributed temporal [CVB05], dynamicepistemic [Bal01], epistemic
temporal [DGMF04, LW06] rstordertemporal [GLL01], dynamicepistemic
temporal [Bie90], and deonticepistemictemporal [GMP92].
All these logics have elucidated important concerns of the security of com
munication and proved the relevance of logical concepts to that security. In
particular, mere enunciation of maybe the three most fundamental protocol
requirements, namely secrecy, authenticity, and nonrepudiation, reveals the
paramount importance of the concept of knowledge, both in its propositional
(socalled knowledge de dicto) and in its individual (socalled knowledge de re)
manifestation. Possible
3
enunciations in natural language of these requirements
are the following (cf. Section 3.3 for their formalisation in CPL). Secrecy for a
protocol: Always and for all messages m, if it is forbidden that the adversary
(Eve) know m then Eve does not know m. (knowledge de re in the present
subjunctive and the present indicative mode, respectively). Authenticity of a
message m from the viewpoint of agent a w.r.t. agent b: a knows that once only
b knew m. (knowledge de dicto in the present and knowledge de re in the past
indicative mode). Nonrepudiation of authorship of a message m
by b w.r.t. a,
corroborated by a proof m (m is a proof for a that b is the author of m
): If
a knew m then a would know that once only b knew m
. (knowledge de re in
the past subjunctive and then in the past indicative mode, and knowledge de
dicto in the conditional mode). However, generalpurpose/standard epistemic
logic is inadequate in a cryptographic setting due to weak paradoxes, as is, for
the same reason, (standard) deontic logic (cf. Section 3.2.3). (We recall that a
weak paradox in a logic is a counterintuitive statement in the logic, whereas
a strong paradox is an inconsistency in the logic.) And doxastic logic is in
adequate because the above requirements are ineable in it, as these crucially
3
as a matter of fact unique, canonical formulations of these requirements do not exist (yet)
3.1. INTRODUCTION 43
rely on knowledge, i.e., necessarily true, and not possibly false, belief (no error
control!). Our slogan, and pun
4
, is:
Slogan 11 Belief (without error control) can be used to show the presence of
attacks, but, as opposed to knowledge, never to show their absence.
5
Further, linear logic has, for our approach, a avour that is too operational to
the extent that it is possible that the combinators of a process calculus are
mapped to [linear] logical connectives [Mil06]. Our approach is diametric, i.e.,
we aim at providing declarative abstractions (the what) of operational aspects
(the how). Finally, specialpurpose logics have been limited in their adequacy
due to their choice of primitive concepts, e.g., belief, no negation/quantication,
too specic primitive concepts at the price of high extension costs.
Logical limitations originate in design decisions of syntactic (languagede
ning operators) and/or semantic (meaningdening notion of truth) nature. The
advantages (or disadvantages) of the cited logics are corollaries of the respec
tive advantages (or disadvantages) of capturing (or not) the discussed and to
bediscussed concepts. In particular, crucial advantages are to capture: (1)
individual and propositional knowledge, with a treatment of weak paradoxes;
(2) permission and prohibition, with a treatment of weak paradoxes; (3) proof
and provability; (4) protocol composition (either with dynamic/Hoarelogic con
structs, or with spatiallogic constructs as in CPL); and (5) time (both qualita
tive and quantitative).
3.1.2.3 Requirements engineeringCPL
Our goal is to supply a formal synthesis of (monodimensional) concepts in a
single, polydimensional
6
modal logic, namely CPL, that yields requirements
that are intuitive but (syntactically) abstract w.r.t. particular conceptions of
cryptography
7
. First, our belief, expressed as a slogan, is:
Slogan 12 The formal method for any science is, ultimately, logic.
Logic, as dened by a relation of satisfaction (model theoretic approach
8
, eec
tuated via modelchecking [CGP99]) or a relation of deduction (proof theoretic
approach, eectuated via automated theoremproving [Fit96]). Second, given
that requirements engineering is mainly about meaning, i.e., understanding and
formalising properties, we believe that a modeltheoretic approach is, at least
at a rst stage, more suitable than a prooftheoretic approach. We argue that
propositional and higherorder (at least beyond second order) logic, and set the
ory are unsuitable as frontend formalisms for requirements engineering. Propo
sitional logic is simply too weak as a specication language but is wellsuited for
4
on the slogan Program testing can be used to show the presence of bugs, but never to
show their absence! by Dijkstra
5
this is the deeper reason for the wellknown limitations of BANlogic
6
cf. [GKWZ03] for a research monograph on polydimensional modal logic, characterised
in [BdRV01] as . . . a branch of modal logic dealing with special relational structures in which
the states, rather than being abstract entities, have some inner structure. . . . Furthermore,
the accessibility relations between these states are (partly) determined by this inner structure
of the states.
7
such logics are called endogenous (or monomodal ), as opposed to exogenous (or poly
modal )
8
not to be confused with a modelbased formalism
44 CHAPTER 3. DOLEVYAO CRYPTOGRAPHY
fullyautomated, approximative verication. Higherorder logic and set theory
may well be semantically suciently expressive; however, we opine that they
are unsuitable for engineers in charge of capturing meaning of protocol require
ments within an acceptable amount of time (i.e., nancial cost per specication)
and space (i.e., intelligibility of specications). The intuitiveness of the speci
cations that a formalism yields is not just luxury, but the very (and dicult to
distil) essence and a measure of its pragmatics, i.e., practical usefulness. Our
slogan
9
is:
Slogan 13 Logic for engineering necessarily is, possibly rstorder, modal logic.
Modal operators (modalities) are objectlevel abstractions of metalevel quanti
ers. In eect, they eliminate variables (and the quantiers that bind them) in
logical (truth) languages as combinators do in programming (eect) languages,
and delimit quantication to the relevant (i.e., accessible) parts of the interpre
tation structure. Their benets are intelligibility of the expressed statement,
and eectiveness and relative eciency of truth establishment, respectively.
The concept of a cryptographic protocol is very rich. A suitable formalism
must organise and hardwire/precompile this conceptual variety in its seman
tics and provide succinct and intuitive linguistic abstractions (syntax) for them.
The resulting added value of such a formalism is empowerment of the engineer
(speedup of the mental process of requirements formalisation)
10
, and more
powerful tools (speedup of modelchecking and automated theoremproving).
Higherorder logic and set theory, having been conceived as generalpurpose
formalisms, obviously lack this specialpurpose semantics and syntax. How
ever, they are wellsuited as logical frameworks (metalogics/backends) for such
specialpurpose formalisms (object logics/frontends). For example, our candi
date language has a modeltheoretic (i.e., relying on set theory) semantics.
CPL has a rstorder fragment for making statements about protocol events
and about the (individual) knowledge (knows) and the structure of crypto
graphic messages induced by those events; and four modal fragments for making
statements about condentiality norms (cf. deontic logic [BC93]); propositional
knowledge (knows that), i.e., knowledge of cryptographic states of aairs, (cf.
epistemic logic [FHMV95]); execution space (cf. spatial logic [Dam89]); and ex
ecution time (cf. temporal logic [MP84]). That is, CPL unies rstorder and
four modal logics in a single, rstorder, polydimensional modal logic. Further,
CPL renes standard epistemic and deontic logic in the sense that it resolves
the longstanding problem of weak paradoxes (caused by logical omniscience and
conicting obligations, respectively) that these logics exhibit when applied in
a cryptographic setting (cf. Section 3.2.3). Yet CPL (a propertybased formal
ism) goes even further in its wholistic ambition in that it integrates the perhaps
most important modelbased framework, namely process algebra [BPS01], in
a novel codesign. First, CPLs temporal accessibility relation (the semantics
of its temporal modalities) can be dened by an eventtrace generating process
(reduction) calculus, for example C
3
(cf. Chapter 4) whose reduction constraints
can moreover be checked via CPLsatisfaction; and second
11
, CPLs epistemic
9
and pun on the two cornerstones of modal logic, namely possibility and necessity
10
in analogy with highlevel programming languages versus machinecode languages
11
This idea seems to have been published rst in [HS04b]. However, the authors adopt a
very dierent approach based on socalled function views.
3.2. LOGIC 45
accessibility relation (the semantics of its epistemic modality knows that) is
the denitional basis for C
3
s observational equivalence, which can be used for
the modelbased (processalgebraic and complementary to propertybased) for
mulation of protocol requirements. We believe that this codesign is also the
key to a genuine modal model theory for cryptography.
Justication A cryptographic protocol involves the concurrent interaction of
agents that are physically separated by and exchange messages across
an unreliable and insecure transmission medium. Expressing properties of con
current interaction (i.e., interactive computation) requires temporal modalities
[MP84]. The physical separation by an unreliable and insecure transmission
medium (i.e., unreliable computation) in turn demands the epistemic and de
ontic modalities. To see why, consider that the existence of such a separating
medium introduces an uncertainty among agents about the trustworthiness of
the execution of protocol actions (sending, receiving) and the contents of ex
changed messages, both w.r.t. actuality (an epistemic concern) and legitimacy
(a deontic concern).
Slogan 14 Trustworthiness = Actuality + Legitimacy
The purpose of a cryptographic protocol is to reestablish this trustworthiness
through the judicious use of cryptographic evidence, i.e., essential information
(e.g., ciphers, signatures and hash values) for the knowledge of other information
(e.g., messages or truth of formulae), bred in a crypto system (e.g., a sharedkey
or publickey system) from cryptographic germs such as keys and nonces, them
selves generated from cryptographic seeds (or seed values). However, any use of
keys (as opposed to hash values and nonces) requires that the knowledge of those
keys be shared a priori. This sharing of key knowledge is established by crypto
graphic protocols called keyestablishment protocols (comprising keytransport
and keyagreement protocols) [MvOV96, Chapter 12], which are executed before
any cryptographic protocol that may then subsequently use those keys. Thus
certain cryptographic protocols must be considered interrelated by a notion of
composition in a common execution space; hence the need of spatial opera
tors. Another argument for spatial operators comes from the fact that a correct
protocol should conserve its sole correctness even when composed with other
protocols, i.e., a compositionally correct protocol should be stable in dierent
execution contexts [Can01, BPW03].
3.2 Logic
3.2.1 Syntax
The language T of CPL is parametric in the language / of its individuals,
i.e., cryptographic messages. It is chiey relational, and functional in exactly
the language / of cryptographic messages it may be instantiated with. The
temporal fragment of T coincides with the syntax of LTLP (linear temporal logic
with past). We shall x our mind on the following, comprehensive language /.
Denition 1 (Cryptographic messages) We form messages M / with
the term constructors displayed in Table 3.1. There, names n N denote agent
46 CHAPTER 3. DOLEVYAO CRYPTOGRAPHY
names a, b, c A, the (for the moment DolevYao [DY83]) adversarys name
Eve, symmetric shortterm (session) (K
1
) and longterm (K
) keys k K,
(asymmetric) private keys p K
p
+
(public keys)
M (message hashes)
[M[
M
(symmetric message ciphers)
[M[
+
p
+
(asymmmetric message ciphers)
[M[
p
(signed messages)
::=
H[]
SC
M
[]
AC
p
+[]
S
p
[]
T[,
M
,
::= A
Adv
K
+
,
::= K
1
X
Message type forms shall be message types with variables in key position.
Observe that (1) for each kind of message there is a corresponding type (e.g.,
H[] for hashes, SC
M
[] for symmetric and AC
p
+[] for asymmetric ciphers, S
p
[]
for signatures, and T[,
denote types
of dynamically generable names. We macrodene A
Adv
:= AAdv, K := K
1
K
,
CK := K K
, K
:= CK K
+
, and N := A
Adv
K
X.
Denition 3 (Logical formulae) The set of formulae T contains precisely
those propositions that are the closed predicates formed with the sentence con
structors displayed in Table 3.2. There, denotes basic, action, and data
formulae; and o denotes tuples of agent names (key owners).
Table 3.2: Predicate language
,
::=
v()
P
{z}
norms
K
a
()
 {z }
knowledge
 {z }
space
_+
 {z }
time
,
::=
::= a n.o
a
F
Eve
b
a
F
Eve
b
 {z }
private comm.
a
F
Eve
b
a
Eve
F
 {z }
public comm.
,
::= n :
a k F
F  F
a@x
Predicates can be transformed into propositions either via binding of free vari
ables, i.e., universal (generalisation) or existential (abstraction) quantication,
or via substitution of individuals for free variables (individuation). In accor
dance with standard logical methodology, basic predicates express elementary
facts
12
.
Our symbols are and their intuitive meaning is as they are pronounced
not, and, v for all v, P it is permitted that, K
a
a knows that,
epistemically implies, conjunctively separates, assumeguarantee,
S since, _ previous, _+ next, U until, a n.o a freshly generated
the name n for owner(s) o, a
F
Eve
b a securely (i.e., over some private channel)
sent F as such (i.e., not only as a strict subterm of another message) to b,
12
a fact is a contingent (particular) truth as opposed to a logical (universal) truth
48 CHAPTER 3. DOLEVYAO CRYPTOGRAPHY
a
F
Eve
b a securely received F as such from b, a
F
Eve
b a insecurely (i.e., over
some public channel) sent o F as such to b, a
Eve
F a insecurely received F
as such, : has type, k knows,  is a subterm of, and @ is in protocol
run/session.
Our predicate language is 1sorted thanks to the standard technique of sort
reduction
13
and to the fact that agents are referred to by their name and names
are transmittable data, i.e., messages.
The modality K expresses propositional knowledge, i.e., the knowledge that
a certain proposition is true. In contrast, the relational symbol k expresses indi
vidual knowledge. Individual knowledge conveys understanding of the purpose
and possession of a certain piece of cryptographic information up to crypto
graphically irreducible parts. It is established based on the capability of agents
to synthesise those pieces from previously analysed pieces. By understanding
of the purpose we mean (1) knowledge of the structure for compound, and (2)
knowledge of the identity for atomic (names) information. Note that such un
derstanding requires that there be a minimal redundancy in that information.
The conditional
(cf.
compositional correctness of a protocol, as mentioned earlier).
Typing formulae F : have an essential and a pragmatic purpose. Typing
of atomic data, i.e., when F designates a name n and an atomic type , is
a linguistic abstraction for the abovementioned essential modelling hypothesis
of minimal redundancy. Typing of compound data simply increases succinct
ness of statements about message structure. It is actually macrodenable in
terms of typing of atomic data, equality (itself macrodenable), and existential
quantication (cf. Appendix B).
3.2.2 Semantics
Our denition of satisfaction
14
is anchored (or rooted) and dened on protocol
states, i.e., tuples (h, P) H T of a protocol model P (i.e., a process term
of parallelcomposable, located threads a.x[ T ]) and a protocol history h (i.e., a
trace of past protocol events). Note that historydependency is characteristic of
interactive computation [GSW06].
The logicallyinclined reader will notice that CPL has a Herbrandsemantics,
i.e., logical constants and functional symbols are selfinterpreted rather than
interpreted in terms of (other, semantic) constants and functions.
13
introduction of unary relational symbols ( : in our case) emulating the dierent sorts
14
the concept was invented by Tarski
3.2. LOGIC 49
Slogan 15 (Symbolic Foundationalism) Meaning, when communicable, is
symbolic. Semantics is interpretation of syntax via rewriting.
For the present purpose, we presuppose a notion of execution, for example
the one of Section 4.1, (H T)
2
(or relation of temporal accessibility
in the jargon of modal logic) producing protocol events of a certain kind and
chaining them up to form protocol histories. We stress that the locality and
parallelcomposability of processes (denoted P P
p@i designates
the set of paths p achored/rooted in s and induced by , and designates
our function of truth denotation from formulae to complex truth values (cf.
Table 3.4). There,
p@i designates the state, sayplease memorise(h, P), at position i in p
h designates the set of events derived from the trace of events h
h
E
a
M designates derivation of M by a fromthis is a novel ideathe
set c of events in as view on h, i.e., the extraction, analysis, and synthesis
of the data that a has generated, received, or sent in h (cf. Table 3.3)
17
15
multivalued logic was invented by Post
16
notice the two notions of a model: namely, the one of a model for a logical formula (i.e.,
a protocol state (h, P)), and the one of a model of a cryptographic protocol (i.e., a process
term P)
17
We could easily account for individual knowledge modulo an equational theory of cryp
50 CHAPTER 3. DOLEVYAO CRYPTOGRAPHY
Table 3.3: Derivation of individual knowledge
Data extraction
h (a, M)
{(a,M)}
a
(a, M)
h
E
a
M
h
E
a
M
Data synthesis Data analysis
h
E
a
M h
E
a
M
h
EE
a
(M, M
)
h
E
a
(M, M
)
h
E
a
M
h
E
a
(M, M
)
h
E
a
M
h
E
a
p
h
E
a
p
+
h
E
a
M
h
E
a
M
h
E
a
M h
E
a
M
h
EE
a
[M[
M
h
E
a
[M[
M
h
E
a
M
h
EE
a
M
h
E
a
M h
E
a
p
+
h
EE
a
[M[
+
p
+
h
E
a
[M[
+
p
+
h
E
a
p
h
EE
a
M
h
E
a
M h
E
a
p
h
EE
a
[M[
p
h
E
a
[M[
p
h
E
a
p
+
h
EE
a
M
designates concatenation of histories conserving uniqueness of events
:= (k : CK)(Eve k k k ck Eve) designates a state formula expressing
the state of violation in a DolevYao adversarial setting, namely the one
where the adversary has come to know a condential key not of her own
a
(HT)
2
designates the relation of epistemic accessibility associated
with the modality K
a
; it is dened hereafter
h
a
designates a unary function (inspired by [AR02]) of cryptographic
parsing dened on protocol states and on logical formulae; it is dened
hereafter on messages and tacitly lifted onto protocol states and logical
formulae
designates a relation of structural equivalence dened on process terms
and on event traces. On process terms, it designates the smallest equiva
lence relation expressing associativity and commutativity of processes. On
event traces, it designates shuing.
The permission modality is included in the logic because we want to highlight
that each new notion of state of violation will give rise to a new notion of
permission, such as the one for real time (cf. Section 3.4.2) or the ones for
tographic messages, i.e., a set of algebraic properties of cryptographic operators expressed
with an equivalence relation M M, by adding a rule
h
E
a
M
h
E
a
M
M M
. Further,
agentname guessing could be modelled by adding an axiom
h
E
a
b
b A
Eve
.
3.2. LOGIC 51
Table 3.4: Truth denotation
a n.o
i
p
:= (c ,= , c) where c :=
xX
N(a, x, n, o)
h
a
M
Eve
b
i
p
:= (c ,= , c) where c :=
xX
sO(a, x, M, b)
h
a
M
Eve
b
i
p
:= (c ,= , c) where c :=
xX
sI(a, x, M, b)
h
a
M
Eve
b
i
p
:= (c ,= , c) where c :=
xX
O(a, x, M, b)
h
a
Eve
M
i
p
:= (c ,= , c) where c :=
xX
I(a, x, M)
h
n :
i
p
:= (n has type , )
a k M
i
p
:= (c ,= , c) where c :=  c
 h
E
a
M
M  M
i
p
:= (M is a subterm of M
, )
a@x
i
p
:= (there is a thread T s.t. P = a.x[ T ] and h = h[
a.x
, )
i
p
:= (not v
,
h \ c
) where
i
p
= (v
, c
i
p
:= (v
and v
, c
) where
i
p
= (v
, c
) and
i
p
= (v
, c
)
v()
i
p
:= (for all M /, v
M
,
S
MM
c
M
) where
M
/
v
i
p
= (v
M
, c
M
)
P
i
p
:= (
) ( ( , ))
i
p
K
a
()
i
p
:= (for all s, if p@0
s and s
a
p@i then s
[=
E
, c
(s,)
)
where (s
) :=
(
(s, ) if s = p@i, and
( s
h
a
,
h
a
) otherwise.
i
p
:= (if v
then v
and ,= c
, c
) where
i
p
= (v
, c
) and
i
p
= (v
, c
i
p
:= (there are Q, Q
1 and h
, h
1 s.t. P Q Q
and h h
and (h
, Q) [=
E
and (h
, Q
) [=
E
, c
i
p
:= (for all (h
, Q) 11 and h
h, if (h
, Q) [=
E
then
(h
, Q P) [=
E
,
S
c
S
c
)
S
i
p
:= (there is k s.t. 0 k i and v
k
and for all j, if k < j i then v
j
,
S
j
c
j
c
k
) where
j
p
= (v
j
, c
j
) and
k
p
= (v
k
, c
k
)
_
i
p
:=
(
i1
p
if i > 0, and
(false, ) otherwise.
_+
i
p
:=
(
i+1
p
if i < [p[ 1, and
(false, ) otherwise.
U
i
p
:= (there is k s.t. i k and v
k
and for all j, if i j < k then v
j
,
S
j
c
j
c
k
) where
j
p
= (v
j
, c
j
) and
k
p
= (v
k
, c
k
)
52 CHAPTER 3. DOLEVYAO CRYPTOGRAPHY
probabilistic polynomialtime settings (cf. Section 5.2.2). That is, we look at
the state formula as a parameter of the logic.
The epistemic accessibility relation has, as previously mentioned, a double
use. It not only serves as the denitional basis for the epistemic modality of
CPL, but also as the denitional basis for the observational equivalence of C
3
(cf. Section 4.1.3).
Notice that the spatial conditional is monotonic w.r.t. positive antecedents,
e.g., [= a k M a k M, but ,[= a k M a k M due to the possibility for a
of learning additional information from the adjunction.
Cryptographic parsing captures an agents capability to understand the
structure of a cryptographically obfuscated message. It allows the denition
of a cryptographically meaningful notion of epistemic accessibility via the inter
mediate concept of structurally indistinguishable protocol histories. The idea is
to parse unintelligible messages to the abstract message B.
Denition 5 (Cryptographic parsing) The cryptographic parsing function
h
a
associated with an agent a T and a protocol history h H (and comply
ing with the assumptions of perfect cryptography) is an identity on names, the
abstract message, and public keys; and otherwise acts as dened in Table 3.5.
Table 3.5: Parsing cryptographic messages
M
h
a
:=
(
M
h
a
if h [= a k M, and
B otherwise.
[M[
M
h
a
:=
(
[ M
h
a
[
M
h
a
if h [= a k M
, and
B otherwise.
[M[
+
p
+
h
a
:=
(
[ M
h
a
[
+
p
+
if h [= a k p (a k M a k p
+
), and
B otherwise.
[M[
p
h
a
:=
(
[ M
h
a
[
p
if h [= a k p
+
, and
B otherwise.
(M, M
)
h
a
:= ( M
h
a
, M
h
a
)
A particularity of this notion of cryptographic parsing is that if h ,[= a k k and
h
[
k
h
a
. That is, two dierent plaintexts
(M and M
) encrypted under the same symmetric key (k) are parsed to the same
(abstract) message (B), when the parsing agent does not know the decrypting
key. This is justied by the fact that in reality, and in an extension of CPL
with a notion of probabilistic (polynomialtime) computation (cf. Chapter 5),
encryption is probabilistic anyway, which has precisely the eect of rendering
the above ciphers (computationally) indistinguishable to a parsing agent.
Denition 6 (Structurally indistinguishable protocol histories) Two
protocol histories h and h
H, h
a
h
:i
h
(h,h
)
a
h
where,
3.2. LOGIC 53
given that a is a legitimate agent or the adversary Eve,
1.
(h,h
)
a
2.
h
l
(h,h
)
a
h
r
h
l
(a, n)
(h,h
)
a
h
r
(a, n)
3.
h
l
(h,h
)
a
h
r
h
l
(a, M)
(h,h
)
a
h
r
(a, M
)
M
h
a
= M
a
given that a is a legitimate agent,
4.
h
l
(h,h
)
a
h
r
h
l
(b)
(h,h
)
a
h
r
a ,= b
h
l
(h,h
)
a
h
r
h
l
(h,h
)
a
h
r
(b)
a ,= b
given that a is the adversary Eve,
5.
h
l
(h,h
)
Eve
h
r
h
l
(b)
(h,h
)
Eve
h
r
Eve ,= b
h
l
(h,h
)
Eve
h
r
h
l
(h,h
)
Eve
h
r
(b)
Eve ,= b
6.
h
l
(h,h
)
Eve
h
r
h
l
I(b, x, M)
(h,h
)
Eve
h
r
I(b, x, M
)
M
h
Eve
= M
Eve
7.
h
l
(h,h
)
Eve
h
r
h
l
O(b, x, M, c)
(h,h
)
Eve
h
r
O(b, x, M
, c)
M
h
Eve
= M
Eve
Note that the observations at the dierent (past) stages h
l
and h
r
in h and h
,
respectively, must be made with the whole (present) knowledge of h and h
(cf.
h
l
(h,h
h
r
). Learning new keys may render intelligible past messages to an
agent a in the present that were not to her before.
Remark 1 For all a A
Eve
,
a
HH is
1. an equivalence with an innite index due to freshname generation
2. not a rightcongruence due to the possibility of learning new keys
3. a renement on the projection H[
a
of H onto as view [FHMV95]
4. decidable.
We lift structural indistinguishability from protocol histories to protocol
states, i.e., tuples of a protocol term and a protocol history, and nally ob
tain our relation of epistemic accessibility.
54 CHAPTER 3. DOLEVYAO CRYPTOGRAPHY
Denition 7 (Observationally equivalent protocol states) Let P
1
and
P
2
designate two cryptographic processes, i.e., models of cryptographic protocols,
of some set T. Then two protocol states (h
1
, P
1
) and (h
2
, P
2
) are observationally
equivalent from the viewpoint of an agent a, written (h
1
, P
1
)
a
(h
2
, P
2
), :i
h
1
a
h
2
.
Proposition 1 Let for all ,
T,
=
i
p
[= , pronounced is a logical truth (or tautology) in CPL, :i for all
s HT, s [= .
Then for all ,
T,
1. if [=
then =
2. if =
then [=
.
Proof. almost by denition
Denition 8 (Logical consequence and equivalence) Let ,
T.
Then,
, :i for all s T H, if
s [= then s [=
, :i
and
.
Remark 2
but
.
Denition 9 (CPL: logic and logical theory)
logic (a body of truth):
(TL :=  [=
logical theory (a system of inference):
CPL :=  there is s HT s.t. s [=
(For all CPL and
T, if
then
CPL.)
Theorem 1 (Barcan and relativised CoBarcan)
Barcan [= m(K
a
()) K
a
(m())
CoBarcan [= K
a
(m(a k m )) m(a k m K
a
())
Proof. see Appendix A
The Barcan property w.r.t. propositional knowledge (K
a
) is quite standard.
However, the relativisation to individual knowledge (k) to obtain the converse
Barcan property is novel. (The plain converse Barcan property obviously does
not hold in a cryptographic context.)
Corollary 1 [= K
a
(m(a k m )) m(a k m K
a
())
In words: propositional knowledge commutes with universal (and analogously
with existential) quantication when that quantication is relativised to (or:
guarded by) individual knowledge.
Remark 3 CPLsatisfaction (modelchecking) is undecidable, as secrecy, be
ing CPLdenable (cf. Section 3.3.2), is.
3.2. LOGIC 55
3.2.3 Discussion
3.2.3.1 Expressiveness
The undecidability of the modelchecking problem of CPL is intriguing because
CPL is overtly rstorder and the modelchecking problem of plain rstorder
logic is decidable, in fact PSPACEcomplete
18
[BvBW07]. The deeper reason
for this intriguing state of aairs is that CPL is actually covertly weak second
order! To see why, consider that the truth condition of the spatial conditional
() involves universal quantication over (adjoint) protocols, which, and that
is the reason, generate via their execution nite sets of messages (CPLs ocial
rstorder individuals). The implicit (at the metalevel) and indirect (via the
spatial conditional and protocols) universal quantication over nite sets of
individuals induces weak secondorder expressiveness.
19
Regarding secrecy, we
will see in Section 3.3.2 that the source of its undecidability is nicely pinpointed
by the prohibition (negated permission) modality, which employs the (negated)
spatial conditional, required for its formalisation. In CPL, weak secondorder
expressiveness is available on demand of the spatial conditional and remains
nicely conned to the use of that conditional.
3.2.3.2 Relevant implication
In the terminology of relevant logics, both the spatial conditional and the
epistemic conditional are relevant (as opposed to the truthfunctional material
conditional ) in the sense that information based on which the antecedent
is evaluated is relevant to the information based on which the consequent is
evaluated. In , the relevant (and potential ) information is represented by the
adjoint state (h
.
As an example, consider (session identier and process term omitted) the
assertion
I(Eve, [M[
k
) [= Eve k k Eve k M
which states what primary knowledge, namely k, Eve requires to derive the
(secondary) knowledge M in the given model. In other words, if Eve knew k
then Eve would know M in the given model. (Notice the conditional mode!)
This is a property of Eves cryptographic knowledge w.r.t. its potentiality. That
is, the addition of information potentially leads to multiplication of knowledge.
In comparison, consider the assertion
I(Eve, [M[
k
) I(Eve, k) [= Eve k M Eve k k
which states how Eve actually derives the secondary knowledge M from the
primary knowledge in the given model (cf. Table 3.6, where it becomes evident
that if Eve knows the plaintext M then possibly because Eve knows the key
k, because: rst, Eve can derive M from the set I(Eve, k), I(Eve, [M[
k
)
of events and k from the set I(Eve, k) of events in her view; and second,
I(Eve, k) I(Eve, k), I(Eve, [M[
k
)). In other words, if Eve knows M then
possibly (not only probably) because Eve knows k in the given model. (Notice
18
however, FOLsatisability is undecidable
19
That a certain form of spatial conjunction (conjunctive separation) also yields second
order expressiveness has been argued in [KR04].
56 CHAPTER 3. DOLEVYAO CRYPTOGRAPHY
T
a
b
l
e
3
.
6
:
D
e
r
i
v
i
n
g
a
p
l
a
i
n
t
e
x
t
I
(
E
v
e
,

[
M
[
k
)
I
(
E
v
e
,
k
)
{
I
(
E
v
e
,
k
)
}
E
v
e
(
E
v
e
,
k
)
I
(
E
v
e
,

[
M
[
k
)
I
(
E
v
e
,
k
)
{
I
(
E
v
e
,
k
)
}
E
v
e
k
I
(
E
v
e
,

[
M
[
k
)
{
I
(
E
v
e
,

[
M
[
k
)
}
E
v
e
(
E
v
e
,

[
M
[
k
)
I
(
E
v
e
,

[
M
[
k
)
{
I
(
E
v
e
,

[
M
[
k
)
}
E
v
e

[
M
[
I
(
E
v
e
,

[
M
[
k
)
I
(
E
v
e
,
k
)
{
I
(
E
v
e
,

[
M
[
k
)
}
E
v
e

[
M
[
I
(
E
v
e
,

[
M
[
k
)
I
(
E
v
e
,
k
)
{
I
(
E
v
e
,
k
)
,
I
(
E
v
e
,

[
M
[
k
)
}
E
v
e
M
3.2. LOGIC 57
the indicative mode!) This is a property of Eves cryptographic knowledge w.r.t.
its actuality. In contrast, consider the tautology (i.e., universal assertion)
[= (Eve k [M[
k
Eve k k) Eve k M
which states a property of a cryptographic operation, namely encryption. We
believe that and are (perhaps the) two natural and incidentally, relevant
notions of implication for cryptographic knowledge.
3.2.3.3 Conicting obligations
A particularly interesting use of the spatial and the epistemic conditional is the
denition of a cryptographically meaningful notion of permission (cf. Table 3.4)
and prohibition (cf. Appendix B). Our denition says that it is permitted that
is true if and only if if were true then whenever a state of violation would
be reached, it would not be due to being true. This (reductionistic) notion
of permission is inspired by [MDW94, Page 9] where a notion of prohibition
is dened in the framework of dynamic logic. The authors resume their basic
idea as . . . some action is forbidden if doing the action leads to a state of
violation. Observe that [MDW94] construe a notion of prohibition based on
actions, whereas we construe a notion of permission based on propositions. We
recall that the motivation of reductionistic approaches to (standard) deontic
logic (SDL) is the existence of weak paradoxes in SDL. That is, SDL actually
contains true statements that are counter to the normative intuition it was
originally intended to capture.
In SDL permission, prohibition, and obligation are interdenable, whereas
in CPL only permission and prohibition are. In fact, there is no notion of obli
gation in CPL because (faulty) cryptographic protocols create a context with
conicting obligations whose treatment would require machinery from defeasible
deontic logic [Nut97]. Consider that it must be obligatory that (1) a state of vio
lation be never reached during protocol execution, and (2) agents always comply
with protocol prescription. These two obligations are obviously conicting in a
context created by the execution of a faulty protocol, which by denition does
reach a state of violation.
3.2.3.4 Logical omniscience
Our semantics for the epistemic modality reconciles the cryptographically intu
itive but incomplete semantics from [AT91] with the complete (but less com
putational), renaming semantics from [CD05a]. We achieve this by casting the
cryptographic intuition from [AT91] in a simple (rulebased) and visibly com
putational formulation of epistemic accessibility. Similarly to [AT91], we parse
unintelligible data in an agents a individual knowledge M into abstract mes
sages B. In addition, and inspired by [CD05b, CD05a], we parse unintelligible
data in an agents a propositional knowledge K
a
(). Thanks to this additional
parsing, our epistemic modality avoids weak paradoxes in the context of Dolev
Yao cryptography that, like in SDL, exist in standard epistemic logic (SEL). In
the context of DolevYao cryptography, these paradoxes are due to epistemic
necessitation
[=
[= K
a
()
58 CHAPTER 3. DOLEVYAO CRYPTOGRAPHY
i.e., the fact that an agent a knows all logical truths (logical omniscience) such
as v([M[
k
= [v[
k
). To illustrate, consider the following simple example.
Let P T and M /. Then paradoxically (, P) [= K
a
(v([M[
k
= [v[
k
))
in SEL but truthfully (, P) ,[= K
a
(v([M[
k
= [v[
k
)) in CPL because [=
v(B = [v[
k
) (cf. otherwiseclause in the truth denotation of K
a
() in
Table 3.4). In a cryptographic setting, epistemic necessitation should and in
CPL does take the following form [CD05a]:
[=
[= a k M K
a
()
M is a tuple of the key values in
In the context of DolevYao cryptography, the presence of logical omni
science in SEL seems, interestingly, to be due to the absence of relevance in
the truth condition of the epistemic modality. The condition is in fact a truth
functional (metalevel) implication, which is true whenever its consequent is
true, which in turn is always the case for a tautological consequent. There
fore, any solution to the problem of logical omniscience must break the truth
functionality of the metalevel implication and make it relevant. This is pre
cisely what we do: the relevant information is represented by the history h
of protocol state p@i from the antecedent, used for cryptographic parsing in
the consequent. Note that our truth condition for the epistemic modality is
a simplication of the one of [CD05b, CD05a] in the sense that we eliminate
one universal quantier (the one over renamings) thanks to the employment of
cryptographic parsing. Further note that our epistemic modality does capture
knowledge, i.e., [= K
a
() , due to the reexivity of its associated accessibility
relation. Treating logical omniscience has a price:
Proposition 2 Logical equivalence () is not a congruence.
Proof. see Appendix A
3.2.3.5 Other connections
What is more, our (basic) location predicate a@x enables us to invent, by
macrodenition, spatial freeze quantiers (in analogy to the wellknown tem
poral freeze quantiers, which we are also able to macrodene, analogously,
in the realtime setting, cf. Section 3.4.3):
a.x
() := (a@x ) and
a.x
() :=
a.x
(), and further
a
() := x(
a.x
()) which corresponds
to the location modality @
a
[] of distributed temporal logic [CVB05]. Spa
tial freeze quantiers are, for example, useful for the macrodenition of action
predicates restricted to particular sessions, e.g., a.x
M
Eve
b :=
a.x
(a
M
Eve
b).
Finally, the popularity of strand spaces [FHG99] as an execution model for
cryptographic protocols justies that we briey compare our classical, trace
based execution model to strand spaces. According to [FHG99, Denition 2.2],
a strand space over a set of message terms (in our case /) is a set (say o)
(of strand names) with a socalled trace mapping tr : o (/)
, where
/ := +M  M / M  M / designates the set of so
called signed message terms. In our terminology, the intended meaning of a
strand (name) is the one of a located session name (a.x), and the one of a
positive (resp. negative) message term is insecure output (resp. input). With
3.3. APPLICATION: FORMALISATION CASE STUDIES 59
these intended meanings and o := a.x  a A
Eve
and x X , strands (and its
concept) are obviously strictly included in our (concept of) traces of insecure and
secure message input/output events. The inclusion is strict because [FHG99,
Denition 2.2] does not allow for secure message input/ouput.
3.3 Application: formalisation case studies
We exemplify the expressiveness of CPL on a selection of tentative formalisations
of fundamental cryptographic states of aairs. To the best of our knowledge,
(1) no other existing crypto logic is suciently expressive to allow for the de
nition of the totality of these properties, and (2) the totality of these properties
has never been expressed before in any other formalism. In fact, entire logics
(e.g., [BAN90], [SS99], [HO02]) have been designed to capture a single crypto
graphic state of aairs (e.g., authenticity, anonymity, resp. secrecy). We invite
the reader to validate our formalisations on the criteria of intuitiveness and suc
cinctness, but also to discern that the simplicity of the formalisation results is in
sharp contradistinction to the diculty of their formalisation process. However,
thanks to the empowerment that CPL confers, a formalisation process involving
such a large number of conceptual degrees of freedom has become tractable at
an engineering level. Observe that our formalisations of cryptographic states of
aairs, except for the one of key separation and those of trustrelated aairs,
involve no actions, just pure knowledge. Note that the formalisations employ
macrodened predicates (cf. Appendix B; the reader is urged to consult it) and
that (b) abbreviates disjunction of name generation, sending, and receiving
performed by b.
3.3.1 Trustrelated aairs
Maliciousness Agent b is malicious, written malicious(b), :i b knowingly per
forms a forbidden action at some time, written
((b)F(b)K
b
(F(b))).
Honesty Agent b is honest, written honest(b), :i b is not malicious, written
malicious(b).
Faultiness b is faulty, written faulty(b), :i b performs a forbidden action at
some time, written
((b) F(b)).
Prudency b is prudent, written prudent(b), :i b is not faulty, written faulty(b).
Trustworthiness Agent a trusts b, written a trusts b, :i a knows that b is
prudent, written K
a
(prudent(b)).
20
3.3.2 Condentialityrelated aairs
Shared Secret Datum M is a shared secret among agents a and b, written
M sharedSecret (a, b), :i only a and b know M, written a k M b k
M (c : A
Adv
)(c k M (c = a c = b)).
20
this is about justied trust (a rightly trusts b) as opposed to blind trust (a possibly wrongly
trusts b)
60 CHAPTER 3. DOLEVYAO CRYPTOGRAPHY
Secrecy A protocol has the (reachabilitybased) secrecy property :i the ad
versary Eve never knows any classied information, written m(F(Eve k
m) Eve k m).
Our formalisation is an instance of the pattern F , relating illegiti
mate to actual states of aairs, and expressing that if something must not
be then it actually is not. The pattern is equivalent to P.
Anonymity Agent b is anonymous to agent a in state of aairs (b) :i if
a knows that some agent is involved in then a cannot identify that
agent with b, written K
a
((c : A)((c))) K
a
((b)), which is logically
equivalent to K
a
((b)).
Data Derivation Agent b knows M
(a,b)
M := b k M
(b k M
a k M)
21
(when a = b we just write M
a
M).
NonInteraction There is absence of interaction between agents a and b, writ
ten a [ b := mm
(m
(a,b)
m
m
(b,a)
m
).
Perfect Forward Secrecy [. . .] compromise of longterm keys [k] does not
compromise past session keys [k
(k :
K
)(k
: K
1
)(k
Eve
k)
KnownKey Attack [. . .] an adversary obtains some keys used previously
and then uses this information to determine new keys. [MvOV96, Page 41],
written (k : CK)(k
: CK)(k
,= k k
Eve
k)
Agent Corruption The adversary, somehow, comes to know all what an agent
(say a) knows in state of aairs , written m(a k m (Eve k m > )).
3.3.3 Authenticationrelated aairs
Key Conrmation [. . .] one party [a] is assured that a second (possibly un
identied) party [b] actually has possession of a particular secret
22
key
[k]. [MvOV96, Page 492], written k : K K
a
(b k k)
Key Authentication
implicit: [. . .] one party [a] is assured that no other party [c] aside
from a specically identied second party [b] (and possibly additional
identied trusted parties) may gain access to a particular secret key
[k]. [MvOV96, Page 492], written k : KK
a
((c : A
Adv
)(c k k (c =
a c = b)))
explicit: [. . .] both (implicit) key authentication and key conrma
tion hold. [MvOV96, Page 492], written simply as conjunction of
implicit key authentication and key conrmation
Message Integrity Agent b knows that M is an intact message from agent a,
written K
b
(M
(a,b)
M).
21
A material conditional would not do here because the antecedent and the consequent are
epistemically and thus not truthfunctionally related via data derivation.
22
in our terminology, secret here means symmetric
3.3. APPLICATION: FORMALISATION CASE STUDIES 61
Message Authorship Agent a authored datum M, written a authored M, :i
once a was the only one to know M, written
(a k M (b : A
Adv
)(b k
M b = a)).
Message Authentication (or Authenticity) Datum M is authentic w.r.t.
its origin (say agent a) from the viewpoint of agent b :i b can authentically
attribute (i.e., in the sense of authorship) M to a, i.e., b knows that a
authored M, written K
b
(a authored M).
Key Transport (safety) between agents a and b initiated by a
unacknowledged uaKT(a, b):
(k : K)(K
b
(a authored k) K
b
(k sharedSecret (a, b)))
acknowledged aKT(a, b):
(k : K)(K
a
(K
b
(a authored k)) K
a
(K
b
(k sharedSecret (a, b))))
Key Agreement (safety) between agents a and b initiated by a
unacknowledged uaKA(a, b):
m
a
m
b
((K
b
(a authored m
a
) K
a
(b authored m
b
))
K
a
((m
a
, m
b
) sharedSecret (a, b)))
acknowledged aKA(a, b):
m
a
m
b
((K
b
(a authored m
a
) K
b
(K
a
(b authored m
b
)))
K
b
(K
a
((m
a
, m
b
) sharedSecret (a, b))))
Entity Authentication (or Identication) (safety) via a shared secret be
tween agents a and b initiated by a
unilateral (or weak) entity authentication uEA(a, b): [. . .] the pro
cess whereby one party [b] is assured (through acquisition of corrob
orative evidence [m]) of the identity of a second party [a] involved in
a protocol, and that the second has actually participated (i.e., is ac
tive at, or immediately prior to, the time the evidence is acquired).
[MvOV96, Page 386], written
m(K
b
(a authored m) K
b
(m sharedSecret (a, b)))
Notice that unilateral entity authentication is unacknowledged trans
port of an arbitrary secret, e.g., not necessarily a symmetric key.
weakly mutual (or strongweak) entity authentication wmEA(a, b):
[. . .] [one party (say a)] has fresh assurance that [the other party
(say b)] has knowledge of [a] as her peer entity. [BM03, Page 39],
written
m
a
m
b
((K
b
(a authored m
a
) K
b
(K
a
(b authored m
b
)))
K
b
(K
a
((m
a
, m
b
) sharedSecret (a, b))))
Notice that weakly mutual entity authentication coincides with ac
knowledged key agreement.
62 CHAPTER 3. DOLEVYAO CRYPTOGRAPHY
strongly mutual (or strongstrong) entity authentication smEA(a, b):
m
a
m
b
((K
a
(K
b
(a authored m
a
)) K
b
(K
a
(b authored m
b
)))
K
a
(K
b
(K
a
((m
a
, m
b
) sharedSecret (a, b)))))
Notice that our formalisations of key transport/agreement and entity authen
tication only address safety, but not liveness, i.e., that some key actually gets
transported/agreed upon and that some entity is authenticated. The reason is
that due to the adversary, liveness cannot be guaranteed.
Visibly, both key transport/agreement and entity authentication rely on
message authentication as well as a shared secret, and authenticationrelated
aairs rely on condentialityrelated aairs.
Slogan 16 Authenticity is epistemic accessibility between agents and their data.
Secrecy is epistemic inaccessibility to agents and their data. The two states of
aairs are linked.
3.3.4 Commitmentrelated aairs
Proof Datum M is a cryptographic
23
proof for the truth of proposition , writ
ten M proofFor , :i assuming an arbitrary agent a knows M guarantees
that a knows that is true, written (a : A
Adv
)(a k M K
a
()).
Evidence Datum M is cryptographic evidence for the truth of proposition ,
written M evidenceFor , :i assuming an arbitrary agent a knows that
is true guarantees that a knows M, written (a : A
Adv
)(K
a
() a k M).
Provability Agent a can prove that proposition is true, written P
a
(), :i a
knows a (cryptographic) proof for , written m(m proofFor a k m).
NonRepudiation Agent b cannot repudiate authorship of M to agent a :i
a can prove that b authored M, written P
a
(b authored M).
Notice that nonrepudiation is authenticity strengthened (from knowledge)
to provability.
Contract Signing [. . .] two players [say a and b] wish to sign a contract m
in such a way that either each player obtains the others signature [S], or
neither player does. (fair exchange of electronic signatures FEES(a, b)),
written
((a k S
b
b k S
a
) (a k S
b
b k S
a
))
Optimism: [. . .] no honest party [neither a nor b] interacts with the
trusted third party [say c]. [ASW00], written a [ c b [ c
Fairness: [. . .] it is infeasible for the adversary [Eve] to get the
honest players [a] signature [S
a
], without the honest player getting
the adversarys signature [S
Eve
]. [ASW00], written (Eve k S
a
(a k S
Eve
))
Completion: [. . .] it is infeasible for the adversary [. . .] to prevent
[a] and [b] from successfully exchanging their signatures. [ASW00],
writtten
(a k S
b
b k S
a
)
23
as opposed to propositional proof (i.e., a sequence of propositions that is compliant with
a relation of deduction); cryptographic proofs can be viewed as cryptographic encodings (i.e.,
cryptographic Godelnumberings) of propositional proofs
3.3. APPLICATION: FORMALISATION CASE STUDIES 63
Accountability: [. . .] if the trusted third party misbehaves [i.e.,
the contract signing property FEES is violated] then this can be
proven. [ASW00], written (FEES(a, b)
(P
a
(FEES(a, b))
P
b
(FEES(a, b))))
Abusefreeness: [. . .] [b] does not obtain publicly veriable informa
tion about (honest) [a] signing the contract until [b] is also bound by
the contract.
24
[GJM99], written P
b
(a authored S
a
)Ub authored S
b
It has been argued that contract signing requires branching time [CKW07].
However, our tentative formalisation of contract signing suggests that
branchingtime logic is not necessary for this purpose. It has even been ar
gued that lineartime is preferable (implying sucient) over branching
time logic in general [Var01]. We shall not settle this argument here, but
conne ourselves to alimenting it. In any case, it would be easy to replace
CPLs lineartime skeleton with a branchingtime skeleton such as CTL
.
Visibly, cryptographic proof and evidence are dual concepts, and commitment
related aairs rely on authenticationrelated aairs.
Then, we have actually been able to macrodene a Godelstyle provability
modality, and, with it, are able to macrodene the intuitionistic conditional in
CPL!
Theorem 2 The operator P
a
is compliant with the modal system S4 adapted to
DolevYao cryptography (i.e., with the necessitation rule N replaced by N
DY
)
25
.
Proof. P
a
complies with (cf. Appendix A for an elementary, Fitchstyle proof)
K [= P
a
(
) (P
a
() P
a
(
))
T [= P
a
()
4 [= P
a
() P
a
(P
a
())
N
DY
[=
[= a k M P
a
()
M is a tuple of the key values in
Hence, (the classical logic) CPL can capture the provability meaning of intu
itionistic implication via the following macrodenition:
:= (a : A
Adv
)(P
a
(
))
The intuitionistic conditional is another example of relevant implication: infor
mation (a proof of ) based on which the antecedent is evaluated is relevant to
the information (a proof of
(cf. K).
The obvious temptation is to attempt a CurryHoward isomorphism [dG95]
between cryptographic protocols and propositions. That is, to look
24
symmetrically for (honest) [b]
25
As P
a
is dened in terms of K
a
, P
a
is compliant with S4 simpliciter when K
a
is compli
ant with S5 simpliciter. Our K
a
can be (re)made compliant with S5 simpliciter by simply
removing the treatment of logical omniscience (i.e., the cryptographic parsing) in its denition.
64 CHAPTER 3. DOLEVYAO CRYPTOGRAPHY
1. at a proposition T for which there are (h, P), (h
, P
) H T, a
A
Eve
, and M / s.t. (h, P) (h
, P
) and (h
, P
) [= M proofFor
a k M as a type for process term P, and
2. at process term P as an interactive proof procedure (to the benet of agent
a) for the cryptographic proof M of .
Our (macrodened) concepts of cryptographic proof and provability are
related to [AN05], where a notion of justication for propositional knowledge
is introduced as a primitive concept in the (propositional) epistemic logic S4
resulting in a hybrid modality for both knowledge and provability. That notion of
justication roughly corresponds in our (rstorder, epistemicS5) setting to the
notion of cryptographic proof. However, [AN05] is currently not quite suitable
for cryptography due to standard epistemic necessitation and an unsuitable
form of positive introspection, namely the one that the existence of a proof of
a proposition implies the (hybrid) knowledgeprovability of that proposition.
Hence, given that Godels 1933 paper on a modal logic of provability left the
26
open problem of nding a precise provability semantics for the modal logic S4
[BvBW07, Page 932], we can justly claim having solved via macrodenition,
i.e., via syntactic translation, a cryptographic analogue of that problem. Godels
problem was solved in its original, noncryptographic format in [Art95, Art01].
3.3.5 Compositionalityrelated aairs
Key Separation The protocol space can be separated in an establishment
(production) and a use (consumption) part w.r.t. the key k, written
m(((a, b : A)(a
m
Eve
b) k
m) k
m)
m(((a, b : A)(a
m
Eve
b) k
m) k
m)
Compositional Correctness Protocol (plugin) P with prehistory h is
1. solely correct w.r.t. an internal correctness criterion, i.e., endocondi
tion :i (h, P) [=
2. compositionally correct, i.e., either
(a) existentially composable w.r.t. an external correctness criterion,
i.e., exocondition
:i (h, P) [=
> ,
27
or
(b) conditionally composable, i.e., composable w.r.t. exocondition
, :i (h, P) [=
, or
(c) universally composable :i (h, P) [= .
28
The concept of an exocondition (endocondition) is to interactive
programs what a precondition (postcondition) is to noninteractive
programs.
29
Our slogan, especially applying to cryptographic proto
cols, is:
26
actually two open problems (cf. [BvBW07, Page 932])
27
the case where
is is obviously uninteresting
28
the name of this notion of correctness coincides with the one from [Can01], and should
roughly correspond to the notion of robust satisfaction [GL91]
29
(h, P) =
:i (h, P) [=
> .
Notice that a statement of an attack scenario is a negated statement of
conditional composability.
Remark 4 The concept of a chosenprotocol attack [KSW98], understood
as the adversarial choice of a dierent (attacking) protocol than P is an
instance of the concept of an attack scenario, and understood as the adver
sarial choice of an arbitrary attacking protocol coincides with the concept
of an attack scenario.
3.3.5.1 A popular attack scenario
We exemplify our concept of attack scenario with the perhaps most popular
attack on a cryptographic protocol, namely the maninthemiddle attack on
the NeedhamSchroeder publickey protocol (NSPuK) for (weakly mutual) en
tity authentication (acknowledged key agreement). Our choice is motivated by
the fact that we wish to explain the unfamiliar (our approach) with the famil
iar (a paradigmatic attack). Notwithstanding the popularity of the attack, we
believe that its contextual formalisation in CPL explicates it to a novel extent
of explicitness. The attack is also particularly interesting because the protocol
requirement that it violates is particularly challenging to formalise satis
factorily. We contend that common formulations of entity authentication are
unsatisfactory. They usually purport to formalise an intuition expressed as I
know who Im talking to.. However the actual formulations then only involve
belief to varying degrees of explicitness [Low97]. Our slogan, and fact, is:
Slogan 18 Debatable requirements entail debatable attacks.
Table 3.7 displays the protocol narration (i.e., an intended run) of core
NSPuK, i.e., NSPuK where the public keys of the initiator (e.g., Alice) and
the responder (i.e., Bob) are assumed to have already been established. The
Table 3.7: Protocol narration for core NSPuK
1. Alice Bob : [(x
Alice
, Alice)[
+
p
+
Bob
2. Bob Alice : [(x
Alice
, x
Bob
)[
+
p
+
Alice
3. Alice Bob : [x
Bob
[
+
p
+
Bob
narration describes (elliptically) that rst, Alice sends to Bob the encryption
under Bobs public key p
+
Bob
of a tuple of a freshlygenerated nonce x
Alice
and her
name Alice; (upon reception, Bob decrypts the message with his private key,
stores the rst component of the tuple, gets the public key p
+
Alice
corresponding
66 CHAPTER 3. DOLEVYAO CRYPTOGRAPHY
to the second component from his key store, generates a fresh nonce x
Bob
, and
encrypts the tuple of Alices and his nonce with Alices public key;) second, Bob
sends his reply to Alice; (upon reception, Alice decrypts the message with her
private key, checks that the rst component of the tuple is her nonce previously
sent to Bob, and encrypts the second component x
Bob
with Bobs public key
p
+
Bob
;) third, Alice sends her reply to Bob. Protocol narrations are elliptical in
the sense that noninteractive protocol actions are visibly not explicit.
The intention of each protocol step is as follows: the intention of the rst
step is to challenge the responder (e.g., Bob) to authenticate with the initiator
(e.g., Alice); the intention of the second step is twofold, i.e., to accomplish au
thentication of the responder with the initiator, and to challenge the initiator to
authenticate with the responder; the intention of the third step is twofold, i.e.,
to acknowledge authentication of the responder with the initiator to the respon
der, and to accomplish authentication of the initiator with the responder. The
protocol intends to achieve weakly (due to the uni lateral acknowledgement) mu
tual entity authentication (acknowledged key agreement) between an initiator
and a responder.
The protocol narration of NSPuK can be transcribed into a (nonelliptic)
formal language, for example into the one of Section 4.1 by instantiating the
protocol template displayed in Table 3.8 via substitution of Alice for init and
Bob for resp. Features of that language are: a primitive for key lookup, an
input primitive with patternmatching and guard, and primitives for outof
band communication. The left (right) column of the table denes the ini
Table 3.8: Protocol template for core NSPuK
NSPuK
INIT
(slf , oth) := NSPuK
RESP
(slf ) :=
New (x
slf
: X).
Get
oth
(k
oth
: K
+
, oth) in Get
slf
(k
slf
: K
, slf ) in
Out
oth
[(x
slf
, slf )[
+
k
oth
. In [(x
oth
, oth)[
+
k
slf
when x
oth
: X oth : A.
New (x
slf
: X).
Get
slf
(k
slf
: K
, slf ) in Get
oth
(k
oth
: K
+
, oth) in
In [(x
slf
, x
oth
)[
+
k
slf
when x
oth
: X. Out
oth
[(x
oth
, x
slf
)[
+
k
oth
.
Out
oth
[x
oth
[
+
k
oth
.1 In [x
slf
[
+
k
slf
.1
NSPuK(init, resp, x
init
, x
resp
) := init.x
init
[ NSPuK
INIT
(init, resp) ]
resp.x
resp
[ NSPuK
RESP
(resp) ]
tiator (responder) role. The bottom row denes the protocol template, dis
tributing (via parallel composition) the roles at the corresponding locations
init.x
init
[ ] and resp.x
resp
[ ], respectively. The protocol template assumes that
each agent has generated her own private and public key, and that each agents
public key has been established with the other agent. The actions of the ini
tiator role are the following: New (x
slf
: X) generation and binding in vari
able x
slf
of a new nonce; Get
oth
(k
oth
: K
+
, oth) in look up and binding
in variable k
oth
of the other agents (cf. subscript oth) public key gener
ated by the other agent herself (cf. parameter oth); Out
oth
[(x
slf
, slf )[
+
k
oth
out
put of the message [(x
slf
, slf )[
+
k
oth
to the other, hopefully responding, agent;
3.3. APPLICATION: FORMALISATION CASE STUDIES 67
Get
slf
(k
slf
: K
. Eve
Alice
Bob : [(x
Alice
, Alice)[
+
p
+
Bob
2
. Bob Eve
Alice
: [(x
Alice
, x
Bob
)[
+
p
+
Alice
2. Eve Alice : [(x
Alice
, x
Bob
)[
+
p
+
Alice
3. Alice Eve : [x
Bob
[
+
p
+
Eve
3
. Eve
Alice
Bob : [x
Bob
[
+
p
+
Bob
orchestrated by an active insider adversary that performs denial of service and
impersonation across two dierent, interleaved sessions, cf. (un)primed number
ing. It consists in:
30
with patternmatching eectuating the identity check on the received nonce
68 CHAPTER 3. DOLEVYAO CRYPTOGRAPHY
1. Eve tricking (wrongly trusting) Alice (believing that Eve is a legitimate
agent) to initiate a regular session
Q := Alice.x
a2
[ NSPuK
INIT
(Alice, Eve) ]
with Eve
2. Eve disabling the execution (denial of service) of the regular session initi
ation
Alice.x
a1
[ NSPuK
INIT
(Alice, Bob) ]
3. Eve impersonating Alice in the face of (wrongly trusting) Bob (lead to
believe that he is talking only to Alice while in fact talking also to Eve)
by enabling the execution of the regular session response
Bob.x
b1
[ NSPuK
RESP
(Bob) ]
concurrently with Q.
In result, Alice is lead to believe that she is talking only to Eve (via session x
a2
)
while in fact talking also to Bob (via impersonator Eve and session x
b1
), and
Bob is lead to believe that he is talking only to Alice (via session x
b1
) while in
fact talking also to Eve (via impersonator Eve and session x
a1
). The protocol
obviously fails to achieve its requirement.
The assumption about private and publickey generation and publickey
establishment is, of course, also valid for Eve and regular interactions between
Alice and Eve, respectively. That is, the protocol context is assumed to con
tain the prehistory h
:= N(Eve, x
e0
, p
Eve
, Eve) sO(Eve, x
e0
, p
+
Eve
, Alice)
sI(Alice, x
a0
, p
+
Eve
, Eve) sO(Eve, x
e0
, p
+
Eve
, Bob) sI(Bob, x
b0
, p
+
Eve
, Eve). More
formally,
(h
, Q) HT and
(h
, NSPuK(Alice, Bob, x
a1
, x
b1
) Q) [= wmEA(Alice, Bob)
by which we obtain
(h, NSPuK(Alice, Bob, x
a1
, x
b1
)) [= uEA(Alice, Eve) > wmEA(Alice, Bob)
representing our (propertybased or logical) attack scenario for NSPuK. We
invite the reader to compare this scenario to the corresponding, modelbased
(or processalgebraic) attack scenario described in Section 4.1.4.
3.4 tCPL: an extension of CPL with real time
We extend (core) CPL (qualitative time) with real time, i.e., time stamps, timed
keys, and potentially drifting local clocks, to tCPL (quantitative time). Our ex
tension is conservative and really simple (a single section is enough to describe
it!). It requires only the renement of two relational symbols (one new dening
rule resp. parameter) and of one modality (one new conjunct in its truth condi
tion), and the addition of two relational symbols (but no operators!). Our work
3.4. TCPL: AN EXTENSION OF CPL WITH REAL TIME 69
thus provides further evidence for Lamports claim that adding real time to an
untimed formalism is really simple [Lam05]. The specialpurpose machinery for
timed (including cryptographic) settings need not be built from scratch nor be
heavyweight.
3.4.1 Historical and topical context
The formal specication, modelling, and verication of generalpurpose timed
systems has received considerable attention from the formal methods commu
nity since the end of the nineteeneighties. See [Wan04] for a survey of timed
system models (automata, Petri nets), model and propertybased specication
languages (process calculi, resp. logics), and verication tools; and [BMN00] for
a survey of timed propertybased specication languages (logics).
However, the formal methods community has paid comparatively little, and
only recent (since the end of the nineteennineties), attention to the timed as
pects of cryptographic systems, e.g., cryptographic protocols, which due to their
complexity deserve specialpurpose models, and formalisms
31
for their specica
tion and verication.
We are aware of the following specialpurpose formalisms for timed crypto
graphic protocols.
Modelbased formalisms (process calculi): [ES00], [GM04], [HJ05] with
discrete time; [Sch99], [BEL05], and our own contribution (cf. Section 4.2)
with dense time
Propertybased formalisms (logics): interval based [HS04a]; timeparame
trised epistemic modalities [KM99] and a secondorder logic [BEL05] both
pointbased, and our hereby presented logic tCPL allowing for both tem
poral points and intervals.
Clearly, [d]ensetime models are better for distributed systems with multiple
clocks and timers, which can be tested, set, and reset independently. [Wan04].
Specically in cryptographic systems, [c]locks can become unsynchronized due
to sabotage on or faults in the clocks or the synchronization mechanism, such
as overows and the dependence on potentially unreliable clocks on remote sites
[. . .] [Gon92]. Moreover, [e]rroneous behaviors are generally expected during
clock failures [. . .] [Gon92].
Timed logics can be classied w.r.t. their order and the nature of their
temporal domain.
Order Propositional logic is simply too weak for specication purposes (but
is good for fullyautomated, approximative verication); modal logics provide
powerful abstractions for specication purposes, but are still not expressive
enough (cf. Section 3.1.2); higherorder logics are too expressive at the cost of
axiomatic and algorithmic incompleteness (but are good as logical frameworks);
nally [f]irstorder logics seem a good compromise between expressiveness and
computability, since they are [axiomatically] complete in general. [Wan04]. We
31
In our view, a formalism consists of exactly three components: a formal (e.g., program
ming or logical) language, a mathematical model (or interpretation structure), and a formal
semantics (e.g., eect or truth) for the language in terms of the model.
70 CHAPTER 3. DOLEVYAO CRYPTOGRAPHY
recall that core CPL is a rstorder, polydimensional modal (norms, knowledge,
space, qualitative time) logic.
Temporal domain We recall that core CPL can be instantiated with a transi
tive, irreexive, linear and bounded in the past, possibly branching (but a priori
attened) and unbounded (depending on the protocol) in the future, discrete
(due to eventinduced protocol states) temporal accessibility relation (cf. Sec
tion 4.1). That is, CPL has a hybrid (state and eventbased) temporal domain:
[. . . ] neither pure statebased nor pure eventbased languages quite support
the natural expressiveness desirable for the specication of realworld systems
[. . . ] [Wan04]. tCPL can be instantiated with a temporal accessibility relation
that additionally accounts for quantitative time (cf. Section 4.2). That is, time is
(1) rationalnumber valued, yielding a dense temporal grain; (2) referenced ex
plicitly (the truth of a timed formula does not depend on its evaluation time),
but implicittime operators are macrodenable (cf. Section 3.4.3); (3) mea
sured with potentially drifting local clocks (one per agent), where the (standard
DolevYao) adversarys local clock has drift rate 1; (4) advanced monotonically
by letting the adversary choose the amount by which she desires to increase
her local clock (de facto the system clock); and (5) determinant for adversarial
break of shortterm keys, enabled jointly by key expiration and ciphertextonly
attacks (the weakest reasonable attack).
Rational versus real numbers Cryptographic messages have nite length,
which implies that real numbers, e.g., realvalued time stamps, are not
transmittable as such, and real clocks only have nite precision.
Timed adversary model Our model amounts to a natural generalisation of
the adversarys scheduling power from the control of the (relative) tempo
ral order of protocol events in the network (space) to the control of their
(absolute) temporal issuing (time).
The following section describes the extension of CPL to tCPL. The extension
depends on the core described in the previous sections (the reader is urged to
consult them) and parallels the extension from C
3
(cf. Section 4.1) to tC
3
(cf.
Section 4.2).
3.4.2 Extension
The notion of execution from Section 4.2, which we adopt as the temporal ac
cessibility relation for tCPL, generates the following two kinds of timed events:
N(a, x, n, (o, V )) for the generation of name n with intended owners o and tem
poral validity V := (t
b
, t
e
) for the declaration of the intended beginning (t
b
) and
end (t
e
) of validity of the generated name (typically a key) by agent a in session
x, and S(a, x, t) for the setting of as local clock to clock value t by a in session
x. By convention, these events are unobservable by the adversary, i.e., they are
secure. t (1 := Q denotes clock values having the associated type CV, and
t
b
, t
e
T 1 := (1 , denote time values having the associated type
TV. Time values are transmittable as messages.
The syntactic and semantic novelties are the following:
1. addition of two new, binary relational symbols and @ (overloading the
session locality symbol) forming atomic formulae E E
E + E
i
p
:= (E is smaller than or equal to E
, )
where designates the obvious evaluation function from temporal ex
pressions to time values (not to be confused with the function of truth
denotation
i
p
); and
E@a
i
p
:= (E = t +
a
, S(a, x, t), S(Eve, B, t
i
))
where
t designates the clock value of as last clockset event in h, i.e., there
are h
1
, h
2
, x s.t. h = h
1
S(a, x, t) h
2
and there is no x
, t
s.t.
S(a, x
, t
)
h
2
a
T 1 designates the drift rate of as local clock
designates the temporal dierence between Eves last clockset
event before S(a, x, t) and Eves last clockset event so far in h, i.e.,
=
_
_
t
2
t
1
if for i 1, 2 there are h
i
, h
i
, t
i
s.t.
h
i
= h
i
S(Eve, B, t
i
) h
i
and there is no t
i
s.t.
S(Eve, B, t
i
)
h
i
, and
0 otherwise.
B serves as a dummy session identier for Eves clockset events
2. renement (i.e., one new parameter) of the relational symbol for new
name generation with a validity tag V := (t
b
, t
e
) for the declaration of
the intended beginning (t
b
T 1) and end (t
e
T 1) of validity of the
generated name (typically a key). Its truth denotation is the following:
a n.o.V )
i
p
:= (c , = , c) where c :=
xX
N(a, x, n, (o, V ))
h
3. renement (i.e., adding of one new dening rule) of the relation
E
a
E
Eve
[M[
k
):
h
E
Eve
[M[
k
h
E
Eve
k
h
[= t@Eve and
h [= expired(k)
t
v
(t
v
validityOf k t
n
(t
n
@Eve t
v
< t
n
t))
where t
v
designates the duration of validity of the considered key (i.e., the
strength of the key, corresponding to its length in a bitstring representa
tion), and t
n
t the duration of the attack on the considered key (i.e., the
time during which the corresponding ciphertext has been known to the
adversary, and during which the adversary has potentially been attacking
72 CHAPTER 3. DOLEVYAO CRYPTOGRAPHY
i.e., performing computations on the ciphertext in order to recover
the desired key); and
expired(k) := t
n
(t
n
@Eve t
e
(k validUntil t
e
t
e
< t
n
))
k validUntil t
e
:= t
b
(k validBetween (t
b
, t
e
))
k validBetween (t
b
, t
e
) := ao(a k.o.(t
b
, t
e
))
t
v
validityOf k := k validBetween (t
b
, t
e
) t
e
t
b
= t
v
4. renement (i.e., one new conjunct) of the state of violation with key
expiration in the truth condition of the permission modality (cf. Table 3.4):
:= (k : CK)(Eve k k k ck Eve expired(k) )
3.4.3 Expressiveness
We demonstrate the expressiveness of tCPL on the macrodenability of impor
tant modalities from generalpurpose timed logics:
pointparametrised futuretime (similarly for pasttime) modalities (so
called freeze quantiers):
t
() := (t@Eve )
t
() :=
t
()
interval parametrised futuretime (similarly for pasttime) modalities with
an:
absolutetime understanding of closed (similarly for open) intervals
[t
1
, t
2
]:
[t
1
,t
2
]
() := t(t
1
t t
2
t
())
[t
1
,t
2
]
() :=
[t
1
,t
2
]
()
understanding of intervals that is relative to the current time t@Eve:
[]
() := t(t@Eve
[t,t+]
())
[]
() := t(t@Eve
[t,t+]
())
the chop connective:
[t,t
:= t
(
[t,t
]
()
[t
,t
]
(
))
durations [ZHR91], [ZH04] (cf. Table 3.11)
The cryptographic states of aairs involving qualitative temporal modalities
from Section 3.3 can easily be quantitatively adapted by replacing the qualitative
temporal modalities by the above quantitative ones with actual time values
(points and/or intervals) as desired.
3.4. TCPL: AN EXTENSION OF CPL WITH REAL TIME 73
Table 3.11: Denability of durations
duration
(t,t
)
:=
t
( duration
t
)
t
( duration
t
)
duration
t
:= ( t
d
(t
d
@Eve
_+(( t
m
((t
m
@Eve t
m
t
)
(t
m
t
d
) duration
t
))
( _+( duration
t
)))))
( _+( duration
t
))
3.4.4 Application: a timed attack scenario
We exemplify our concept of attack scenario in the timed setting with another
popular attack on a cryptographic protocol, namely the maninthemiddle at
tack on the WideMouthedFrog protocol (WMF) (cf. Table 3.12). WMF is a
serverbased, (session) keytransport protocol employing symmetric cryptogra
phy intended to guarantee timely, unacknowledged transport of a session key be
tween an initiator and a responder mediating a trusted third party (the server).
Timeliness of key transport means that the responder only accepts session keys
within a xed interval of time. The protocol presumes that the longterm sym
Table 3.12: Protocol narration for WMF
1a. Alice Trent : Alice
1b. Alice Trent : [((t
Alice
, Bob), k
AliceBob
)[
k
AliceTrent
2. Trent Bob : [((t
Trent
, Alice), k
AliceBob
)[
k
BobTrent
metric keys (e.g., k
AliceTrent
and k
BobTrent
) between the initiator (Alice) and
the server (Trent) and between the responder (Bob) and the server have al
ready been generated by the server and established with all other corresponding
clients.
The intention of each protocol step is as follows: the intention of the rst
step is to announce the initiator to the server; the intention of the second step
is twofold, i.e., to transport the session key (e.g., k
AliceBob
) from the initiator to
the server and to solicit the server to transport the session key to the responder;
the intention of the third step is twofold, i.e., to transport the session key from
the server to the responder and to transmit from the server to the responder
the intention of the initiator to communicate securely with the responder by
means of the transported session key. The time stamps are from the initiators
and the servers local clock, respectively. Their purpose is to ensure freshness
of the session key.
The protocol narration can be transcribed into a formal language, for exam
ple into the one of Section 4.2, a timed extension of the one of Section 4.1, by
instantiating the protocol template displayed in Table 3.13 via substitution of
Alice for init, Trent for serv, and Bob for resp; and choice of a positive time
value for
v
, i.e., half the desired duration of validity of the transported key.
Features of that language are: a doublepurpose primitive for lookup of stored
74 CHAPTER 3. DOLEVYAO CRYPTOGRAPHY
T
a
b
l
e
3
.
1
3
:
P
r
o
t
o
c
o
l
t
e
m
p
l
a
t
e
f
o
r
W
M
F
W
M
F
I
N
I
T
(
s
l
f
,
s
r
v
,
o
t
h
,
v
)
:
=
W
M
F
S
E
R
V
(
s
l
f
,
v
)
:
=
W
M
F
R
E
S
P
(
s
l
f
,
s
r
v
,
v
)
:
=
G
e
t
s
l
f
(
t
s
:
C
V
,
B
)
i
n
N
e
w
(
k
s
o
:
K
,
(
(
s
l
f
,
o
t
h
)
,
(
t
s
,
t
s
+
v
+
v
)
)
)
.
G
e
t
s
r
v
(
k
s
s
:
K
,
(
s
l
f
,
s
r
v
)
)
i
n
O
u
t
s
r
v
s
l
f
.
I
n
f
s
t
w
h
e
n
f
s
t
:
A
.
G
e
t
s
l
f
(
k
s
f
:
K
,
(
s
l
f
,
f
s
t
)
)
i
n
O
u
t
s
r
v

[
(
(
t
s
,
o
t
h
)
,
k
s
o
)
[
k
s
s
.
1
I
n

[
(
(
t
,
s
n
d
)
,
k
e
y
)
[
k
s
f
w
h
e
n
t
:
T
V
t
s
(
t
s
:
T
V
t
s
@
s
l
f
t
+
t
s
)
s
n
d
:
A
k
e
y
:
K
.
G
e
t
s
l
f
(
k
s
s
:
K
,
(
s
l
f
,
s
n
d
)
)
i
n
G
e
t
s
r
v
(
k
s
s
:
K
,
(
s
l
f
,
s
r
v
)
)
i
n
O
u
t
s
n
d

[
(
(
t
s
,
f
s
t
)
,
k
e
y
)
[
k
s
s
.
1
I
n

[
(
(
t
,
o
t
h
)
,
k
e
y
)
[
k
s
s
w
h
e
n
t
:
T
V
t
s
(
t
s
:
T
V
t
s
@
s
l
f
t
+
t
s
)
o
t
h
:
A
k
e
y
:
K
.
1
W
M
F
(
i
n
i
t
,
s
r
v
,
r
e
s
p
,
x
i
n
i
t
,
x
s
e
r
v
,
x
r
e
s
p
,
v
)
:
=
i
n
i
t
.
x
i
n
i
t
[
W
M
F
I
N
I
T
(
i
n
i
t
,
s
r
v
,
r
e
s
p
,
v
)
]
s
r
v
.
x
s
r
v
[
W
M
F
S
E
R
V
(
s
r
v
,
v
)
]
r
e
s
p
.
x
r
e
s
p
[
W
M
F
R
E
S
P
(
r
e
s
p
,
s
r
v
,
v
)
]
3.4. TCPL: AN EXTENSION OF CPL WITH REAL TIME 75
keys and (local) time, an input primitive with patternmatching and guard,
and primitives for outofband communication. The left (right) column of the
table denes the initiator (responder) role, and the middle column the server
role. The bottom row denes the protocol template, distributing (via parallel
composition) the roles at the corresponding locations init.x
init
[ ], srv.x
srv
[ ],
and resp.x
resp
[ ], respectively. Observe that lookup of local time is done in
two dierent ways, namely imperatively by means of the getinstruction (with
B serving as a dummy owner), and declaratively by means of the @predicate.
The previously mentioned assumption about preliminary symmetric key gen
eration and establishment can be modelled by means of corresponding key
generation and outofband communication events, chained up to form the pro
tocol prehistory displayed in Table 3.14. Observe that the prehistory includes
set events for the resetting of all local clocks (with B serving as a dummy session
identier for Eves set event).
Table 3.14: Prehistory for WMF
h := N(Trent, x
t0
, k
AliceTrent
, ((Trent, Alice), (, )))
N(Trent, x
t0
, k
BobTrent
, ((Trent, Bob), (, )))
sO(Trent, x
t0
, k
AliceTrent
, Alice) sI(Alice, x
a0
, k
AliceTrent
, Trent)
sO(Trent, x
t0
, k
BobTrent
, Bob) sI(Bob, x
b0
, k
BobTrent
, Trent)
S(Eve, B, 0) S(Alice, x
a0
, 0) S(Bob, x
b0
, 0) S(Trent, x
t0
, 0)
This completes the denition of the initial state
(h, WMF(Alice, Trent, Bob, x
a1
, x
t1
, x
b1
,
v
))
of (our attack scenario for) WMF.
Table 3.15 displays the narration of the actual attack. The attack can be
orchestrated by an active outsider adversary that performs interception, imper
sonation, and reection (i.e., replay to the same agent) across three dierent,
interleaved sessions. However, the attack does not exploit drifting of local clocks
(i.e., all drift rates are 1). It consists in:
1. Eve impersonating Bob in the face of Trent by reecting back to Trent a
previously intercepted service reply [((t
Trent
, Alice), k
AliceBob
)[
k
BobTrent
Table 3.15: Attack narration for WMF
1a
. Eve
Bob
Trent : Bob
1b
. Eve
Bob
Trent : [((t
Trent
, Alice), k
AliceBob
)[
k
BobTrent
2
. Trent Eve
Alice
: [((t
Trent
, Bob), k
AliceBob
)[
k
AliceTrent
1a
. Eve
Alice
Trent : Alice
1b
. Eve
Alice
Trent : [((t
Trent
, Bob), k
AliceBob
)[
k
AliceTrent
2
Trent
, Alice), k
AliceBob
)[
k
BobTrent
76 CHAPTER 3. DOLEVYAO CRYPTOGRAPHY
perceived as a service request from Bob by (forgetful) Trent from Trent
to Bob to a service request from Alice
2. Eve intercepting Trents service reply [((t
Trent
, Bob), k
AliceBob
)[
k
AliceTrent
destined to Alice
3. Eve impersonating Alice in the face of Trent by reecting back to Trent
Trents service reply destined to Alice perceived as a service request
from Alice by (forgetful) Trent and Trent marshalling the corresponding
service reply [((t
Trent
, Alice), k
AliceBob
)[
k
BobTrent
to Bob.
In result, Bob accepts a session key that possibly is stale due to Eve achieving
rst delay of key delivery through repeated reection of service replies from
Trent back to Trent, and second prolongation of key validity through Trent,
who, on each reection, trustingly restamps the key with a new time stamp
(cf. t
Trent
and t
Trent
) of his, each time more advanced, local clock. The session
key necessarily is stale when Eve delays each reection by
v
time units. In
sum, the protocol fails to achieve its requirement of timely, unacknowledged key
transport between initiating Alice, mediating Trent, and responding Bob.
More formally, let
tuaKT
(a, b) := (k : K)((K
b
(a authored k) K
b
(k sharedSecret (a, b)))
[]
(a authored k))
Q := Trent.x
t2
[ WMF
SERV
(Trent,
v
) ]
Trent.x
t3
[ WMF
SERV
(Trent,
v
) ]
Then:
(h, Q) HT and
(h, Q) [= tuaKT
v
(Eve, Trent) tuaKT
v
(Eve, Trent) and
(h h, WMF(Alice, Trent, Bob, x
a1
, x
t1
, x
b1
,
v
) Q) [=
tuaKT
v
+
v
(Alice, Bob)
by which we obtain
(h, WMF(Alice, Trent, Bob, x
a1
, x
t1
, x
b1
,
v
)) [=
(tuaKT
v
(Eve, Trent) tuaKT
v
(Eve, Trent)) >
tuaKT
v
+
v
(Alice, Bob)
representing our (propertybased or logical) attack scenario for WMF. We in
vite the reader to compare this scenario to the corresponding, modelbased (or
processalgebraic) attack scenario described in Section 4.2.2.
Chapter 4
Calculus of Cryptographic
Communication
We exemplify the temporal accessibility relation (HT)
2
of CPL with a
reduction relation, dened by a reduction calculus
1
C
3
(or operational semantics
in the jargon of formal program semantics), on protocol states s HT.
Based on the operational semantics, we dene an observational equivalence
a
(H T)
2
on protocol states w.r.t. some observing agent a A
Eve
. The
purpose of that observational equivalence is algebraic analysis of cryptographic
protocols. We illustrate this purpose on the application of the observational
equivalence to the algebraic analysis of the attack scenario analysed logically in
Section 3.3.5.1. Further, we extend C
3
with real time to tC
3
, and illustrate the
use of this timed calculus on the application of the (timed) observational equiv
alence to the algebraic analysis of the timed attack scenario analysed logically
in Section 3.4.4. Furthermore, we dene a denotational semantics of crypto
graphic protocols. The purpose of denotational semantics in general is to dene
meaning in our case, the meaning of a cryptographic protocol. From the
meaning of a cryptographic protocol, we obtain natural denitions of the con
cepts of (1) a protocol invariant, (2) protocol safety, (3) protocol renement,
and (4) protocol information content.
Codesign The programming language T for cryptographic protocols that we
dene is complementary to the logical language T of CPL. The complementar
ity of the two languages is the result of ve natural, but notwithstanding novel
(except for Item 4 and 5) integrating design decisions: (1) dene the meaning
of a cryptographic protocol (its denotational semantics) in terms of the mean
ing of the cryptographic messages it produces during its execution, i.e., dene
the what (denotation) in terms of the how (operation); (2) dene the meaning
of a cryptographic message in terms of the propositional knowledge a protocol
agent would acquire from the (individual ) knowledge of that message; (3) de
ne dynamic observational equivalence (indistinguishability of execution paths)
in terms of static observational equivalence (indistinguishability of execution
1
In general, a calculus is a set of axioms and rules inductively dening a set. Typically, the
dened set is a binary relation, e.g., a relation of deduction (a proof system for some logical
language) or reduction (an operational semantics for some programming language).
77
78 CHAPTER 4. CALCULUS OF CRYPTOGRAPHIC COMMUNICATION
states); (4) identify static observational equivalence with epistemic accessibility
a
(H T)
2
(the semantics of propositional knowledge); and (5) identify
the operational semantics (protocol execution) with temporal accessibility (the
semantics of temporal propositions).
From the (denotational) meaning of a cryptographic message, we obtain (1)
an equational denition of its contextsensitivity, and (2) a formalisation of the
rst of Abadi and Needhams principles for prudent engineering practice for
cryptographic protocols. Last but not least, we show that protocol agents can
be conceived as evolving Scott information systems.
4.1 Core calculus
4.1.1 Syntax
Our programming language T for cryptographic protocols provides highlevel
linguistic abstractions P for the computation and agentbased communication
of cryptographic messages M /. We refer to its programs P T as C
3

processes. Our communication model is based on agents rather than channels
for the sake of separating specication (highlevel) from implementation (low
level) concerns.
C
3
processes are parallel compositions of located threads. A nonidle thread
T located at the agent c and session x, written c.x[ T ], has either an action
prex or a lookup prex. The action prexes Out
a
F and sOut
a
F stipulate
insecure (intercepted by the adversary) resp. secure (unobservable by the ad
versary) output of F
2
to a; In when and sIn
a
when stipulate insecure
resp. secure input (from a) of a message matching the pattern and having the
property ; and New (v : , O) stipulates the generation and binding to the vari
able v of a fresh name of type tagged with O, where O (a tuple of agent names)
stipulates intended ownership. The lookup prex Get
a
(v : , O) in stipulates
the lookup and binding to v of a name of type generated by a with ownership
tag O.
Denition 10 (C
3
processes) C
3
processes P T are dened in Table 4.1.
There, a, b A 1. A process P is epistemically local :i for all located
threads c.x[ T ] in P and for all a n.O and a k F in T, a = c. Socalled
implementation processes must be epistemically local, whereas socalled speci
cation processes need not be. In addition, in implementation processes v may
not bind v in any F, whereas in specication processes this need not be.
Action prexes , as opposed to the lookup prex, generate events when
executed. Action prexes for secure I/O generate unobservable events; they
model outofband communication such as trusted couriers, personal contact
between communicating parties, and dedicated communication links. The same
prexes can also be used for (1) encoding extensions to the core calculus, such
as vertical composition, i.e., subprotocol calls (cf. [BKN06, Section 3.2]), and
conditionals (i.e., execution guards); (2) dening specication processes relied
upon by equivalencebased specication of secrecy `a la SpiCalculus; and (3)
dening initialisation traces (cf. Table 3.9 and 3.14). The purpose of including
2
recall that F denotes message forms, i.e., messages with variables, which are used in
processes where they may instantiate to (transmittable) messages
4.1. CORE CALCULUS 79
Table 4.1: C
3
processes
P ::= c.x[ T ]
P P
T ::= 1
.T
Get
a
(v : , O) in T
::= Out
a
F
sOut
a
F
In when
sIn
a
when
New (v : , O)
::= F
(, )
[[
F
[[
+
F
[[
F
::= a n.O
n :
a k F
F  F
v()
session identiers x in locations c.x[ T ] is to enable the factorisation of the
history of a protocol execution into individual sessions (cf. Section 3.2.3.5).
Remark 5 Names in C
3
are pure logical constants. In contrast, the concept
of names in classical process calculi such as the Pi and the SpiCalculus is
hybrid in the sense that their names have both boundvariable character via
convertibility and logicalconstant character via substitutability in free (in
put) variables. Philosophically speaking, a bound variable has no individuality,
whereas a logical constant has only individuality. The advantage of the classi
cal concept of names is that it does not demand a new (Pittsstyle) newname
quantier in the logical language.
4.1.2 Semantics
C
3
provides patternmatching in the style of [HJ04] as a highlevel linguistic
abstraction for cryptographic computation. The result of a patternmessage
match is a substitution relating variables to matched subterms. Substitutions
are partial functions from variables to messages, and are tacitly lifted to terms in
the standard way. Matching is computed by the partial function match dened
in Table 4.2. There, denotes composition, if the domains of the operands are
disjoint, and is otherwise undened. For example, the pattern [[
v
matches
any message signed with the private key corresponding to the public key v. The
line over the letter v is part of the pattern, recalling that the pattern matches
a message encrypted with the key dual to v without needing this key (e.g., the
private key of another agent) occur in the pattern term.
Table 4.2: Pattern matching
match(v, M) :=
M
/
v
match(M, M) :=
match((,
), (M, M
)) := match(, M) match(
, M
)
match([[
M
, [M[
M
) := match(, M)
match([[
+
p
, [M[
+
p
+
) := match(, M)
match([[
p
+
, [M[
p
) := match(, M)
80 CHAPTER 4. CALCULUS OF CRYPTOGRAPHIC COMMUNICATION
A novel, integrating feature of C
3
is that all its reduction constraints (e.g.,
freshness of new names, input guards, key lookup constraints) are CPLdenable
and decidable, and thus checkable via CPLsatisfaction.
The key store of an agent is induced (on the syntactic object level) by the
protocol history. (The popular alternative of a lookup table on the semantic
metalevel is, for syntactic purists, an obnoxious alternative because it would
harm the syntactic uniformity of their framework.) Keys are looked up in the
protocol history w.r.t. the local view of the retrieving agent and by referring to
their creator and the tag they were given at creation. A lookup succeeds only
if the desired tag is a subterm of the one used at the creation of the key. Our
lookup policy is CPLdenable: looksUp(c, x, n, , d, O) T, pronounced c in
session x looks up n of type generated by d with a tag containing O, is dened
in Table 4.3 (cf. Appendix B for the macrodenitions of the employed auxiliary
predicates). The policy enforces that the retrieved key (1) has the desired type
(n : ); (2) was known by c (c k n); (3) was generated by d (d v.o); (4) has
a compatible, intended ownership (O  o); and (5) when a session key, was
received in the current session (m(c.x m n  m)).
Table 4.3: Lookup predicate
looksUp(c, x, n, , d, O) := n : c k n vo(d v.o (n = v n = v
+
)
O  o (n : K
1
m(c.x m n  m)))
Denition 11 (Calculus of Cryptographic Communication) Let
(HT)
2
, dened in Table 4.4, designate reduction of protocol states s HT.
Then,
C
3
:= HT, ).
The generation of a new name (Rule New and NewEve) is possible only
if that name has not been generated yet, i.e., generated names are always fresh
w.r.t. the current state. The adversary Eve may generate a new name at any
time. Insecure input (Rule In) is incepted by the adversary and may consist
in any message from her knowledge that matches the input pattern and that
satises the input constraint . Successful input results in the substitution of
the matching message parts for the matched variables in the receiving thread.
Secure communication (Rule sOut, sIn and sComL, with sComr being tacit)
is synchronous. To achieve this, we introduce two auxiliary transition relations
sI
and
sO
not visible on the top level. Insecure communication between two
legitimate agents is asynchronous because it goes through the adversary, and
secure communication is synchronous because it does not. Reduction of paral
lel processes happens via interleaving concurrency (Rule Parl, Parr being
tacit). Finally, observe how nondeterminism abstracts away three determin
ing choices in the execution of a protocol, i.e., the choice of (1) the message
sent by the adversary in an insecure input, (2) the new name selected at name
generation time, and (3) the scheduling of located threads.
Slogan 19 Actions are potentiality of eect events, actuality.
4.1. CORE CALCULUS 81
Table 4.4: Process and thread execution
Below,
,
sO
,
sI
.
New
h [= n : ao(a n.o)
c.x[
n
/
v
T ]
h N(c, x, n, O)
NewEve
h [= Eve k O ao(a n.o)
P
h
P
h N(Eve, B, n, O)
Out
c.x[ Out
d
M.T ]
h
c.x[ T ]
h O(c, x, M, d) I(Eve, B, M)
In
h [= Eve k M match(, M)
c.x[ In when .T ]
h
sOut
c.x[ sOut
d
M.T ]
h
sO
c.x[ T ]
h sO(c, x, M, d)
sIn
h [= match(, M)
d.x[ sIn
c
when .T ]
h sO(c, x
, M, d)
sI
, M, d) sI(d, x, M, c)
sComl
P
h
sO
Q
h
sI
P Q
h
LookUp
c.x[
n
/
v
T ]
h
c.x[ T
]
h
h [= looksUp(c, x, n, , d, O)
c.x[ Get
d
(v : , O) in T ]
h
c.x[ T
]
h
Parl
P
h
P Q
h
Q
h
a
s
2
, :i
for all s
1
HT, if s
1
1
then there is s
2
HT s.t. s
2
2
and s
1
a
s
2
; and
s
1
and s
2
are observationally equivalent from the viewpoint of a, written
s
1
a
s
2
, :i s
1
_
a
s
2
and s
2
_
a
s
1
.
Observe how dynamic observational equivalence (on protocol states) is dened
in terms of static observational equivalence on protocol states, i.e., epistemic
accessibility (
a
, cf. Denition 7) between protocol states. As previously stated,
the idea of identifying an observational equivalence with epistemic accessibility
seems to have been published rst in [HS04b]. However, the authors adopt a
very dierent approach based on socalled function views.
4.1.4 Application: an algebraic attack scenario
We recall that algebraic correctness statements of cryptographic protocols enun
ciate a purported observational equivalence between two models (processes) of
the protocol under scrutiny. The choice of the actual processes depends on the
cryptographic requirement that the correctness statement is intended to encode.
For example, authenticity can be encoded as an observational equivalence be
tween, on the one side, an obviously (via dierent kinds of magic) correct
specication and, on the other side, an implementation expressing the proto
col as it would be coded in a realistic, and thus possibly lessobviously correct
implementation.
In our case, we use our observational equivalence w.r.t. Eves point of obser
vation
Eve
and create the specication and implementation via a minor adap
tation of the responder process. More precisely, we introduce an additional,
formal parameter oth
) := . . . In [(x
oth
, oth)[
+
k
slf
when x
oth
: X oth : A . . .
where . . . designates the parts left unchanged by the modication. The spec
ication process NSPuK
spec
is then obtained from NSPuK
RESP
by stipulating
that := (oth
, Alice.x
a1
[ NSPuK
INIT
(Alice, Eve) ]
Bob.x
b1
[ NSPuK
impl
(Bob, Eve) ])
where h h
N(Alice, x
a1
, x
Alice
, B)
O(Alice, x
a1
, [(x
Alice
, Alice)[
+
p
+
Eve
, Eve) I(Eve, B, [(x
Alice
, Alice)[
+
p
+
Eve
)
O(Eve, B, [(x
Alice
, Alice)[
+
p
+
Bob
, Bob) I(Bob, x
b1
, [(x
Alice
, Alice)[
+
p
+
Bob
)
N(Bob, x
b1
, x
Bob
, B)
O(Bob, x
b1
, [(x
Alice
, x
Bob
)[
+
p
+
Alice
, Alice) I(Eve, B, [(x
Alice
, x
Bob
)[
+
p
+
Alice
)
O(Eve, B, [(x
Alice
, x
Bob
)[
+
p
+
Alice
, Alice) I(Alice, x
a1
, [(x
Alice
, x
Bob
)[
+
p
+
Alice
)
O(Alice, x
a1
, [x
Bob
[
+
p
+
Eve
, Eve) I(Eve, B, [x
Bob
[
+
p
+
Eve
)
O(Eve, B, [x
Bob
[
+
p
+
Bob
, Bob) I(Bob, x
b1
, [x
Bob
[
+
p
+
Bob
)
In contrast, our specication setup
s
spec
:= (h h
, Alice.x
a1
[ NSPuK
INIT
(Alice, Eve) ]
Bob.x
b1
[ NSPuK
spec
(Bob, Eve) ])
cannot, due to the failure of the authentication guarantee (Eve ,= Alice), yield
a trace h
spec
that matches the implementation trace h
impl
beyond the event
I(Eve, B, [(x
Alice
, Alice)[
+
p
+
Eve
). Hence, s
impl
,
Eve
s
spec
.
4.2 tC
3
: an extension of C
3
with real time
For practical usability, specialpurpose models of timed cryptographic proto
cols are preferable over their generalpurpose counterparts because (untimed)
generalpurpose models tend to create considerable (en)coding overhead: [. . .]
the coding up required would make the complex behaviour dicult to under
stand, and it is preferable to use a language designed to express such realtime
behaviour. [ES00].
84 CHAPTER 4. CALCULUS OF CRYPTOGRAPHIC COMMUNICATION
Related work In tockCSP [ES00], tCryptoSPA [GM04], and the timed Spi
Calculus [HJ05] time is natural number valued, yielding a discrete time domain.
tockCSP and tCryptoSPA provide local processes that globally synchronise
through socalled tock events resp. tick actions, which represent the passage
of one unit of time. And the timed SpiCalculus provides a process construc
tor for querying a global clock. Thus, tockCSP, tCryptoSPA, and the timed
SpiCalculus lack local clocks that potentially advance at dierent rates across
dierent processes/locations. As pointed out in Section 3.4.1, this lack becomes
a deciency in distributed systems. Hence, a faithful model of timed crypto
graphic protocols must allow for potentially desynchronised, local clocks.
In [BEL05] (which we will refer to as tBEL), time in particular, a time
stamp is real number valued, yielding a dense time domain. We contend that
realvalued timestamps are too negrained because cryptographic messages
have nite length, which implies that real numbers are not transmittable as
such. Moreover, real clocks only have nite precision. tBEL does provide local
clocks, yet they advance at the same rate as time. [BEL05, Page 2]. Further,
adversarial break of shortterm keys is modelled only indirectly with a parallel
process rather than directly as part of the adversary model. Furthermore, tBEL
lacks a process equivalence. On the other hand, tBEL comes with a (second
order) specialpurpose logic for reasoning about tBEL models, and a decision
procedure for a class of reachability properties of bounded protocols based on
syntactic control points. In our opinion, tBEL and its associated logic are
unnecessarily domainspecic. They seem to have been built from scratch rather
than as Occhamsrazor extensions of untimed formalisms. Adding realtime to a
model or logic without explicit time can be simple [Lam05]. Moreover, the logics
according to the authors, main modality is actually not a modality (i.e.,
a nontruthfunctional operator on formulae), but rather a relational symbol
between individuals (and nite sets thereof).
Our approach In contrast to the models discussed, tC
3
(1) inherits the ob
servational equivalence of its core C
3
, and (2) extends C
3
with (2.1) rational 
number valued time (which still is dense), (2.2) local clocks that may progress
at dierent rates across dierent locations, and (2.3) adversarial break of short
term keys based on ciphertextonly attacks enabled by key expiration. C
3
neatly
extends to tC
3
by maintaining backwards compatibility. Essentially, only two
additional axioms (and no modied axioms/rules!) are needed in its operational
semantics.
We extend C
3
to tC
3
according to the following two design principles: rst,
for every legitimate participant and the adversary, we introduce a rational
number valued, local clock with an associated drift rate, where the adversarys
clock always displays the actual time; and second, we model the advancement
of (real) time by means of the adversary, who, at any (logical) time of protocol
execution, may advance the time by an arbitrary but always nite amount
by advancing her local clock. In this way, the adversary is de facto in full
control of time though subject to monotonicity. Adding communication and/or
computation delays imposes nonzero lower bounds on the advancement of time
between certain pairs of actions, and could be handled by only considering traces
where the adversary respects these bounds.
4.2. TC
3
: AN EXTENSION OF C
3
WITH REAL TIME 85
4.2.1 Extension
Syntax
1. addition of an action prex Set E for the (re)setting of local clocks to a
value E (cf. Section 3.4.2 for temporal expressions E)
2. extension of the ownership tag O of the action prex New (v : , (O, V ))
for newname generation with a tag V for the validity of the generated
name (cf. Section 3.4.2 for validity tags V )
A process P is epistemically local :i for all located threads c.x[ T ] in P and for
all a n.(O, V ), a k F, and t@a in T, a = c (cf. Section 3.4.2 for the time
predicate t@a and the associated concept of drift rate).
Semantics
1. addition of the axiom Set to the operational semantics:
Set _
a.x[ Set t.T ]
h
_
_
a.x[ T ]
h S(a, x, t)
_
2. addition of the axiom Time to the operational semantics:
Time _
P
h
_
_
P
h S(Eve, B, t)
_ h [= t
(t
@Eve t
t < )
where B acts as a dummy session identier.
Notice that the choice of the time value by which the adversary advances
time is abstracted away by nondeterminism.
3. adaptation of the lookup predicate (cf. Table 4.6) so that the retrieved
name n either is the locallymeasured time (n@c), or is a key that (1) has
the desired type (n : ); (2) was known by c (c k n); (3) was generated by
d (d v.(o, (t
b
, t
e
))); (4) has a compatible, intended ownership (O  o);
and (5) is perceived as timely by c (t
c
(t
c
@c t
b
t
c
t
e
)).
Table 4.6: Timed lookup predicate
looksUp(c, x, n, , d, O) := n : c k n (n@c
vot
b
t
e
(d v.(o, (t
b
, t
e
))
(n = v n = v
+
) O  o t
c
(t
c
@c t
b
t
c
t
e
)))
Observe that thanks to sorts (cf. Section 3.4.2 for timed sorts), tags, and the
abstract message the newname and the lookupprex can also elegantly handle
timed information: newtimedkey generation as New (v : K, (O, V )), timedkey
lookup as Get
a
(v : K, O) in , and time lookup as Get
a
(v : CV, B) in with B
acting as a dummy ownership tag.
86 CHAPTER 4. CALCULUS OF CRYPTOGRAPHIC COMMUNICATION
Observational equivalence No redenition is required: clockset events are,
by convention (cf. Section 3.4.2), unobservable, and unobservable events are
generically covered by Clause 5 of Denition 6.
4.2.2 Application: a timed, algebraic attack scenario
We are interested in the timeliness requirement for WMF, namely that the
responder only accepts the session key within a xed interval of time (cf. Sec
tion 3.4.4). It turns out that the requirement can be checked in a similar setup
as for authenticity, i.e., as an equivalence from Eves viewpoint (
Eve
) between
a specication and an implementation.
We create the specication and implementation again via a minor adaptation
of the responder process. More precisely, we introduce (again) an additional
guardconjunct and (additionally) an additional actionprex Out
Eve
t in the
(insecure) input prex
In [((t, oth), key)[
k
ss
when t : TV
t
s
(t
s
: TV t
s
@slf t +
v
t
s
)
oth : A
key : K.1
of the template WMF
RESP
(slf , srv,
v
) (cf. Table 3.8).
The modied responder process thus is
WMF
RESP
(slf , srv,
v
) := . . . In [((t, oth), key)[
k
ss
when t : TV
t
s
(t
s
: TV t
s
@slf t +
v
t
s
)
oth : A
key : K
.
Out
Eve
t .1
where . . . designates the part left unchanged by the modication. The spec
ication process WMF
spec
is then obtained from WMF
RESP
by stipulating that
:= tt
)) t
s
(t
s
@slf t t
s
t
), and the
implementation process WMF
impl
by stipulating (again) that := .
The magic in our specication process is the nontrivial and epistemically
nonlocal guard of the input of the responder process. In the implementation,
we only check the types of the atoms in the message and that the time stamp is
recent. In the specication, we additionally check that the key has been created
by the initiator for communication with the responder and that the locally
measured time is within the validity interval of the key, as expressed by the
additional guardconjunct. It is possible to have the simple time stamp check
succeed but the more obviously correct validity check fail, namely with the
setup
(h, WMF(Alice, Trent, Bob, x
a1
, x
t1
, x
b1
,
v
)
Trent.x
t2
[ WMF
SERV
(Trent,
v
) ]
Trent.x
t3
[ WMF
SERV
(Trent,
v
) ])
from Section 3.4.4.
This setup can, via process reduction, produce the family of traces that is
generated by instantiating the parameters t
1
, t
2
, and t
3
of the history template
4.3. DENOTATIONAL SEMANTICS 87
Table 4.7: History template for WMF
h := h
init
N(Alice, x
a1
, k
(Alice,Bob)
, ((Alice, Bob), (, 2
v
)))
O(Alice, x
a1
, Alice, Trent)
O(Alice, x
a1
, [((0, Bob), k
(Alice,Bob)
)[
k
(Alice,Trent)
, Trent) S(Eve, B,
v
)
I(Trent, x
t1
, Alice) I(Trent, x
t1
, [((0, Bob), k
(Alice,Bob)
)[
k
(Alice,Trent)
)
O(Trent, x
t1
, [((t
1
, Alice), k
(Alice,Bob)
)[
k
(Bob,Trent)
, Bob) S(Eve, B, 2
v
)
I(Trent, x
t2
, Bob) I(Trent, x
t2
, [((t
1
, Alice), k
(Alice,Bob)
)[
k
(Bob,Trent)
)
O(Trent, x
t2
, [((t
2
, Bob), k
(Alice,Bob)
)[
k
(Alice,Trent)
, Alice) S(Eve, B, 3
v
)
I(Trent, x
t3
, Alice) I(Trent, x
t3
, [((t
2
, Bob), k
(Alice,Bob)
)[
k
(Alice,Trent)
)
O(Trent, x
t3
, [((t
3
, Alice), k
(Alice,Bob)
)[
k
(Bob,Trent)
, Bob)
I(Bob, x
b1
, [((t
3
, Alice), k
(Alice,Bob)
)[
k
(Bob,Trent)
) O(Bob, x
b1
, t
3
, Eve)
shown in Table 4.7 for clarity, without interception events (cf. Rule Out and
In in Table 4.4). The only possible time values for the parameters t
1
, t
2
, and t
3
in this history template are those mentioned in the setevents of the adversary.
For the implementation, we may have t
1
=
v
, t
2
= 2
v
, and t
3
= 3
v
,
where t
3
is observed by the adversary in clear in the last event. However, the
specication cannot accept a stale key, i.e., a key older than 2
v
. Hence, the
specication cannot generate a history that conforms to the above template, in
particular a history such that the respondent outputs 3
v
as her last action.
Thus the implementation and the specication are not equivalent from the point
of view of the adversary, so the specication is not met.
4.3 Denotational semantics
Our denition of the meaning of a cryptographic protocol is motivated by our
denition of the meaning of a cryptographic message, which in turn is moti
vated by Abadi and Needhams Principle 1 for designing cryptographic protocols
[AN96a]. The principle says:
Every message should say what it means: the interpretation of the
message should depend only on its contents. [. . .]
With a clin dil and thus for the nonce, oneeyed, we observe that the principle
is both selfdenying and not selfdenying and thus paradoxical, and that this fact
can be proven by applying the principle to itself. Here is an informal proof, by
contradiction:
Assume that the principle is not selfdenying. Apply it
to itself by particularising it with itself. (The principle
is itself a message
3
and employs universal quantication
over messages.) The message of the principle does not say
3
Observe that the principle speaks about messages tout court rather than cryptographic
messages. If the principle is to speak about cryptographic messages, then it must depend on
a context (which [AN96a] of course constitutes) that properly frames it (which [AN96a] of
course does). Yet, that very dependence the principle denies.
88 CHAPTER 4. CALCULUS OF CRYPTOGRAPHIC COMMUNICATION
what it means: the interpretation of the message does not
depend only on its contents. (The principle does not say
what message meaning means.) Hence, the principle is
selfdenying. Contradiction.
Deduce that the principle is selfdenying. Yet, by this very fact the
principle is not selfdenying. (Every message, as the example of the
principle demonstrates, should really say what it means.) Conclude
that the principle is paradoxical.
This recreational proof is paradoxical in the (double) sense that it demonstrates
the paradoxical nature of Principle 1 and paradoxically the importance of the
subject matter of the principle. That is, explicitness and contextsensitivity of
meaning. Our task shall be to dene, in a unique sense, the meaning
4
of a
cryptographic message relative to an execution state and communicating agent.
Related work The most relevant work (though not addressing the problem of
logical omniscience) related to ours is [PR03], where, according to the authors,
the meaning of a message is given in terms of how it aects the knowledge of the
agents involved in the communication. This idea is spiritually close to ours (and
is given a very nice philosophical treatment by the authors), but has incarnated
in a very dierent body (of knowledge, so to say) as will become clear in the
sequel. The authors dene the denotation of a message at a state and w.r.t. an
agent as a socalled view transformer. And a view transformer is a set of ordered
pairs (, ) of propositions and such that if knowledge of is part of the
view that [agent] i has of the global system state before the communication
event, then knowledge of is part of its view after the communication.
Another relevant work related to ours is [Gro92]. There, the socalled (1)
objective semantics of a message is dened to be the set of all points, states
in our terminology, where the message was sent; and (2) KSsemantics of a
message is dened to be the set of pairs of a point and an agent such that that
agent sends the message at that point. The problem with this approach is,
according to the authors, that it is not yet suitable for cryptography.
The relevant commonality between [PR03], [Gro92], and our approach is that
all approaches employ epistemic logic as a means to dening message meaning.
The dierence is how each approach does so, as we shall see now with the
presentation of our approach.
4.3.1 Message meaning
Denition 13 (The meaning of a cryptographic message) The (com
municable) meaning of a cryptographic message M / w.r.t. an agent a
A
Eve
and a protocol state s H T shall be the set of equivalence classes []
of those propositions T whose truth a would know (resp., be able to prove)
if a knew M in s. (Notice the conditional mode!) Formally,
M
s
a
:= []  T and s [= a k M K
a
() , and
M
s
P
a
:= []  T and s [= a k M P
a
() respectively.
4
in the sense of Freges sense (a message makes to an agent) as opposed to reference (to
a bitstring)
4.3. DENOTATIONAL SEMANTICS 89
Message meaning is dened as a set of equivalence classes of propositions rather
than as a set of propositions because we are concerned with just what a message
means rather than with the manifold how it may mean it.
Message meaning is communicable when dened in terms of provability be
cause provability requires the capability to produce an actual proof (i.e., a mes
sage of a certain cryptographic form), which, by denition, is communicable.
Theorem 3 Message meaning is a distributive proper lter (and thus a proper
sublattice and a topped
structure) w.r.t. the Boolean lattice T/
, ), i.e.,
it is (1) a nonempty proper subset of T/
] := [
] (meet) [] [
] := [
] (join)
[] [
] :i
and keys(
:i [] [
] and [
2. (a) if [], [
] M
s
a
then [] [
] M
s
a
(b) if [] M
s
a
and [
] T/
and
then [
] M
s
a
3. if [] [
] M
s
a
and [] [
] M
s
a
then [] ([
] [
]) M
s
a
.
Proof. see Appendix A
Filters represent deductively closed (cf. Condition 2.(b)), consistent (i.e.,
[] , M
s
a
, otherwise M
s
a
= T/
, ).
Proof. see Appendix A
Proposition 3 Communicable message meaning is orderembedded strictly
within message meaning. Formally, M
s
P
a
M
s
a
and M
s
P
a
M
s
a
.
Proof. see Appendix A
Denition 14 (Contextsensitivity of message meaning) A cryptogra
phic message M / is contextsensitive :i there are a, b A
Eve
and s, s
HT s.t. M
s
a
,= M
s
b
. A cryptographic message M / that is not context
sensitive is contextfree.
5
this is a renement of the classical LindenbaumTarskialgebra construction: the partial
ordering is not mere logical consequence (); thus the resulting equivalence () is ner than
logical equivalence ()
90 CHAPTER 4. CALCULUS OF CRYPTOGRAPHIC COMMUNICATION
Note that our notion of contextsensitivity is semantic as opposed to the classical
notion of formal language theory, which is syntactic.
Formalisation 1 (Abadi and Needhams Principle 1)
Every message should say what it means: the interpretation of the message
should depend only on its contents. [. . .] [AN96a]
Every cryptographic message should be contextfree (cf. Denition 14).
Examples of contextsensitive cryptographic messages abound. Perhaps the
starkest example is the one of sending a bare nonce as the opening of a cryp
tographic protocol. See [BM03] for several dierent, and reportedly awed pro
tocols with such identical openings. Another way of creating contextsensitive
cryptographic messages is the use of indexicals (i.e., phrases in natural lan
guage that refer to past or future messages, or to extraprotocol outofband
communication such as personal contact and trusted couriers) in plaintexts. An
advantage of our denition of the contextsensitivity of a cryptographic message
is that the denition is, being equational, indierent to the many ways of how
contextsensitivity is created. It
6
only cares about that contextsensitivity is
created.
Denition 15 (The information content of a cryptographic message)
The information content (in the sense of Kolmogorovcomplexity [LV97]) of a
cryptographic message M / to agent a A
Eve
, written K
a
(M), is dened to
be the smallest
7
state s HT s.t. s [= a k M.
Note that [PR03] also dene the information content of a message, but their
denition is, as opposed to ours, in the sense of Shannon.
4.3.2 Protocol meaning
Recall Slogan 8. In other words, cryptographic protocols aim at inducing propo
sitional knowledge, i.e., knowledge of cryptographic states of aairs expressed
as propositions, by means of individual knowledge, i.e., knowledge of messages
(values). Values are only the means not the ends of cryptographic
8
com
putation.
Slogan 20 In cryptography, individual knowledge is the key to propositional
knowledge.
Denition 16 (The meaning of a cryptographic protocol) The mea
ning (or denotational semantics) s
a
of a cryptographic protocol s H T
w.r.t. to an agent a A
Eve
shall be the (directed) union of the meanings w.r.t. a
of all those messages that a comes to know during protocol execution. Formally,
let T() :=
_
Min() designate a template for the meetcompletion of .
6
It, the footnote marker in this line, and this are three examples of indexicals.
7
bear in mind that our protocol states are just nite strings of symbols, each string con
taining a process term (the program) as a substring
8
and possibly of interactive computation [GSW06] in general
4.3. DENOTATIONAL SEMANTICS 91
Then,
s
a
:= T
_
_
_
_
_
_
M M
s = a k M
M
s
a
_
_
_
_
_
s
n
a
:= T
_
_
_
_
_
_
s
HP
s
n
s
a
_
_
_
_
_
s
a
:= T
_
_
_
_
_
_
s
HP
s
a
_
_
_
_
_
s :=
aA
Eve
s
a
s
n
:=
aA
Eve
s
n
a
s
:=
aA
Eve
s
a
.
The meetcompletion ensures that each collective meaning has again a least
element, by taking the meet of the set of minimal elements in the union of
individual meanings. (The least element in each individual meaning becomes a
minimal element in the union of individual meanings.)
Note that our denition of the meaning (or denotational semantics) of a
cryptographic protocol
1. is dened in terms of
(a) the meaning of cryptographic messages
(b) the operational semantics of that protocol, which is a very nat
ural, but nevertheless, a novel idea. It is natural to dene the what
(the denotation) in terms of the how (the operations), rather than
the other way round or dening them independently of each other.
2. has the advantage of being syntaxindependent. The denotational seman
tics does not require inductive denition on the structure of cryptographic
protocol terms P T.
Theorem 5 s
a
= s
a
i [ for all T, s [= K
a
() i s
[= K
a
() ]
Proof. see Appendix A
In other words, two protocol states (worlds) that make equal sense to a protocol
agent are epistemically indistinguishable (w.r.t. to language T) to that agent.
In Wittgensteins words: The limits of my language mean the limits of my
world. [Wit75, Paragraph 5.6].
Theorem 6
1. s
n
a
s
n+1
a
is ordercontinuous
9
2. s
a
, s
n
a
, and s
a
are topped algebraic
structures (thus algebraic lat
tices, thus complete lattices, and thus complete partial orders [DP02])
3. s, s
n
, and s
are preCPOs
Proof. see Appendix A
An algebraic
. Formally,
s s
:i s
.
It is wellknown that renement orderings on a set of specication processes
on the one side and on a set of implementation processes on the other side
induce a Galoisconnection between the two sides of sets (cf. [DP02]).
Denition 17 (The information content of a cryptographic protocol)
The information content (in the sense of Kolmogorovcomplexity [LV97]) of a
protocol state s HT, containing the protocol(s), to agent a A
Eve
, written
K
a
(s), is dened to be the smallest message M / s.t. M
s
a
= s
a
.
Chapter 5
Towards Probabilistic
Polynomialtime
Cryptography
5.1 Introduction
We sketch an Ockhams razor extension of core CPL (cf. Chapter 3) with a
notion of probabilistic polynomialtime (PP) computation. We hope to intrigue
the reader that adding a notion of PPcomputation to a (propertybased) formal
ism for cryptographic protocols can perhaps be simple and conceived through a
renement of the DolevYao conception of cryptographic operators. The special
purpose machinery for PP (as for real time, cf. Section 3.4 and [Lam05]), need
not be built from scratch nor be heavyweight.
Related work We are aware of the following existing formalisms
1
for the
specication and verication of cryptographic constructions.
Propertybased: [DMP03, DDMP05, DDM
+
05] in the tradition of Hoare
logic, with satisfaction and deduction relations, and originally conceived
for cryptographic protocols; and [IK06] a higherorder logic, deduction
based, and originally conceived for cryptographic operators
Modelbased: [MRST06] a process algebra for equivalencebased speci
cation and verication.
Our approach In contrast, ppCPL is in the tradition of rstorder
2
, temporal
more precisely, polydimensional (i.e., norms, knowledge, space, qualitative
and possibly quantitative time, cf. Section 3.4) monomodal logic, (for the
moment still) satisfactionbased, and originally conceived for cryptographic pro
tocols but here extended to encompass cryptographic operators to some extent.
1
In our view, a formalism consists of exactly three components: a formal (e.g., program
ming or logical) language, a mathematical model (or interpretation structure), and a formal
semantics (e.g., eect or truth) for the language in terms of the model.
2
higherorder logics are too expressive at the cost of axiomatic incompleteness
93
94 CHAPTER 5. TOWARDS PPCRYPTOGRAPHY
Our general idea is to identify agents with feasible algorithms and, con
sequently, to resourcebound only the truth establishment of individual and
propositional knowledge. That is, the machinery for probabilistic polynomial
time computation does not aect the whole logic (as opposed to [DDM
+
05],
[IK06], where it does), but remains nicely conned to and is observable only
through the looking glass of epistemic operators.
5.1.1 Symbolic logic
We qualify a logic as symbolic
3
when its language allows quantication over
individuals that are represented as syntactic terms formed with term construc
tors (i.e., functional symbols). In this sense, CPL is symbolic; its language
allows quantication over individuals, i.e., cryptographic messages, represented
as message terms.
Core CPL (cf. Chapter 3) can further be qualied as abstract (in the sense
of DolevYao) because message terms are not interpreted as bitstrings. In
contrast, ppCPL is concrete (in the sense of PPcomputation) because mes
sage terms are interpreted as bitstrings. More precisely, in ppCPL message
terms are denoted to probability distributions of bitstrings by interpreting log
ical constants as bitstrings and functional symbols as possibly probabilistic
polynomialtime, i.e., feasible, algorithms on bitstrings (cf. Table 5.1
4
).
Table 5.1: Syntactic representation of individual concepts
Concept Representation
formal variable possibly primed letters v
adhoc variable lowercase roman letter except vs (e.g., m for messages)
metavariable roman letter except vs (e.g., M for messages)
abstract value atomic or compound message term
concrete value bitstring
Furthermore, core CPL can be qualied as positive about truth and knowl
edge because false positives, i.e., false statements wrongly established as true,
and false belief respectively, are impossible. In contrast, ppCPL is probabilis
tic about truth and knowledge because false positives are, w.r.t. truth, possible
(though only) with negligible probability, and w.r.t. knowledge, (im)probable
with variable degrees of support.
Finally, we highlight that in the language of ppCPL probability is implicit
except for belief where it parametrises the (new) doxastic modality. In partic
ular, there is no likelihood operator (cf. [Hal03]) in ppCPL. The reason is that
in modern cryptography truth must be established with overwhelming proba
bility, whereas belief of a human being may be established with possibly non
overwhelming degrees of support. Philosophically speaking (cf. Carnap
5
), prob
3
traditional usage of the term is philosophical and not standardised
4
[T]o be is to be the value of a variable. More precisely, what one takes there to be are
what one admits as values of ones bound variables. [Gib04, Page 111]
5
Incidentally, Carnap wrote a [rst] thesis setting out an axiomatic theory of space and
time. The physics department said it was too philosophical, and [. . .] the philosophy depart
ment said it was pure physics. (cf. http://en.wikipedia.org/wiki/Rudolf Carnap). . .
5.1. INTRODUCTION 95
ability can be an (epistemological) measure of our (subjective) belief of states
of aairs as well as an (ontological) measure of their (objective) possibility. The
renement of the doxastic modality with probability allows the expression of
degrees of certitude that an agent may experience w.r.t. her apprehension of
cryptographic states of aairs.
5.1.2 Probability theory
A fundamental concept of probability theory is the one of a probabilistic ex
periment characterised by the indeterminacy of its outcome, i.e., its entropy.
The fact that such experiments are probabilistic implies that they are stateful,
i.e., they represent states (with an inherent potential future) of the considered
model, and their execution means probabilistic state transition. A priori, an ex
perimenter, i.e., a human being about to experience the considered experiment,
typically has an uncertainty about the actual outcome of the experiment, and
makes a hypothesis about its expected outcome. A posteriori, the experimenter
typically makes an epistemic error about the actual outcome of the experiment
w.r.t. the hypothesis made a priori.
In ppCPL, exactly two kinds of probabilistic experiments are relevant: pro
cess reduction, i.e., protocol execution, (cf. Table 5.2) and message denotation,
i.e., message evaluation, (cf. Table 5.3).
Table 5.2: Probabilistic process reduction
Probability theory CPL
sample space 11
variable (experiment) X protocol state (h, P)
atomic event transition (h, P) (h
, P
)
possible value (outcome) of X (h
, P
) s.t. (h, P) (h
, P
)
probability distribution P(X)  ((h
, P
), p)  (h, P) (h
, P
) and p ]0, 1]
such that
pP((h,P))
p = 1
hypothesis h about outcome proposition
hypothesis H about outcome  (h
, P
)  (h, P) (h
, P
) [=
Note that interleaving concurrency implies that atomic events are mutually
exclusive and independent within each branching. Applying the principle of
indierence, we x P(s) to the uniform distribution for all s HT.
In Table 5.3, designates the function of message denotation.
5.1.3 Probabilistic polynomialtime cryptography
The distinguishing features of probabilistic polynomialtime cryptography are
that (1) key and signature generation, and encryption are probabilistic (or ran
domised); (2) the execution time of the operations under Item 1 and decryption
are polynomially bounded in a security parameter (the length of the key) used
for key generation; (3) adversaries are PP Turing machines with oracle access;
and (4) oracles are PP Turing machines.
96 CHAPTER 5. TOWARDS PPCRYPTOGRAPHY
Table 5.3: Probabilistic message denotation
Probability theory CPL
sample space 0, 1
s.t. s = M
probability distribution P(X)  (s, p)  s = M and p ]0, 1]
such that
pP(M)
p = 1
hypothesis h about outcome M = s
hypothesis H about outcome  s  s = M
5.2 ppCPL: an extension of CPL with proba
bilistic polynomialtime
This section describes the extension of CPL to ppCPL. The extension depends
on the core described in Chapter 3 (the reader is urged to consult it).
5.2.1 Syntax
The syntactic novelties are the following:
1. logical constants (atomic message terms): renement of the abstract mes
sage B
l
with a length indication l N; addition of bitstrings s ::=
0
NGA
n.o for newname generation with a
security parameter N, and a parameter NGA ::= SEA
AEA
SA
for the name of the employed generation algorithm
(b) addition of a binary relational symbol for the comparison of proba
bility values (actually the same as for the comparison of time values,
cf. Section 3.4)
4. logical operators: addition of a modality B
q
a
for belief with error control
q, where q is the probability for agent a not to err in her apprehension of
the truth of the considered proposition (say ), written B
q
a
()
5.2. PPCPL: AN EXTENSION OF CPL WITH PP 97
5.2.2 Semantics
The principal semantic novelties are the following:
1. (backwardscompatible) renement of temporal accessibility simpliciter to
PP temporal accessibility: addition of denotation events D(a, M, s, ALGO)
stating that agent a denoted the message term M to the string s 0, 1
) otherwise.
where M
:=
nnames(M)
_
n
h
a
/
n
_
M designates the message that results
from the substitution of all names n in M with the corresponding deno
tations n
h
a
. (The act of choosing s could be made strictly formal with
Hilberts choice operator [Sla06].)
3. let
/
a
(p, i) := s  p@0
s and s
a
p@i
B
a
(p, i) := s  p@0
s and s
a
p@i and
there is a polynomial p : N N s.t. [s[ p([p@i[)
[(h, P)[ := [
h[
(a) renement of propositional knowledge simpliciter
K
a
()
i
p
:= (for all s, if s /
a
(p, i) then s
[=
E
, c
(s,)
)
where (s
) :=
_
(s, ) if s = p@i, and
( s
p@i
a
,
p@i
a
) otherwise.
to PP propositional knowledge
K
a
()
i
p
:= (for all s, if s /
a
(p, i)
then s
[=
E
(s,)
)
where (s
) :=
_
(s, ) if s = p@i, and
( s
p@i
a
,
p@i
a
) otherwise.
(b) addition of believe with error control q T1
B
q
a
()
i
p
:= (q =
B
a
(p,i)
K
a
(p,i)
and
for all s, if s B
a
(p, i) then s
[=
E
, c
(s,)
)
where (s
) :=
_
(s, ) if s = p@i, and
( s
p@i
a
,
p@i
a
) otherwise.
98 CHAPTER 5. TOWARDS PPCRYPTOGRAPHY
Table 5.4: PP derivation of individual knowledge
Random coin tossing
h
(,1)
a
0 h
(,1)
a
1
Input data extraction
h (a, M)
({(a,M)},0)
a
(a, M)
h
(E,r)
a
M
h
(E,r)
a
M
Data synthesis Data analysis
h
(E,r)
a
M h
(E
,r
)
a
M
h
(EE
,r+r
)
a
(M, M
)
h
(E,r)
a
(M, M
)
h
(E,r)
a
M
h
(E,r)
a
(M, M
)
h
(E,r)
a
M
h
(E,r)
a
p
h
(E,r)
a
p
+
h
(E,r)
a
M
h
(E,r)
a
M
h
(E,r)
a
M h
(E
,r
)
a
M
h
(EE
,r+r
)
a
[M]
M
h
(E,r)
a
[M]
M
h
(E
,r
)
a
M
h
(EE
,r+r
)
a
M
h
(E,r)
a
M h
(E
,r
)
a
p
+
h
(EE
,r+r
)
a
[M]
p
+
h
(E,r)
a
[M]
p
+
h
(E
,r
)
a
p
h
(EE
,r+r
)
a
M
h
(E,r)
a
M h
(E
,r
)
a
p
h
(EE
,r+r
)
a
]M[
p
h
(E,r)
a
]M[
p
h
(E
,r
)
a
p
+
h
(EE
,r+r
)
a
M
Data concretisation Data abstraction
h
(E,r)
a
M
h
(E,r)
a
s
s = M
h
a
h
(E,r)
a
s
h
(E,r)
a
M
M
h
a
= s
PPabstraction
h
(E,r)
a
M
h
E
a
M
there is a polynomial p : N N s.t. r p(
(a,M)E
[(a, M)
h
a
[)
4. redenition of the state of violation with the desired kind(s) of breaks (i.e.,
successful attacks) of cryptographic schemes as formalised in Section 5.3.2.
The polynomial bound on the computational complexity of individual resp.
propositional knowledge (cf. Item 2 resp. 3) induces a corresponding bound on
the complexity of cryptographic proofs resp. provability (cf. Section 3.3.4).
Remark 6 In analogy to nonstandard analysis, it could be worthwhile to in
vestigate the introduction of innitesimals for negligible probabilities.
5.3. APPLICATION: FORMALISATION CASE STUDIES 99
5.3 Application: formalisation case studies
Denitions can be worthwhile even in the absence of theorems and
proofs.
Phillip Rogaway
(cf. [Rog04])
We illustrate the expressiveness of ppCPL on tentative formalisation case
studies of fundamental and applied concepts. Fundamental concepts: (1) one
way function, (2) hardcore predicate, (3) computational indistinguishability,
(4) (nparty) interactive proof, and (5) (nprover) zeroknowledge. Applied
concepts: (1) security of encryption schemes, (2) unforgeability of signature
schemes, (3) attacks on encryption schemes, (4) attacks on signature schemes,
and (5) breaks of signature schemes.
Note that in core CPL we focused on cryptographic protocols and their
requirements, but here (in ppCPL) we focus on cryptographic operators and
their attacks and breaks. Naturally, properties of good operators take the form
of tautologies, i.e., propositions that hold in any (protocol) model (cf. Table 5.5).
Table 5.5: Expressing properties of protocols, operators, and messages
Subject
Expression of a
property as a
Linking concept Style of expression
Protocol
proposition in an
assertion (h, P) [=
(true statement)
satisability
endogenous (i.e.,
pointfree/intensional
w.r.t. protocols)
Operator
proposition in an
assertion [=
(tautology)
validity
pointwise/extensional
w.r.t. messages
(quantication!)
Message unary predicate ()
substitution
((M))
Slogan 21 Predicates speak of individuals (e.g., messages). Propositions talk
about models (e.g., protocols). Both express purported facts.
Our formalisations illustrate the dramatic expressive power that results from
the combined use of epistemic and spatial operators.
5.3.1 Fundamental concepts
This section is in the spirit of [Gol01].
Denition 18 (Random propositional guessing)
RG
a
() := (q : PV)(
1
2
< q B
q
a
())
Denition 19 (Hard proposition) A proposition is hard :i in any model,
any agent a can only guess the truth of . That is, RG
a
() is a tautology.
[= RG
a
()
100 CHAPTER 5. TOWARDS PPCRYPTOGRAPHY
We generalise the concept of a hard proposition (a closed formula) to the
concept of a hard predicate (an open formula).
Denition 20 (Hard predicate) An nary predicate (M
1
, . . . , M
n
) is hard
on M
1
, . . . , M
n
satisfying the (n+1ary) predicate (M
1
, . . . , M
n
, a) :i in any
model, if (M
1
, . . . , M
n
, a) then any a can only randomly guess the truth of
(M
1
, . . . , M
n
).
[= (M
1
, . . . , M
n
, a) RG
a
((M
1
, . . . , M
n
))
Formalisation 2 (Oneway function)
[. . .] a function that is easy to compute but hard to invert. [Gol01, Page 32]
Ease of computation [= a k M a k f(M)
Hardness of invertibility f
1
(M
) = M is hard on M and M
satisfying
f(M) = M
a k M.
Notice that the standard denition of oneway functions only requires the op
erator f to be computable in deterministic polynomialtime, whereas the satis
ability of a k f(M) may be computable only in probabilistic polynomialtime
(cf. Table 5.4). We could easily provide a deterministic variant of k by simply
disallowing random coin tossing. Further, observe that our denition implies
that cryptographic operators are common knowledge among agents. In order to
express (individual) knowledge of operators, we would need quantication over
functional symbols, which would make our logic higherorder.
Formalisation 3 (Hardcore predicate)
[. . .] a polynomialtime predicate b is called a hardcore of a function f if
every ecient algorithm, given f(x), can guess b(x) with success probability
that is only negligibly better than onehalf. [Gol01, Page 64]
Let the satisability of (M) be computable in polynomialtime. Then (M) is a
hardcore of a function f :i (M) is hard on M satisfying a k f(M)a k M.
) is hard on M
and M
satisfying (M = M
).
5.3. APPLICATION: FORMALISATION CASE STUDIES 101
Denition 21 (Cryptographic evidence and proof )
M necessaryEvidenceFor := a(K
a
() (K
a
() a k M))
M sucientEvidenceFor := a(K
a
() (a k M K
a
()))
M strictEvidenceFor := M necessaryEvidenceFor
M sucientEvidenceFor
M evidenceFor := M necessaryEvidenceFor
M sucientEvidenceFor
M necessaryProofFor := a(a k M (K
a
() a k M))
M sucientProofFor := a(a k M (a k M K
a
()))
M strictProofFor := M necessaryProofFor
M sucientProofFor
M proofFor := M necessaryProofFor
M sucientProofFor
Observe that these concepts of cryptographic evidence and proof are renements
of the respective (basic) concepts dened in Section 3.3.4.
Conjecture 1
1. [= M necessaryProofFor M necessaryEvidenceFor
2. [= M sucientProofFor M sucientEvidenceFor
3. [= M strictProofFor M strictEvidenceFor
Formalisation 5 (2party interactive proof)
A 2party interactive proof (or 2party computation or 2party protocol) M
between a verier a and prover b (initiated by a) for a proposition (protocol
goal) is a (possibly minimal) nite chain M = (M
0
, . . . , M
n
) of messages s.t. (1)
M
n
is a proof of for a, and (2) for all consecutive pairs (M
i
, M
j
) in M, M
j
derives from M
i
due to communication between a and b. [authors formulation]
M ::= (M, B)
(M, M)
I ::= B
M
M iProofFor
(a,b)
:= M iProofFor
a
(a,b)
(M, B) iProofFor
c
(a,b)
:= c k M M proofFor
(M, (M
, I)) iProofFor
c
(a,b)
:= M
(a,b)
M (M
, I) iProofFor
c
(b,a)
Formalisation 7 (ZeroKnowledge)
Zeroknowledge proofs are dened as those [interactive] proofs that convey no
additional knowledge other than the correctness of the proposition [] in ques
tion. [GMR89]
ZK
(a,b)
() := IP
(a,b)
(K
a
(m
(K
b
(m
proofFor )))
m
(K
a
(K
b
(m
evidenceFor ))))
Spelled out, a (the verier) knows through interaction with b (the prover) that
b knows a proof (m
(b, A)
M iProofFor
(a,A)
:= M iProofFor
a
(a,A)
(M, B) iProofFor
c
(a,)
:= c k M M proofFor
(M, (M
, I)) iProofFor
c
(a,(b,A))
:= M
(a,b)
M (M
, I) iProofFor
c
(b,A)
:= (a k M a k M
)
(a k M
a k M)
(M, M
) disjointEvidenceFor := a(K
a
() (K
a
() a k (M, M
)
M [
a
M
))
(M, B) mutuallyDisjointEvidenceFor := M evidenceFor
(M, M) mutuallyDisjointEvidenceFor := (M, M) disjointEvidenceFor
M mutuallyDisjointEvidenceFor
M quotientProofFor := M proofFor
M mutuallyDisjointEvidenceFor
We pronounce M [
a
M
w.r.t. to
as knowledge. Quotient proofs could also be called compositional proofs.
Denition 24 (Multiprover ZeroKnowledge)
ZK
(a,A)
() := IP
(a,A)
(K
a
(m
(m
quotientProofFor A k m
))
m
(K
a
(m
evidenceFor A k m
)))
where
(a, B) k (M, B) := a k M
(b, A) k (M, M) := b k M A k M
Observe again the importance of the scope of the existential quantiers.
Formalisation 9 (Oblivious Transfer)
[. . .] we can view this protocol as one in which Alice sends a [condential]
letter to Bob, which arrives exactly half the time. [Kil88] (cf. [Rab81] for the
original reference of the idea)
m(a k m (c : A)(c k m (c = a c = b)) RG
b
(b k m))
[M]
p
+
This is again a logical formulation of an instance of the simulation
paradigm [GM84]. Observe the similarity with the previous instance.
Indistinguishability of encryptions
[M]
k
(or [M]
p
+
) and [M
]
k
(or [M
]
p
+
) are computationally in
distinguishable (in the sense of our formalisation)
there is l N s.t. [M]
k
(or [M]
p
+
) and B
l
are computationally
indistinguishable (in the sense of our formalisation)
2. Nonmalleability [. . .] it [is] infeasible for an adversary, given a ci
phertext, to produce a valid ciphertext (under the same encryptionkey)
for a related plaintext. [Gol04, Page 470]
[= (Eve k [M]
k
(M) (M
)
. .
M
is related to M
) (Eve k [M
]
k
Eve k k)
[= (Eve k [M]
p
+
(M) (M
)) (Eve k [M
]
p
+
Eve k M
)
Formalisation 10 (Unforgeability of signature schemes)
it is infeasible to produce signatures of other users to documents they did not
sign. [Gol04, Page 498]
[= a authored ]M[
p
a k p
)(Eve k [M]
p
+
)
Eve k k ((m
1
: SC
k
[M])(Eve k m
1
) (m
n
: SC
k
[M])(Eve k m
n
))
Eve k p ((m
1
: AC
p
+[M])(Eve k m
1
) (m
n
: AC
p
+[M])(Eve k m
n
))
(M
Eve
(m, [m]
k
)))))
(p : K
)(Eve k [M]
p
+
m(Eve k m
(Eve k [m]
p
+
>
(M
Eve
(m, [m]
p
+
)))))
Our interpretation of plaintext can be rened from the plaintext to some of
the plaintext by replacing Eve k M with m
1
(m
1
 M Eve k m
1
)
m
n
(m
n
 M Eve k m
n
).
Formalisation 14 (Adaptive chosenplaintext attack)
[. . .] a chosenplaintext attack wherein the choice of plaintext may depend on
the ciphertext received from previous requests. [MvOV96, Page 41]
Let A denote chosenplaintext chains in the public key p
+
of the form
A ::= B
((M, [M]
p
+
), A)
and aCPC
p
+
a
an inductivelydened macro expressing the realisation of such a
chain for agent a
B aCPC
p
+
a
:=
((M, [M]
p
+
), A) aCPC
p
+
a
:= a k M (a k [M]
p
+
> A aCPC
p
+
a
)
Then
(p : K
)(Eve k [M]
p
+
m(m
(m
aCPC
p
+
Eve
Eve k m)
(Eve k [m]
p
+
>
(M
Eve
(m, [m]
p
+
)))))
formalises an adaptive chosenplaintext attack on a private key. (The formali
sation of a corresponding attack on a symmetric key is similar.)
106 CHAPTER 5. TOWARDS PPCRYPTOGRAPHY
Formalisation 15 (Chosenciphertext attack)
[. . .] the adversary selects the ciphertext and is then given the corresponding
plaintext. [MvOV96, Page 41]
(k : K)(Eve k [M]
k
m(Eve k [m]
k
(Eve k m >
(M
Eve
(m, [m]
k
)))))
(([M]
k
, M), S)
and sCCC
k
a
an inductivelydened macro expressing the realisation of such a
chain for agent a
B sCCC
k
a
:=
(([M]
k
, M), S) sCCC
k
a
:= a k [M]
k
(a k M > S sCCC
k
a
)
Then
(k : K)(Eve k [M]
k
m(m
(m
sCCC
k
Eve
Eve k m)
(Eve k [m]
k
>
(M
Eve
(m, [m]
k
)))))
formalises an adaptive chosenplaintext attack on a symmetric key. (The for
malisation of a corresponding attack on an asymmetric key is similar.)
Attacks on signature schemes We state formalisations of attacks on sig
nature schemes in increasing strength.
Formalisation 17 (Keyonly attack)
[. . .] an adversary knows only the signers public key. [MvOV96, Page 432]
v(a : A)(v
+
puk a Eve k v
+
m(Eve k ]m[
v
Eve k m))
m
1
m
n
(Eve k ]m
1
[
v
Eve k ]m
n
[
v
Eve k m
1
Eve k m
n
))
m
1
m
n
((Eve k m
1
Eve k m
n
)
(Eve k ]m
1
[
v
Eve k ]m
n
[
v
)))
((M, ]M[
p
), C)
and CMC
p
a
an inductivelydened macro expressing the realisation of such a
chain for agent a
B CMC
p
a
:=
((M, ]M[
p
), C) CMC
p
a
:= a k M (a k ]M[
p
> C CMC
p
a
)
Then
v(a : A)(v
+
puk a Eve k v
+
m(m CMC
v
a
Eve k m))
formalises an adaptive chosenmessage attack on a signing key.
Breaks of signature schemes We state formalisations of breaks of signature
schemes in increasing strength.
Formalisation 21 (Existential forgery)
An adversary is able to forge a signature for at least one message. The adver
sary has little or no control over the message whose signature is obtained, and
the legitimate signer may be involved in the deception . . . [MvOV96, Page 432]
v(a : A)(v
+
puk a Eve k v
+
m(]m[
v
Eve
m))
Part III
Epilogue
109
Chapter 6
Conclusion
6.1 Review of achievements
We believe having achieved with CPL an original construction and powerful tool
for the logical conceptualisation of the security of communication. In particular,
we have:
1. dened a cryptographically meaningful (cf. Section 3.2.3.4) and indeed
omnipresent epistemic modality (for propositional knowledge) that com
mutes in both senses with quantiers being relativised (this is a novel idea)
to individual knowledge (cf. Corollary 1)
2. invented a cryptographically interesting (cf. Section 3.2.3.2) epistemic con
ditional thanks to the auxiliary invention of complex truth values
3. pioneered the application of spatial logic (cf. Section 3.2.3.2) to the for
malisation of cryptographic states of aairs and auxiliary concepts such
as choice, compositionality, and corruption (cf. Section 3.3.5, 5.3.1, 5.3.2)
4. invented, by macrodenition, spatial freeze quantiers, and shown that
with them distributed temporal logic is denable within the spatiotempo
ral fragment of CPL (cf. Section 3.2.3.5)
5. (a) demonstrated the macrodenability of a Godelstyle provability mo
dality within the spatioepistemic fragment of CPL (cf. Theorem 2).
With this modality, CPL can capture the provability meaning of
intuitionistic implication, and provability is shown to be the key to
the formalisation of commitment and related cryptographic states of
aairs (cf. Section 3.3.4).
(b) sketched a promising generalisation of the (noninteractive) provabil
ity modality to an interactive provability modality (cf. Denition 22)
and applied it to the formalisation of zeroknowledge
6. demonstrated the denability of cryptographically meaningful (cf. Sec
tion 3.2.3.3) deontic modalities within the spatioepistemicotemporal fra
gment of CPL, and by that, shown that cryptographic permission (and
prohibition) is parametrically reducible to the desired notion of (unde
sired) state of violation of the employed crypto system
111
112 CHAPTER 6. CONCLUSION
7. demonstrated that the addition of dense realtime to an untimed, property
based formalism for cryptographic protocols (core CPL) can be simple
and backwardscompatible, when properly conceived, but is still powerful
enough for the macrodenition of durations (cf. Section 3.4)
8. conceived and exemplied an original and promising codesign of poly
dimensional modal logic (CPL) and formal program semantics (C
3
):
Codesign In particular, we have demonstrated that
(a) temporal accessibility can be identied with protocol execution
(cf. Chapter 4)
(b) the execution constraints of the operational semantics (dening
protocol execution) are CPLdenable and checkable (cf. Ta
ble 4.4)
(c) epistemic accessibility can be identied with static observational
equivalence on program execution states (cf. Section 4.1.3)
(d) the meaning of a cryptographic protocol, its denotational seman
tics (cf. Section 4.3.2), can be dened in terms of the (possibly
contextsensitive) meaning of the cryptographic messages it pro
duces during its execution, and the (communicable) meaning of a
cryptographic message (cf. Section 4.3.1) can in turn be dened
via hypothetical knowledge (and provability)
(e) the information content (in the sense of Kolmogorov) of a cryp
tographic protocol can be dened in terms of the information
content of a cryptographic message, which in turn can be de
ned in terms of the minimal process inducing the (individual)
knowledge of that message (cf. Denition 17 resp. 15)
(f) protocol agents can be conceived as evolving Scott information
systems (cf. Section 4.3.2)
C
3
In particular, we have (in joint work):
(a) invented a dynamic key lookup mechanism based on the explicit
declaration of key ownership via tagging (cf. Table 4.3)
(b) dened a comprehensive message reception mechanism integrat
ing patternmatching (cf. Table 4.2) and conditional input (cf.
Rules In and sIn in Table 4.4) as linguistic abstractions for cryp
tographic computation
(c) demonstrated that the addition of dense realtime to an untimed,
model based formalism for cryptographic protocols can be sim
ple and backwardscompatible, when properly conceived (cf. Sec
tion 4.2)
(d) invented a powerful specication technique based on epistemically
nonlocal processes complementing the traditional techniques of
metacommunication (via formal parameters) and outofband
communication (via secure I/O primitives) (cf. Section 4.2.2)
9. conceived a promising, backwardscompatible extension of core CPL with
a notion of probabilistic polynomialtime computation by resourceboun
ding individual and propositional knowledge in a novel way and by invent
ing a notion of belief with error control (cf. Chapter 5)
6.1. REVIEW OF ACHIEVEMENTS 113
10. conceived a novel modal encoding of weak secondorder logic via individual
generating individuals (messagegenerating protocols) (cf. Section 3.2.3.1).
The key to our backwardscompatible extensions is the paradigm of eventbased
modelling. That is, the conservative extension of protocol histories with new
protocol events, e.g., clockset events for the extension with real time and de
notation events for the extension with probabilistic polynomialtime. In conse
quence, old languages can be interpreted over new models because new mod
elling events are irrelevant to that (oblivious) interpretation.
Thanks to the powerful linguistic abstractions that CPL provides, we have
also achieved the logical formalisation of an unprecedented variety of crypto
graphic states of aairs and cryptographic concepts. Concretely, these for
malised states of aairs are:
Trustrelated aairs maliciousness, honesty, faultiness, prudency, and trust
worthiness of protocol agents (cf. Section 3.3.1).
Condentialityrelated aairs shared secret, secrecy, anonymity, data deri
vation, noninteraction, perfect forward secrecy, knownkey attack, and
agent corruption (cf. Section 3.3.2).
Authenticationrelated aairs key conrmation, key authentication (impli
cit and explicit), message integrity, message authorship, message authenti
cation (authenticity), key transport (unacknowledged and acknowledged),
key agreement (unacknowledged and acknowledged), entity authentica
tion (identication) (unilateral, weakly mutual, and strongly mutual) (cf.
Section 3.3.3).
Commitmentrelated aairs cryptographic proof, cryptographic evidence,
provability, nonrepudiation, contract signing, (optimism, completion, ac
countability, and abusefreeness) (cf. Section 3.3.4).
Compositionalityrelated aairs key separation, compositional correctness
(existential composability, conditional composability, and universal com
posability), and attack scenario (cf. Section 3.3.5).
Concretely, these (tentatively) formalised concepts are:
Fundamental concepts oneway function, hardcore predicate, computatio
nal indistinguishability, (nparty) interactive proof, interactive provabil
ity, proof of knowledge, and (nprover) zeroknowledge (cf. Section 5.3.1).
Applied concepts security of encryption schemes (standard, semantic, via in
distinguishability, and via nonmalleability), unforgeability of signature
schemes, attacks on encryption schemes (ciphertextonly attack, known
plaintext attack, chosenplaintext attack, adaptive chosenplaintext at
tack, chosenciphertext attack, and adaptive chosenciphertext attack),
attacks on signature schemes (keyonly attack, knownmessage attack,
chosenmessage attack, and adaptive chosenmessage attack), and breaks
of signature schemes (existential forgery, selective forgery, universal for
gery, and total break) (cf. Section 5.3.2).
We hope that our tentative formalisations have convinced the reader that CPL
is an interesting candidate as a lingua franca for requirementsengineering cryp
tographic protocols.
114 CHAPTER 6. CONCLUSION
6.2 Future work
CPL
Shortterm Our immediate concerns are the consolidation of ppCPL, and the
validation of our formalisations of fundamental and applied concepts w.r.t.
their traditional Turingmachinebased denitions.
Midterm Our next concerns are the construction of proof systems for core
CPL, tCPL, and ppCPL; and the study of decidable fragments of core
CPL and its extensions.
Longterm Our longterm concerns are the construction of a CurryHoward
isomorphism between cryptographic protocols and propositions; and the
extension of CPL with quantum cryptography.
C
3
Shortterm Our shortterm concerns are a symbolic version of C
3
, and the
axiomatisation of C
3
s observational equivalence.
Midterm Our midterm concern is the extension of C
3
with a notion of
probabilisticpolynomialtime computation.
Longterm Our longterm concerns are the extension of C
3
with quantum
computation and communication; the investigation of dierent degrees of
communication (of: messages, message types, logical formulae, processes,
process types); and the extension of C
3
with further key management
capabilities (e.g., publickey certicate issuing and revocation) and object
orientation (e.g., methodbased subprotocol calls and dynamic session
creation).
Finally, we are concerned with the conception of an integrated engineer
ing methodology for our formalisms, and the development of tool support, and
application to more case studies.
Appendix A
Proofs
Proof of Theorem 1
Barcan: Suppose that s H T and s [= m(K
a
()). Then, for all
M /, s [= K
a
(). Hence, for all M /, s [= (by [= K
a
() ),
and thus s [= m(). Conclude that s [= K
a
(m()) by the hypothesis
that s [= K
a
() and the fact that keys(m()) keys() (fullling the
truth condition for propositional knowledge).
Relativised coBarcan: Suppose that s H T and s [= K
a
(m(a k
m )). Further, suppose that M / and s [= a k M. Hence,
s [= K
a
(a k M) and s [= K
a
(a k M ). Consequently, s [= K
a
() (by
[= K
a
(
) (K
a
() K
a
(
i [=
Proof.
[=
i
for all s, s [=
i
for all s, s [=
i
for all s, s [= (
) i
115
116 APPENDIX A. PROOFS
for all s, not s [=
i
for all s, not (s [= and s [=
) i
for all s, not (not not s [= and not s [=
) i
for all s, not (s [= and not s [=
) i
for all s, not s [= or not not s [=
i
for all s, not s [= or s [=
i
for all s, if s [= then s [=
Proposition 5 [= P
a
(
) (P
a
() P
a
(
))
Proof.
1. s [= P
a
(
) hyp.
2. s [= P
a
() hyp.
3. s [= m(m proofFor (
) a k m) 1
4. there is M / s.t. s [= M proofFor (
) a k M 3
5. M / and s [= M proofFor (
) a k M hyp.
6. s [= m(m proofFor () a k m) 2
7. there is M / s.t. s [= M proofFor () a k M 6
8. M
/ and s [= M
proofFor () a k M
hyp.
9. s [= M proofFor (
) and s [= a k M 5
10. s [= (v : A
Adv
)(v k M K
v
(
)) 9
11. for all v A
Eve
, s [= v k M K
v
(
) 10
12. s [= M
proofFor () and s [= a k M
8
13. s [= (v : A
Adv
)(v k M
K
v
()) 12
14. for all v A
Eve
, s [= v k M
K
v
() 13
15. v A
Eve
hyp.
16. s
[= v k (M, M
) hyp.
17. s
[= v k M 16, property of k
18. s [= v k M K
v
(
) 11, 15
19. for all s
, if s
[= v k M then s
s [= K
v
(
) 18
20. if s
[= v k M then s
s [= K
v
(
) 19
21. s
s [= K
v
(
) 17, 20
22. s
[= v k M
16, property of k
23. s [= v k M
K
v
() 14, 15
24. for all s
, if s
[= v k M
then s
s [= K
v
() 23
25. if s
[= v k M
then s
s [= K
v
() 24
26. s
s [= K
v
() 22, 25
27. s
s [= K
v
(
[= v k (M, M
) then s
s [= K
v
(
) 16, 27
117
29. for all s
, if s
[= v k (M, M
) then s
s [= K
v
(
) 28
30. s [= v k (M, M
) K
v
(
) 29
31. if v A
Eve
then s [= v k (M, M
) K
v
(
) 15, 30
32. for all v A
Eve
, s [= v k (M, M
) K
v
(
) 31
33. s [= (v : A
Adv
)(v k (M, M
) K
v
(
)) 32
34. s [= (M, M
) proofFor
33
35. s [= a k (M, M
) 9, 12, property of k
36. s [= (M, M
) proofFor
and s [= a k (M, M
) 34, 35
37. s [= (M, M
) proofFor
a k (M, M
) 36
38. there is M
/ s.t. s [= M
proofFor
a k M
37
39. s [= m(m proofFor
a k m) 38
40. s [= P
a
(
) 39
41. s [= P
a
(
) 7, 40
42. s [= P
a
(
) 4, 41
43. if s [= P
a
() then s [= P
a
(
) 2, 42
44. s [= P
a
() P
a
(
) 43
45. if s [= P
a
(
) then s [= P
a
() P
a
(
) 1, 44
46. for all s, if s [= P
a
(
) then s [= P
a
() P
a
(
) 45
47. P
a
(
) P
a
() P
a
(
) 46, Denition 8
48. [= P
a
(
) (P
a
() P
a
(
)) 47, Lemma 1
Proposition 6 [= P
a
() K
a
()
Proof.
1. s [= P
a
() hyp.
2. s [= m(m proofFor a k m) 1
3. there is M / s.t. s [= M proofFor a k M 2
4. M / and s [= M proofFor a k M hyp.
5. s [= M proofFor and s [= a k M 4
6. s [= (v : A
Adv
)(v k M K
v
()) 5
7. for all v A
Eve
, s [= v k M K
v
() 6
8. s [= a k M K
a
() 7
9. for all s
, if s
[= a k M then s
s [= K
a
() 8
10. if s [= a k M then s s [= K
a
() 9
11. s s [= K
a
() 5, 10
12. s [= K
a
() 11
1
13. s [= K
a
() 3, 12
14. if s [= P
a
() then s [= K
a
() 1, 13
1
is supposed to preserve uniqueness of process terms and of protocol events in protocol
histories, i.e., is supposed to be idempotent
118 APPENDIX A. PROOFS
15. for all s, if s [= P
a
() then s [= K
a
() 14
16. P
a
() K
a
() 15, Denition 8
17. [= P
a
() K
a
() 16, Lemma 1
Proposition 7 [= P
a
()
Proof.
1. [= P
a
() K
a
() Proposition 6
2. [= K
a
() property of K
3. [= P
a
() 1, 2
Proposition 8 [= P
a
() P
a
(P
a
())
Proof.
1. s [= P
a
() hyp.
2. s [= m(m proofFor a k m) 1
3. there is M / s.t. s [= M proofFor a k M 2
4. M / and s [= M proofFor and s [= a k M 3
5. v A
Eve
hyp.
6. s
[= v k M hyp.
7. s
s [= v k M 6
8. s
s [= K
v
(a k M) 4, 7, denition of K
9. s
s [= K
v
(M proofFor ) 4, 7
10. s
s [= K
v
(P
a
()) 8, 9
11. if s
[= v k M then s
s [= K
v
(P
a
()) 6, 10
12. for all s
, if s
[= v k M then s
s [= K
v
(P
a
()) 11
13. s [= v k M K
v
(P
a
()) 12
14. if v A
Eve
then s [= v k M K
v
(P
a
()) 5, 13
15. for all v A
Eve
, s [= v k M K
v
(P
a
()) 14
16. s [= (v : A
Adv
)(v k M K
v
(P
a
())) 15
17. s [= M proofFor P
a
() and s [= a k M 4, 16
18. there is M / s.t. s [= M proofFor P
a
() a k M 17
19. s [= m(m proofFor P
a
() a k m) 18
20. s [= P
a
(P
a
()) 19
21. s [= P
a
(P
a
()) 3, 20
22. if s [= P
a
() then s [= P
a
(P
a
()) 1, 21
23. for all s, if s [= P
a
() then s [= P
a
(P
a
()) 22
24. P
a
() P
a
(P
a
()) 23, Denition 8
25. [= P
a
() P
a
(P
a
()) 24, Lemma 1
119
Proposition 9
[=
[= a k M P
a
()
M is a tuple of the key values in
Proof.
1. [= and M is a tuple of the key values in hyp.
2. s [= a k M hyp.
3. v A
Eve
hyp.
4. s
[= v k M hyp.
5. s
s [= v k M 4
6. s
s [= K
v
() 1, 5, epistemic necessitation
7. if s
[= v k M then s
s [= K
v
() 4, 6
8. for all s
, if s
[= v k M then s
s [= K
v
() 7
9. s [= v k M K
v
() 8
10. if v A
Eve
then s [= v k M K
v
() 3, 9
11. for all v A
Eve
, s [= v k M K
v
() 10
12. s [= (v : A
Adv
)(v k M K
v
()) 11
13. s [= M proofFor and s [= a k M 2, 12
14. there is M / s.t. s [= M proofFor a k M 13
15. s [= m(m proofFor a k m) 14
16. s [= P
a
() 15
17. if s [= a k M then s [= P
a
() 2, 16
18. for all s, if s [= a k M then s [= P
a
() 17
19. a k M P
a
() 18, Denition 8
20. [= a k M P
a
() 19, Lemma 1
Proof of Theorem 3
1. , = M
s
a
T/
: , = M
s
a
because [] M
s
a
due to [= K
a
() (and
also [a k M] M
s
a
due to [= a k M K
a
(a k M)); and M
s
a
T/
because [] T/
, but [] , M
s
a
due to ,[= K
a
().
2. (a) if [], [
] M
s
a
then [] [
] M
s
a
:
1 [] M
s
a
and [
] M
s
a
hyp.
2 s [= a k M K
a
() and s [= a k M K
a
(
) 1
3 for all s
, if s
[= a k M then s
s [= K
a
() and
for all s
, if s
[= a k M then s
s [= K
a
(
) 2
4 for all s
, (if s
[= a k M then s
s [= K
a
()) and
(if s
[= a k M then s
s [= K
a
(
)) 3
5 for all s
, if s
[= a k M then
_
s
s [= K
a
() and
s
s [= K
a
(
)
_
4
6 for all s
, if s
[= a k M then s
s [= K
a
() K
a
(
) 5
7 [= (K
a
() K
a
(
)) K
a
(
) property of K
a
120 APPENDIX A. PROOFS
8 for all s
, if s
[= a k M then s
s [= K
a
(
) 6, 7
9 s [= a k M K
a
(
) 8
10 [] [
] M
s
a
9
(b) if [] M
s
a
and [
] T/
and
then [
] M
s
a
:
1 [] M
s
a
and [
] T/
and
hyp.
2 s [= a k M K
a
() and
and keys(
) keys() 1
3 for all s
, if s
[= a k M then s
s [= K
a
() 2
4
i [=
Lemma
5 [=
2, 4
6 if [=
then [= a k K K
a
(
) where
K designates a tuple built from keys(
) prop. of K
a
7 [= a k K K
a
(
) 5, 6
8 [= K
a
() a k K
were
K
[= a k M hyp.
10 s
s [= K
a
() 3, 9
11 s
s [= a k K
8, 10
12 s
s [= a k K 2, 11(, property of k)
13 s
s [= K
a
(
) 7, 12
14 [= K
a
(
) (K
a
() K
a
(
)) property of K
a
15 s
s [= K
a
() K
a
(
) 13, 14
16 s
s [= K
a
(
) 10, 15
17 for all s
, if s
[= a k M then s
s [= K
a
(
) 9, 16
18 s [= a k M K
a
(
) 17
19 [
] M
s
a
18
3. if [] [
] M
s
a
and [] [
] M
s
a
then [] ([
] [
]) M
s
a
:
1 [] [
] M
s
a
and [] [
] M
s
a
hyp.
2 s [= a k M K
a
(
) and s [= a k M K
a
(
) 1
3 for all s
, if s
[= a k M then s
s [= K
a
(
) and
for all s
, if s
[= a k M then s
s [= K
a
(
) 2
4 s
[= a k M hyp.
5 s
s [= K
a
(
) and s
s [= K
a
(
) 3, 4
6 s
s [= K
a
(
) K
a
(
) 5
7 [= (K
a
(
) K
a
(
)) K
a
((
) (
))prop. K
a
8 s
s [= K
a
((
) (
)) 6, 7
9 s
s [= K
a
( (
)) 8
10 for all s
, if s
[= a k M then s
s [= K
a
( (
)) 4, 9
11 s [= a k M K
a
( (
)) 10
12 [] ([
] [
])] M
s
a
11
121
Proof of Theorem 4 Analogous to the proof of Theorem 3 because that proof
only relies on S4 (adapted to the cryptographic setting), not full S5 (adapted
to the cryptographic setting), and provability is about S4.
Proof of Proposition 3
1. M
s
P
a
M
s
a
: because [= P
a
() K
a
() (cf. Proposition 6), but ,[=
K
a
() P
a
()
2. there is an orderembedding e : M
s
P
a
M
s
a
: take e := id
M
s
a
M
s
P
a
),
i.e., the restriction to M
s
P
a
of the identity on M
s
a
.
Proof of Theorem 5
s
a
= s
a
i
T
_
_
_
_
_
_
M M
s = a k M
M
s
a
_
_
_
_
_
= T
_
_
_
_
_
_
M M
s
= a k M
M
s
a
_
_
_
_
_
i
_
M M
s = a k M
M
s
a
=
_
M M
s
= a k M
M
s
a
i
_
M M
s = a k M
[]  T ; s [= a k M K
a
() =
_
M M
s
= a k M
[]  T ; s
[= a k M K
a
() i
[]  M / ; s [= a k M ; T ; s [= a k M K
a
() =
[]  M / ; s
[= a k M ; T ; s
[= a k M K
a
() i
_
[ for all M /, s [= a k M; for all T, s [= a k M K
a
() ] i
[ for all M /, s
[= a k M; for all T, s
[= a k M K
a
() ]
_
i
_
[ for all M /, s [= a k M; for all T, s [= K
a
() ] i
[ for all M /, s
[= a k M; for all T, s
[= K
a
() ]
_
i
_
[ for all M /, s [= K
a
(a k M); for all T, s [= K
a
() ] i
[ for all M /, s
[= K
a
(a k M); for all T, s
[= K
a
() ]
_
i
_
for all T, s [= K
a
() i
for all T, s
[= K
a
()
_
i
[ for all T, s [= K
a
() i s
[= K
a
() ]
Proof of Theorem 6
1. the map _ (a) orderembeds s
n
a
in s
n+1
a
, and (b) is order
continuous:
(a)
i _ _
because [= K
a
() _+K
a
(_)
122 APPENDIX A. PROOFS
(b) the map _ is ordercontinuous because it is orderembedding
(thus orderpreserving) and s
n
a
, being topped, satises the socalled
ascending chain condition [DP02, Page 148]
where _ designates the previoustime and _+ the nexttime operator of
CPL from linear temporal logic [MP84].
2. s
a
, s
n
a
, and s
a
are topped algebraic
structures because being (di
rected) unions of lters they are topped, and closed under intersection and
directed unions.
3. s, s
n
, and s
:= (
) or
:=
if then
:= (
) (
) if and only if
:= (
) (
) is epistemically equivalent to
:= (
) disjunctively separates
:= everywhere
:= somewhere
> := (
) assert
guarantee
:= _ in the beginning
:= _+ in the end
:= S so far
:= once
1. := _
:= eventually
:= (
) (
) before
:= (
) (
) correlates
123
124 APPENDIX B. SPECIFICATION LIBRARY (GLOSSARY)
Relational symbols
F = F
:= F  F
 F F is equal to F
F F
:= F = F
F  F
F is a strict subterm of F
a h F := v(F  v a k v) a has/possesses F
a tk F := a h F a k F a tacitly knows F
F : :=
F : H[] := (v : )(F = v)
F : SC
F
[] := (v : )(F = [v[
F
)
F : AC
p
+[] := (v : )(F = [v[
+
p
+
)
F : S
p
[] := (v : )(F = [v[
p
)
F : T[,
] := (v : )(v
)(F = (v, v
))
F :
:= F : F :
F :
:= F : F :
F : \
:= F : F :
F : M :=
F : SC[] := v(F : SC
v
[])
F : AC[] := (v : K
+
)(F : AC
v
[])
F : C[] := F : SC[] AC[]
F : S[] := (v : K
)(F : S
v
[])
:= (v : )(v :
) is a subtype of
:=
:=
,=
F F
:= v([v[
F
 F
)
p
+
+
F := v([v[
+
p
+
 F)
p
F := v([v[
p
 F)
F
:= F F
F
+
F
F is operational in F
F F
:= vv
(F  v [v[
v
 F
)
F
+
F
:= v(p
+
: K
+
)(F  v [v[
+
p
+
 F
)
F
:= v(p : K
)(F  v [v[
p
 F
)
F
:= F F
F
+
F
F is guarded in F
a := k sk a k : K