\documentclass{article} \usepackage{rcs} \RCS$Date: 2026/01/22 10:32:58 $ \RCS$RCSfile: aspen-doc.ltx,v $ \RCS$Revision: 1.33 $ \RCS$State: Exp $ \RCS$Author: aa $ %\savercsinfo{Date,RCSfile,Revision,State,Author} \usepackage[T1]{fontenc} \usepackage[utf8]{inputenc} \usepackage[color,ban=aa]{aspen} \usepackage[charter,expert]{mathdesign} \usepackage[scaled=.96,osf]{XCharter}% matches the size used in math \linespread{1.04} \usepackage[a4paper,margin=3cm]{geometry} \usepackage{graphicx} \usepackage[dvipsnames,x11names]{xcolor} \usepackage[most]{tcolorbox} \usepackage{xltabular} \usepackage{makecell} %\usepackage{amssymb} \usepackage{wasysym} \usepackage{fancyvrb} \usepackage{fvextra} \usepackage{hologo} \usepackage{luamplib} \everymplib{ verbatimtex %&latex \documentclass{article} \usepackage[color,ban=aa]{aspen} \usepackage[charter,expert]{mathdesign} \usepackage[scaled=.96,osf]{XCharter}% matches the size used in math \linespread{1.04} \begin{document} etex ahlength:=2.5; beginfig(0); } \everyendmplib{ endfig; } \usepackage[hang,flushmargin]{footmisc} \usepackage{caption} \usepackage[numbib,nottoc]{tocbibind} \usepackage{hyperref} % \hypersetup{ % colorlinks=true, % linkcolor=blue, % filecolor=magenta, % urlcolor=cyan, % pdftitle={Overleaf Example}, % pdfpagemode=FullScreen, % } \parindent=0pt \parskip=\bigskipamount \renewenvironment{quotation}{\begin{quote}}{\end{quote}} \topsep=0pt \partopsep=0pt %\usepackage{minted2} % TEMP work-around: should be minted %\usemintedstyle{manni} %\usemintedstyle{autumn} \makeatletter \def\latex{L\kern -.29em{\sbox \z@ T\vbox to\ht \z@ {\hbox {\check@mathfonts \fontsize \sf@size \z@ \math@fontsfalse \selectfont A}\vss }}\kern -.12em\TeX} \makeatother \colorlet{LightLightCyan}{LightCyan2!40!} \colorlet{LightLightGrey}{gray!15!} \colorlet{LightGrey}{gray!80!} \colorlet{LightCyan}{cyan!80!} \newcommand{\extxt}[1]{\textcolor{gray}{#1}} \newcommand{\givesarrow}{\extxt{\ensuremath{\rightarrow}}} \newcommand{\gives}{\ensuremath{\quad\givesarrow\quad}} % \NewDocumentCommand{\cs}{mo}{% % \acmd{\textbackslash #1}% % \IfNoValueTF{#2}{}{\texttt{\{#2\}}}} %\def\cs#1{\acmd{\textbackslash #1}} %\newcommand{\imptxt}[1]{\textcolor{NavyBlue}{#1}} %\newcommand{\impcmd}[1]{\imptxt{\texttt{#1}}} % \tcbset{on line, % boxsep=4pt,left=0pt,right=0pt,top=0pt,bottom=0pt, % colframe=white,colback=LightLightCyan, % highlight math style={enhanced}} \newtcbox{\exbox}{on line, boxsep=4pt,left=0pt,right=0pt,top=-2pt,bottom=0pt, colframe=white,colback=LightLightGrey, highlight math style={enhanced}} \newtcbox{\shadedbox}{on line, boxsep=0pt,left=0pt,right=0pt,top=0pt,bottom=4pt, colframe=white,colback=white, highlight math style={enhanced}} \newcommand{\example}[1]{\hspace*{\fill}\shadedbox{\exbox{\small \ensuremath{\begin{array}{c}#1\end{array}}}}\hspace*{\fill}} %\DeclareRobustCommand\iff{\;\Longleftrightarrow\;} % Inspired by the example environment in % https://tug.ctan.org/macros/latex/contrib/minted/minted.dtx \fvset{formatcom=\color{NavyBlue}} \newlength{\codewith} \newenvironment{ltxexample}[1]{% \setlength{\codewith}{#1}% \VerbatimEnvironment \begin{VerbatimOut}[gobble=2]{example.out}} {\end{VerbatimOut}% \begin{center} \fbox{% \begin{minipage}[c]{\codewith}% % \inputminted[resetmargins]{latex}{example.out}% \VerbatimInput{example.out}% \vspace*{-2ex}% % The \fvset adds extra space (bug?) \end{minipage}% \vrule \input{example.out}\hspace{-0.5em}}% \end{center}} \newenvironment{ltxexample*}[1]{% \setlength{\codewith}{#1}% \VerbatimEnvironment \begin{VerbatimOut}[gobble=2]{example.out}} {\end{VerbatimOut}% \begin{center} \fbox{% \begin{minipage}[c]{\codewith}% % \inputminted[resetmargins]{latex}{example.out}% \VerbatimInput{example.out}% \vspace*{-2ex}% % The \fvset adds extra space (bug?) \end{minipage}}% \end{center}} \DeclareFontFamily{U}{lasy}{} \DeclareFontShape{U}{lasy}{m}{n}{ <-5.5> lasy5 <5.5-6.5> lasy6 <6.5-7.5> lasy7 <7.5-8.5> lasy8 <8.5-9.5> lasy9 <9.5-> lasy10 }{} \DeclareFontShape{U}{lasy}{m}{b}{ <-5.5> lasy5 <5.5-6.5> lasy6 <6.5-7.5> lasy7 <7.5-8.5> lasy8 <8.5-9.5> lasyb10 <9.5-> lasyb10 }{} \DeclareRobustCommand{\Leadsto}{% \mathrel{\text{\usefont{U}{lasy}{m}{b}\symbol{"3B}}}% } %\DeclareRobustCommand{\rLeadsto}{% % \mathrel{\text{\reflectbox{\usefont{U}{lasy}{m}{n}\symbol{"3B}}}}% %} \begin{document} \title{{\aspen}\\[.5\baselineskip] A suggested security protocol notation} \author{Anders Andersen} \date{\RCSRawDate} \maketitle \thispagestyle{empty} In security literature, different notations for cryptographic values, functions and protocols have been used and suggested. Three often cited references for such notations are ``Kerberos: An Authentication Service for Open Network Systems''~\cite{steiner1988a}, ``Exploring Kerberos, the Protocol for Distributed Security in Windows 2000''~\cite{chappell1999a}, and ``A Formal Semantics for Protocol Narrations''~\cite{briais2005a}. The notation {\aspen} presented here is strongly inspired by notations found in these three references, notations found in text books~\cite{anderson2020a}, and the notation used in my own publications, teaching and presentations. {\aspen} is closely related to what is often called ``security protocol notation'', ``standard protocol engineering notation''~\cite{anderson2001a,anderson2008a}, ``standard protocol notation''~\cite{anderson2020a}, or ``protocol narrations''~\cite{briais2005a}. This text documents the {\aspen} notation and how this notation can be used in {\latex} documents using the {\latex} package \Verb|aspen|. Since the {\latex} package \Verb|aspen| optionally provides support for the BAN logic notation, we have included the BAN logic notation in the documentation. \parbox[t]{.47\linewidth}{% {\aspen}\footnotemark{} is \emph{not} a formalism, like BAN (Burrows–Abadi–Needham) logic~\cite{burrows1989a}, or a calculus for analysis of cryptographic protocols, like Spi calculus~\cite{abadi1999a}. For a more detailed analysis of cryptographic protocols, more expressive notations like BAN logic, Spi calculus, or something similar should be considered. Other references presenting relevant notations include, but are not limited to: \cite{briais2007a,davis1989a,schafer2001a}.\\ \hfil\begin{steps*} \send{A}{S}{\apri{A},\apri{B},\nonce{a}} \\ \send*{S}{A}{\encrypted{A,S}{\nonce{a},\apri{B},\key{A,B},% \encrypted{B,S}{\key{A,B},\apri{A}}}} \\ \send*{A}{B}{\encrypted{B,S}{\key{A,B},A}} \\ \send*{B}{A}{\encrypted{A,B}{\nonce{b}}} \\ \send*{A}{B}{\encrypted{A,B}{\nonce{b}-1}} \end{steps*}\hfil%\\[-1ex] \captionof{figure}{{\aspen} example (what protocol is it?)}}% \hfil \parbox[t]{.46\linewidth}{{\small \vspace*{-1.6\baselineskip}\tableofcontents}} \footnotetext{{Originally, I had no intention to name the notation presented here. While working on this text, it became clear that it was inconvenient to not be able to refer to the notation with a short name. The name {\aspen} \emph{can} be an abbreviation for ``A Security Protocol Engineering Notation'', but for me it is now short for ``Anderson-inspired Standard Protocol Engineering Notation'', in memory of the late \href{https://www.cl.cam.ac.uk/archive/rja14/}% {Professor Ross J.\ Anderson} who has meant so much for the fields of computer security, distributed systems, and, in particular, \href{https://www.cl.cam.ac.uk/archive/rja14/book.html}{security engineering}~\cite{anderson2001a,anderson2008a,anderson2020a}.}} \clearpage \section{Introduction} \label{sec:intro} \begin{figure} {\renewcommand{\arraystretch}{1.2} \begin{xltabular}{\textwidth}{llX} Values: & \atrue, \sval{m}, \chash{m} & Values, structured values and typed structured values. In this notation a message is seen as a structured value. \\ Principals: & \apri{A}, \apri{B}, \apri{S} & Principals in security protocols, including clients, servers, and other participants. \\ Keys: & \key{A,B}, \key'{C,S}, \key+{A}, \key-{B} & Cryptographic keys, used to encrypt, decrypt, sign and verify values and messages. \\ Nonces: & \nonce{A}, \nonce{B}, \nonce{S} & Nonces are generated to be fresh and commonly include a timestamp or a number that is used only once. \\ Random: & \random{x}, \random'{1} & Random values can be a variant of nonces. The $\smark$ mark hints about limited useful lifetime (once, or during a session). \\ Time: & \ats{T_S}, \ats{T_A}, \attl{L} & Timestamps and lifetime are often used, together with nonces, to avoid replay and session keys that are too old. \\ Strings: & \astr{Hello world!} & Not necessary for the intended notation usage, but text strings are often found in examples in the litterateur. \\ Variables: & \avar{x}, \avar{y}, \avar{z}, \avar{a}, \avar{b}, \avar{c} & A variable can be assigned a value. Might also be used in the context of ``we are not sure about its value''. \\ Functions: & \chashf{m}, \func{Func}{\avar{x},\avar{y}}\ret\avar{z} & A function can take arguments and produce a value. Some functions are the constructor of typed structured values. \\ Labels: & \alabel{M_1}, \alabel{S_1} & Labels are used to label steps when a security protocols is presented as a series of steps. \\ {\latex} code: & \acmd{\Verb|\func{Func}{x,y}|} & {\latex} code is shown when documenting the usage of the notation in text using the {\latex} package \acmd{aspen}. \end{xltabular}\vspace*{\baselineskip}} \caption{In the text, color is used to distinguish different features} \label{fig:col} \end{figure} Why {\aspen} then? One motivation is to have an expressive notation that can be used in publications where security protocols are presented. Another motivation is to have a notation that can be used when teaching security related topics. This text is an attempt to document a notation that have been used and refined over years. The notation should be familiar, but with some new useful refinements and contributions not found in similar notations. It should also be possible to use the notations together with other notations, like BAN logic. A more detailed discussion on the choices made for the {\aspen} notation is found in Appendix~\ref{sec:notes-notation}, \emph{\nameref{sec:notes-notation}}. The {\latex} package can be downloaded from \href{https://www.ctan.org/tex-archive/macros/latex/contrib/aspen}{CTAN} or its home: \begin{quote} \href{https://www.pg12.org/dist/texmf/tex/latex/aspen/}{\acmd{https://www.pg12.org/dist/texmf/tex/latex/aspen/}} \end{quote} When using {\aspen}, colors can be used to distinguish different types of features. Figure~\ref{fig:col} illustrates how the different features are colored. Colors are optional when using the notation. They are enabled by the \acmd{color} option to the {\latex} package \acmd{aspen}. Colors are only added for readability. The {\latex} package \acmd{aspen} provides different color profiles for typesetting the notation (see Appendix~\ref{sec:notes-options}, \emph{\nameref{sec:notes-options}}). If the \acmd{aspen} package is loaded with the option \acmd{ban}, the BAN logic notation from ``A Logic of Authentication»~\cite{burrows1989a} is included (see Section~\ref{sec:notation-ban} and~\ref{sec:latex-ban}). \clearpage \section{The notations} \label{sec:notation} In the description of the notation below, notation that might be obvious is included. It is done for completeness and consistency. For some notations, usage examples are provided. These examples might include notations explained later in the text. \subsection{{\aspen}} \label{sec:notation-aspen} {\renewcommand{\arraystretch}{1.6} \begin{xltabular}{\textwidth}{lX}\Xhline{0.5pt} \textbf{Notation} & \textbf{Description} \\\Xhline{0.5pt} $=,<,\leq,>,\geq$ & $=$ means \emph{``is equal''}, either as a statement or a claim (e.g.,~a claim that can be, or has to be, verified). $<$, $\leq$, $>$ and $\geq$ means \emph{``less than''}, \emph{``less than or equal''}, \emph{``greather than''}, and \emph{``greather than or equal''}, respectively. These notations are typically used to compare counters and timestamps in protocols. \\\hline $\!\axor\!,\aconcat$ & The binary operator $\axor$ is exclusive or, and the binary operator $\aconcat$ is concatenation (used to concatenate two values or strings). The concatenation operator has precedence over the exclusive or operator. In Section \ref{sec:notes-options}, other options for the binary concatenation operator is presented. \\\hline $\aifthen,\aiffthen$ & $\avar{x}\aifthen\avar{y}$ means \emph{``\avar{y}, if~\avar{x}''}. $\avar{x}\aiffthen\avar{y}$ means \emph{``\avar{y}, if and only if~\avar{x}''}. This is an example used with the \afname{\verifytext} function (see below for the description of other notations used in the example): \newline \example{\verify+[big]{A}{\signed{x}{m}} = \atrue \enspace \aiffthen \enspace \key{x} = \privkey{A}} \\\hline $\avar{x}\leadsto\avar{y}$ & We use a leads-to arrow $\leadsto$ to show more details or to unpack a value or a message. The following example shows that a digital signature is actually a cryptographic hash value of the message encrypted with a private key (see below for the description of other notations used in the example): \newline \example{\sig-{A}{m}\leadsto\encrypted-[big]{A}{\chash{m}}} \\\hline \atrue, \afalse & The boolean values \emph{true} and \emph{false}. The value {\atrue} will also be used to show that an operation completed with success (if that is important). For example, when we verify a digital signature and it is found valid, the function doing the verification returns the value {\atrue}. Otherwise, the value {\afalse} is returned. \\\hline \key{X} & A shared or secret key, also known as a symmetric encryption and decryption key. \\\hline \key{A,B} & A shared key for \apri{A} and \apri{B} (this notation can be extended, for example with \key{A,B,C} for a key shared between \apri{A}, \apri{B}, and \apri{C}, or \key{\agroup{M}} for a key shared among $n$ group members \agroup*{M}). \\\hline \key'{C,S} & A session key for \apri{C} and \apri{S} (this notation can be extended, for example with \key'{A,B,S} for a key session key shared between \apri{A}, \apri{B}, and \apri{S}, or \key'{\agroup{M}} for a session key shared among $n$ group members \agroup*{M}). \\\hline \key+{A} & The public key of a public-private key pair of \apri{A}: $(\key+{A},\key-{A})$. \\\hline \key-{A} & The private key of a public-private key pair of \apri{A}: $(\key+{A},\key-{A})$. \\\hline \sval{m} & A structured value or message containing \aval{m}. A structured value can be nested. \\\hline \tval{\extxt{t}}{m} & A structured value or message with the type $\extxt{t}$. An example of a structured value marked with the type \aval{\textit{Sig}}: \newline \example{\sig!{A}{m}\mbox{ has the type \emph{\aval{\textit{\sigtext}}} and the superscript }\aname{A}\mbox{ (signed by \apri{A})}} \\\hline \send{A}{B}{m} & Message \msg{m} sent from \apri{A} to \apri{B}. \\\hline \func{\extxt{func}}{\avar{x},\avar{y}} & A function $\textit{\extxt{func}}$ with two arguments \avar{x} and \avar{y} (\afname{Encrypt} and \afname{Decrypt} described below are examples of such a function). \\\hline \func{\extxt{func}}{\avar{x},\avar{y}}[\avar{z}] & We use an arrow {\produces} to illustrate what a function produces (in this case \avar{z}). The following example shows that the function \afname{Encrypt} produces a ciphertext encrypted with the given shared key (see below for the description of other notations used in the example): \newline \example{\encrypt{A,B}{m}[\encrypted{A,B}{m}]} \\\hline \encrypted*{\raisebox{-2pt}{\akey{\square}}}{m} & In general, a subscripted structured value means an encrypted value or message (a ciphertext), where the subscript \raisebox{0pt}{\akey{\square}} represents the encryption key (or the holder of the encryption key). This is an example where the plain text \aval{m} is encrypted with the encryption key \akey{K}: \newline \example{\encrypted*{K}{m}} \\\hline \signed*{\raisebox{0pt}{\akey{\square}}}{m} & In general, a superscripted structured value means a signed value or message, where the superscript \raisebox{0pt}{\akey{\square}} represents the key used to sign (or the holder of the key used to sign). This is an example where the plain text \aval{m} is signed by principal \apri{A}: \newline \example{\signed!{A}{m}} \\\hline % \encrypted*{K}{m} % & Plain text \aval{m} is encrypted with key \akey{K}. % \\\hline % \encrypted+{A}{m} % & Plain text \aval{m} is encrypted with public key \key+{A}. % \\\hline \encrypt{A,B}{m} & Encrypt plain text \aval{m} with shared key \key{A,B}: \newline \example{\encrypt{A,B}{m}[\encrypted{A,B}{m}]} \\\hline \decrypt{A,B}{\avar{c}} & Decrypt cipher text \avar{c} with shared key \key{A,B}, where $\avar{c}=\encrypted{A,B}{m}$: \newline \example{\decrypt{A,B}{\avar{c}}\leadsto \decrypt[big]{A,B}{\encrypted{A,B}{m}}[m]} \\\hline \encrypt+{A}{m} & Encrypt plain text \aval{m} with public key \key+{A}: \newline \example{\encrypt+{A}{m}[\encrypted+{A}{m}]} \\\hline \decrypt-{A}{\avar{c}} & Decrypt cipher text \avar{c} with private key \key-{A}, where $\avar{c}=\encrypted+{A}{m}$: \newline \example{\decrypt-{A}{\avar{c}}\leadsto \decrypt-[big]{A}{\encrypted+{A}{m}}[m]} \\\hline \chash{m} & A cryptographic hash value of \aval{m}. \\\hline \chashf{m} & A cryptographic hash function producing the cryptographic hash value of \aval{m}: \newline \example{% \chashf{m}[\chash{m}]} \\\hline \mac{A}{m} & The message authentication code of \aval{m} with key \key{A}. \\\hline \cmac{A}{m} & The cipher-based message authentication code of \aval{m} with key \key{A}. \\\hline \hmac{A}{m} & The HMAC message authentication code of \aval{m} with key \key{A}. \\\hline \macf{A}{m} & The message authentication code function producing the message authentication code of \aval{m} with key \key{A}: \newline \example{\macf{A}{m}[\mac{A}{m}]} \\\hline \cmacf{A}{m} & The cipher-based message authentication code function producing the cipher-based message authentication code of \aval{m} with key \key{A}: \newline \example{% \cmacf{A}{m}[\cmac{A}{m}]} \\\hline \hmacf{A}{m} & The HMAC message authentication code function producing the HMAC message authentication code of \aval{m} with key \key{A}: \newline \example{% \hmacf{A}{m}[\hmac{A}{m}]\leadsto \chash[big]{\akey{\overline{K}_A}\axor\textit{opad}\aconcat \chash{\akey{\overline{K}_A}\axor\textit{ipad}\aconcat m}}\\ \akey{\overline{K}_A} \ = \ \; \Biggr\{ \raisebox{0pt}{% $\def\arraystretch{1}\begin{array}{ll} \chash{\key{A}} & \textrm{if \key{A} is larger than block size} \\ \key{A} & \textrm{otherwise} \end{array}$}}\newline The two block-sized paddings, \aval{\textit{opad}} (outer padding) and \aval{\textit{ipad}} (inner padding), each consists of a repeating byte value (\aval{0\textrm{x}5\textrm{c}} and \aval{0\textrm{x}36}, respectively). \\\hline \sig!{A}{m} & Digital (cryptographic) signature of \aval{m} signed by \apri{A}. \\\hline \sig-{A}{m} & Digital (cryptographic) signature of \aval{m} signed with private key \key-{A}: \newline \example{\sig-{A}{m}\leadsto\encrypted-[big]{A}{\chash{m}}} \\\hline \sig!{A,B}{m} & Digital (cryptographic) signature of \aval{m} based on shared secret between \apri{A} and \apri{B}. \\\hline \sig{A,B}{m} & Digital (cryptographic) signature of \aval{m} signed with the shared key \key{A,B} (a shared secret between \apri{A} and \apri{B}): \newline \example{\sig{A}{m}\leadsto\encrypted[big]{A,B}{\chash{m}}} \\\hline \sigf-{A}{m} & Function creating a digital (cryptographic) signature of \aval{m} with private key \key-{A}: \newline \example{\sigf-{A}{m}[\sig-{A}{m}]} \\\hline \sigf!{A,B}{m} & Function creating a digital (cryptographic) signature of \aval{m} based on shared secret between \apri{A} and \apri{B}: \newline \example{\sigf!{A,B}{m}[\sig!{A,B}{m}]} \\\hline \sigf{A,B}{m} & Function creating a digital (cryptographic) signature of \aval{m} with the shared key \key{A,B} (a shared secret between \apri{A} and \apri{B}): \newline \example{\sigf{A,B}{m}[\sig{A,B}{m}]} \\\hline \signed!{A}{m} & \aval{m} is signed by \apri{A} (\aval{m} signed is a combination of \aval{m} itself and a digital signature of \aval{m}, in this case a digital signature signed by \apri{A}): \newline \example{\signed!{A}{m}\leadsto\sval[big]{m,\sig!{A}{m}}} \\\hline \signed-{A}{m} & \aval{m} is signed with private key \key-{A} (\aval{m} signed is a combination of \aval{m} itself and a digital signature of \aval{m}, in this case a digital signature signed with \key-{A} implemented by encrypting the cryptographic hash value of \aval{m} with \key-{A}): \newline \example{\signed-{A}{m}\leadsto\sval[big]{m,\sig-{A}{m}} \leadsto\sval[Big]{m,\encrypted-[big]{A}{\chash{m}}}} \\\hline \signed!{A,B}{m} & \aval{m} is signed with shared secret of \apri{A} and \apri{B}\/ (\aval{m} signed is a combination of \aval{m} itself and a digital signature of \aval{m}, in this case a digital signature signed with a shared secret of \apri{A} and \apri{B}): \newline \example{\signed!{A,B}{m}\leadsto\sval[big]{m,\sig!{A,B}{m}}} \\\hline \signed{A,B}{m} & \aval{m} is signed with a shared secret of \apri{A} and \apri{B}; the shared key \key{A,B} (\aval{m} signed is a combination of \aval{m} itself and a digital signature of \aval{m}, in this case a digital signature signed with the shared key \key{A,B} implemented by encrypting the cryptographic hash value of \aval{m} with \key{A,B}): \newline \example{\signed{A,B}{m}\leadsto\sval[big]{m,\sig{A,B}{m}} \leadsto\sval[Big]{m,\encrypted[big]{A,B}{\chash{m}}}} \\\hline \sign!{A}{m} & \apri{A} signs \aval{m} (\aval{m} signed is a combination of \aval{m} itself and a digital signature of \aval{m}, in this case a digital signature signed by \apri{A} implemented by \aname{A} encrypting the cryptographic hash value of \aval{m}): \newline \example{\sign!{A}{m}[\signed!{A}{m}]\leadsto \sval[big]{m,\sig!{A}{m}}} \\\hline \sign-{A}{m} & Sign \aval{m} with private key \key-{A} (\aval{m} signed is a combination of \aval{m} itself and a digital signature of \aval{m}, in this case a digital signature signed with \key-{A} implemented by encrypting the cryptographic hash value of \aval{m} with \key-{A}): \newline \example{\sign-{A}{m}[\signed-{A}{m}]\leadsto \sval[big]{m,\sig-{A}{m}}\leadsto \sval[Big]{m,\encrypted-[big]{A}{\chash{m}}}} \\\hline \sign!{A,B}{m} & Sign \aval{m} with shared secret of \apri{A} and \apri{B} (\aval{m} signed is a combination of \aval{m} itself and a digital signature of \aval{m}, in this case a digital signature signed with a shared secret of \apri{A} and \apri{B} implemented by encrypting the cryptographic hash value of \aval{m} with a key based on a shared secret of \aname{A} and \aname{B}): \newline \example{\sign!{A,B}{m}[\signed!{A,B}{m}]\leadsto \sval[big]{m,\sig!{A,B}{m}}} \\\hline \sign{A,B}{m} & Sign \aval{m} with a shared secret of \apri{A} and \apri{B}\/; the shared key \key{A,B} (\aval{m} signed is a combination of \aval{m} itself and a digital signature of \aval{m}, in this case a digital signature signed with the shared key \key{A,B} implemented by encrypting the cryptographic hash value of \aval{m} with \key{A,B}): \newline \example{\sign{A,B}{m}[\signed{A,B}{m}]\leadsto \sval[big]{m,\sig{A,B}{m}}\leadsto \sval[Big]{m,\encrypted[big]{A,B}{\chash{m}}}} \\\hline \verify+{A}{\avar{s}} & Verify that the signed structured value (message) \avar{s} is signed by the matching private key \key-{A} of public key \key+{A} and, as a consequence, verify that \avar{s} is signed by~\apri{A}: \newline \example{% \verify+{A}{\avar{s}}\leadsto \verify+[big]{A}{\signed!{x}{m}} \leadsto \verify+[Big]{A}{\sval[big]{m,\sig!{x}{m}}}\leadsto \\ \verify+[Big]{A}{\sval[big]{m,\sig-{x}{m}}}\leadsto \verify+[bigg]{A}{\sval[Big]{m,\encrypted-[big]{x}{\chash{m}}}}: \\[1.5ex]\hline \begin{array}{c} \decrypt+[big]{A}{\sig!{x}{m}}=\chash{m} \enspace \leadsto \\ \decrypt+[big]{A}{\sig-{x}{m}}=\chash{m} \enspace \leadsto \\ \decrypt+[Big]{A}{\encrypted-[big]{x}{\chash{m}}}=\chash{m} \end{array} \raisebox{-2pt}{$\Bigggggr\}$} \quad \raisebox{-2pt}{$\aiffthen$} \quad \raisebox{-2pt}{$\key-{A} = \key-{x}$} \\[1.5ex]\hline \verify+{A}{\avar{s}}[\atrue] \quad \aiffthen \quad \key-{A} = \key-{x}} \\\hline \certificate!{C}{\apri{A},\key+{A}} & A certificate where CA \apri{C} binds identity \apri{A} to public key \key+{A} (where \aval{\ldots} is other certificate related meta-data): \newline \example{% \certificate!{C}{\apri{A},\key+{A}}\leadsto \signed!{C}{\apri{A},\key+{A},\aval{\ldots}}} \\\hline \certificate-{C}{\apri{A},\key+{A}} & A certificate where a CA with private key \key-{C} binds identity \apri{A} to public key \key+{A} (where \aval{\ldots} is other certificate related meta-data): \newline \example{% \certificate-{C}{A,\key+{A}}\leadsto \signed-{C}{A,\key+{A},\aval{\dots}} \\\hline \verify+{C}{\certificate-{C}{A,\key+{A}}}\enspace\leadsto \enspace\verify+{C}{% \signed-{C}{A,\key+{A},\aval{\dots}}}[\atrue]} \\\Xhline{0.5pt} \end{xltabular}} \subsection{BAN logic} \label{sec:notation-ban} The description below of the BAN logic notation is copied directly, with some minor modifications, from the original paper presenting the BAN logic, ``A Logic of Authentication''~\cite{burrows1989a}. {\renewcommand{\arraystretch}{1.6} \begin{xltabular}{\textwidth}{lX}\Xhline{0.5pt} \textbf{Notation} & \textbf{Description} \\\Xhline{0.5pt} \apri{A}\believes\aval{X} & \apri{A} \emph{believes} \aval{X}, or \apri{A} would be entitled to believe \aval{X}. In particular the principal \apri{A} may act as though \aval{X} is true. This construct is central to the BAN logic. \\\hline \apri{A}\sees\aval{X} & \apri{A} \emph{sees} \aval{X}. Someone has sent a message containing \aval{X} to \apri{A}, who can read and repeat \aval{X} possibly after doing some decryption. \\\hline \apri{A}\oncesaid\aval{X} & \apri{A} \emph{once said} \aval{X}. The principal \apri{A} at some time sent a message including the statement \aval{X}. It is not known whether the message was sent long ago or during the current run of the protocol, but it is known that \apri{A} believed \aval{X} when \apri{A} sent the message. \\\hline \apri{A}\controls\aval{X} & \apri{A} has \emph{jurisdiction} over \aval{X} (\apri{A} \emph{controls} \aval{X}). The principal \apri{A} is an authority on \aval{X} and should be trusted on this matter. This construct is used when a principal has delegated authority over some statement. For example, encryption keys need to be generated with some care, and in some protocols certain servers are trusted to do this properly. This may be expressed by the assumption that the principals believe that the server has jurisdiction over statements about the quality of keys. \\\hline \fresh{X} & The formula \aval{X} is \emph{fresh}, that is, \aval{X} has not been sent in a message at any time before the current run of the protocol. This is usually true for nonces, that is expressions generated for the purpose of being fresh (nonce---number used once). Nonces commonly include a timestamp or a number that is used only once, such as a sequence number. \\\hline \apri{A}\asharedkey{K}\apri{B} & \apri{A} and \apri{B} may use the \emph{shared key} \akey{K} to communicate. The key \akey{K} is good, in that it will never be discovered by any principal except \apri{A} or \apri{B}, or a principal trusted by either \apri{A} or~\apri{B}. (In {\aspen}, a shared key \apri{A} and \apri{B} may use to communicate can be denoted~\key{A,B}.) \\\hline \thepubkey{K}\apri{A} & \apri{A} has \akey{K} as a \emph{public key}. The matching secret key (the inverse of \akey{K}, denoted \akey{K^{-1}}) will never be discovered by any principal except \apri{A}, or a principal trusted by \apri{A}. (In {\aspen}, a public key of \apri{A} can be denoted \key+{A}, and the inverse of \key+{A}, the private key, can be denoted~\key-{A}.) \\\hline \apri{A}\asecret{X}\apri{B} & The formula \aval{X} is a \emph{secret} known only to \apri{A} and \apri{B}, and possibly to principals trusted by them. Only \apri{A} and \apri{B} may use \aval{X} to prove their identities to one another. Often \aval{X} is fresh as well as secret. An example of a shared secret is a password. \\\hline \encryptedwith{K}{X} & This represents the formula \aval{X} \emph{encrypted} under the key \akey{K}. Formally, \encryptedwith{K}{X} is an abbreviation for an expression of the form \encryptedwith{K}{X} \emph{from} \apri{A}. We make the realistic assumption that each principal is able to recognize and ignore his own messages; the originator of each message is mentioned for this purpose. In the in terests of brevity, we typically omit this in our examples. \\\hline \combine{\aval{X}}{\aval{Y}} & This represents \aval{X} \emph{combined} with the formula \aval{Y}; it is intended that \aval{Y} be a secret, and that its presence prove the identity of whoever utters\combine{\aval{X}}{\aval{Y}}. In implementations, \aval{X} is simply concatenated with the password \aval{Y}; our notation highlights that \aval{Y} plays a special r{\^o}le, as proof of origin for \aval{X}. The notation is intentionally reminiscent of that for encryption, which also guarantees the identity of the source of a message through knowledge of a certain kind of secret. \\\Xhline{0.5pt} \end{xltabular}} In the {\aspen} notation, when we write \key{A,B}, it is implicit that \apri{A} and \apri{B} may use \key{A,B} to communicate. We can use the BAN logic notation to make it explicit: \[ \apri{A}\asharedkey{\key{A,B}}\apri{B} \] In a similar manner, \key+{A} is in the {\aspen} notation implicit a \emph{public key} of \apri{A}. We can use the BAN logic notation to make it explicit: \[ \thepubkey{\key+{A}}\apri{A} \] Both the BAN logic notation and {\aspen} use the notation \encrypted*{K}{m} for the formula \aval{m} \emph{encrypted} under the key \key*{K} (\aval{m} encrypted with the key \key*{K}). In this case, {\aspen} has adopted the notation used in BAN logic and in a lot of other related publications and text books. \clearpage \section{Use the notations in text} \label{sec:write-notation-latex} This section explains how to use this notation in {\latex} documents. The new {\latex} commands and environments used are defined in the {\latex} package \acmd{aspen}. We will in the text include notation examples that might not make sense in a security protocol perspective. However, it is included for completeness. We will try to include a wide range of possibilities available from the {\latex} package \acmd{aspen}. \subsection{{\aspen}} \label{sec:latex-aspen} The table below lists the {\aspen} notation with the matching {\latex} commands. More examples of usage are found in Section \ref{sec:ex-notation-usage}. {\renewcommand{\arraystretch}{1.6} \begin{xltabular}{\textwidth}{l@{\hspace{.8em}}X}\Xhline{0.5pt} \textbf{Notation} & \textbf{{\latex} code and description} \\\Xhline{0.5pt} $\privkey[]{},\pubkey[]{},\sessionkey[]{},\;\ldots$ & Some command markers are used throughout the {\aspen} {\latex} package: \newline {\renewcommand{\arraystretch}{1}\begin{tabular}{c@{\::\:~}l} \acmd{*} & Means no specific variant (argument is the key, not the label of it): \acmd{\Verb|\key*{K}|} \\ \acmd{-} & Mark that it is a private key (from a public-private key pair): \acmd{\Verb|\key-{A}|} \\ \acmd{+} & Mark that it is a public key (from a public-private key pair): \acmd{\Verb|\key+{A}|} \\ \acmd{!} & Mark by principal instead of key (the key of): \acmd{\Verb|\key!{A}|} \\ \acmd{'} & Mark that it is temporary (session key or limited lifetime): \acmd{\Verb|\key'{A}|} \\ \end{tabular}}\newline \example{\begin{tabular}{lcl} \acmd{\Verb|\key*{K}|} & \givesarrow & $\key*{K}$ \\ \acmd{\Verb|\sig-{A}{m}|} & \givesarrow & $\sig-{A}{m}$ \\ \acmd{\Verb|\encrypt+{B}{m}|} & \givesarrow & $\encrypt+{B}{m}$ \\ \acmd{\Verb|\signed!{S}{m}|} & \givesarrow & $\signed!{S}{m}$ \\ \acmd{\Verb|\decrypt'{A,B}{c}|} & \givesarrow & $\decrypt'{A,B}{c}$ \end{tabular}} \\\hline $=,<,\leq,>,\geq$ & \acmd{=},\acmd{<},\acmd{\Verb|\leq|},\acmd{>},\acmd{\Verb|\geq|}, used to compare values. \\\hline $\!\axor\!,\aconcat$ & \acmd{\Verb|\axor|}, \acmd{\Verb|\aconcat|}, used as binary operators for \emph{exclusive or} and \emph{concatenation} (used to concatenate two values or strings), respectively. \\\hline $\aifthen,\aiffthen$ & \acmd{\Verb|\aifthen|},\acmd{\Verb|\aiffthen|}, used to reason about protocols and protocol steps (meaning, \emph{``if, then''} and \emph{``if, and only if, then''}, respectively). \\\hline $\extxt{x}\leadsto\extxt{y}$ & \acmd{\Verb|x \leadsto y|}, used to unpack more details. \\\hline $\aval{1},\aval{2}$ & \acmd{\Verb|\aval{1}|},\acmd{\Verb|\aval{2}|}, used for values. \\\hline $\atrue,\afalse$ & \acmd{\Verb|\atrue|},\acmd{\Verb|\afalse|}, used for the boolean values. \\\hline $\apri{A},\apri{B},\apri{S}$ & \acmd{\Verb|\apri{A}|},\acmd{\Verb|\apri{B}|},\acmd{\Verb|\apri{S}|}, used for principals. \\\hline $\anonce{N_A},\nonce{S}$ & \acmd{\Verb|\anonce{N_A}|},\acmd{\Verb|\nonce{S}|}, used for nonces. The \acmd{\Verb|\nonce|} command has an optional first argument to change the symbol (letter): \acmd{\Verb|\nonce[n]{0}|}\;\givesarrow\;\nonce[n]{0} \\\hline $\arandom{R_x},\random{y},\random'{1}$ & \acmd{\Verb|\arandom{R_x}|},\acmd{\Verb|\random{y}|},% \acmd{\Verb|\random'{1}|}, used for random values (the $\smark$ hints about limited useful lifetime). The \acmd{\Verb|\random|} command has an optional first argument to change the symbol (letter): \acmd{\Verb|\random[r]{z}|}\;\givesarrow\;\random[r]{z} \\\hline $\ats{T_A},\ts{S},\attl{L},\ttl{1}$ & \acmd{\Verb|\ats{T_A}|},\acmd{\Verb|\ts{S}|},\acmd{\Verb|\attl{L}|},% \acmd{\Verb|\ttl{1}|}, used for time related values, like time stamps and lifetime (time to live). Both the \acmd{\Verb|\ts|} and \acmd{\Verb|\ttl|} command have an optional first argument to change the symbol (letter): \acmd{\Verb|\ts[t]{0}|}\;\givesarrow\;\ts[t]{0}, \acmd{\Verb|\ttl[l]{1}|}\;\givesarrow\;\ttl[l]{1} \\\hline $\astr{Hello}$ & \acmd{\Verb|\astr{Hello}|}, used for text strings. \\\hline $\avar{x},\avar{y}$ & \acmd{\Verb|\avar{x}|},\acmd{\Verb|\avar{y}|}, used for variables. \\\hline $\akey{K}$ & \acmd{\Verb|\akey{K}|}, used for (non-specific) encryption keys. If you mark a key with a \acmd{*}, the produced output is the same: \newline \example{% \mbox{\acmd{\Verb|\key*{K}|}}\gives\key*{K}} \\\hline \key{A}, \sharedkey{A,B} & \acmd{\Verb|\key{A}|},\acmd{\Verb|\sharedkey{A,B}|}, used for shared (secret/symmetric) keys (provided by two different {\latex} commands, where the first is a more compact version; use whatever you prefer). The \acmd{\Verb|\sharedkey|} command has an optional first argument to change the symbol (letter): \acmd{\Verb|\sharedkey[k]{B}|}\;\givesarrow\;\sharedkey[k]{B} \\\hline \key'{C,S}, \sessionkey{A,B,S} & \acmd{\Verb|\key'{C,S}|},\acmd{\Verb|\sessionkey{A,B,S}|}, used for session keys (provided by two different {\latex} commands, where the first is a more compact version; use whatever you prefer). The \acmd{\Verb|\sessionkey|} command has an optional first argument to change the symbol (letter): \acmd{\Verb|\sessionkey[k]{A,B}|}\;\givesarrow\;\sessionkey[k]{A,B} \\\hline \key+{A}, \pubkey{B} & \acmd{\Verb|\key+{A}|},\acmd{\Verb|\pubkey{B}|}, used for public keys (provided by two different {\latex} commands, where the first is a more compact version; use whatever you prefer). The \acmd{\Verb|\pubkey|} command has an optional first argument to change the symbol (letter): \acmd{\Verb|\pubkey[k]{S}|}\;\givesarrow\;\pubkey[k]{S} \\\hline \key-{A}, \privkey{B} & \acmd{\Verb|\key-{A}|},\acmd{\Verb|\privkey{B}|}, used for private keys (provided by two different {\latex} commands, where the first is a more compact version; use whatever you prefer). The \acmd{\Verb|\privkey|} command has an optional first argument to change the symbol (letter): \acmd{\Verb|\privkey[k]{A}|}\;\givesarrow\;\privkey[k]{A} \\\hline % \key!{A}, \akey{\aname{B}} % & \acmd{\Verb|\key!{A}|},\acmd{\Verb|\akey{\aname{B}}|}, used for % unspecific keys of a principal (or a group of principals), typically % in the context of \emph{``encrypted by''}, or \emph{``signed by''}. % (two different {\latex} commands, where the first is a more compact % version). % \\\hline \aname{A} & \acmd{\Verb|\aname{A}|}, typically used to indicate who signed (or encrypted) a message, but no specific key is given, known or relevant. If you mark a key with a \acmd{!}, the produced output is the same: \newline \example{% \mbox{\acmd{\Verb|\key!{A}|}}\gives\key!{A}} \\\hline \agroup{M} & \acmd{\Verb|\agroup{M}|}, typically used as a label for a shared key shared within a group with $n$ members: \newline \example{% \mbox{\acmd{\Verb|\key{\agroup{M}}|}}\gives\key{\agroup{M}}} \\\hline \agroup[0][s]{M} & \acmd{\Verb|\agroup[0][s]{M}|}, where group member indexes are non-standard: \newline \example{% \mbox{\acmd{\Verb|\key{\agroup[0][s]{M}}|}}\gives \key{\agroup[0][s]{M}}} \\\hline \agroup*{M} & \acmd{\Verb|\agroup*{M}|}, typically used in a text when referring to a group (with $n$ members). \\\hline \agroup*[0][s]{M} & \acmd{\Verb|\agroup*[0][s]{M}|}, where group member indexes are non-standard. \\\hline \sval{m},\msg{\apri{A},\apri{B}} & \acmd{\Verb|\sval{m}|},\acmd{\Verb|\msg{\apri{A},\apri{B}}|}, used to type a structured value or message (a message can be seen as structured value). \\\hline \sval[big]{m} & \acmd{\Verb|\sval[big]{m}|}, or \acmd{\Verb|\msg[big]{m}|}, where first optional size argument can be \acmd{big}, \acmd{Big}, \acmd{bigg}, or \acmd{Bigg} for increased size of parenthesis (typically used with nested structured values and/or functions): \newline \example{% \mbox{\acmd{\Verb|\sval{x}|}}\gives\sval{x} \\ \mbox{\acmd{\Verb|\sval[big]{\sval{x}}|}}\gives \sval[big]{\sval{x}} \\ \mbox{\acmd{\Verb|\sval[Big]{\sval[big]{\sval{x}}}|}}\gives \sval[Big]{\sval[big]{\sval{x}}} \\ \mbox{\acmd{\Verb|\sval[bigg]{\sval[Big]{\sval[big]{\sval{x}}}}|}}% \gives\sval[bigg]{\sval[Big]{\sval[big]{\sval{x}}}}% }\vspace*{-2.2ex} \\ & We can even use more size specifiers: \acmd{big}, \acmd{Big}, \acmd{bigg}, \acmd{Bigg}, \acmd{biggg}, \acmd{Biggg}, \acmd{bigggg}, \acmd{Bigggg}, \acmd{biggggg}, and \acmd{Biggggg}: \newline \example{% \sval[Biggggg]{\sval[biggggg]{\sval[Bigggg]{\sval[bigggg]{% \sval[Biggg]{\sval[biggg]{\sval[Bigg]{\sval[bigg]{\sval[Big]{% \sval[big]{\sval{x}}}}}}}}}}}}\vspace*{-2.2ex} \\ & The optional size argument applies for all {\aspen} {\latex} commands that produces a pair of parenthesis, both ordinary parenthesis and curly brackets. A few examples (see below for more details on these commands):\newline \example{\begin{tabular}{lcl}% \mbox{\acmd{\Verb|\tval[big]{Type}{m}|}} & \givesarrow & \tval[big]{Type}{m} \\ \mbox{\acmd{\Verb|\send[big]{A}{B}{m}|}} & \givesarrow & \send[big]{A}{B}{m} \\ \mbox{\acmd{\Verb|\func[big]{Func}{x,y}|}} & \givesarrow & \func[big]{Func}{x,y} \\ \mbox{\acmd{\Verb|\encrypted[big]{A,B}{m}|}} & \givesarrow & \encrypted[big]{A,B}{m} \end{tabular}} \\\hline \tval{Type}{m} & \acmd{\Verb|\tval{Type}{m}|}, used for a typed structured value where the first argument is the type. \\\hline % \tval[big]{Type}{m} % & \acmd{\Verb|\tval[big]{Type}{m}|}, % where the optional argument of \acmd{\Verb|\tval|} can be % \acmd{big}, \acmd{Big}, \acmd{bigg}, or \acmd{Bigg} for % increased size of parenthesis (see examples with structured % values above). % \\\hline \send{A}{B}{m} & \acmd{\Verb|\send{A}{B}{m}|}, used to specify that a message \sval{m} is sent from \apri{A} to \apri{B}. \\\hline % \send[big]{A}{B}{m} % & \acmd{\Verb|\send[big]{A}{B}{m}|}, where the optional % argument of \acmd{\Verb|\send|} can be % \acmd{big}, \acmd{Big}, \acmd{bigg}, or \acmd{Bigg} for increased % size of parenthesis (see examples with structured values above). % \\\hline \send*{A}{B}{\avar{\extxt{x}}} & \acmd{\Verb|\send*{A}{B}{x}|}, used to specify that \avar{\extxt{x}} is sent from \apri{A} to \apri{B}, but \avar{\extxt{x}} is not wrapped as a structured value or message. This is typically used when what-is-sent is already wrapped as a structured value (e.g.,~encrypted or signed data): \newline \example{% \mbox{\acmd{\Verb|\send*{A}{B}{\encrypted+{B}{m}}|}}\gives \send*{A}{B}{\encrypted+{B}{m}}\\ \mbox{\acmd{\Verb|\send*{A}{B}{\encrypted+[big]{B}{\chash{m}}}|}}% \gives\send*{A}{B}{\encrypted+[big]{B}{\chash{m}}}} \\\hline \func{Func}{x,y} & \acmd{\Verb|\func{Func}{x,y}|}, used for any functions. \\\hline % \func[big]{Func}{x,y} % & \acmd{\Verb|\func[big]{Func}{x,y}|}, where first optional argument % can be \acmd{big}, \acmd{Big}, \acmd{bigg}, or \acmd{Bigg} % for increased size of parenthesis (see examples with structured % values above). % \\\hline \func{Func}{x,y}[z] & \acmd{\Verb|\func{Func}{x,y}[z]|}, used when the return value of the function is given. \\\hline % \func[big]{Func}{x,y}[z] % & \acmd{\Verb|\func[big]{Func}{x,y}[z]|}, used when the % return value of the function is given, and the first optional % argument is \acmd{big}, \acmd{Big}, \acmd{bigg}, or % \acmd{Bigg} for increased size of parenthesis (see examples with % structured values above). % \\\hline \encrypted{A,B}{m} & \acmd{\Verb|\encrypted{A,B}{m}|}, where the message is encrypted with an shared secret encryption key (in this case, the shared key \key{A,B} of \apri{A} and \apri{B}). The other options (with markers) are: % \acmd{*}~indicates that the message is encrypted with given key % (the first non-optional argument is the key, and not the label of the % key). % \acmd{+}~indicates that the message is encrypted with a public % key. \acmd{-}~indicates that the message is % encrypted with a private key (sometimes used in digital % signatures). \acmd{!}~indicates that the message is encrypted % by a principal (not specifying the specific encryption key). All the % different options of \acmd{\Verb|\encrypted|} demonstrated: \newline \example{% \begin{tabular}{lcl} \mbox{\acmd{\Verb|\encrypted*{K}{m}|}} & \givesarrow & \encrypted*{K}{m} \\ %\mbox{\acmd{\Verb|\encrypted{A,B}{m}|}} & \givesarrow %& \encrypted{A,B}{m} \\ \mbox{\acmd{\Verb|\encrypted+{A}{m}|}} & \givesarrow & \encrypted+{A}{m} \\ \mbox{\acmd{\Verb|\encrypted-{A}{m}|}} & \givesarrow & \encrypted-{A}{m} \\ \mbox{\acmd{\Verb|\encrypted!{A}{m}|}} & \givesarrow & \encrypted!{A}{m} \\ \mbox{\acmd{\Verb|\encrypted'{A,B}{m}|}} & \givesarrow & \encrypted'{A,B}{m} \end{tabular}} \\\hline % \encrypted[big]{A,B}{m} % & \acmd{\Verb|\encrypted[big]{A,B}{m}|}, where the optional % argument can be \acmd{big}, \acmd{Big}, \acmd{bigg}, or % \acmd{Bigg} for increased size of parenthesis (see examples with % structured values above). The optional size argument can be used for all % different options of \acmd{\encrypted} (see previous). % Typically used with structured values: % \newline % \example{% % \mbox{\acmd{\Verb|\encrypted+[big]{B}{\signed-{A}{m}}|}}\gives % \encrypted+[big]{B}{\signed-{A}{m}}} % \\\hline \encrypt{A,B}{m} & \acmd{\Verb|\encrypt{A,B}{m}|}, where the value \aval{m} is encrypted with a secret shared encryption key (in this case, a shared key of \apri{A} and \apri{B}). Other options are \acmd{*}, \acmd{+}, \acmd{-}, \acmd{!}, and \acmd{'} (see above for explanation). Since \acmd{\Verb|\encrypt|} is a function, we can include a return value as an optional last argument: \newline \example{% \mbox{\acmd{\Verb|\encrypt+{B}{m}[\encrypted+{B}{m}]|}}\gives \encrypt+{B}{m}[\encrypted+{B}{m}]} \\\hline % \encrypt[big]{A,B}{m} % & \acmd{\Verb|\encrypt[big]{A,B}{m}|}, where the first optional argument % can be \acmd{big}, \acmd{Big}, \acmd{bigg}, or \acmd{Bigg} % for increased size of parenthesis (see examples with structured values % above). Typically used with nested structured values: % \newline % \example{% % \mbox{\acmd{\Verb|\encrypt+[big]{B}{\signed-{A}{m}}|}}\gives % \encrypt+[big]{B}{\signed-{A}{m}}} % \\\hline \decrypt{A,B}{\avar{c}} & \acmd{\Verb|\decrypt{A,B}{\avar{c}}|}, where the cipher text \avar{c} is decrypted with an secret shared encryption key (in this case, a shared key between \apri{A} and \apri{B}). Other options are \acmd{*}, \acmd{+}, \acmd{-}, \acmd{!}, and \acmd{'} (see above for explanation). Since \acmd{\Verb|\decrypt|} is a function, we can include a return value as an optional last argument: \newline \example{% \mbox{\acmd{\Verb|\decrypt-{B}{\encrypted+{B}{m}}[m]|}}\gives \decrypt-{B}{\encrypted+{B}{m}}[m]} \\\hline % \decrypt[big]{A,B}{\avar{c}} % & \acmd{\Verb|\decrypt[big]{A,B}{\avar{c}}|}, where the first optional % argument can be \acmd{big}, \acmd{Big}, \acmd{bigg}, or \acmd{Bigg} % for increased size of parenthesis (see examples with structured values % above). Typically used with nested structured values: % \newline % \example{% % \mbox{\acmd{\Verb|\decrypt-[big]{B}{\encrypted+{B}{m}}[m]|}}% % \gives \decrypt-[big]{B}{\encrypted+{B}{m}}[m]} % \\\hline \chash{m} & \acmd{\Verb|\chash{m}|}, used for a cryptographic hash value of \aval{m}. \\\hline % \chash[big]{m} % & \acmd{\Verb|\chash[big]{m}|}, where the first optional argument % can be \acmd{big}, \acmd{Big}, \acmd{bigg}, or \acmd{Bigg} % for increased size of parenthesis (see examples with structured values % above). % \\\hline \chashf{m} & \acmd{\Verb|\chashf{m}|}, used for a cryptographic hash value function producing the cryptographic hash value of \aval{m}. \\\hline % \chashf[big]{m} % & \acmd{\Verb|\chashf[big]{m}|}, where the first optional argument % can be \acmd{big}, \acmd{Big}, \acmd{bigg}, or \acmd{Bigg} % for increased size of parenthesis (see examples with structured values % above). % \\\hline \mac{A}{m} & \acmd{\Verb|\mac{A}{m}|}, used for message authentication code of \aval{m} with \key{A}. \\\hline \cmac{A}{m} & \acmd{\Verb|\cmac{A}{m}|}, used for cipher-based message authentication code of \aval{m} with \key{A}. \\\hline \hmac{A}{m} & \acmd{\Verb|\hmac{A}{m}|}, used for HMAC message authentication code of \aval{m} with \key{A}. \\\hline \macf{A}{m} & \acmd{\Verb|\macf{A}{m}|}, used for a message authentication code function with the arguments \key{A} and \aval{m}. Since \acmd{\Verb|\macf|} is a function, we can include a return value as an optional last argument: \newline \example{\mbox{\acmd{\Verb|\macf{A}{m}[\mac{A}{m}]|}}\gives \macf{A}{m}[\mac{A}{m}]} \\\hline \cmacf{A}{m} & \acmd{\Verb|\cmacf{A}{m}|}, used for a cipher-based message authentication code with the arguments \key{A} and \aval{m}. Since \acmd{\Verb|\cmacf|} is a function, we can include a return value as an optional last argument: \newline \example{\mbox{\acmd{\Verb|\cmacf{A}{m}[\cmac{A}{m}]|}}\gives \cmacf{A}{m}[\cmac{A}{m}]} \\\hline \hmacf{A}{m} & \acmd{\Verb|\hmacf{A}{m}|}, used for a HMAC message authentication code with the arguments \key{A} and \aval{m}. Since \acmd{\Verb|\hmacf|} is a function, we can include a return value as an optional last argument: \newline \example{\mbox{\acmd{\Verb|\hmacf{A}{m}[\hmac{A}{m}]|}}\gives \hmacf{A}{m}[\hmac{A}{m}]} \\\hline \sig-{A}{m} & \acmd{\Verb|\sig-{A}{m}|}, used for the signature of \apri{A} on \aval{m}, where the \acmd{-} says that the signature is signed with a private key (in this case, the private key of \apri{A}). No markers, or the other command markers, can also be used (see the first item in this table for an overview of the command markers). % Other options are no markers, % \acmd{*}, \acmd{+} (rarely used) and~\acmd{!}: % \newline % \example{% % \begin{array}{lcl@{\quad}l} % \mbox{\acmd{\Verb|\sig{A,B}{m}|}} & \givesarrow % & \sig{A,B}{m} % & \mbox{Signature from shared key \key{A,B}} \\ % \mbox{\acmd{\Verb|\sig*{K}{m}|}} & \givesarrow % & \sig*{K}{m} % & \mbox{Signature from specific key \akey{K}} \\ % \mbox{\acmd{\Verb|\sig+{B}{m}|}} & \givesarrow % & \sig+{A}{m} % & \mbox{Signature from public key \key+{A}} \\ % \mbox{\acmd{\Verb|\sig!{A}{m}|}} & \givesarrow % & \sig!{A}{m} % & \mbox{Signature signed by \apri{A}} \\ % \mbox{\acmd{\Verb|\sig!{A,B}{m}|}} & \givesarrow % & \sig!{A,B}{m} % & \mbox{Signature based on a shared secret} % \end{array}} \\\hline \sigf-{A}{m} & \acmd{\Verb|\sigf-{A}{m}|}, used to create a signature of \apri{A} on \aval{m}, where the \Verb|-| says that the signature is signed with a private key (in this case, the private key of \apri{A}). No markers, or the other command markers, can also be used (see the first item in this table for an overview of the command markers). \\\hline \signed-{A}{m} & \acmd{\Verb|\signed-{A}{m}|}, used for \aval{m} signed, where the \acmd{-} says that the signature is signed with a private key (in this case, the private key of \apri{A}). No markers, or the other command markers, can also be used (see the first item in this table for an overview of the command markers). % Other, often used, options are % no marker, \acmd{*}, \acmd{+} (rarely used) and % \acmd{!}: % \newline % \example{% % \begin{array}{lcl@{\quad}l} % \mbox{\acmd{\Verb|\signed{A,B}{m}|}} & \givesarrow % & \signed{A,B}{m} % & \mbox{\aval{m} signed with shared key \key{A,B}} \\ % \mbox{\acmd{\Verb|\signed*{K}{m}|}} & \givesarrow % & \signed*{K}{m} % & \mbox{\aval{m} signed with specific key \akey{K}} \\ % \mbox{\acmd{\Verb|\signed+{A}{m}|}} & \givesarrow % & \signed+{A}{m} % & \mbox{\aval{m} signed with public key \key+{A}} \\ % \mbox{\acmd{\Verb|\signed!{A}{m}|}} & \givesarrow % & \signed!{A}{m} % & \mbox{\aval{m} signed by \apri{A}} \\ % \mbox{\acmd{\Verb|\signed!{A,B}{m}|}} & \givesarrow % & \signed!{A,B}{m} % & \mbox{\aval{m} signed with a shared secret} % \end{array}} \\\hline \sign-{A}{m} & \acmd{\Verb|\sign-{A}{m}|}, used to sign \aval{m}, where the \acmd{-} says that the signature is signed with a private key (in this case, the private key of \apri{A}). No markers, or the other command markers, can also be used (see the first item in this table for an overview of the command markers). \\\hline \verify+{A}{\avar{s}} & \acmd{\Verb|\verify+{A}{\avar{s}}|}, used to verify the signed data \avar{s}, where the \acmd{+} says that the signed data is verified towards the public key of \apri{A}. \\\hline \cert-{C}{A} & \acmd{\Verb|\cert-{C}{A}|}, used for a certificate binding the public key \akey+{A} (public key of \apri{A}) to the principal \apri{A}, where the \acmd{-} says that the signature is signed with a private key (in this case, the private key of the CA \apri{C}). \\\hline \certificate!{C}{\apri{B},\key+{B}} & \acmd{\Verb|\certificate!{C}{\apri{B},\key+{B}}|}, used for a certificate binding the public key \key+{B} (public key of \apri{B}) to the principal \apri{B}, where \acmd{!} says that the signature is signed by the CA \apri{C}. \\\hline ${}_{\aval{\ldots}}$ & \acmd{\Verb|_{…}|}, where the marker is used to provide more details about a structured value or a function. A few examples where the markers are \aval{\textit{MD5}}, \aval{\textit{RSA}}, \aval{\textit{AES}}, \aval{\textit{DSA}}, and \aval{\textit{SHA-2}}:\newline \example{\begin{tabular}{lcl} \mbox{\acmd{\Verb|\chash_{MD5}{m}|}} & \givesarrow & $\chash_{MD5}{m}$ \\ \mbox{\acmd{\Verb|\encrypt+_{RSA}{B}{m}|}} & \givesarrow & $\encrypt+_{RSA}{B}{m}$ \\ \mbox{\acmd{\Verb|\decrypt'_{AES}{A,B}{c}|}} & \givesarrow & $\decrypt'_{AES}{A,B}{c}$ \\ \mbox{\acmd{\Verb|\sig-_{DSA}{S}{m}|}} & \givesarrow & $\sig-_{DSA}{S}{m}$ \\ \mbox{\acmd{\Verb|\hmac_{SHA-2}{A}{m}|}} & \givesarrow & $\hmac_{SHA-2}{A}{m}$ \end{tabular}} \\\hline %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Final & test \\\Xhline{0.5pt} \end{xltabular}} \subsection{BAN logic} \label{sec:latex-ban} The table below lists the BAN logic notation with the matching {\latex} commands. These notations are available when the {\latex} package \acmd{aspen} is loaded with the option \acmd{ban}. {\renewcommand{\arraystretch}{1.6} \begin{xltabular}{\textwidth}{l@{\hspace{.8em}}X}\Xhline{0.5pt} \textbf{Notation} & \textbf{{\latex} code and description} \\\Xhline{0.5pt} \believes & \acmd{\Verb|\believes|}, used to state that someone \emph{believes} something (and acts as it is true): \newline \example{\mbox{\acmd{\Verb|\apri{A}\believes\aval{X}|}}\gives \apri{A}\believes\aval{X}} \\\hline \sees & \acmd{\Verb|\sees|}, used to state that someone sees something (Someone has sent a message to someone and they have bee able to read it): \newline \example{\mbox{\acmd{\Verb|\apri{A}\sees\aval{X}|}}\gives \apri{A}\sees\aval{X}} \\\hline \oncesaid & \acmd{\Verb|\oncesaid|}, used to state to someone at some time said something (someone some time sent a message including the statement): \newline \example{\mbox{\acmd{\Verb|\apri{A}\oncesaid\aval{X}|}}\gives \apri{A}\oncesaid\aval{X}} \\\hline \controls & \acmd{\Verb|\controls|}, used to state that someone has \emph{jurisdiction} (controls) over something: \newline \example{\mbox{\acmd{\Verb|\apri{A}\controls\aval{X}|}}\gives \apri{A}\controls\aval{X}} \\\hline \fresh{X} & \acmd{\Verb|\fresh{X}|}, used to state that something is fresh (\aval{X} has not been sent in a message at any time before in the current run of the protocol). \\\hline \asharedkey{K} & \acmd{\Verb|\asharedkey{K}|}, used to state that a key is shared: \newline \example{\mbox{\acmd{\Verb|\apri{A}\asharedkey{\key{A,B}}\apri{B}|}}\gives \apri{A}\asharedkey{\key{A,B}}\apri{B}} \\\hline \thepubkey{K} & \acmd{\Verb|\thepubkey{K}|}, used to state that a key is a public key of someone: \newline \example{\mbox{\acmd{\Verb|\thepubkey{\key+{A}}\apri{A}|}}\gives \thepubkey{\key+{A}}\apri{A}} \\\hline \asecret{X} & \acmd{\Verb|\asecret{X}|}, used to state that a secret (\aval{X}, in this case) is only known to them: \newline \example{\mbox{\acmd{\Verb|\apri{A}\asecret{X}\apri{B}|}}\gives \apri{A}\asecret{X}\apri{B}} \\\hline \encryptedwith{K}{X} & \acmd{\Verb|\encryptedwith{K}{X}|}, used to state that something is encrypted with the key (\aval{X} is encrypted with the key \akey{K}). \\\hline \combine{x}{y} & \acmd{\Verb|\combine{x}{y}|}, used to state that $x$ is combined with $y$: \newline \example{\mbox{\acmd{\Verb|\combine{\aval{X}}{\aval{Y}}|}}\gives \combine{\aval{X}}{\aval{Y}}} \\\Xhline{0.5pt} \end{xltabular}} \subsection{Series of steps} \label{sec:latex-steps} The {\latex} package \acmd{aspen} provides support for presenting a security protocol as a series of messages and steps with the \acmd{steps} environment. A message between to principals is in the \acmd{steps} environment is typeset with the familiar \acmd{\Verb|\send|} command. With \acmd{\Verb|\send|} commands, the \acmd{steps} environment can be used like this: \begin{ltxexample}{230pt} \begin{steps} \send*{A}{B}{\encrypted+{B}{m_1}}[m1] \\ \send*{B}{A}{\encrypted+{A}{m_2}}[m2] \end{steps} \end{ltxexample} Notice that each step is separated by the \acmd{\Verb|\\|} command. Each step is labeled and can be refereed to by its name (\acmd{\Verb|\ref{m1}|} {\givesarrow} \ref{m1}, and \acmd{\Verb|\ref{m2}|} {\givesarrow} \ref{m2}). The \acmd{steps*} version of the environment is without the labels: \begin{ltxexample}{209pt} \begin{steps*} \send*{A}{B}{\encrypted+{B}{m_1}} \\ \send*{B}{A}{\encrypted+{A}{m_2}} \end{steps*} \end{ltxexample} By default, the \acmd{steps} environment has two types of labels; \acmd{M} for messages and \acmd{S} for other steps. In the example above only messages (\acmd{\Verb|\send|} commands) are used. Other steps are given with the \acmd{\Verb|\astep|} or the \acmd{\Verb|\astepat|} commands. In the following example the \acmd{\Verb|\astep|} command is used and the space between the label and the step is adjusted with the optional key-value argument \acmd{lspace} (the default value is \acmd{1.5em}): \begin{ltxexample}{170pt} \begin{steps}[lspace=1em] \astep{\encrypt+{B}{m_1}% [\encrypted+{B}{m_1}]} \\ \astep{\sign-[big]{A}{% \encrypted+{B}{m_1}}% [{\signed-[big]{A}{% \encrypted+{B}{m_1}}}]} \end{steps} \end{ltxexample} The optional key-value argument \acmd{rmarg} sets the right margin width of the steps environment and \acmd{lmarg} sets the left margin width of the steps environment. The default margin widths are \acmd{\Verb|\tabcolsep|}. In the following example the margins are removed: \begin{ltxexample}{190pt} \begin{steps*}[lmarg=0pt,rmarg=0pt] \astep{No margins} \end{steps*} \end{ltxexample} We can also change the margins, and the space between the label and the step, by adjusting the lengths \acmd{\Verb|\stepsleftmargin|}, \acmd{\Verb|\stepsrightmargin|} and \acmd{\Verb|\stepslabelspace|}. To change these values for the whole document we can place these commands at the beginning of the {\latex} file (after the {\latex} package \acmd{aspen} is loaded): \begin{ltxexample*}{178pt} \setlength{\stepsleftmargin}{0pt} \setlength{\stepsrightmargin}{0pt} \setlength{\stepslabelspace}{1em} \end{ltxexample*} The \acmd{\Verb|\astepat|} command can be used to specified \emph{where} a step is performed. The command has an extra first argument where this is specified (in this example, at principal \apri{A}): \begin{ltxexample}{182pt} \begin{steps}* \astepat{A}{\sign-{A}{m_1}% [\signed-{A}{m_1}]} \\ \astepat{A}{\encrypt+[big]{B}{% \signed-{A}{m_1}}% [{\encrypted+[big]{B}{% \signed-{A}{m_1}}}]} \end{steps} \end{ltxexample} The \acmd{*} marker of the \acmd{steps} environment (not to be confused with the \acmd{steps*} version of the environment) means that the counters of the labels are \emph{not} reset (the counting continues from the previous \acmd{steps} environment). It is also possible to add new types of labels with the optional key-value argument \acmd{labels}. In this example, new label types \acmd{A} and \acmd{B} are introduced and the \acmd{\Verb|\astepat|} commands are labeled with the new label types by using the optional first argument to the command: \begin{ltxexample}{207pt} \begin{steps}[labels={A,B}] \astepat[A]{A}{\encrypt+{B}{m_1}% [\encrypted+{B}{m_1}]} \\ \send*{A}{B}{\encrypted+{B}{m_1}} \\ \astepat[B]{B}{\decrypt-[big]{B}{% \encrypted+{B}{m_1}}[m_1]} \end{steps} \end{ltxexample} The \acmd{\Verb|\astepat*|} version of the \acmd{\Verb|\astepat|} command changes the horizontal position of the text of such steps so the colons are aligned: \begin{ltxexample}{242pt} \begin{steps*} \send*{A}{B}{\signed-{A}{m_1}} \\ \astepat*{B}{\verify+{A}{\signed-{A}{m_1}}} \end{steps*} \end{ltxexample} The \acmd{\Verb|\astep*|} version of the \acmd{\Verb|\astep|} command changes the horizontal position of the text of the step in a similar way: \begin{ltxexample}{215pt} \begin{steps*} \send*{A}{B}{\signed-{A}{m_1}} \\ \astep*{\verify+{A}{\signed-{A}{m_1}}} \end{steps*} \end{ltxexample} The \acmd{\Verb|\arawstep|} command is a low-level command that we usually is not necessary. In a \acmd{steps*} environment it has four optional arguments followed by one non-optional argument. In a \acmd{steps} environment another optional first argument and an optional last argument is added related to the labels of the step. To better understand the command we show it here used together with a \acmd{\Verb|\send|} command in a \acmd{steps} environment: \begin{ltxexample}{184pt} \begin{steps} \send{A}{B}{m}[s1] \\ \arawstep[M][a][--][b][;]{m}[s2] \end{steps} \end{ltxexample} % The last optional argument of the commands \acmd{\Verb|\send|} and % \acmd{\Verb|\arawstep|} is a label name that we can use to refer to these % steps, \ref{s1} and \ref{s2} in this case. The first optional argument % of \acmd{\Verb|\arawstep|} is the label type for this step. The \acmd{steps} % environment has two default label types, \acmd{S} for the steps % commands and \acmd{M} for the send commands (messages). In the example, % the \acmd{\Verb|\arawstep|} command uses the \acmd{M} label type instead of the % default S label type. The next five arguments (four optional arguments % and one non-optional argu- ment) illustrate how the \acmd{\Verb|\arawstep|} % command can be used to place elements at the different horizontal % positions of a line representing one step in \acmd{steps} or % \acmd{steps*} environments. % \begin{center} % \begin{minipage}[c]{0.49\linewidth} % \begin{minted}{latex} % \begin{steps} % \astepat{A}{\encrypt+{B}{m_1}% % [\encrypted+{B}{m_1}]} \\ % \send*{A}{B}{\encrypted+{B}{m_1}} \\ % \astepat{B}{\decrypt-[big]{B}{% % \encrypted+{B}{m_1}}[m_1]} \\ % \astepat{B}{\encrypt+{A}{m_2}% % [\encrypted+{A}{m_2}]} \\ % \send*{B}{A}{\encrypted+{A}{m_2}} \\ % \astepat{A}{\decrypt-[big]{A}{% % \encrypted+{A}{m_2}}[m_2]} % \end{steps} % \end{minted} % \end{minipage}\gives % \begin{steps} % \astepat{A}{\encrypt+{B}{m_1}% % [\encrypted+{B}{m_1}]} \\ % \send*{A}{B}{\encrypted+{B}{m_1}} \\ % \astepat{B}{\decrypt-[big]{B}{% % \encrypted+{B}{m_1}}[m_1]} \\ % \astepat{B}{\encrypt+{A}{m_2}% % [\encrypted+{A}{m_2}]} \\ % \send*{B}{A}{\encrypted+{A}{m_2}} \\ % \astepat{A}{\decrypt-[big]{A}{% % \encrypted+{A}{m_2}}[m_2]} % \end{steps} % \end{center} \section{Notation usage examples} \label{sec:ex-notation-usage} % \send{A}{B}{m}, \send[big]{A}{B}{\msg{m, A}}, % \send*{A}{B}{\encrypted{A,B}{m}}, \send*{A}{B}{\encrypted+{B}{m}} To illustrate the usability of the notation, a few examples where the notation is used to describe well-known, and not so well-known, security protocols. The \emph{Needham–Schroeder protocol}~\cite{needham1978a} aims to establish a session key between two parties on a network, typically to protect further communication. The protocol is based on a symmetric encryption and it forms the basis for the Kerberos protocol. In {\aspen}, the original Needham–Schroeder protocol is written like seen in Figure~\ref{fig:ns-protocol}. \anonce{N_a} and \anonce{N_b} are nonces and the shared key \key{A,B} should be fresh, \fresh{\key{A,B}}. \begin{figure} \begin{center} \begin{steps} \send{A}{S}{A, B, \nonce{a}} \\ \send*{S}{A}{\encrypted[big]{A,S}{\nonce{a}, B, \key{A,B}, \encrypted{B,S}{\key{A,B}, A}}} \\ \send*{A}{B}{\encrypted{B,S}{\key{A,B}, A}} \\ \send*{B}{A}{\encrypted{A,B}{\nonce{b}}} \\ \send*{A}{B}{\encrypted{A,B}{\nonce{b} - 1}} \end{steps} \end{center} \caption{The original Needham-Schroeder protocol} \label{fig:ns-protocol} \end{figure} The \emph{Kerberos protocol}~\cite{steiner1988a} is based on the Needham-Schroeder protocol, but makes use of timestamps as nonces to remove the problems of the Needham-Schroeder protocol and to reduce the number of messages needed. Figure \ref{fig:kerberos-protocol} shows the Kerberos protocol in {\aspen}. \ats{T_s} and \ats{T_a} are timestamps and \ats{L} is a lifetime. \begin{figure} \begin{center} \begin{steps} \send{A}{S}{A, B} \\ \send*{S}{A}{\encrypted[big]{A,S}{\ts{s}, \ttl{}, \key{A,B}, \apri{B}, \encrypted{B,S}{\ts{s}, \ttl{}, \key{A,B}, \apri{A}}}} \\ \send[big]{A}{B}{\encrypted{B,S}{\ts{s}, \ttl{}, \key{A,B}, \apri{A}}, \encrypted{A,B}{\apri{A}, \ts{a}}} \\ \send*{B}{A}{\encrypted{A,B}{\ts{a} + 1}} \end{steps} \end{center} \caption{The Kerberos protocol} \label{fig:kerberos-protocol} \end{figure} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \appendix \clearpage \bibliographystyle{splncs04x} \bibliography{aspen-doc} \clearpage \section{Notes} \subsection{Notes on the suggested notation} \label{sec:notes-notation} The notations used for security protocols in different articles and textbooks is not consistent. {\aspen} is an attempt to create one consistent notation. Mostly, for my own usage, but if the suggested notation is found useful for others, it is a nice bonus. In the following, the choices of {\aspen} will be discussed and compared with similar notations used in articles and textbooks. This is not an attempt to provide a complete overview over existing notations and how they compare to {\aspen}. It is more a discussion of notations that inspired {\aspen} and the choices made in the suggested notation. \href{mailto:Anders.Andersen@uit.no?subject=Feedback Aspen}{Feedback} on the notation are welcome. The notation used in the original Kerberos documentation includes secret keys (called private keys, but they are not the private key of a public-private key pair), session keys and encrypted messages. Below, {\aspen} is compared with the notation used in litterateur. The following sources of different notations are used: \vspace*{-1.7ex} \begin{enumerate} \item {\aspen} \label{not:aspen} \item Kerberos: An Authentication Service for Open Network Systems~\cite{steiner1988a} \label{not:kerberos} \item A formal semantics for protocol narrations~\cite{briais2007a} \label{not:prot-narrations} \item Security Engineering: A Guide to Building Dependable Distributed Systems~\cite{anderson2020a} \label{not:anderson} \item Current Approaches to Authentication in Wireless and Mobile Communications Networks~\cite{schafer2001a} \label{not:mob} \end{enumerate} \newcolumntype{C}{>{\small}c} \newcolumntype{Y}{>{\small\centering}X} {\renewcommand{\arraystretch}{1.3} \begin{xltabular}{\textwidth}{lYYYYYc}\Xhline{0.5pt} \textbf{Description} & \textbf{\ref{not:aspen}} & \textbf{\ref{not:kerberos}} & \textbf{\ref{not:prot-narrations}} & \textbf{\ref{not:anderson}} & \textbf{\ref{not:mob}} & $\mathbf{\ast}$ \\\Xhline{0.5pt} Secret key & \key{A} & \akey{K_A} & \akey{k_A} & \akey{K} & \akey{K_A} & C \\ Shared key & \key{A,B} & $-$ & \akey{k_{A\;B}} & $-$ & $-$ & C \\ Session key & \key'{A,B} & \akey{K_{A,\averythinspace B}} & $-$ & $-$ & $-$ & B \\ Public key & \key+{A} & $-$ & \akey{\textrm{pub}(k_A)} & \akey{KR} & \akey{+K_A} & A \\ Private key & \key-{A} & $-$ & \akey{\textrm{priv}(k_A)} & \akey{KR^{-1}} & \akey{-K_A} & A \\ Encrypted & \encrypted*{\akey{K}}{m} & $\msg{m}\akey{K}$ & $\msg{m}_{\akey{K}}$ & $\msg{m}_{\akey{K}}$ & $\msg{m}_{\akey{K}}$ & C \\ Signed with & \signed*{\akey{K}}{m} & $-$ & $-$ & \aval{\textrm{sig}_{\akey{K}}\{m\}} & $-$ & A \\ Signed by & \signed!{A}{m} & $-$ & $-$ & $-$ & \aval{\apri{A}\,[m]} & A \\ Send & \csend{A}{B}{m} & \raisebox{-1.5pt}{% \begin{mplibcode} draw fullcircle scaled 10pt shifted (-10pt,0); label(btex $\scriptstyle \apri{A}$ etex, (-10pt,0)); drawarrow (-5pt,0)--(5pt,0); label(btex $\scriptstyle \aval{m}$ etex, (0,3.5pt)); draw fullcircle scaled 10pt shifted (10pt,0); label(btex $\scriptstyle \apri{B}$ etex, (10pt,0)); \end{mplibcode}} & $\apri{A}\!\leadsto\!\apri{B}\!:\!\aval{m}$ & $\apri{A}\!\csends\!\apri{B}\!:\!\aval{m}$ & $\apri{A}\!\csends\!\apri{B}\!:\!\aval{m}$ & B \\ Hash value & \chash{m} & $-$ & \aval{\textrm{H}(m)} & \aval{\textit{h}(m)} & \aval{\textit{H}(m)} & B \\ MAC & \mac*{\akey{K}}{m} & $-$ & $-$ & \aval{\textrm{MAC}_{\akey{K}}(m)} & $-$ & B \\ HMAC & \hmac*{\akey{K}}{m} & $-$ & $-$ & \aval{\textrm{HMAC}_{\akey{K}}(m)} & $-$ & B \\ Signature & \sig*{\akey{K}}{m} & $-$ & $-$ & $-$ & $-$ & A \\ Certificate & \certificate-{CA}{\apri{A},\key+{A}} & $-$ & $-$ & \aval{\textit{Cert}_{\akey{KC^{-1}}}\!(A,\akey{KR})} & \aval{\textit{Cert}_{\akey{-K_{CA}}}\!(\akey{+K_A})} & B \\ Certificate by & \certificate!{CA}{\apri{A},\key+{A}} & $-$ & $-$ & $-$ & \aval{\apri{CA}\,\langle\langle\,\apri{A}\,\rangle\rangle} & A \\\Xhline{0.5pt} \end{xltabular}} In the table, the rightmost column classifies the notation in these groups: \vspace*{-1.7ex} \begin{itemize} \item[C:] The notation is commonly used in textbooks and other publications \item[B:] The notation (or similar) is found in textbooks and other publications \item[A:] The notation is believed to be unique for {\aspen} (invented here) \end{itemize} \subsection{Notes on the typesetting options} \label{sec:notes-options} \subsubsection*{Colors} The {\latex} package \acmd{aspen} provides the option \acmd{color}: \begin{quote} \acmd{\Verb|\usepackage[color]{aspen}|} \end{quote} The package provides different color profiles. The default color profile is called \acmd{aspen}. Other color profiles are loaded by assigning a color profile to the \acmd{color} option. The following statement will load the same default color profile as the example above: \begin{quote} \acmd{\Verb|\usepackage[color=aspen]{aspen}|} \end{quote} In addition, a few color profiles from \href{https://pygments.org/}{Pygments} are available: \acmd{autumn}, \acmd{colorful}, \acmd{default} (the default profile of Pygments), \acmd{emacs}, \acmd{friendly}, %\acmd{fruity}, \acmd{gruvboxlight} (called \acmd{gruvbox-light} in Pygments), \acmd{manni}, and \acmd{staroffice}. Figure \ref{fig:color-profiles} shows the colors of all the color profiles of the {\aspen} package. \makeatletter \def\mkcolorprofiletbl#1{% \begin{tabular}[c]{l@{\,\,}cl} \multicolumn{3}{l}{\textbf{\acmd{#1}}} \\\hline Value & \texttt{\small no} & {\csname #1@PY@tok@no\endcsname \PY@tc{\@aval{1}}, \PY@tc{\@atrue}} \\ Principle & \texttt{\small na} & {\csname #1@PY@tok@na\endcsname \PY@tc{\@apri{A}}} \\ Key & \texttt{\small kt} & {\csname #1@PY@tok@kt\endcsname \PY@tc{\@sharedkey{K}{A}}} \\ Nonce & \texttt{\small nn} & {\csname #1@PY@tok@nn\endcsname \PY@tc{\@anonce{N_1}}} \\ Timestamp & \texttt{\small nt} & {\csname #1@PY@tok@nt\endcsname \PY@tc{\@ats{T_s}}} \\ String & \texttt{\small sc} & {\csname #1@PY@tok@sc\endcsname \PY@tc{\@astr{Hello}}} \\ Variable & \texttt{\small nv} & {\csname #1@PY@tok@nv\endcsname \PY@tc{\@avar{x}}, \PY@tc{\@avar{y}}, \PY@tc{\@avar{z}}} \\ Function & \texttt{\small nf} & {\csname #1@PY@tok@nf\endcsname \PY@tc{\@afunc{H(\@aval{m})}}} \\ Code & \texttt{\small go} & {\csname #1@PY@tok@gp\endcsname \PY@tc{\@acmd{\textbackslash key\{A\}}}} \\ Label & \texttt{\small nl} & {\csname #1@PY@tok@nl\endcsname \PY@tc{\@alabel{M_1}}} \end{tabular}}% \makeatother \begin{figure} \begin{center} \mkcolorprofiletbl{aspen}\qquad \mkcolorprofiletbl{autumn}\qquad \mkcolorprofiletbl{colorful}\\[.5em] \mkcolorprofiletbl{default}\qquad \mkcolorprofiletbl{emacs}\qquad \mkcolorprofiletbl{friendly}\\[.5em] % \mkcolorprofiletbl{fruity}\qquad \mkcolorprofiletbl{gruvboxlight}\qquad \mkcolorprofiletbl{manni}\qquad \mkcolorprofiletbl{staroffice} \end{center} \caption{The color profiles of the \texttt{\textcolor{NavyBlue}{aspen}} package} \label{fig:color-profiles} \end{figure} \subsubsection*{Other typesetting options} \makeatletter \def\tradpubkey#1{\@tradpubkey{K}{#1}}% \def\tradprivkey#1{\@tradprivkey{K}{#1}}% \makeatother The default way of typesetting the public and the private key of the public-private key pair of \apri{A} in {\aspen} is with a $+$ superscript and a $-$ superscript, like \key+{A} and \key-{A} respectively. This behavior can be changed with the to package options \acmd{tradpubkey} and \acmd{tradprivkey}: \begin{quote} \acmd{\Verb|\usepackage[tradpubkey,tradprivkey]{aspen}|} \end{quote} The result is that the public key of \apri{A} will be typeset \akey{\tradpubkey{A}} and the private key of \apri{A} will be typeset \akey{\tradprivkey{A}}. The default way of typesetting concatenation in {\aspen} is with the binary operator ``$\aconcat$'' (used to typeset concatenation of two values or strings). The {\aspen} package provides three options for typesetting concatenation: ``$\adotconcat$'', ``$\adblbarconcat$'', or ``$\aplusconcat$''. This can be changed by passing a value to the \acmd{concat} option of the package. The valid values are \acmd{dot}, \acmd{dblbar}, and \acmd{plus}. The default is ``$\aconcat$''. In this example ``$\adblbarconcat$'' is chosen to be the concatenation operator: \begin{quote} \acmd{\Verb|\usepackage[concat=dblbar]{aspen}|} \end{quote} \end{document}