Commit 21c24370 authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

new entry Relational_Method

parent b33e4e32b4ec
......@@ -445,6 +445,7 @@ Regular_Algebras
Relation_Algebra
Relational-Incorrectness-Logic
Relational_Disjoint_Set_Forests
Relational_Method
Relational_Paths
Rep_Fin_Groups
Residuated_Lattices
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
chapter AFP
session Relational_Method (AFP) = "HOL" +
description \<open>The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols\<close>
options [timeout = 300]
theories
Definitions
Authentication
Anonymity
Possibility
document_files
"root.bib"
"root.tex"
@article {
Paulson98,
author = {Lawrence C. Paulson},
title = {The Inductive Approach to Verifying Cryptographic Protocols},
journal = {Journal of Computer Security},
month = dec,
year = 1998
}
@article {
Noce17,
author = {Pasquale Noce},
title = {Verification of a Diffie-Hellman Password-based Authentication Protocol by Extending the Inductive Method},
journal = {Archive of Formal Proofs},
month = jan,
year = 2017,
note = {\url{http://isa-afp.org/entries/Password_Authentication_Protocol.html}, Formal proof development},
ISSN = {2150-914x}
}
@manual {
ICAO15,
title = {Doc 9303 -- Machine Readable Travel Documents -- Part 11: Security Mechanisms for MRTDs},
organization = {International Civil Aviation Organization (ICAO)},
edition = {7th},
year = 2015
}
@manual{
Paulson20,
author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
title = {Isabelle/HOL -- A Proof Assistant for Higher-Order Logic},
month = apr,
year = 2020,
note = {\url{https://isabelle.in.tum.de/website-Isabelle2020/dist/Isabelle2020/doc/tutorial.pdf}}
}
@manual{
Nipkow20,
author = {Tobias Nipkow},
title = {Programming and Proving in Isabelle/HOL},
month = apr,
year = 2020,
note = {\url{https://isabelle.in.tum.de/website-Isabelle2020/dist/Isabelle2020/doc/prog-prove.pdf}}
}
@manual{
Krauss20,
author = {Alexander Krauss},
title = {Defining Recursive Functions in Isabelle/HOL},
note = {\url{https://isabelle.in.tum.de/website-Isabelle2020/dist/Isabelle2020/doc/functions.pdf}}
}
@manual{
Nipkow11,
author = {Tobias Nipkow},
title = {A Tutorial Introduction to Structured Isar Proofs},
note = {\url{https://isabelle.in.tum.de/website-Isabelle2011/dist/Isabelle2011/doc/isar-overview.pdf}}
}
\documentclass[11pt,a4paper,fleqn]{article}
\usepackage{isabelle,isabellesym}
\renewcommand{\isastyletxt}{\isastyletext}
% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed
%\usepackage{amssymb}
%for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
%\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
%\<triangleq>, \<yen>, \<lozenge>
%\usepackage{eurosym}
%for \<euro>
%\usepackage[only,bigsqcap]{stmaryrd}
%for \<Sqinter>
%\usepackage{eufrak}
%for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
%\usepackage{textcomp}
%for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
%\<currency>
% this should be the last package used
\usepackage{pdfsetup}
% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}
% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}
\begin{document}
\title{The Relational Method with Message Anonymity\\for the Verification of Cryptographic Protocols}
\author{Pasquale Noce\\Software Engineer at HID Global, Italy\\pasquale dot noce dot lavoro at gmail dot com\\pasquale dot noce at hidglobal dot com}
\maketitle
\begin{abstract}
This paper introduces a new method for the formal verification of cryptographic protocols, the
relational method, derived from Paulson's inductive method by means of some enhancements aimed at
streamlining formal definitions and proofs, specially for protocols using public key cryptography.
Moreover, this paper proposes a method to formalize a further security property, message anonymity,
in addition to message confidentiality and authenticity.
The relational method, including message anonymity, is then applied to the verification of a sample
authentication protocol, comprising Password Authenticated Connection Establishment (PACE) with Chip
Authentication Mapping followed by the explicit verification of an additional password over the PACE
secure channel.
\end{abstract}
\tableofcontents
% sane default for proof documents
\parindent 0pt\parskip 0.5ex
% generated text of all theories
\input{session}
% bibliography
\bibliographystyle{abbrv}
\bibliography{root}
\end{document}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment