Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
isa-afp
afp-2020
Commits
caaedd506d3d
Commit
caab59e8
authored
Dec 07, 2020
by
Lawrence Paulson
Browse files
Relational_Method website
parent
cdc40199823d
Changes
6
Expand all
Hide whitespace changes
Inline
Side-by-side
metadata/metadata
View file @
caaedd50
...
...
@@ -1231,6 +1231,26 @@ abstract =
</p>
notify =
[Relational_Method]
title = The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols
author = Pasquale Noce <mailto:pasquale.noce.lavoro@gmail.com>
topic = Computer science/Security
date = 2020-12-05
notify = pasquale.noce.lavoro@gmail.com
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.
[List_Interleaving]
title = Reasoning about Lists via List Interleaving
author = Pasquale Noce <mailto:pasquale.noce.lavoro@gmail.com>
...
...
web/entries/Relational_Method.html
0 → 100644
View file @
caaedd50
<!DOCTYPE html>
<html
lang=
"en"
>
<head>
<meta
charset=
"utf-8"
>
<title>
The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols - Archive of Formal Proofs
</title>
<link
rel=
"stylesheet"
type=
"text/css"
href=
"../front.css"
>
<link
rel=
"icon"
href=
"../images/favicon.ico"
type=
"image/icon"
>
<link
rel=
"alternate"
type=
"application/rss+xml"
title=
"RSS"
href=
"../rss.xml"
>
<!-- MathJax for LaTeX support in abstracts -->
<script>
MathJax
=
{
tex
:
{
inlineMath
:
[[
'
$
'
,
'
$
'
],
[
'
\\
(
'
,
'
\\
)
'
]]
},
processEscapes
:
true
,
svg
:
{
fontCache
:
'
global
'
}
};
</script>
<script
id=
"MathJax-script"
async
src=
"../components/mathjax/es5/tex-mml-chtml.js"
></script>
</head>
<body
class=
"mathjax_ignore"
>
<table
width=
"100%"
>
<tbody>
<tr>
<!-- Navigation -->
<td
width=
"20%"
align=
"center"
valign=
"top"
>
<p>
</p>
<a
href=
"https://www.isa-afp.org/"
>
<img
src=
"../images/isabelle.png"
width=
"100"
height=
"88"
border=
0
>
</a>
<p>
</p>
<p>
</p>
<table
class=
"nav"
width=
"80%"
>
<tr>
<td
class=
"nav"
width=
"100%"
><a
href=
"../index.html"
>
Home
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../about.html"
>
About
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../submitting.html"
>
Submission
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../updating.html"
>
Updating Entries
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../using.html"
>
Using Entries
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../search.html"
>
Search
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../statistics.html"
>
Statistics
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../topics.html"
>
Index
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../download.html"
>
Download
</a></td>
</tr>
</table>
<p>
</p>
<p>
</p>
</td>
<!-- Content -->
<td
width=
"80%"
valign=
"top"
>
<div
align=
"center"
>
<p>
</p>
<h1>
<font
class=
"first"
>
T
</font>
he
<font
class=
"first"
>
R
</font>
elational
<font
class=
"first"
>
M
</font>
ethod
with
<font
class=
"first"
>
M
</font>
essage
<font
class=
"first"
>
A
</font>
nonymity
for
the
<font
class=
"first"
>
V
</font>
erification
of
<font
class=
"first"
>
C
</font>
ryptographic
<font
class=
"first"
>
P
</font>
rotocols
</h1>
<p>
</p>
<table
width=
"80%"
class=
"data"
>
<tbody>
<tr>
<td
class=
"datahead"
width=
"20%"
>
Title:
</td>
<td
class=
"data"
width=
"80%"
>
The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols
</td>
</tr>
<tr>
<td
class=
"datahead"
>
Author:
</td>
<td
class=
"data"
>
Pasquale Noce (pasquale /dot/ noce /dot/ lavoro /at/ gmail /dot/ com)
</td>
</tr>
<tr>
<td
class=
"datahead"
>
Submission date:
</td>
<td
class=
"data"
>
2020-12-05
</td>
</tr>
<tr>
<td
class=
"datahead"
valign=
"top"
>
Abstract:
</td>
<td
class=
"abstract mathjax_process"
>
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.
</td>
</tr>
<tr>
<td
class=
"datahead"
valign=
"top"
>
BibTeX:
</td>
<td
class=
"formatted"
>
<pre>
@article{Relational_Method-AFP,
author = {Pasquale Noce},
title = {The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols},
journal = {Archive of Formal Proofs},
month = dec,
year = 2020,
note = {\url{http://isa-afp.org/entries/Relational_Method.html},
Formal proof development},
ISSN = {2150-914x},
}
</pre>
</td>
</tr>
<tr><td
class=
"datahead"
>
License:
</td>
<td
class=
"data"
><a
href=
"http://isa-afp.org/LICENSE"
>
BSD License
</a></td></tr>
</tbody>
</table>
<p></p>
<table
class=
"links"
>
<tbody>
<tr>
<td
class=
"links"
>
<a
href=
"../browser_info/current/AFP/Relational_Method/outline.pdf"
>
Proof outline
</a><br>
<a
href=
"../browser_info/current/AFP/Relational_Method/document.pdf"
>
Proof document
</a>
</td>
</tr>
<tr>
<td
class=
"links"
>
<a
href=
"../browser_info/current/AFP/Relational_Method/index.html"
>
Browse theories
</a>
</td></tr>
<tr>
<td
class=
"links"
>
<a
href=
"../release/afp-Relational_Method-current.tar.gz"
>
Download this entry
</a>
</td>
</tr>
<tr><td
class=
"links"
>
Older releases:
None
</td></tr>
</tbody>
</table>
</div>
</td>
</tr>
</tbody>
</table>
<script
src=
"../jquery.min.js"
></script>
<script
src=
"../script.js"
></script>
</body>
</html>
\ No newline at end of file
web/index.html
View file @
caaedd50
...
...
@@ -88,6 +88,14 @@ of a scientific journal, is indexed by <a href="http://dblp.uni-trier.de/db/jour
<tr>
<td
class=
"head"
>
2020
</td>
</tr>
<tr>
<td
class=
"entry"
>
2020-12-05:
<a
href=
"entries/Relational_Method.html"
>
The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols
</a>
<br>
Author:
Pasquale Noce
</td>
</tr>
<tr>
<td
class=
"entry"
>
2020-11-22:
<a
href=
"entries/Isabelle_Marries_Dirac.html"
>
Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information
</a>
...
...
web/rss.xml
View file @
caaedd50
...
...
@@ -9,7 +9,27 @@
and larger scientific developments, mechanically checked
in the theorem prover Isabelle.
</description>
<pubDate>
22 Nov 2020 00:00:00 +0000
</pubDate>
<pubDate>
05 Dec 2020 00:00:00 +0000
</pubDate>
<item>
<title>
The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols
</title>
<link>
https://www.isa-afp.org/entries/Relational_Method.html
</link>
<guid>
https://www.isa-afp.org/entries/Relational_Method.html
</guid>
<dc:creator>
Pasquale Noce
</dc:creator>
<pubDate>
05 Dec 2020 00:00:00 +0000
</pubDate>
<description>
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.
</description>
</item>
<item>
<title>
Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information
</title>
<link>
https://www.isa-afp.org/entries/Isabelle_Marries_Dirac.html
</link>
...
...
@@ -572,27 +592,5 @@ implementation may be used as the basis for a model of Peano arithmetic in
ZF. While recursion and the natural numbers are already available in Isabelle/ZF, this clean development
is much easier to follow.
</description>
</item>
<item>
<title>
An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation
</title>
<link>
https://www.isa-afp.org/entries/LTL_Normal_Form.html
</link>
<guid>
https://www.isa-afp.org/entries/LTL_Normal_Form.html
</guid>
<dc:creator>
Salomon Sickert
</dc:creator>
<pubDate>
08 May 2020 00:00:00 +0000
</pubDate>
<description>
In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical
theorem stating that every formula of Past LTL (the extension of LTL
with past operators) is equivalent to a formula of the form
$\bigwedge_{i=1}^n \mathbf{G}\mathbf{F} \varphi_i \vee
\mathbf{F}\mathbf{G} \psi_i$, where $\varphi_i$ and $\psi_i$ contain
only past operators. Some years later, Chang, Manna, and Pnueli built
on this result to derive a similar normal form for LTL. Both
normalisation procedures have a non-elementary worst-case blow-up, and
follow an involved path from formulas to counter-free automata to
star-free regular expressions and back to formulas. We improve on both
points. We present an executable formalisation of a direct and purely
syntactic normalisation procedure for LTL yielding a normal form,
comparable to the one by Chang, Manna, and Pnueli, that has only a
single exponential blow-up.
</description>
</item>
</channel>
</rss>
web/statistics.html
View file @
caaedd50
This diff is collapsed.
Click to expand it.
web/topics.html
View file @
caaedd50
...
...
@@ -436,6 +436,7 @@
<a
href=
"entries/Multi_Party_Computation.html"
>
Multi_Party_Computation
</a>
<a
href=
"entries/Noninterference_Generic_Unwinding.html"
>
Noninterference_Generic_Unwinding
</a>
<a
href=
"entries/Noninterference_Ipurge_Unwinding.html"
>
Noninterference_Ipurge_Unwinding
</a>
<a
href=
"entries/Relational_Method.html"
>
Relational_Method
</a>
<a
href=
"entries/UPF.html"
>
UPF
</a>
<a
href=
"entries/UPF_Firewall.html"
>
UPF_Firewall
</a>
<a
href=
"entries/CISC-Kernel.html"
>
CISC-Kernel
</a>
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment