Search

Background: Older adults are less likely to access mental health services than younger adults despite experiencing similar rates of mental health problems. Older adults experiencing mental health problems are more likely to be offered medication than psychological interventions compared with younger adults. There is a recognized need to increase access to early, psychological intervention and preventative mental healthcare for older adults globally. Improving access to mental health services in rural areas is a national priority. The combined risks of an ageing population, inadequate service preparedness and comparatively poor mental health service utilisation by older adults, increases the likelihood of a large-scale mental health crisis. Mental health literacy (MHL) is associated with the recognition of mental health needs, service utilisation and improved mental health outcomes. Psychoeducation is often an integral part of low-intensity psychological intervention and receiving it is arguably linked to mental health literacy. Older adults have been found to have lower MHL and are more likely to use avoidance based coping strategies than younger adults. Little is known about the factors within older adults that perpetuate, ameliorate or confound these associations, particularly in a rural context. Objectives: A systematic review 'The Effectiveness of Low-intensity Psychological Interventions on the Well-being of Older Adults' synthesised the evidence for effectiveness and acceptability of low-intensity psychological interventions (self-help, psychoeducation, bibliotherapy, internet cognitive-behavioural therapy: iCBT) for older adults with mild-to-moderate mental health problems. A cross-sectional questionnaire-based survey 'An Exploration into the Relationships between Mental Health Literacy, Experiential Avoidance and Mental Health in Older Adults in a Rural Scottish Region' was used to explore the level of MHL, and the relationships between MHL, mental health, experiential avoidance, willingness to use mental health services and demographic variables in community-dwelling older adults in a rural Scottish region. Methods: The systematic review protocol was registered on Prospero prior to data extraction. Ovid, EBSCOhost and ProQuest were searched for articles describing low-intensity psychological interventions. Pre and post outcome measures and a mean age of at least 50 (age range ≥40) were required for inclusion. One hundred and fifty two respondents (aged ≥65, M = 71.9) took part in the questionnaire study. The MHL Scale, Acceptance in Action Questionnaire-II (experiential avoidance) and Clinical Outcomes in Routine Evaluation-10 (mental health status) measured the variables of interest. Results: The 26 articles describing 23 studies included in the systematic review described (guided) iCBT, bibliotherapy, self-help, psychoeducation and audio interventions. The majority of studies were of good quality and reported improvements in participant's mental health scores post intervention. Participants were more likely to be female, aged 60-70 and to have obtained further education. Eight studies reported obtaining participant satisfaction ratings. Three studies reported collecting data from both rural and urban areas. The empirical study found that respondents had good MHL. Half of the respondents reported being aware of local mental health services for older adults. Older age (r (146) = -.32, p < .001) and lower educational attainment (F (1,145) = 5.34, p = .020) were associated with poorer MHL in our sample. MHL was not significantly correlated with mental health problem severity or experiential avoidance. Self-reported willingness to use mental health services was associated with lower experiential avoidance (ρ (146) = -.266, p = .001), better mental health (ρ (146) = -.193, p = .018) and better MHL (ρ (146) = .467, p ≤ .001). However, the single-item measure of willingness to use mental health services was unreliable due to its significant negative skew and narrow range of data points. Those who had used mental health services had higher MHL, higher experiential avoidance and poorer mental health than those who had not. Conclusions: The findings from the systematic review provide tentative evidence to support the use of guided, low-intensity psychological interventions for mild-to-moderate mental health problems in older adults. Guided iCBT and bibliotherapy may be beneficial for older adults in their 60s and 70s experiencing mild-to-moderate levels of depression. iCBT may also be beneficial for reducing symptoms of mild-to-moderate anxiety. Providing the option of low-intensity psychological intervention, particularly iCBT, may help to increase participant engagement with treatment. Given difficulties in mental health service accessibility (both face-to-face and online) for those living in rural areas, future research should strive to specify whether participants are from rural or urban areas and explore any differences in outcomes. Improving rural-dwelling, older adults' MHL and their awareness of locally available services and supports may help to increase their willingness to seek mental health support.

