This dissertation presents a logical investigation of epistemic protocols, focussing on protocol-dynamics, epistemic modelling, and epistemic model checking. In Part I, we introduce logics for specifying epistemic protocols including their goals and their dynamics. Chapter 3 departures from the existing discussions about protocols in the field of Dynamic Epistemic Logic by introducing a logic which can specify both the epistemic protocols and their goals within the language. We formalize the verification problem of epistemic protocols under the assumption of meta knowl- edge about the intended goal. The subtlety of this verification problem is discussed in theory and examples. In Chapter 4, we address the question: “How can people get to know a protocol?” For this, we develop logics which are convenient for reasoning about knowledge change and protocol change. With various protocol-changing op- erators we can handle the dynamics of protocols and formalize how actions acquire new meanings as a result of protocol change. We show that all the three logics we introduced can be translated back to Propositional Dynamic Logic (PDL) on standard Kripke models, thus the techniques of modelling and model checking we develop in the other parts of the dissertation can be applied to these logics. In Part II we address the issue of epistemic modelling, in order to study model checking for the logics introduced in Part I. In Chapter 5 we propose new compo- sition operations on static and event models with arbitrary vocabularies, aiming at a compositional method for generating initial epistemic models. We prove decom- position theorems w.r.t. our new operator and demonstrate the use of our methods by various examples. Chapter 6 reports results on counting the number of different models given a finite set of initial assumptions. Restricted to image-finite models, we show that if a modal μ-calculus formula has an infinite model modulo bisimulation thenithas2א0 (cardinalityofthecontinuum)differentmodelsmodulobisimulation. On the other hand, if it does not have any infinite models modulo bisimulation then all its models can be represented in a normal form. Part III introduces abstraction techniques that are particularly useful on making the model checking more efficient. A 3-valued semantics for Public Announcement Logic is defined and studied in Chapter 7 to facilitate abstractions of models. We define a relation with vocabulary and agent mappings between concrete models and their abstractions, thus making it possible to also abstract the signatures of models. We then give a logical characterization of this abstraction relation thus showing it is safe to check properties on the abstract model instead of the original concrete model. Chapter 8 studies the PDL on so-called accelerated Kripke models where the transitions in the models are labelled by regular expressions in order to obtain informative ab- stractions. By making use of a technique of regular expression rewriting, we analyse the complexity of the model checking and satisfiability problems of this logic and give a complete axiomatization. In Part IV (Chapter 9) we survey the epistemic approaches to security protocol verification. We summarize the most important techniques in the Epistemic Tempo- ral Logic and Dynamic Epistemic Logic approaches to security protocol verification, and compare these two approaches in term of convenience. We argue that some se- curity properties can only be faithfully formalized by temporal logic with knowledge operators, but are not expressible by standard temporal logic. However, we need to pay some cost in model checking complexity, in exchange to the expressiveness we gain.