This thesis presents the synthesis and characterisation of a range of heterometallated porphyrin oligomers and other novel 3D π-conjugated porphyrin nanostructures. Subsequently, their physical organic properties were evaluated which revealed some fascinating electronic properties. Chapter 1 summarises some of the work done in the Anderson group on porphyrin nanostructures and reviews the literature regarding heterometallated porphyrin oligomers. In addition it introduces the main concepts and techniques used in the remainder of the thesis. In Chapter 2 the stabilities of a family of four linear porphyrin pentamer complexes are determined by UV-vis-NIR titrations and analysed using chemical double-mutant cycles which reveal that the binding energy of the copper centre to an axial pyridine ligand is -6.2 kJ mol-1. Subsequently, the Zn-Zn-Cu-Zn-Zn pentamer is used in the synthesis of a heterometallated 10-porphyrin nanoring. Chapter 3 will describe the investigation of quantum interference phenomena in a bis-copper six-porphyrin nanoring by using EPR spectroscopy. We show that the exchange coupling between two spin centres is increased by a factor 4.5 in the ring structure with two parallel coupling pathways as compared to an otherwise identical system with just one coupling path. In Chapter 4 the syntheses of three isomers of the bis-copper 6-porphyrin nanoring are described. DFT calculations have indicated potential destructive interference phenomena in one of the isomers which would allow for the formation of a molecular system with behaviour resembling that of a hypothetical molecular interferometer. Chapter 5 reports on the template-directed synthesis of a π-conjugated 14-porphyrin nanoball. This bicyclic structure consists of two intersecting nanorings of 6 and 10 porphyrin units. Fluorescence up-conversion spectroscopy experiments demonstrate that electronic excitation delocalises over the whole 3D π-system within 0.3 ps if the nanoball is bound to its templates or within 5 ps if the nanoball is empty. In Chapter 6 the synthesis and characterisation of a D4h symmetric analogue of the porphyrin nanoball is described. The structure consists of ten porphyrin units arranged as two perpendicular 6-porphyrin nanorings intersecting at two porphyrins. In the synthesis, a combination of magnesium and zinc porphyrins are used which allows for the introduction of a selective demetallation method crucial for accessing this novel structure.

This study examines the theme of violence against women, in three novels of Emile Zola, representing respectively the bourgeoisie, the working class, and the peasant class: La Curee, L'Assommoir, and La Terre. Some of Rene Girard's ideas, as put forth in La Violence et le sacre, The Scapegoat, and Des Choses cachees depuis la fondation du monde, provide the theoretical basis for our analysis.

Analysing the security of cryptographic protocols by hand is a challenging endeavour. It requires substantial expertise, weeks of intensive effort and the resulting proof of security often arrives long after the protocol design has been finalised and even deployed. However, automated protocol verification tools, such as Tamarin and ProVerif, offer a compelling alternative as they require less expertise, promise quicker results and have been used to successfully analyse complex real world protocols such as TLS, 5G and Signal. These tools are built on a idealised model of cryptography, termed the symbolic model, which requires strong assumptions about the properties of cryptographic primitives. Consequently, automated protocol analyses may miss attacks which rely on properties of real primitives which are missing from the symbolic model. Furthermore, some protocols are not amenable to automated analysis as they use cryptographic primitives for which no suitable symbolic model currently exists. This motivates natural research questions: How closely does the contemporary symbolic model approximate the real world behaviour of common cryptographic primitives? Can we improve the accuracy and breadth of the symbolic model by developing new approaches to underlying formalism? In this thesis, we set out to address these questions for two popular cryptographic primitives: digital signatures and Diffie-Hellman groups. The symbolic model of digital signatures was first published nearly two decades ago and is widely used. We uncover a startling mismatch between the standard cryptographic definition of signature scheme security and the symbolic description. We repair this mismatch through the development of a novel symbolic model which we use to discover a number of new attacks on deployed protocols. We also document a number of previous analyses which missed these attacks due to their traditional symbolic model. Next we consider Diffie-Hellman groups. Unlike digital signatures, symbolic Diffie-Hellman models have evolved considerably in recent years and we review the progress in this area, highlighting two key limitations. Firstly, that these models only describe prime order groups, despite the popularity of non-prime order groups in practice. We develop new symbolic models to remedy this and use them to discover new attacks on real world protocols. Secondly, that there is no effective procedure for analysing protocols which make use of the full field structure of Diffie-Hellman exponents. We develop a new formalism which can be used to mechanically analyse such protocols and demonstrate its effectiveness on hand-worked examples. Finally, we conclude by examining the methodology behind our approach. We argue that the techniques behind our new symbolic models can be applied to many other cryptographic primitives to yield more accurate symbolic models. We go on to summarise our contributions and sketch several promising lines of future work.

In our increasingly connected world, daily life depends on the correct and unimpaired operation of the computers controlling our infrastructure. These systems are increasingly complex, both within the computers themselves, and in the communications between them that create larger systems. This complexity increases both functionality and potential vulnerability. In turn, this makes ensuring the security of these critical systems simultaneously harder and more important than ever. Ensuring that systems are not meaningfully vulnerable to attack requires a wide range of techniques. During design and implementation, the foremost of these is formal verification. Large, real-world systems and protocols made up of multiple computers or components are rarely designed with verification or analysis in mind. By the same token, these same systems have very often proved tricky to analyse formally. Can we meaningfully verify the security properties of large, real-world, multi-component systems, in a reasonable amount of time? Is there value in making the modelling and analysis as fine-grained as we can, or does the extra effort fail to buy us anything? Can these systems still operate correctly and securely even when partially compromised by an attacker? Can we improve the languages and tools we use to model systems under partial compromise? In this thesis, we address these questions through a mixture of theory and practice. We first consider a major power grid communications standard, DNP3. We show that its "Secure Authentication" protocols meet their security goals, and that a previously claimed attack is not possible. We then consider the security of 5G, and its main Authentication and Key-Agreement protocol. Our analysis reveals that 5G-AKA's security relies on unstated assumptions; in practice this means 'correct' implementations can be vulnerable to a security-critical race condition. Our analyses show how far we have to go in terms of resilience under partial compromise. Neither studied system fares well against attackers which control any one of its components: this is no longer acceptable in elements of critical national infrastructure, as these systems increasingly come under sophisticated attack. We then consider the formalisation of partial compromise, building the idea of an attacker controlling part of a system into models from the start. Our new techniques give approachable yet powerful ways to model a wide range of multi-component systems and protocols against fine-grained threat models. We finish with two main conclusions. First, the time is now right for formal methods. We show that precise, fine-grained modelling of complex, multi-component protocols is both possible and valuable in the real world. Second, partial compromise resilience must be built in from the start. With little hope of securing all end-points completely, it is essential that resilience is also built into the network protocols.

Authenticated key exchange protocols are ubiquitous in modern-day life. They are used to secure numerous types of data exchange, ranging from online banking to instant messaging conversations. In this thesis, we extend the state of the art for authenticated key exchange security, following the three themes of realistic, strong and provable. First, we tackle the theme of provable security. We develop generic techniques, applicable to a wide range of security models, to assist in proofs of security of cryptographic schemes. Specifically, a "game hopping" proof is a powerful technique to prove strong statements about the security of a protocol. However, the proof technique often involves esoteric and repetitive steps. We demystify the methodology and prove generic theorems to reduce the length and complexity of a wide class of game hopping proofs. Next, we use this new framework to analyse strong and previously unstudied formal security guarantees of authenticated key exchange protocols. These protocols are able to achieve strong security guarantees because they share and update state across sessions. Using our framework, we are able to push the state of the art by defying the folklore of what was previously thought provable of authenticated key exchange protocols. Specifically, it was previously thought that no protocol can achieve a security guarantee about communication with a peer if the peer was already fully compromised. We show that this is not true by formally defining a new concept, which we name post-compromise security. We capture an intuitive "self-healing" property of protocols. We then construct and formally prove protocols can achieve this strong security notion. Finally, we leverage all of this work to analyse realistic protocols. Signal, which is used to encrypt messages in WhatsApp, Facebook Messenger and Google Allo amongst others, is one such protocol we consider. Despite being used by billions of people, Signal was completely unstudied in the academic literature prior to this work. Two reasons for this were that Signal had no documentation at the time and it did not fit into existing models: it shares state across sessions and has over ten different types of key, most of which continually update. Despite its complexity, we are able to use the other work in this thesis to give the first ever analysis and proof of security of Signal. Overall, this thesis aims to bridge the gap between theory and practice in the current state of the art of authenticated key exchange protocols.

What formal guarantees should a secure messaging application provide? Do the most widely-used protocols provide them? Can we do better? In this thesis we answer these questions and with them give a formal study of modern secure messaging protocols, which encrypt the personal messages of billions of users. We give definitions and analyses of two protocols: one existing (Signal) and one new (ART). For Signal, we begin by extending and generalising classic computational models, in order to apply them to its complex ratcheting key derivations. With a threat model in mind we also define a security property, capturing strong secrecy and authentication guarantees including a new one which we call "post-compromise security". We instantiate Signal as a protocol in our model, stating its security theorem and sketching a computational reduction. Signal only supports encrypting messages between two devices, and so most implementers have built custom protocols on top of it to support group conversations. These protocols usually provide weaker security guarantees, and in particular usually do not have post-compromise security. We propose a new protocol called ART, whose goal is to bring Signal's strong security properties to conversations with multiple users and devices. We give a design rationale and a precise definition of ART, and again generalise existing computational models in order to formally specify its security properties and sketch a security reduction. ART has enjoyed widespread interest from industry, and we aim to turn it into an open standard for secure messaging. To that end, we have brought it to the IETF and formed a working group called Messaging Layer Security, with representatives from academia as well as Facebook, Google, Twitter, Wire, Cisco and more. Through MLS, we hope to bring ART's strong guarantees to practical implementations across industry. After concluding our analyses we pause for a moment, and start looking towards the future. We argue that for complex protocols like Signal and ART we are reaching the limits of computational methods, and that the future for their analysis lies with symbolic verification tools. To that end we return to the symbolic model and give a number of case studies, in each one showing how a traditional limitation of symbolic models can in fact be seen as a modelling artefact.

Secrets are the basis of most protocol security, enabling authentication and secrecy over untrusted channels even in the presence of active adversaries. The compromise and misuse of secrets can therefore undermine the properties that people and systems rely on for their security. In this thesis, we develop foundations and constructions for security protocols that can automatically detect, without false positives, if a secret such as a key or password has been misused. These constructions allow protocol participants to automatically trigger an appropriate response and minimize the effects of compromise. Our threat model includes malicious agents, (temporarily or permanently) compromised agents, and clones. Unlike existing approaches to detection, for which designs are interwoven with domain-specific considerations and which usually do not enable fully automatic response (i.e., they need human assessment), our approach makes it clear where automatic action is possible. Our results unify, justify the design of, and suggest improvements for existing domain-specific solutions. For example, we propose an improvement to Cloudflare's Keyless SSL protocol that enables key misuse detection, and a modified ISO-IEC 9798 protocol for use in high-security smart-card applications such as the Common Access Card. Our results show that protocols which detect misuse must be stateful. Although stateful protocols are becoming more common, formally analyzing them remains a challenge. We develop and implement several improvements to the Tamarin prover to alleviate this difficulty, and use them to formally verify our proposed detection protocols. We demonstrate the wide applicability of our improvements to Tamarin by analyzing several real-world protocols. Notably, we perform the first full formal analysis of both WireGuard, and the DNP3 Secure Authentication protocol---a complex multi-stage stateful protocol used to authenticate critical monitor and control functionality in SCADA systems.

While research has been done in the past on evaluating standardised security protocols, most notably TLS, there is still room for improvement. Modern security protocols need to be rigorously and thoroughly analysed, ideally before they are widely deployed, so as to minimise the impact of often creative, powerful adversaries. We explore the potential vulnerabilities of modern security protocols specified in current standards, including TLS 1.2, TLS 1.3, and SSH. We introduce and formalise the threat of Actor Key Compromise (AKC), and show how this threat can and cannot be avoided in the protocol design stage. We find AKC-related and other serious security flaws in protocols from the ISO/IEC 11770 standard, find realistic exploits, and harden the protocols to ensure strong security properties. Based on our work, the ISO/IEC 11770 working group is releasing an updated version of the standard that incorporates our suggested improvements. We analyse the unilaterally and mutually authenticated modes of the TLS 1.3 Handshake and Record protocols according to revision 06 of their specification draft. We verify session key secrecy and perfect forward secrecy in both modes with respect to a powerful symbolic attacker and an unbounded number of threads. Subsequently, we model and verify the standard authenticated key exchange requirements in revision 10. We analyse a proposal for its extension and uncover a flaw in it, which directly impacts the draft of revision 11.