\documentclass{article} \usepackage{rcs} \RCS$Date: 2026/04/14 10:46:07 $ \RCS$RCSfile: aspen-doc.ltx,v $ \RCS$Revision: 2.5 $ \RCS$State: Exp $ \RCS$Author: aa $ \edef\AADate{\RCSDate} \edef\AARawDate{\RCSRawDate} %\typeout{XXX: \AARawDate} \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=2.8cm]{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{comment} % This is used for MetaPost figures in the text. Some figures might % use my two MetaPost packages aamisc and aaobj: % https://www.pg12.org/dist/texmf/mp/aaobj/ \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 input aamisc; input aaobj; numeric width, height, orad, v; orad:=0.5cm; width:=5orad; height:=3orad; v:=27; pair p[], q[], c, d; 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 \setcounter{tocdepth}{2} %\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} \renewenvironment{quote}{% \list{}{\listparindent=0em %\itemindent=\listparindent %\leftmargin=\parindent \rightmargin=\leftmargin \topsep=0em \partopsep=0em \parsep\z@\@plus\p@}% \item\relax}{\endlist} \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}{@{\hskip 2pt\relax}c@{\hskip 2pt\relax}}#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} \newif\iftolfileexists \newcommand\ttol[2]{\hyperlink{ttol:#1}{\emph{#2}}} \newcommand\tableoflisting{% \IfFileExists{aspen-doc.tol}{\tolfileexiststrue}{\tolfileexistsfalse}% \begin{tabular}{@{\qquad}ll} \iftolfileexists \input{aspen-doc.tol} \fi \end{tabular}\vspace*{-\baselineskip} % Compensate for last \\ \newwrite\tolfile \immediate\openout\tolfile=\jobname.tol } \newcommand\tol[2]{% \hypertarget{ttol:#1}{\subsection*{#2}}%{\textbf{#2}~} \immediate\write\tolfile{\unexpanded{$\bullet$\quad\ttol}{#1}{#2} & {\unexpanded{\latex}} code: \unexpanded{\refltxcode}{#1} \unexpanded{\\}}} \newwrite\locfile \immediate\openout\locfile=\jobname.loc \newenvironment{ltxcode}[2]{% % #1 label / file name % #2 Title / description \VerbatimEnvironment \def\lblfn{#1}% \def\locdesc{#2}% \begin{VerbatimOut}[gobble=2]{loc/#1.tex}} {\end{VerbatimOut}% \immediate\write\locfile{\unexpanded{\subsubsection}{\locdesc}}% \immediate\write\locfile{\unexpanded{\label}{loc:\lblfn}}% \immediate\write\locfile{\unexpanded{\VerbatimInput}{loc/\lblfn .tex}}% \immediate\write\locfile{\unexpanded{\global\let\ASteplabel\AEatit}}% \immediate\write\locfile{\unexpanded{\input}{loc/\lblfn .tex}}% \immediate\write\locfile{\unexpanded{\global\let\ASteplabel\label}}} \newcommand\useltxcode[1]{\input{loc/#1.tex}} \newcommand\showltxcode[1]{\VerbatimInput{loc/#1.tex}} \newcommand\refltxcode[1]{\ref{loc:#1}} \newcommand\pagerefltxcode[1]{\pageref{loc:#1}} \newenvironment{ltxex}[2]{% \VerbatimEnvironment \def\lfn{#1}% \def\ltitle{#2}% \begin{ltxcode}{#1}{#2}} {\end{ltxcode}% \qquad \begin{tabular}{@{\hskip 1pt\relax}l@{}} \emph{\ltitle} \\\hline \\[-1.3\medskipamount] \begin{tabular}{@{}l@{}} \useltxcode{\lfn} \end{tabular} \end{tabular}} \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}} % \newcommand\cmdargs[2]{\ACmd{\textbackslash\Verb|#1|}: \ACmd{\Verb|#2|}} \NewDocumentCommand\cmdargs{mmo}{% \ACmd{\textbackslash\Verb|#1|}: \ACmd{\Verb|#2|}% \IfValueT{#3}{\AReturns{\ACmd{\Verb|#3|}}}} \NewDocumentCommand\cmdmarg{m}{% \ACmd{\{\emph{<#1>}\}}} \NewDocumentCommand\cmdoarg{m}{% \ACmd{[\emph{<#1>}]}} \NewDocumentCommand\cmdparg{m}{% \ACmd{(\emph{<#1>})}} \NewDocumentCommand\cmdtarg{m}{% \ACmd{\emph{<#1>}}} \NewDocumentCommand\cmdkarg{}{% \cmdtarg{T}} \NewDocumentCommand\cmdsarg{}{% \cmdtarg{*}} \NewDocumentCommand\cmdearg{}{% \ACmd{\Verb|_|\{\emph{}\}}} \NewDocumentCommand\cmdargexx{mm}{% \ACmd{\emph{\textbackslash\Verb|#1|}#2}} \NewDocumentCommand\cmdargex{mmo}{% \ACmd{\textbackslash\Verb|#1|#2}% \IfValueT{#3}{\newline\AReturns{#3}}} \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 security protocol notation} \author{Anders Andersen\\[.3\baselineskip] UiT The Arctic University of Norway} \date{\AARawDate\\[.2\baselineskip] (\ACmd{aspen.sty} version \RCSRevision)} \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}\footnotemark{} 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, the BAN logic notation is included in the documentation. \parbox[t]{.47\linewidth}{% The {\Aspen} notation is \emph{not} a formalism, like BAN (Burrows–Abadi–Needham) logic~\cite{burrows1990a}, 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{ASteps*} \ASend{A}{S}{\APri{A},\APri{B},\ANonce{A}} \\ \ASend*{S}{A}{\AEncrypted{A,S}{\ANonce{A},\APri{B},\AKey{A,B},% \AEncrypted{B,S}{\AKey{A,B},\APri{A}}}} \\ \ASend*{A}{B}{\AEncrypted{B,S}{\AKey{A,B},A}} \\ \ASend*{B}{A}{\AEncrypted{A,B}{\ANonce{B}}} \\ \ASend*{A}{B}{\AEncrypted{A,B}{\ANonce{B}-1}} \end{ASteps*}\hfil%\\[-1ex] \captionof{figure}{{\Aspen} example (what protocol is it?)}}% \hfil \parbox[t]{.46\linewidth}{{\small \vspace*{-2\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, \ASval{m}, \AChash{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: & \AKey{A,B}, \AKey'{C,S}, \AKey+{A}, \AKey-{B} & Cryptographic keys, used to encrypt, decrypt, sign and verify values and messages. \\ Nonces: & \ANonce{A}, \ANonce{B}, \ANonce{S} & Nonces are generated to be fresh and commonly include a timestamp or a number that is used only once. \\ Counter: & \ACounter{A}, \ACounter[C]{B} & Counter or indexes can be used to identify a session or a number in a sequence. \\ Random: & \ARandom{x}, \ARandom'{1} & Random values can be a variant of nonces. The $\ASmark$ 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 literature. \\ 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: & \AChashf{m}, \AFunc{Func}{\AVar{x},\AVar{y}}\ARet\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|\AFunc{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} %\kkey{A}, \kkey*{A}, \kkey-{A}, \kkey+{A}, \kkey!{A}, \kkey'{A}, \kkey"{A}, %\AKey{B}, \AKey*{B}, \AKey-{B}, \AKey+{B}, \AKey!{B}, \AKey'{B}, \AKey"{B}, %\AMkfunc{MyTest}[chash] %|\AFuncMyTest{x}[*]| %|\AChashf{m}[*]| %\AMkkfunc{MyK}[encrypted] %|\AKfuncMyK{x}{y}[*]| %|\AEncrypt+{A}{m}[*]| |\APwkeyf{P}(s)[P]| |\APwkeyf{P}(s)[*]| %|\AEncrypted{x}{m}| %|\AMacf{A}{m}[*]| |\ACmacf{A}{m}[*]| |\AHmacf{A}{m}[*]| %|\ASigf-{A}{m}[*]| |\ASign!{A}{m}[*]| 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 notation 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://ctan.org/pkg/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{burrows1990a} is included (see Section~\ref{sec:notation-ban} and~\ref{sec:latex-ban}). \clearpage \section{The notation} \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 notation constructs, usage examples are provided. These examples might include notation constructs 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 notation constructs 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 \AFunctionname{\AVerifytext} function (see below for the description of other parts of the notation used in the example): \newline \example{\AVerify+[big]{A}{\ASigned{x}{m}} = \ATrue \enspace \AIffthen \enspace \AKey{x} = \APrivkey{A}} \\\hline $\AVar{x}\AUnpack\AVar{y}$ & We use an unpack (leads-to) arrow {\AUnpack} 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 parts of the notation used in the example): \newline \example{\ASig-{A}{m}\AUnpack\AEncrypted-[big]{A}{\AChash{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 \AKey{X} & A shared or secret key, also known as a symmetric encryption and decryption key. \\\hline \AKey{A,B} & A shared key for \APri{A} and \APri{B} (this notation can be extended, for example with \AKey{A,B,C} for a key shared between \APri{A}, \APri{B}, and \APri{C}, or \AKey{\AGroup{M}} for a key shared among $n$ group members \AGroup*{M}). \\\hline \AKey'{C,S} & A session key for \APri{C} and \APri{S} (this notation can be extended, for example with \AKey'{A,B,S} for a key session key shared between \APri{A}, \APri{B}, and \APri{S}, or \AKey'{\AGroup{M}} for a session key shared among $n$ group members \AGroup*{M}). \\\hline \AKey+{A} & The public key of a public-private key pair of \APri{A}: $(\AKey+{A},\AKey-{A})$. \\\hline \AKey-{A} & The private key of a public-private key pair of \APri{A}: $(\AKey+{A},\AKey-{A})$. \\\hline \APwkey{P} & A secret key generated from the password \AVal{P}. \\\hline \ASval{m} & A structured value or message containing \AVal{m}. A structured value can be nested. \\\hline \ATval{\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{\ASig!{A}{m}\mbox{ has the type \emph{\AVal{\textit{\ASigtext}}} and the superscript }\AName{A}\mbox{ (signed by \APri{A})}} \\\hline \ASend{A}{B}{m} & Message \AMsg{m} sent from \APri{A} to \APri{B}. \\\hline \AFunc{\extxt{func}}{\AVar{x},\AVar{y}} & A function $\textit{\extxt{func}}$ with two arguments \AVar{x} and \AVar{y} (\AFunctionname{Encrypt} and \AFunctionname{Decrypt} described below are examples of such a function). \\\hline \AFunc{\extxt{func}}{\AVar{x},\AVar{y}}[\AVar{z}] & We use an arrow {\AProduces} to illustrate what a function produces (in this case \AVar{z}). The following example shows that the function \AFunctionname{Encrypt} produces a ciphertext encrypted with the given shared key (see below for the description of other parts of the notation used in the example): \newline \example{\AEncrypt{A,B}{m}[*]} \\\hline \AEncrypted*{\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{\AEncrypted*{K}{m}} \\\hline \ASigned*{\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{\ASigned!{A}{m}} \\\hline % \AEncrypted*{K}{m} % & Plain text \AVal{m} is encrypted with key \AKey*{K}. % \\\hline % \AEncrypted+{A}{m} % & Plain text \AVal{m} is encrypted with public key \AKey+{A}. % \\\hline \AEncrypt{A,B}{m} & Encrypt plain text \AVal{m} with shared key \AKey{A,B}: \newline \example{\AEncrypt{A,B}{m}[*]} \\\hline \ADecrypt{A,B}{\AVar{c}} & Decrypt cipher text \AVar{c} with shared key \AKey{A,B}, where $\AVar{c}=\AEncrypted{A,B}{m}$: \newline \example{\ADecrypt{A,B}{\AVar{c}}\AUnpack \ADecrypt[big]{A,B}{\AEncrypted{A,B}{m}}[m]} \\\hline \AEncrypt+{A}{m} & Encrypt plain text \AVal{m} with public key \AKey+{A}: \newline \example{\AEncrypt+{A}{m}[*]} \\\hline \ADecrypt-{A}{\AVar{c}} & Decrypt cipher text \AVar{c} with private key \AKey-{A}, where $\AVar{c}=\AEncrypted+{A}{m}$: \newline \example{\ADecrypt-{A}{\AVar{c}}\AUnpack \ADecrypt-[big]{A}{\AEncrypted+{A}{m}}[m]} \\\hline \AChash{m} & A cryptographic hash value of \AVal{m}. \\\hline \AChashf{m} & A cryptographic hash function producing the cryptographic hash value of \AVal{m}: \newline \example{% \AChashf{m}[*]} \\\hline \AMac{A}{m} & The message authentication code of \AVal{m} with key \AKey{A}. \\\hline \ACmac{A}{m} & The cipher-based message authentication code of \AVal{m} with key \AKey{A}. \\\hline \AHmac{A}{m} & The HMAC message authentication code \cite{bellare1996a} of \AVal{m} with key \AKey{A}. \\\hline \AMacf{A}{m} & The message authentication code function producing the message authentication code of \AVal{m} with key \AKey{A}: \newline \example{\AMacf{A}{m}[*]} \\\hline \ACmacf{A}{m} & The cipher-based message authentication code function producing the cipher-based message authentication code of \AVal{m} with key \AKey{A}: \newline \example{% \ACmacf{A}{m}[*]} \\\hline \AHmacf{A}{m} & The HMAC message authentication code function producing the HMAC message authentication code of \AVal{m} with key \AKey{A}: \newline \example{% \AHmacf{A}{m}[*]\AUnpack \AChash[big]{\AKey*{\overline{K}_A}\AXor\textit{opad}\AConcat \AChash{\AKey*{\overline{K}_A}\AXor\textit{ipad}\AConcat m}}\\ \AKey*{\overline{K}_A} \ = \ \; \Biggr\{ \raisebox{0pt}{% $\def\arraystretch{1}\begin{array}{ll@{}} \AChash{\AKey{A}} & \textrm{if \AKey{A} is larger than block size} \\ \AKey{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 \ASig!{A}{m} & Digital (cryptographic) signature of \AVal{m} signed by \APri{A}. \\\hline \ASig-{A}{m} & Digital (cryptographic) signature of \AVal{m} signed with private key \AKey-{A}: \newline \example{\ASig-{A}{m}\AUnpack\AEncrypted-[big]{A}{\AChash{m}}} \\\hline \ASig!{A,B}{m} & Digital (cryptographic) signature of \AVal{m} based on shared secret between \APri{A} and \APri{B}. \\\hline \ASig{A,B}{m} & Digital (cryptographic) signature of \AVal{m} signed with the shared key \AKey{A,B} (a shared secret between \APri{A} and \APri{B}): \newline \example{\ASig{A}{m}\AUnpack\AEncrypted[big]{A,B}{\AChash{m}}} \\\hline \ASigf-{A}{m} & Function creating a digital (cryptographic) signature of \AVal{m} with private key \AKey-{A}: \newline \example{\ASigf-{A}{m}[*]} \\\hline \ASigf!{A,B}{m} & Function creating a digital (cryptographic) signature of \AVal{m} based on shared secret between \APri{A} and \APri{B}: \newline \example{\ASigf!{A,B}{m}[*]} \\\hline \ASigf{A,B}{m} & Function creating a digital (cryptographic) signature of \AVal{m} with the shared key \AKey{A,B} (a shared secret between \APri{A} and \APri{B}): \newline \example{\ASigf{A,B}{m}[*]} \\\hline \ASigned!{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{\ASigned!{A}{m}\AUnpack\ASval[big]{m,\ASig!{A}{m}}} \\\hline \ASigned-{A}{m} & \AVal{m} is signed with private key \AKey-{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 \AKey-{A} implemented by encrypting the cryptographic hash value of \AVal{m} with \AKey-{A}): \newline \example{\ASigned-{A}{m}\AUnpack\ASval[big]{m,\ASig-{A}{m}} \AUnpack\ASval[Big]{m,\AEncrypted-[big]{A}{\AChash{m}}}} \\\hline \ASigned!{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{\ASigned!{A,B}{m}\AUnpack\ASval[big]{m,\ASig!{A,B}{m}}} \\\hline \ASigned{A,B}{m} & \AVal{m} is signed with a shared secret of \APri{A} and \APri{B}; the shared key \AKey{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 \AKey{A,B} implemented by encrypting the cryptographic hash value of \AVal{m} with \AKey{A,B}): \newline \example{\ASigned{A,B}{m}\AUnpack\ASval[big]{m,\ASig{A,B}{m}} \AUnpack\ASval[Big]{m,\AEncrypted[big]{A,B}{\AChash{m}}}} \\\hline \ASign!{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{\ASign!{A}{m}[*]\AUnpack \ASval[big]{m,\ASig!{A}{m}}} \\\hline \ASign-{A}{m} & Sign \AVal{m} with private key \AKey-{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 \AKey-{A} implemented by encrypting the cryptographic hash value of \AVal{m} with \AKey-{A}): \newline \example{\ASign-{A}{m}[*]\AUnpack \ASval[big]{m,\ASig-{A}{m}}\AUnpack \ASval[Big]{m,\AEncrypted-[big]{A}{\AChash{m}}}} \\\hline \ASign!{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{\ASign!{A,B}{m}[*]\AUnpack \ASval[big]{m,\ASig!{A,B}{m}}} \\\hline \ASign{A,B}{m} & Sign \AVal{m} with a shared secret of \APri{A} and \APri{B}\/; the shared key \AKey{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 \AKey{A,B} implemented by encrypting the cryptographic hash value of \AVal{m} with \AKey{A,B}): \newline \example{\ASign{A,B}{m}[*]\AUnpack \ASval[big]{m,\ASig{A,B}{m}}\AUnpack \ASval[Big]{m,\AEncrypted[big]{A,B}{\AChash{m}}}} \\\hline \APwkeyf{P}(s) & Create a secret key from the password \AVal{P} with the salt \AVal{s}. The salt is optional in the notation. \emph{PBKDF2} is an examples of a password-based key derivation function. The function creates a new secret key:\newline \example{% \APwkeyf{P_1}[*] \\ \APwkeyf_{PBKDF2}{P_2}(s)[*]} \\\hline \ADhpubkeyf{A}(p) & Make a public key \AKey+{A} (a key share) from the private key \AKey-{A} and the public parameters \AVal{p}, typically used in a Diffie–Hellman key exchange protocol~\cite{diffie1976a} (a Diffie–Hellman key share). The public parameters argument is optional:\newline \example{% \ADhpubkeyf{A}[A]\\ \ADhpubkeyf{B}(p)[B]}\newline In the original implementation of Diffie-Hellman (Finite Field Diffie–Hellman) the public parameters consists of a agreed upon prime and a primitive root. \\\hline \ADhkeyf{A}{B}(p) & Combine private key \AKey-{A} with public key \AKey+{B} and the public parameters \AVal{p} (optional) to generate a new secret (shared) key \AKey{A,B}, typically the result of a Diffie–Hellman key exchange protocol~\cite{diffie1976a}. The public parameters argument is optional:\newline \example{% \ADhkeyf{A}{B}[A,B]\\ \ADhkeyf{B}{A}(p)[A,B]}\newline These functions are one-way functions where the private keys \AKey-{A} and \AKey-{B} can not be calculated (in reasonable time) with only the knowledge of the public keys \AKey+{A} and \AKey+{B} and the public parameters \AVal{p}. And as a consequence the new shared secret key \AKey{A,B} is also difficult (impossible in practice) to calculate. \\\hline \AVerify+{A}{\AVar{s}} & Verify that the signed structured value (message) \AVar{s} is signed by the matching private key \AKey-{A} of public key \AKey+{A} and, as a consequence, verify that \AVar{s} is signed by~\APri{A}: \newline \example{% \AVerify+{A}{\AVar{s}}\AUnpack \AVerify+[big]{A}{\ASigned!{x}{m}} \AUnpack \AVerify+[Big]{A}{\ASval[big]{m,\ASig!{x}{m}}}\AUnpack \\ \AVerify+[Big]{A}{\ASval[big]{m,\ASig-{x}{m}}}\AUnpack \AVerify+[bigg]{A}{\ASval[Big]{m,\AEncrypted-[big]{x}{\AChash{m}}}}: \\[1.5ex]\hline \begin{array}{@{}c} \ADecrypt+[big]{A}{\ASig!{x}{m}}=\AChash{m} \enspace \AUnpack \\ \ADecrypt+[big]{A}{\ASig-{x}{m}}=\AChash{m} \enspace \AUnpack \\ \ADecrypt+[Big]{A}{\AEncrypted-[big]{x}{\AChash{m}}}=\AChash{m} \end{array} \raisebox{-2pt}{$\Bigggggr\}$} \quad \raisebox{-2pt}{$\AIffthen$} \quad \raisebox{-2pt}{$\AKey-{A} = \AKey-{x}$} \\[1.5ex]\hline \AVerify+{A}{\AVar{s}}[\ATrue] \quad \AIffthen \quad \AKey-{A} = \AKey-{x}} \\\hline \AVerify!{C}{\AVar{s}} & Verify that the signed structured value (message) \AVar{s} is signed by principal \APri{C}. \\\hline \ACertificate!{C}{\APri{A},\AKey+{A}} & A certificate where certificate authority \APri{C} binds identity \APri{A} to public key \AKey+{A} (in the example, \AVal{\ldots} is other certificate related meta-data): \newline \example{% \ACertificate!{C}{\APri{A},\AKey+{A}}\AUnpack \ASigned!{C}{\APri{A},\AKey+{A},\AVal{\ldots}}} \\\hline \ACertificate-{C}{\APri{A},\AKey+{A}} & A certificate where a certificate authority with private key \AKey-{C} binds identity \APri{A} to public key \AKey+{A} (in the example, \AVal{\ldots} is other certificate related meta-data): \newline \example{% \ACertificate-{C}{A,\AKey+{A}}\AUnpack \ASigned-{C}{A,\AKey+{A},\AVal{\dots}} \\\hline \AVerify+{C}{\ACertificate-{C}{A,\AKey+{A}}}\enspace\AUnpack \enspace\AVerify+{C}{% \ASigned-{C}{A,\AKey+{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{burrows1990a}. {\renewcommand{\arraystretch}{1.6} \begin{xltabular}{\textwidth}{lX}\Xhline{0.5pt} \textbf{Notation} & \textbf{Description} \\\Xhline{0.5pt} \APri{A}\BANBelieves\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}\BANSees\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}\BANOncesaid\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}\BANControls\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 \BANFresh{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}\BANSharedkey{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~\AKey{A,B}.) \\\hline \BANPubkey{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 \AKey+{A}, and the inverse of \AKey+{A}, the private key, is denoted~\AKey-{A}.) \\\hline \APri{A}\BANSecret{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 \BANEncryptedwith{K}{X} & This represents the formula \AVal{X} \emph{encrypted} under the key \AKey*{K}. Formally, \BANEncryptedwith{K}{X} is an abbreviation for an expression of the form \BANEncryptedwith{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 interests of brevity, we typically omit this in our examples. \\\hline \BANCombine{\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\BANCombine{\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 \AKey{A,B}, it is implicit that \APri{A} and \APri{B} may use \AKey{A,B} to communicate. We can use the BAN logic notation to make it explicit: \[ \APri{A}\BANSharedkey{\AKey{A,B}}\APri{B} \] In a similar manner, \AKey+{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: \[ \BANPubkey{\AKey+{A}}\APri{A} \] Both the BAN logic notation and {\Aspen} use the notation \AEncrypted*{K}{m} for the formula \AVal{m} \emph{encrypted} under the key \AKey*{K} (\AVal{m} encrypted with the key \AKey*{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 notation in text} \label{sec:write-notation-latex} This section explains how to use {\Aspen} 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, they are included for completeness. We will in the documentation try to include a wide range of possibilities available from the {\latex} package \ACmd{aspen}. For commands with arguments, the argument types are given using a notation inspired by the \ACmd{xparse} argument specification: {\renewcommand{\arraystretch}{1.3}% \begin{xltabular}{\textwidth}{% @{\hskip 1em\relax}lX@{\hskip -1.2em\relax}|@{\hskip 1.2em\relax}lX} \ACmd{\Verb|m|} & Mandatory arguments\newline \emph{Examples:} \Verb|\cmd{arg}| & \ACmd{\Verb|B|} & Optional bracket sizes (\ACmd{big}, \ACmd{Big}, \ldots)\newline \emph{Examples:} \Verb|\cmd|, \Verb|\cmd[Big]| \\ \ACmd{\Verb|o|} & Optional arguments\newline \emph{Examples:} \Verb|\cmd|, \Verb|\cmd[arg]| & \ACmd{\Verb|s|} & Optional stars (alternative versions)\newline \emph{Examples:} \Verb|\cmd|, \Verb|\cmd*| \\ \ACmd{\Verb|O{default}|} & Optionals with default value \newline \emph{Examples:} \Verb|\cmd|, \Verb|\cmd[arg]| & \ACmd{\Verb|T|} & Optional key types: \Verb|*|, \Verb|-|, \Verb|+|, \Verb|!|, \Verb|'|, or \Verb|"|\newline \emph{Examples:} \Verb|\cmd|, \Verb|\cmd-|, \Verb|\cmd!| \\ \ACmd{\Verb|p|} & Optionals in parenthesis \newline \emph{Examples:} \Verb|\cmd|, \Verb|\cmd(arg)| & \ACmd{\Verb|x|} & Optionals with magic return \newline \emph{Examples:} \Verb|\cmd|, \Verb|\cmd[*]|, \Verb|\cmd[arg]| \\ \ACmd{\Verb|P{default}|} & Parenthesis optionals with default\newline \emph{Examples:} \Verb|\cmd|, \Verb|\cmd(arg)| & \ACmd{\Verb|i|} & Optional markers (more details)\newline \emph{Examples:} \Verb|\cmd|, \Verb|\cmd_{arg}| \\ \ACmd{\Verb|t'|} & Optional single quote marks\newline \emph{Examples:} \Verb|\cmd|, \Verb|\cmd'| & \givesarrow & Arguments of returned command\newline \emph{Examples:} \cmdargs{mkcmd}{omo}[Bimx] \end{xltabular}} We can use this notation to specify the type of the arguments to a command. For example, \ACmd{\Verb|om|} says that the command takes two arguments where the first one is optional (in square brackets). We use the symbol {\AProduces} to specify the arguments of a command created by another command. For example, \ACmd{\Verb|\AMktval|} has one optional argument (\ACmd{\Verb|o|}) and one mandatory argument (\ACmd{\Verb|m|}) and returns a new command that has one optional star argument (\ACmd{\Verb|s|}), one optional bracket size argument (\ACmd{\Verb|B|}), one optional marker (\ACmd{\Verb|i|}), and one mandatory argument (\ACmd{\Verb|m|}): \begin{quote} \cmdargs{AMktval}{om}[sBim] \end{quote} The optional magic return type \ACmd{\Verb|x|} is available for some predefined functions and can be be made available for functions created with the commands \ACmd{\Verb|\AMkfunc|} and \ACmd{\Verb|\AMkkfunc|}. The magic return value \ACmd{\Verb|*|} will create the return value based on what the function does. For example, if magic return is used with the encrypt function, the return value created will be the encrypted value: \begin{quote} \cmdargs{AEncrypt}{TBimmx} \newline \ACmd{\Verb|\AEncrypt+{A}{m}[*]|}\gives\AEncrypt+{A}{m}[*] \end{quote} % A few commands provided creates new {\latex} commands (these commands % typically starts with \ACmd{\Verb|\mk|}. In these cases, we can then % specify the arguments both for the \ACmd{\Verb|\mk|} command and for % command created: \ACmd{\Verb|om|}~{\AProduces}~\ACmd{\Verb|sBim|}. \clearpage \subsection{{\Aspen}} \label{sec:latex-aspen} The table below lists the {\Aspen} notation with the matching {\latex} commands. More examples of the usage of the notation 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} $=,<,\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}\AUnpack\extxt{y}$ & \ACmd{\Verb|x \AUnpack y|}, used to unpack more details. \\\hline $\AVal{1},\AVal{2}$ & \ACmd{\Verb|\AVal{1}|},\ACmd{\Verb|\AVal{2}|}, used for values.\\[-1ex]\nopagebreak \emph{Arguments:} & \cmdargs{AVal}{m}\newline \cmdargex{AVal}{\cmdmarg{value}} \\\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.\\[-1ex]\nopagebreak \emph{Arguments:} & \cmdargs{APri}{m}\newline \cmdargex{APri}{\cmdmarg{principal}} \\\hline $\ANonce*{N_A},\ANonce{S}$ & \ACmd{\Verb|\ANonce*{N_A}|},\ACmd{\Verb|\ANonce{S}|}, used for nonces. The \ACmd{\Verb|\ANonce|} command has an optional first argument to change the symbol (the letter): \ACmd{\Verb|\ANonce[n]{0}|}\;\givesarrow\;\ANonce[n]{0} \\[-1ex]\nopagebreak \emph{Arguments:} & \cmdargs{ANonce}{sO{N}m}\newline \cmdargex{ANonce}{\cmdsarg\cmdoarg{symbol}\cmdmarg{id}} \\\hline $\ACounter*{C_A},\ACounter{B}$ & \ACmd{\Verb|\ACounter*{C_A}|},\ACmd{\Verb|\ACounter{B}|}, used for indexes or counters. The \ACmd{\Verb|\ACounter|} command has an optional first argument to change the symbol (the letter): \ACmd{\Verb|\ACounter[i]{0}|}\;\givesarrow\;\ACounter[i]{0} \\[-1ex]\nopagebreak \emph{Arguments:} & \cmdargs{ACounter}{sO{I}m}\newline \cmdargex{ACounter}{\cmdsarg\cmdoarg{symbol}% \cmdmarg{id}} \\\hline $\ARandom*{R_x},\ARandom{y},\ARandom'{1}$ & \ACmd{\Verb|\ARandom*{R_x}|},\ACmd{\Verb|\ARandom{y}|},% \ACmd{\Verb|\ARandom'{1}|}, used for random values (the $\ASmark$ hints about limited useful lifetime). The \ACmd{\Verb|\ARandom|} command has an optional first argument to change the symbol (the letter): \ACmd{\Verb|\ARandom[r]{z}|}\;\givesarrow\;\ARandom[r]{z} \\[-1ex]\nopagebreak \emph{Arguments:} & \cmdargs{ARandom}{st'O{R}m}\newline \cmdargex{ARandom}{\cmdsarg\cmdtarg{'}% \cmdoarg{symbol}\cmdmarg{id}} \\\hline $\ATS*{T_A},\ATS{S},\ATTL*{L},\ATTL{1}$ & \ACmd{\Verb|\ATS*{T_A}|},\ACmd{\Verb|\ATS{S}|},\ACmd{\Verb|\ATTL*{L}|},% \ACmd{\Verb|\ATTL{1}|}, used for time related values, like time stamps and lifetime (time to live). Both the \ACmd{\Verb|\ATS|} and \ACmd{\Verb|\ATTL|} command have an optional first argument to change the symbol (the letter): \ACmd{\Verb|\ATS[t]{0}|}\;\givesarrow\;\ATS[t]{0}, \ACmd{\Verb|\ATTL[l]{1}|}\;\givesarrow\;\ATTL[l]{1}\\[-1ex]\nopagebreak \emph{Arguments:} & \cmdargs{ATS}{sO{T}m}, \cmdargs{ATTL}{sO{L}m}\newline \cmdargex{ATS}{\cmdsarg\cmdoarg{symbol}% \cmdmarg{id}},\newline \cmdargex{ATTL}{\cmdsarg\cmdoarg{symbol}\cmdmarg{id}} \\\hline $\AStr{Hello}$ & \ACmd{\Verb|\AStr{Hello}|}, used for text strings.\\[-1ex]\nopagebreak \emph{Arguments:} & \cmdargs{AStr}{m}\newline \cmdargex{AStr}{\cmdmarg{str}} \\\hline $\AVar{x},\AVar{y}$ & \ACmd{\Verb|\AVar{x}|},\ACmd{\Verb|\AVar{y}|}, used for variables. \\[-1ex]\nopagebreak \emph{Arguments:} & \cmdargs{AVar}{m}\newline \cmdargex{AVar}{\cmdmarg{variable}} \\\hline $\APrivkey[]{},\APubkey[]{},\ASessionkey[]{},\;\ldots$ & Some command markers (key type markers) are used throughout the {\Aspen} {\latex} package to specify the key type involved: \newline {\renewcommand{\arraystretch}{1}\begin{tabular}{c@{\::\:~}l} \ACmd{*} & Means no specific variant (argument is the key, not the label): \ACmd{\Verb|\AKey*{K}|} \\ \ACmd{-} & Mark that it is a private key (from a public-private key pair): \ACmd{\Verb|\AKey-{A}|} \\ \ACmd{+} & Mark that it is a public key (from a public-private key pair): \ACmd{\Verb|\AKey+{A}|} \\ \ACmd{!} & Mark by principal instead of key (the key of): \ACmd{\Verb|\AKey!{A}|} \\ \ACmd{'} & Mark that it is temporary (session key or limited lifetime): \ACmd{\Verb|\AKey'{A}|} \\ \ACmd{"} & Mark that it is a key generated from the password: \ACmd{\Verb|\AKey"{P}|} \\ \end{tabular}}\newline \example{\begin{tabular}{@{}lcl@{}} \ACmd{\Verb|\AKey*{K}|} & \givesarrow & $\AKey*{K}$ \\ \ACmd{\Verb|\AEncrypted"{P}{\AKey-{B}}|} & \givesarrow & $\AEncrypted"{P}{\AKey-{B}}$ \\ \ACmd{\Verb|\ASig-{A}{m}|} & \givesarrow & $\ASig-{A}{m}$ \\ \ACmd{\Verb|\AEncrypt+{B}{m}|} & \givesarrow & $\AEncrypt+{B}{m}$ \\ \ACmd{\Verb|\ASigned!{S}{m}|} & \givesarrow & $\ASigned!{S}{m}$ \\ \ACmd{\Verb|\ADecrypt'{A,B}{c}|} & \givesarrow & $\ADecrypt'{A,B}{c}$ \end{tabular}}\vspace*{-2.0ex} \\ \nopagebreak \emph{Arguments:} & \ACmd{\Verb|T|} (the symbol used for these optional markers in argument specifications) \\\hline $\AKey*{K}$ & \ACmd{\Verb|\AKey*{K}|}, used for (non-specific) encryption keys. The argument is the key itself, and not a label for the key symbol. \\[-1ex]\nopagebreak \emph{Arguments:} & \cmdargs{AKey}{Tm}\newline \cmdargex{AKey}{*\cmdmarg{key}} \\\hline $\AKey{A},\ASharedkey{A,B}$ & \ACmd{\Verb|\AKey{A}|},\ACmd{\Verb|\ASharedkey{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|\ASharedkey|} command has an optional first argument to change the symbol (the letter): \ACmd{\Verb|\ASharedkey[k]{B}|}\;\givesarrow\;\ASharedkey[k]{B} \\[-1ex]\nopagebreak \emph{Arguments:} & \cmdargs{AKey}{Tm}, \cmdargs{ASharedkey}{O{K}m}\newline \cmdargex{AKey}{\cmdmarg{id}}, \cmdargex{ASharedkey}{\cmdoarg{symbol}\cmdmarg{id}} \\\hline $\AKey'{C,S},\ASessionkey{A,B,S}$ & \ACmd{\Verb|\AKey'{C,S}|},\ACmd{\Verb|\ASessionkey{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|\ASessionkey|} command has an optional first argument to change the symbol (the letter): \ACmd{\Verb|\ASessionkey[k]{A,B}|}\;\givesarrow\;\ASessionkey[k]{A,B}% \\[-1ex]\nopagebreak \emph{Arguments:} & \cmdargs{AKey}{Tm}, \cmdargs{ASessionkey}{O{K}m}\newline \cmdargex{AKey}{'\cmdmarg{id}}, \cmdargex{ASessionkey}{\cmdoarg{symbol}\cmdmarg{id}} \\\hline $\AKey+{A},\APubkey{B}$ & \ACmd{\Verb|\AKey+{A}|},\ACmd{\Verb|\APubkey{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|\APubkey|} command has an optional first argument to change the symbol (the letter): \ACmd{\Verb|\APubkey[k]{S}|}\;\givesarrow\;\APubkey[k]{S} \\[-1ex]\nopagebreak \emph{Arguments:} & \cmdargs{AKey}{Tm}, \cmdargs{APubkey}{O{K}m}\newline \cmdargex{AKey}{+\cmdmarg{id}}, \cmdargex{APubkey}{\cmdoarg{symbol}\cmdmarg{id}} \\\hline $\AKey-{A},\APrivkey{B}$ & \ACmd{\Verb|\AKey-{A}|},\ACmd{\Verb|\APrivkey{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|\APrivkey|} command has an optional first argument to change the symbol (the letter): \ACmd{\Verb|\APrivkey[k]{A}|}\;\givesarrow\;\APrivkey[k]{A} \\[-1ex]\nopagebreak \emph{Arguments:} & \cmdargs{AKey}{Tm}, \cmdargs{APrivkey}{O{K}m}\newline \cmdargex{AKey}{-\cmdmarg{id}}, \cmdargex{APrivkey}{\cmdoarg{symbol}\cmdmarg{id}} \\\hline $\AKey"{P_1},\APwkey{P_2}$ & \ACmd{\Verb|\AKey"{P_1}|},\ACmd{\Verb|\APwkey{P_2}|}, used for keys generated from a password (provided by two different {\latex} commands, where the first is a more compact version; use whatever you prefer). The \ACmd{\Verb|\APwkey|} command has an optional first argument to change the symbol (the letter): \ACmd{\Verb|\APwkey[k]{P}|}\;\givesarrow\;\APwkey[k]{P} \\[-1ex]\nopagebreak \emph{Arguments:} & \cmdargs{AKey}{Tm}, \cmdargs{APwkey}{O{K}m}\newline \cmdargex{AKey}{"\cmdmarg{password}}, \cmdargex{APwkey}{\cmdoarg{symbol}\cmdmarg{password}} \\\hline % $\AKey!{A},\AKey*{\AName{B}}$ % & \ACmd{\Verb|\AKey!{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: \ACmd{\Verb|\AKey!{A}|}\gives\AKey!{A} \\[-1ex]\nopagebreak \emph{Arguments:} & \cmdargs{AName}{m}, \cmdargs{AKey}{Tm}\newline \cmdargex{AName}{\cmdmarg{id}}, \cmdargex{AKey}{!\cmdmarg{id}} \\\hline $\AGroup{M}$ & \ACmd{\Verb|\AGroup{M}|}, specifies a group and is typically used as a label for a shared key shared within a group with $n$ members: \newline \example{% \mbox{\ACmd{\Verb|\AKey{\AGroup{M}}|}}\gives\AKey{\AGroup{M}}}% \vspace*{-2.2ex}\\ %$\AGroup[0][s]{M}$ & \ACmd{\Verb|\AGroup[0][s]{M}|}, used when th group member indexes are non-standard: \newline \example{% \mbox{\ACmd{\Verb|\AKey{\AGroup[0][s]{M}}|}}\gives \AKey{\AGroup[0][s]{M}}}\vspace*{-2.2ex}\\ & \ACmd{\Verb|\AGroup*{M}|}, typically used in a text when referring to a group (with $n$ members): \newline \example{% \mbox{\ACmd{\Verb|\AKey{\AGroup*{M}}|}}\gives \AKey{\AGroup*{M}}}\vspace*{-2.2ex}\\ %$\AGroup*[0][s]{M}$ & \ACmd{\Verb|\AGroup*[0][s]{M}|}, used when group member indexes are non-standard:\newline \example{% \mbox{\ACmd{\Verb|\AKey{\AGroup*[0][s]{M}}|}}\gives \AKey{\AGroup*[0][s]{M}}}\vspace*{-2.0ex}\\ \nopagebreak \emph{Arguments:} & \cmdargs{AGroup}{sO{1}O{n}m}\newline \cmdargex{AGroup}{% {\cmdsarg}\cmdoarg{first}\cmdoarg{last}\cmdmarg{id}} \\\hline $\ASval{m},\AMsg{\APri{A},\APri{B}}$ & \ACmd{\Verb|\ASval{m}|},\ACmd{\Verb|\AMsg{\APri{A},\APri{B}}|}, used for a structured value or message (a message can be seen as structured value).\\[-1ex] \nopagebreak \emph{Arguments:} & \cmdargs{ASval}{Bm}, \cmdargs{AMsg}{Bm}\newline \cmdargex{ASval}{\cmdoarg{size}\cmdmarg{value}}, \cmdargex{AMsg}{\cmdoarg{size}\cmdmarg{message}} \\\hline $\ASval[big]{m}$ & \ACmd{\Verb|\ASval[big]{m}|}, or \ACmd{\Verb|\AMsg[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|\ASval{x}|}}\gives\ASval{x} \\ \mbox{\ACmd{\Verb|\ASval[big]{\ASval{x}}|}}\gives \ASval[big]{\ASval{x}} \\ \mbox{\ACmd{\Verb|\ASval[Big]{\ASval[big]{\ASval{x}}}|}}\gives \ASval[Big]{\ASval[big]{\ASval{x}}} \\ \mbox{\ACmd{\Verb|\ASval[bigg]{\ASval[Big]{\ASval[big]{\ASval{x}}}}|}}% \gives\ASval[bigg]{\ASval[Big]{\ASval[big]{\ASval{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{% \ASval[Biggggg]{\ASval[biggggg]{\ASval[Bigggg]{\ASval[bigggg]{% \ASval[Biggg]{\ASval[biggg]{\ASval[Bigg]{\ASval[bigg]{\ASval[Big]{% \ASval[big]{\ASval{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|\ATval[big]{Type}{m}|}} & \givesarrow & \ATval[big]{Type}{m} \\ \mbox{\ACmd{\Verb|\ASend[big]{A}{B}{m}|}} & \givesarrow & \ASend[big]{A}{B}{m} \\ \mbox{\ACmd{\Verb|\AFunc[big]{Func}{x,y}|}} & \givesarrow & \AFunc[big]{Func}{x,y} \\ \mbox{\ACmd{\Verb|\AEncrypted[big]{A,B}{m}|}} & \givesarrow & \AEncrypted[big]{A,B}{m} \end{tabular}}\vspace*{-2.0ex}\\ \nopagebreak \emph{Arguments:} & \cmdargs{ASval}{Bm}, \cmdargs{AMsg}{Bm}\newline \cmdargex{ASval}{\cmdoarg{size}\cmdmarg{value}}, \cmdargex{AMsg}{\cmdoarg{size}\cmdmarg{message}} \\\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|\AChash_{MD5}{m}|}} & \givesarrow & $\AChash_{MD5}{m}$ \\ \mbox{\ACmd{\Verb|\AEncrypt+_{RSA}{B}{m}|}} & \givesarrow & $\AEncrypt+_{RSA}{B}{m}$ \\ \mbox{\ACmd{\Verb|\ADecrypt'_{AES}{A,B}{c}|}} & \givesarrow & $\ADecrypt'_{AES}{A,B}{c}$ \\ \mbox{\ACmd{\Verb|\ASig-_{DSA}{S}{m}|}} & \givesarrow & $\ASig-_{DSA}{S}{m}$ \\ \mbox{\ACmd{\Verb|\AHmac_{SHA-2}{A}{m}|}} & \givesarrow & $\AHmac_{SHA-2}{A}{m}$ \end{tabular}}\vspace*{-2.0ex} \\ \nopagebreak \emph{Arguments:} & \ACmd{\Verb|i|} (the symbol used for such optional embellishment in argument specifications) \\\hline $\ATval{Type}{m}$ & \ACmd{\Verb|\ATval{Type}{m}|}, used for a typed structured value where the first argument is the type. % \\\hline % $\ATval*{Type}{\ASval{m}}$ % & The \ACmd{\Verb|\ATval*|} variant is used for a typed structured value where the first argument is the type, but the value is not wrapped with curly brackets. This is typically used when the value is already wrapped as a structured value (e.g., encrypted or signed data). This is an example with a Kerberos Authenticator as a typed structured value:\newline \example{\begin{tabular}{@{}c@{}}% \mbox{\ACmd{% \Verb|\ATval*{KA}{\AEncrypted{S,C}{\APri{C},\textit{Addr}_C,\ATS{t}}}|}} \\ \givesarrow\quad \ATval*{KA}{\AEncrypted{S,C}{\APri{C},\textit{Addr}_C,\ATS{t}}} \end{tabular}} \vspace*{-2.2ex}\\ & The marker (\Verb|_{RSA}| in the example below) can be used to give more details about the typed structured value:\newline \example{\begin{tabular}{@{}c@{}}% \mbox{\ACmd{% \Verb|\ATval*{KA}_{RSA}{\AEncrypted{S,C}{\APri{C},\textit{Addr}_C,\ATS{t}}}|}}\\ \givesarrow\quad \ATval*{KA}_{RSA}{\AEncrypted{S,C}{\APri{C},\textit{Addr}_C,\ATS{t}}} \end{tabular}} \vspace*{-2.0ex}\\ \nopagebreak \emph{Arguments:} & \cmdargs{ATval}{sBmim}\newline \cmdargex{ATval}{{\cmdsarg}\cmdoarg{size}% \cmdmarg{type}{\cmdearg}\cmdmarg{value}} \\\hline % \ATval[big]{Type}{m} % & \ACmd{\Verb|\ATval[big]{Type}{m}|}, % where the optional argument of \ACmd{\Verb|\ATval|} can be % \ACmd{big}, \ACmd{Big}, \ACmd{bigg}, or \ACmd{Bigg} for % increased size of parenthesis (see examples with structured % values above). % \\\hline $\ASend{A}{B}{m}$ & \ACmd{\Verb|\ASend{A}{B}{m}|}, used to specify that a message \ASval{m} is sent from \APri{A} to \APri{B}. % \\\hline % \ASend[big]{A}{B}{m} % & \ACmd{\Verb|\ASend[big]{A}{B}{m}|}, where the optional % argument of \ACmd{\Verb|\ASend|} can be % \ACmd{big}, \ACmd{Big}, \ACmd{bigg}, or \ACmd{Bigg} for increased % size of parenthesis (see examples with structured values above). % \\\hline % \ASend*{A}{B}{\AVar{\extxt{x}}} % & The \ACmd{\Verb|\ASend*|} variant is used to specify that the message 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|\ASend*{A}{B}{\AEncrypted+{B}{m}}|}}\gives \ASend*{A}{B}{\AEncrypted+{B}{m}}\\ \mbox{\ACmd{\Verb|\ASend*{A}{B}{\AEncrypted+[big]{B}{\AChash{m}}}|}}% \gives\ASend*{A}{B}{\AEncrypted+[big]{B}{\AChash{m}}}} \vspace*{-2.0ex}\\ \nopagebreak \emph{Arguments:} & \cmdargs{ASend}{sBmmm}\newline \cmdargex{ASend}{{\cmdsarg}\cmdoarg{size}% \cmdmarg{sender}\cmdmarg{receiver}\cmdmarg{message}} \\\hline $\AFunc{Func}{x,y}$ & \ACmd{\Verb|\AFunc{Func}{x,y}|}, used for any functions. %\\\hline % \AFunc[big]{Func}{x,y} % & \ACmd{\Verb|\AFunc[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 %$\AFunc{Func}{x,y}[z]$ % & An optional last argument is used if a return value of the function is given:\newline \example{% \mbox{\ACmd{\Verb|\AFunc{Func}{x,y}[z]|}}\gives \AFunc{Func}{x,y}[z]} \vspace*{-2.0ex}\\ \nopagebreak \emph{Arguments:} & \cmdargs{AFunc}{Bmimo}\newline \cmdargex{AFunc}{\cmdoarg{size}\cmdmarg{name}% {\cmdearg}\cmdmarg{arguments}\cmdoarg{returns}} \\\hline % \AFunc[big]{Func}{x,y}[z] % & \ACmd{\Verb|\AFunc[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 $\AEncrypted{A,B}{m}$ & \ACmd{\Verb|\AEncrypted{A,B}{m}|}, where the message is encrypted with an shared secret encryption key (in this case, the shared key \AKey{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|\AEncrypted|} demonstrated: \newline \example{% \begin{tabular}{@{}lcl@{}} \mbox{\ACmd{\Verb|\AEncrypted*{K}{m}|}} & \givesarrow & \AEncrypted*{K}{m} \\ %\mbox{\ACmd{\Verb|\AEncrypted{A,B}{m}|}} & \givesarrow %& \AEncrypted{A,B}{m} \\ \mbox{\ACmd{\Verb|\AEncrypted+{A}{m}|}} & \givesarrow & \AEncrypted+{A}{m} \\ \mbox{\ACmd{\Verb|\AEncrypted-{A}{m}|}} & \givesarrow & \AEncrypted-{A}{m} \\ \mbox{\ACmd{\Verb|\AEncrypted!{A}{m}|}} & \givesarrow & \AEncrypted!{A}{m} \\ \mbox{\ACmd{\Verb|\AEncrypted'{A,B}{m}|}} & \givesarrow & \AEncrypted'{A,B}{m} \\ \mbox{\ACmd{\Verb|\AEncrypted"{P}{m}|}} & \givesarrow & \AEncrypted"{P}{m} \end{tabular}}\vspace*{-2.0ex}\\ \nopagebreak \emph{Arguments:} & \cmdargs{AEncrypted}{TBimm}\newline \cmdargex{AEncrypted}{{\cmdkarg}\cmdoarg{size}% {\cmdearg}\cmdmarg{key}\cmdmarg{plain}} \\\hline % \AEncrypted[big]{A,B}{m} % & \ACmd{\Verb|\AEncrypted[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{\AEncrypted} (see previous). % Typically used with structured values: % \newline % \example{% % \mbox{\ACmd{\Verb|\AEncrypted+[big]{B}{\ASigned-{A}{m}}|}}\gives % \AEncrypted+[big]{B}{\ASigned-{A}{m}}} % \\\hline $\AEncrypt{A,B}{m}$ & \ACmd{\Verb|\AEncrypt{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{!}, \ACmd{'} and \ACmd{"} (see above for explanation). Since \ACmd{\Verb|\AEncrypt|} is a function, we can include a return value as an optional last argument (and it supports magic return making straightforward to include the return value): \newline \example{% \mbox{\ACmd{\Verb|\AEncrypt+{B}{m}[\AEncrypted+{B}{m}]|}}\gives \AEncrypt+{B}{m}[\AEncrypted+{B}{m}] \\ \mbox{\ACmd{\Verb|\AEncrypt+{B}{m}[*]|}}\gives \AEncrypt+{B}{m}[*]}\vspace*{-2.0ex}\\ \nopagebreak \emph{Arguments:} & \cmdargs{AEncrypt}{TBimmx}\newline \cmdargex{AEncrypt}{{\cmdkarg}\cmdoarg{size}% {\cmdearg}\cmdmarg{key}\cmdmarg{plain}% \cmdoarg{returns}} \\\hline % \AEncrypt[big]{A,B}{m} % & \ACmd{\Verb|\AEncrypt[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|\AEncrypt+[big]{B}{\ASigned-{A}{m}}|}}\gives % \AEncrypt+[big]{B}{\ASigned-{A}{m}}} % \\\hline $\ADecrypt{A,B}{\AVar{c}}$ & \ACmd{\Verb|\ADecrypt{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{!} \ACmd{'}, and \ACmd{"} (see above for explanation). Since \ACmd{\Verb|\ADecrypt|} is a function, we can include a return value as an optional last argument: \newline \example{% \mbox{\ACmd{\Verb|\ADecrypt-{B}{\AEncrypted+{B}{m}}[m]|}}\gives \ADecrypt-{B}{\AEncrypted+{B}{m}}[m]}\vspace*{-2.0ex}\\ \nopagebreak \emph{Arguments:} & \cmdargs{ADecrypt}{TBimmo}\newline \cmdargex{ADecrypt}{{\cmdkarg}\cmdoarg{size}% {\cmdearg}\cmdmarg{key}\cmdmarg{cipher}% \cmdoarg{returns}} \\\hline % \ADecrypt[big]{A,B}{\AVar{c}} % & \ACmd{\Verb|\ADecrypt[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|\ADecrypt-[big]{B}{\AEncrypted+{B}{m}}[m]|}}% % \gives \ADecrypt-[big]{B}{\AEncrypted+{B}{m}}[m]} % \\\hline $\AChash{m}$ & \ACmd{\Verb|\AChash{m}|}, used for a cryptographic hash value of \AVal{m}.\\[-1ex]\nopagebreak \emph{Arguments:} & \cmdargs{AChash}{Bim}\newline \cmdargex{AChash}{\cmdoarg{size}{\cmdearg}% \cmdmarg{value}} \\\hline % \AChash[big]{m} % & \ACmd{\Verb|\AChash[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 $\AMac{A}{m}$ & \ACmd{\Verb|\AMac{A}{m}|}, used for message authentication code of \AVal{m} with \AKey{A}.\\[-1ex]\nopagebreak \emph{Arguments:} & \cmdargs{AMac}{TBimm}\newline \cmdargex{AMac}{{\cmdkarg}\cmdoarg{size}{\cmdearg}% \cmdmarg{key}\cmdmarg{value}} \\\hline $\ACmac{A}{m}$ & \ACmd{\Verb|\ACmac{A}{m}|}, used for cipher-based message authentication code of \AVal{m} with \AKey{A}.\\[-1ex]\nopagebreak \emph{Arguments:} & \cmdargs{ACmac}{TBimm}\newline \cmdargex{ACmac}{{\cmdkarg}\cmdoarg{size}{\cmdearg}% \cmdmarg{key}\cmdmarg{value}} \\\hline $\AHmac{A}{m}$ & \ACmd{\Verb|\AHmac{A}{m}|}, used for HMAC message authentication code of \AVal{m} with \AKey{A}.\\[-1ex]\nopagebreak \emph{Arguments:} & \cmdargs{AHmac}{TBimm}\newline \cmdargex{AHmac}{{\cmdkarg}\cmdoarg{size}{\cmdearg}% \cmdmarg{key}\cmdmarg{value}} \\\hline $\AChashf{m}$ & \ACmd{\Verb|\AChashf{m}|}, used for a cryptographic hash value function producing the cryptographic hash value of \AVal{m}. Since \ACmd{\Verb|\AChashf|} is a function, we can include a return value as an optional last argument: \newline \example{\mbox{\ACmd{\Verb|\AChashf{m}[*]|}}\gives \AChashf{m}[*]}\vspace*{-2.0ex}\\ \nopagebreak \emph{Arguments:} & \cmdargs{AChashf}{Bimo}\newline \cmdargex{AChasf}{\cmdoarg{size}{\cmdearg}% \cmdmarg{value}\cmdoarg{returns}} \\\hline % \AChashf[big]{m} % & \ACmd{\Verb|\AChashf[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 $\AMacf{A}{m}$ & \ACmd{\Verb|\AMacf{A}{m}|}, used for a message authentication code function with the arguments \AKey{A} and \AVal{m}. Since \ACmd{\Verb|\AMacf|} is a function, we can include a return value as an optional last argument: \newline \example{\mbox{\ACmd{\Verb|\AMacf{A}{m}[*]|}}\gives \AMacf{A}{m}[*]}\vspace*{-2.0ex}\\ \nopagebreak \emph{Arguments:} & \cmdargs{AMacf}{TBimmo}\newline \cmdargex{AMacf}{{\cmdkarg}\cmdoarg{size}{\cmdearg}% \cmdmarg{key}\cmdmarg{value}\cmdoarg{returns}} \\\hline $\ACmacf{A}{m}$ & \ACmd{\Verb|\ACmacf{A}{m}|}, used for a cipher-based message authentication code with the arguments \AKey{A} and \AVal{m}. Since \ACmd{\Verb|\ACmacf|} is a function, we can include a return value as an optional last argument: \newline \example{\mbox{\ACmd{\Verb|\ACmacf{A}{m}[*]|}}\gives \ACmacf{A}{m}[*]}\vspace*{-2.0ex}\\ \nopagebreak \emph{Arguments:} & \cmdargs{ACmacf}{TBimmo}\newline \cmdargex{ACmacf}{{\cmdkarg}\cmdoarg{size}{\cmdearg}% \cmdmarg{key}\cmdmarg{value}\cmdoarg{returns}} \\\hline $\AHmacf{A}{m}$ & \ACmd{\Verb|\AHmacf{A}{m}|}, used for a HMAC message authentication code with the arguments \AKey{A} and \AVal{m}. Since \ACmd{\Verb|\AHmacf|} is a function, we can include a return value as an optional last argument: \newline \example{\mbox{\ACmd{\Verb|\AHmacf{A}{m}[*]|}}\gives \AHmacf{A}{m}[*]}\vspace*{-2.0ex}\\ \nopagebreak \emph{Arguments:} & \cmdargs{AHmacf}{TBimmo}\newline \cmdargex{AHmacf}{{\cmdkarg}\cmdoarg{size}{\cmdearg}% \cmdmarg{key}\cmdmarg{value}\cmdoarg{returns}} \\\hline $\ASig-{A}{m}$ & \ACmd{\Verb|\ASig-{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}). The other key type markers can also be used with this command. % Other options are no markers, % \ACmd{*}, \ACmd{+} (rarely used) and~\ACmd{!}: % \newline % \example{% % \begin{array}{lcl@{\quad}l} % \mbox{\ACmd{\Verb|\ASig{A,B}{m}|}} & \givesarrow % & \ASig{A,B}{m} % & \mbox{Signature from shared key \AKey{A,B}} \\ % \mbox{\ACmd{\Verb|\ASig*{K}{m}|}} & \givesarrow % & \ASig*{K}{m} % & \mbox{Signature from specific key \AKey*{K}} \\ % \mbox{\ACmd{\Verb|\ASig+{B}{m}|}} & \givesarrow % & \ASig+{A}{m} % & \mbox{Signature from public key \AKey+{A}} \\ % \mbox{\ACmd{\Verb|\ASig!{A}{m}|}} & \givesarrow % & \ASig!{A}{m} % & \mbox{Signature signed by \APri{A}} \\ % \mbox{\ACmd{\Verb|\ASig!{A,B}{m}|}} & \givesarrow % & \ASig!{A,B}{m} % & \mbox{Signature based on a shared secret} % \end{array}} \\[-1ex]\nopagebreak \emph{Arguments:} & \cmdargs{ASig}{TBimm}\newline \cmdargex{ASig}{{\cmdkarg}\cmdoarg{size}{\cmdearg}% \cmdmarg{key}\cmdmarg{value}} \\\hline $\ASigf-{A}{m}$ & \ACmd{\Verb|\ASigf-{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}). The other key type markers can also be used with this command. Since \ACmd{\Verb|\ASigf|} is a function, we can include a return value as an optional last argument (and it supports magic return making straightforward to include the return value). \\[-1ex]\nopagebreak \emph{Arguments:} & \cmdargs{ASigf}{TBimmx}\newline \cmdargex{ASigf}{{\cmdkarg}\cmdoarg{size}{\cmdearg}% \cmdmarg{key}\cmdmarg{value}\cmdoarg{returns}} \\\hline $\ASigned-{A}{m}$ & \ACmd{\Verb|\ASigned-{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}). The other key type markers can also be used with this command. % Other, often used, options are % no marker, \ACmd{*}, \ACmd{+} (rarely used) and % \ACmd{!}: % \newline % \example{% % \begin{array}{lcl@{\quad}l} % \mbox{\ACmd{\Verb|\ASigned{A,B}{m}|}} & \givesarrow % & \ASigned{A,B}{m} % & \mbox{\AVal{m} signed with shared key \AKey{A,B}} \\ % \mbox{\ACmd{\Verb|\ASigned*{K}{m}|}} & \givesarrow % & \ASigned*{K}{m} % & \mbox{\AVal{m} signed with specific key \AKey*{K}} \\ % \mbox{\ACmd{\Verb|\ASigned+{A}{m}|}} & \givesarrow % & \ASigned+{A}{m} % & \mbox{\AVal{m} signed with public key \AKey+{A}} \\ % \mbox{\ACmd{\Verb|\ASigned!{A}{m}|}} & \givesarrow % & \ASigned!{A}{m} % & \mbox{\AVal{m} signed by \APri{A}} \\ % \mbox{\ACmd{\Verb|\ASigned!{A,B}{m}|}} & \givesarrow % & \ASigned!{A,B}{m} % & \mbox{\AVal{m} signed with a shared secret} % \end{array}} \\[-1ex]\nopagebreak \emph{Arguments:} & \cmdargs{ASigned}{TBimm}\newline \cmdargex{ASigned}{{\cmdkarg}\cmdoarg{size}{\cmdearg}% \cmdmarg{key}\cmdmarg{value}} \\\hline $\ASign-{A}{m}$ & \ACmd{\Verb|\ASign-{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}). The other key type markers can also be used with this command. Since \ACmd{\Verb|\ASign|} is a function, we can include a return value as an optional last argument (and it supports magic return making straightforward to include the return value). \\[-1ex]\nopagebreak \emph{Arguments:} & \cmdargs{ASign}{TBimmx}\newline \cmdargex{ASign}{{\cmdkarg}\cmdoarg{size}{\cmdearg}% \cmdmarg{key}\cmdmarg{value}\cmdoarg{returns}} \\\hline $\APwkeyf{P}(s)$ & \ACmd{\Verb|\APwkeyf{P}(s)|}, used to create a secret key from a password \AVal{P}. Optionally, a salt value \AVal{s} can be provided Since \ACmd{\Verb|\APwkeyf|} is a function, we can include a return value as an optional last argument (and it supports magic return making straightforward to include the return value): \newline \example{% \mbox{\ACmd{\Verb|\APwkeyf{P_1}(s)[*]|}}\gives\APwkeyf{P_1}(s)[*]\\ \mbox{\ACmd{\Verb|\APwkeyf{P_2}[x]|}}\gives \APwkeyf{P_2}[x]}\vspace*{-2.0ex}\\ \nopagebreak \emph{Arguments:} & \cmdargs{APwkeyf}{sBimpx}\newline \cmdargex{APwkeyf}{{\cmdsarg}\cmdoarg{size}{\cmdearg}% \cmdmarg{password}\cmdparg{salt}\cmdoarg{returns}} \\\hline $\ADhpubkeyf{A}(p)$ & \ACmd{\Verb|\ADhpubkeyf{A}(p)|}, used to create a public key \AKey+{A} (a key share) from a private key \AKey-{A} and the optional public parameters \AVal{p}, typically used in a Diffie–Hellman key exchange protocol~\cite{diffie1976a}. \newline \example{% \mbox{\ACmd{\Verb|\ADhpubkeyf{A}(p)[A]|}}\gives\ADhpubkeyf{A}(p)[A] \\ \mbox{\ACmd{\Verb|\ADhpubkeyf*{x}[y]|}}\gives\ADhpubkeyf*{x}[y]}% \vspace*{-2.0ex}\\ \nopagebreak \emph{Arguments:} & \cmdargs{ADhpubkeyf}{sBimpo}\newline \cmdargex{ADhpubkeyf}{{\cmdsarg}\cmdoarg{size}% {\cmdearg}\cmdmarg{key}\cmdparg{parms}\cmdoarg{returns}} \\\hline $\ADhkeyf{A}{B}(p)$ & \ACmd{\Verb|\ADhkeyf{A}{B}(p)|}, used to combine a private key \AKey-{A} with public key \AKey+{B} and the optional public parameters \AVal{p} to generate a new secret (shared) key \AKey{A,B}, typically used in a Diffie–Hellman key exchange protocol~\cite{diffie1976a}. \newline \example{% \mbox{\ACmd{\Verb|\ADhkeyf{A}{B}(p)[A,B]|}}\gives\ADhkeyf{A}{B}(p)[A,B] \\ \mbox{\ACmd{\Verb|\ADhkeyf*{x}{y}[z]|}}\gives\ADhkeyf*{x}{y}[z]}% \vspace*{-2.0ex}\\ \nopagebreak \emph{Arguments:} & \cmdargs{ADhkeyf}{sBimmpo}\newline \cmdargex{ADhkeyf}{{\cmdsarg}\cmdoarg{size}{\cmdearg}% \cmdmarg{key}\cmdmarg{key}\cmdparg{parms}% \cmdoarg{returns}} \\\hline $\AVerify+{A}{\AVar{s}}$ & \ACmd{\Verb|\AVerify+{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}. The other key type markers can also be used with this command. \\[-1ex]\nopagebreak \emph{Arguments:} & \cmdargs{AVerify}{TBimmo}\newline \cmdargex{AVerify}{{\cmdkarg}\cmdoarg{size}{\cmdearg}% \cmdmarg{key}\cmdmarg{value}\cmdoarg{returns}} \\\hline $\ACertificate!{C}{\APri{B},\AKey+{B}}$ & \ACmd{\Verb|\ACertificate!{C}{\APri{B},\AKey+{B}}|}, used for a certificate binding the public key \AKey+{B} (public key of \APri{B}) to the principal \APri{B}, where \ACmd{!} says that the signature is signed by the certificate authority \APri{C}. The other key type markers can also be used with this command. \\[-1ex]\nopagebreak \emph{Arguments:} & \cmdargs{ACertificate}{TBimm}\newline \cmdargex{ACertificate}{{\cmdkarg}\cmdoarg{size}% {\cmdearg}\cmdmarg{key}\cmdmarg{content}} \\\hline $\ACert-{C}{A}$ & \ACmd{\Verb|\ACert-{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 certificate authority \APri{C}). The other key type markers can also be used with this command. \\[-1ex]\nopagebreak \emph{Arguments:} & \cmdargs{ACert}{TBimm}\newline \cmdargex{ACert}{{\cmdkarg}\cmdoarg{size}% {\cmdearg}\cmdmarg{key}\cmdmarg{principal}} \\\hline $\AMktval{X}\ATvalX{m}$ & \ACmd{\Verb|\AMktval{X}|}, used to create a new typed structured value type where the argument is the type. In this example, the result is a new {\latex} command \ACmd{\Verb|\ATvalX|} (created combining the prefix \ACmd{\Verb|tval|} and the given name). We can for example use this to create a new typed structured type for a specific message type:\newline \example{% % \mbox{\ACmd{% % \Verb|\ATval{KT}{\APri{S},\APri{C},\mbox{Addr},\ATS{t},\ATTL{l}}|}} % & \givesarrow % & \ATval{KT}{\APri{S},\APri{C},\mbox{Addr},\ATS{t},\ATTL{l}} \\ \begin{tabular}{@{}l@{}} \mbox{\ACmd{\Verb|\AMktval{ReqMsg}|}} \\ \mbox{\ACmd{\Verb|\ATvalReqMsg{\APri{A},m}|}} \end{tabular}\gives \AMktval{ReqMsg}\ATvalReqMsg{\APri{A},m}% }\vspace*{-2.2ex} \\ & The new command will have a \ACmd{\Verb|*|} version similar to the \ACmd{\Verb|\ATval*|} command (the value is not wrapped with curly brackets). The \ACmd{\Verb|\AMktval|} has an optional first argument to specify the name of the command created:\newline \example{ \begin{tabular}{@{}l@{}} \mbox{\ACmd{\Verb|\AMktval[reqmsg]{RMsg}|}} \\ \mbox{\ACmd{\Verb|\reqmsg{m}|}} \end{tabular}\gives \AMktval[reqmsg]{RMsg}\reqmsg{m}}\vspace*{-2.0ex}\\ \nopagebreak \emph{Arguments:} & \cmdargs{AMktval}{om}[sBim]\newline \cmdargex{AMktval}{\cmdoarg{cmd}\cmdmarg{type}}% [\cmdargexx{cmd}{{\cmdsarg}\cmdoarg{size}% {\cmdearg}\cmdmarg{value}}] \\\hline $\AMketval{X}\AEtvalX{A}{m}$ & \ACmd{\Verb|\AMketval{X}|}, used to create a new \emph{encrypted} typed structured value type where the argument is the type. In this example, the result is a new {\latex} command \ACmd{\Verb|\AEtvalX|} (created combining the prefix \ACmd{\Verb|AEtval|} and the given name). We can for example use this to create a new typed structured type for an encrypted message type:\newline \example{% \begin{tabular}{@{}l@{}} \mbox{\ACmd{\Verb|\AMketval{EMsg}|}} \\ \mbox{\ACmd{\Verb|\AEtvalEMsg'{C,S}{m}|}} \end{tabular}\gives \AMketval{EMsg}\AEtvalEMsg'{C,S}{m}}\vspace*{-2.2ex}\\ & The \ACmd{\Verb|\AMketval|} has an optional first argument to specify the name of the command created (here we define the command \ACmd{\Verb|\aka|} for Kerberos Authenticators):\newline \example{% \begin{tabular}{@{}l@{}} \mbox{\ACmd{\Verb|\AMketval[aka]{KA}|}} \\ \mbox{\ACmd{% \Verb|\aka'{S,C}{\APri{C},\textit{Addr}_C,\ATS{s}}|}} \end{tabular}\gives \AMketval[aka]{KA}\aka'{S,C}{\APri{C},\textit{Addr}_C,\ATS{s}}}% \vspace*{-2.2ex}\\ & In this case, it might be a good idea to create a new {\latex} command \ACmd{\Verb|\ka|} implemented with \ACmd{\Verb|\aka|} and the proper arguments (implementation details not shown):\newline \example{% \begin{tabular}{@{}l@{}} \mbox{\ACmd{\Verb|\newcommand{\ka}[3]{\aka'{...}}|}}\\ \mbox{\ACmd{\Verb|\ka{S,C}{C}{s}|}} \end{tabular}\gives \AMketval[aka]{KA}% \NewDocumentCommand\ka{mmm}{\aka'{#1}{% \APri{#2},\textit{Addr}_{\APri{#2}},\ATS{#3}}}% \ka{S,C}{C}{s}% }\vspace*{-2.0ex}\\ \nopagebreak \emph{Arguments:} & \cmdargs{AMketval}{om}[TBimm]\newline \cmdargex{AMketval}{\cmdoarg{cmd}\cmdmarg{type}}% [\cmdargexx{cmd}{{\cmdkarg}\cmdoarg{size}% {\cmdearg}\cmdmarg{key}\cmdmarg{value}}] \\\hline $\AMkstval{X}\AStvalX{A}{m}$ & \ACmd{\Verb|\AMkstval{X}|}, used to create a new \emph{signed} typed structured value type where the argument is the type. In this example, the result is a new {\latex} command \ACmd{\Verb|\AStvalX|} (created combining the prefix \ACmd{\Verb|AStval|} and the given name). We can for example use this to create a new typed structured type for an signed message type:\newline \example{% % \mbox{\ACmd{% % \Verb|\ATval{KT}{\APri{S},\APri{C},\mbox{Addr},\ATS{t},\ATTL{l}}|}} % & \givesarrow % & \ATval{KT}{\APri{S},\APri{C},\mbox{Addr},\ATS{t},\ATTL{l}} \\ \begin{tabular}{@{}l@{}} \mbox{\ACmd{\Verb|\AMkstval{SMsg}|}} \\ \mbox{\ACmd{\Verb|\AStvalSMsg-{A}{m}|}} \end{tabular}\gives \AMkstval{SMsg}\AStvalSMsg-{A}{m}}\vspace*{-2.2ex} \\ & The \ACmd{\Verb|\AMkstval|} has an optional first argument to specify the name of the command created:\newline \example{% \begin{tabular}{@{}l@{}} \mbox{\ACmd{\Verb|\AMkstval[smsg]{SMsg}|}} \\ \mbox{\ACmd{\Verb|\smsg-{S}{m}|}} \end{tabular}\gives \AMkstval[smsg]{SMsg}\smsg-{S}{m}}\vspace*{-2.0ex}\\ \nopagebreak \emph{Arguments:} & \cmdargs{AMkstval}{om}[TBimm]\newline \cmdargex{AMkstval}{\cmdoarg{cmd}\cmdmarg{type}}% [\cmdargexx{cmd}{{\cmdkarg}\cmdoarg{size}% {\cmdearg}\cmdmarg{key}\cmdmarg{value}}] \\\hline $\AMkfunc{X}\AFuncX{x,y}$ & \ACmd{\Verb|\AMkfunc{X}|}, used when creating a new function type where the argument is the name of the function type. In this example the result is a new {\latex} command \ACmd{\Verb|\AFuncX|} (created combining the prefix \ACmd{\Verb|func|} and the given name). We can for example use this to create a new function type for a creating a Kerberos Authenticator:\newline \example{% % \mbox{\ACmd{% % \Verb|\ATval{KT}{\APri{S},\APri{C},\mbox{Addr},\ATS{t},\ATTL{l}}|}} % & \givesarrow % & \ATval{KT}{\APri{S},\APri{C},\mbox{Addr},\ATS{t},\ATTL{l}} \\ \begin{tabular}{@{}l@{}} \mbox{\ACmd{\Verb|\AMkfunc{KA}|}} \\ \mbox{\ACmd{\Verb|\AFuncKA{\APri{C},\textit{Addr}_C,\ATS{s}}|}} \end{tabular}\gives \AMkfunc{KA}\AFuncKA{\APri{C},\textit{Addr}_C,\ATS{s}}}\vspace*{-2.2ex} \\ & The \ACmd{\Verb|\AMkfunc|} has an optional first argument to specify the name of the command created:\newline \example{% \begin{tabular}{@{}l@{}} \mbox{\ACmd{\Verb|\AMkfunc[kaf]{KA}|}} \\ \mbox{\ACmd{\Verb|\kaf{\APri{C},\textit{Addr}_C,\ATS{s}}|}} \end{tabular}\gives \AMkfunc[kaf]{KA}\kaf{\APri{C},\textit{Addr}_C,\ATS{s}}}\vspace*{-2.2ex} \\ & The \ACmd{\Verb|\AMkfunc|} has an optional third and last argument to specify the name of the command used for magic return:\newline \example{% \begin{tabular}{@{}l@{}} \mbox{\ACmd{\Verb|\AMktval[aset]{Set}]|}} \\ \mbox{\ACmd{\Verb|\AMkfunc[asetf]{Set}[aset]|}} \\ \mbox{\ACmd{\Verb|\asetf{\AVal{x},\AVal{y}}[*]|}} \end{tabular}\gives \AMktval[aset]{Set} \AMkfunc[asetf]{Set}[aset]% \asetf{\AVal{x},\AVal{y}}[*]}\vspace*{-2.0ex} \\ \nopagebreak \emph{Arguments:} & \cmdargs{AMkfunc}{omo}[Bimx]\newline \cmdargex{AMkfunc}{% \cmdoarg{cmd}\cmdmarg{name}\cmdoarg{magic-return}}% [\cmdargexx{cmd}{\cmdoarg{size}{\cmdearg}% \cmdmarg{arguments}\cmdoarg{returns}}] \\\hline $\AMkkfunc{X}\AKfuncX{A}{x,y}$ & \ACmd{\Verb|\mkkfunk{X}|}, used when creating a new function type for functions where the first argument is an encryption key. The argument is the name of the function type. In this example the result is a new {\latex} command \ACmd{\Verb|\AKfuncX|} (created combining the prefix \ACmd{\Verb|kfunc|} and the given name) with two arguments; the first argument is an encryption key and the second argument is a comma separated list of the rest of the function arguments. We can for example use this to create this new function type with an encryption key as the first argument (a session key in this example):\newline \example{% % \mbox{\ACmd{% % \Verb|\ATval{KT}{\APri{S},\APri{C},\mbox{Addr},\ATS{t},\ATTL{l}}|}} % & \givesarrow % & \ATval{KT}{\APri{S},\APri{C},\mbox{Addr},\ATS{t},\ATTL{l}} \\ \begin{tabular}{@{}l@{}} \mbox{\ACmd{\Verb|\AMkkfunc{KeyF}|}} \\ \mbox{\ACmd{\Verb|\AKfuncKeyF'{A}{\textit{Addr},\ATS{s}}|}} \end{tabular}\gives \AMkkfunc{KeyF}\AKfuncKeyF'{A}{\textit{Addr},\ATS{s}}}\vspace*{-2.2ex} \\ & The \ACmd{\Verb|\AMkkfunc|} has an optional first argument to specify the name of the command created:\newline \example{% \begin{tabular}{@{}l@{}} \mbox{\ACmd{\Verb|\AMkkfunc[kf]{KeyF}|}} \\ \mbox{\ACmd{\Verb|\kf'{A}{\textit{Addr},\ATS{s}}|}} \end{tabular}\gives \AMkkfunc[kf]{KeyF}\kf'{A}{\textit{Addr},\ATS{s}}}\vspace*{-2.2ex} \\ & The \ACmd{\Verb|\AMkkfunc|} has an optional third and last argument to specify the name of the command used for magic return:\newline \example{% \begin{tabular}{@{}l@{}} \mbox{\ACmd{\Verb|\AMkstval[sset]{SSet}]|}} \\ \mbox{\ACmd{\Verb|\AMkkfunc[ssetf]{SignSet}[sset]|}} \\ \mbox{\ACmd{\Verb|\ssetf-{A}{\AVal{x},\AVal{y}}[*]|}} \end{tabular}\gives \AMkstval[sset]{SSet} \AMkkfunc[ssetf]{SignSet}[sset]% \ssetf-{A}{\AVal{x},\AVal{y}}[*]}\vspace*{-2.0ex} \\ \nopagebreak \emph{Arguments:} & \cmdargs{AMkkfunc}{omo}[TBimmx]\newline \cmdargex{AMkkfunc}{% \cmdoarg{cmd}\cmdmarg{name}\cmdoarg{magic-return}}% [\cmdargexx{cmd}{{\cmdkarg}\cmdoarg{size}{\cmdearg}% \cmdmarg{key}\cmdmarg{arguments}\cmdoarg{returns}}] \\\Xhline{0.5pt} \end{xltabular}} %\clearpage \subsection{BAN logic} \label{sec:latex-ban} The table below lists the BAN logic notation with the matching {\latex} commands. This notation is 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} \BANBelieves & \ACmd{\Verb|\BANBelieves|}, used to state that someone \emph{believes} something (and acts as it is true): \newline \example{\mbox{\ACmd{\Verb|\APri{A}\BANBelieves\AVal{X}|}}\gives \APri{A}\BANBelieves\AVal{X}} \\\hline \BANSees & \ACmd{\Verb|\BANSees|}, 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}\BANSees\AVal{X}|}}\gives \APri{A}\BANSees\AVal{X}} \\\hline \BANOncesaid & \ACmd{\Verb|\BANOncesaid|}, 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}\BANOncesaid\AVal{X}|}}\gives \APri{A}\BANOncesaid\AVal{X}} \\\hline \BANControls & \ACmd{\Verb|\BANControls|}, used to state that someone has \emph{jurisdiction} (controls) over something: \newline \example{\mbox{\ACmd{\Verb|\APri{A}\BANControls\AVal{X}|}}\gives \APri{A}\BANControls\AVal{X}} \\\hline \BANFresh{X} & \ACmd{\Verb|\BANFresh{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 \BANSharedkey{K} & \ACmd{\Verb|\BANSharedkey{K}|}, used to state that a key is shared: \newline \example{\mbox{\ACmd{\Verb|\APri{A}\BANSharedkey{\AKey{A,B}}\APri{B}|}}\gives \APri{A}\BANSharedkey{\AKey{A,B}}\APri{B}} \\\hline \BANPubkey{K} & \ACmd{\Verb|\BANPubkey{K}|}, used to state that a key is a public key of someone: \newline \example{\mbox{\ACmd{\Verb|\BANPubkey{\AKey+{A}}\APri{A}|}}\gives \BANPubkey{\AKey+{A}}\APri{A}} \\\hline \BANSecret{X} & \ACmd{\Verb|\BANSecret{X}|}, used to state that a secret (\AVal{X}, in this case) is only known to them: \newline \example{\mbox{\ACmd{\Verb|\APri{A}\BANSecret{X}\APri{B}|}}\gives \APri{A}\BANSecret{X}\APri{B}} \\\hline \BANEncryptedwith{K}{X} & \ACmd{\Verb|\BANEncryptedwith{K}{X}|}, used to state that something is encrypted with the key (\AVal{X} is encrypted with the key \AKey*{K}). \\\hline \BANCombine{x}{y} & \ACmd{\Verb|\BANCombine{x}{y}|}, used to state that $x$ is combined with $y$: \newline \example{\mbox{\ACmd{\Verb|\BANCombine{\AVal{X}}{\AVal{Y}}|}}\gives \BANCombine{\AVal{X}}{\AVal{Y}}} \\\Xhline{0.5pt} \end{xltabular}} %\clearpage \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{ASteps} environment. A message between to principals is in the \ACmd{ASteps} environment typeset with the familiar \ACmd{\Verb|\ASend|} command. With \ACmd{\Verb|\ASend|} commands, the \ACmd{ASteps} environment can be used like this: \begin{ltxexample}{238pt} \begin{ASteps} \ASend*{A}{B}{\AEncrypted+{B}{m_1}}[m1] \\ \ASend*{B}{A}{\AEncrypted+{A}{m_2}}[m2] \end{ASteps} \end{ltxexample} Notice that each step is separated by the \ACmd{\Verb|\\|} command. Each step is labeled and can be referred to by its name (\ACmd{\Verb|\ARef{m1}|} {\givesarrow} \ARef{m1}, and \ACmd{\Verb|\ARef{m2}|} {\givesarrow} \ARef{m2}). The \ACmd{ASteps*} version of the environment is without the labels: \begin{ltxexample}{217pt} \begin{ASteps*} \ASend*{A}{B}{\AEncrypted+{B}{m_1}} \\ \ASend*{B}{A}{\AEncrypted+{A}{m_2}} \end{ASteps*} \end{ltxexample} By default, the \ACmd{ASteps} environment has two types of labels; \ACmd{M} for messages and \ACmd{S} for other steps. In the example above only messages (\ACmd{\Verb|\ASend|} 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}{185pt} \begin{ASteps}[lspace=1em] \AStep{\AEncrypt+{B}{m_1}[*]} \\ \AStep{\ASign-[big]{A}{% \AEncrypted+{B}{m_1}}[*]} \end{ASteps} \end{ltxexample} The optional key-value argument \ACmd{rmarg} sets the right margin width of the ASteps environment and \ACmd{lmarg} sets the left margin width of the ASteps environment. The default margin widths are \ACmd{\Verb|\tabcolsep|}. In the following example the margins are removed: \begin{ltxexample}{194pt} \begin{ASteps*}[lmarg=0pt,rmarg=0pt] \AStep{No margins} \end{ASteps*} \end{ltxexample} We can also change the margins, and the space between the label and the step, by adjusting the lengths \ACmd{\Verb|\AStepsleftmargin|}, \ACmd{\Verb|\AStepsrightmargin|} and \ACmd{\Verb|\AStepslabelspace|}. 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*}{182pt} \setlength{\AStepsleftmargin}{0pt} \setlength{\AStepsrightmargin}{0pt} \setlength{\AStepslabelspace}{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}{195pt} \begin{ASteps}* \AStepat{A}{\ASign-{A}{m_1}[*]} \\ \AStepat{A}{\AEncrypt+[big]{B}{% \ASigned-{A}{m_1}}[*]} \end{ASteps} \end{ltxexample} The \ACmd{*} marker of the \ACmd{ASteps} environment (not to be confused with the \ACmd{ASteps*} version of the environment) means that the counters of the labels are \emph{not} reset (the counting continues from the previous \ACmd{ASteps} environment). It is also possible to set the value of each counter using the standard {\latex} command \ACmd{\Verb|\setcounter|}. For example, if you want the counter of the \ACmd{S} labels to start with zero, you add this as the first command inside a \ACmd{ASteps} environment: \ACmd{\Verb|\setcounter{counterS}{-1}|} (see \refltxcode{smc-mean} for an example). 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}{227pt} \begin{ASteps}[labels={A,B}] \AStepat(A){A}{\AEncrypt+{B}{m_1}[*]} \\ \ASend*{A}{B}{\AEncrypted+{B}{m_1}} \\ \AStepat(B){B}{\ADecrypt-[big]{B}{% \AEncrypted+{B}{m_1}}[m_1]} \end{ASteps} \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}{252pt} \begin{ASteps*} \ASend*{A}{B}{\ASigned-{A}{m_1}} \\ \AStepat*{B}{\AVerify+{A}{\ASigned-{A}{m_1}}} \end{ASteps*} \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}{225pt} \begin{ASteps*} \ASend*{A}{B}{\ASigned-{A}{m_1}} \\ \AStep*{\AVerify+{A}{\ASigned-{A}{m_1}}} \end{ASteps*} \end{ltxexample} The \ACmd{\Verb|\ARawstep|} command is a low-level command that usually is not necessary. In a \ACmd{ASteps*} environment it has four optional arguments followed by one non-optional argument. In a \ACmd{ASteps} 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|\ASend|} command in a \ACmd{ASteps} environment: \begin{ltxexample}{184pt} \begin{ASteps} \ASend{A}{B}{m}[s1] \\ \ARawstep(M)[a][--][b][;]{m}[s2] \end{ASteps} \end{ltxexample} % The last optional argument of the commands \ACmd{\Verb|\ASend|} and % \ACmd{\Verb|\ARawstep|} is a label name that we can use to refer to these % steps, \ARef{s1} and \ARef{s2} in this case. The first optional argument % of \ACmd{\Verb|\ARawstep|} is the label type for this step. The \ACmd{ASteps} % 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{ASteps} or % \ACmd{ASteps*} environments. % \begin{center} % \begin{minipage}[c]{0.49\linewidth} % \begin{minted}{latex} % \begin{ASteps} % \AStepat{A}{\AEncrypt+{B}{m_1}[]} \\ % \ASend*{A}{B}{\AEncrypted+{B}{m_1}} \\ % \AStepat{B}{\ADecrypt-[big]{B}{% % \AEncrypted+{B}{m_1}}[m_1]} \\ % \AStepat{B}{\AEncrypt+{A}{m_2}[*]} \\ % \ASend*{B}{A}{\AEncrypted+{A}{m_2}} \\ % \AStepat{A}{\ADecrypt-[big]{A}{% % \AEncrypted+{A}{m_2}}[m_2]} % \end{ASteps} % \end{minted} % \end{minipage}\gives % \begin{ASteps} % \AStepat{A}{\AEncrypt+{B}{m_1}[*]} \\ % \ASend*{A}{B}{\AEncrypted+{B}{m_1}} \\ % \AStepat{B}{\ADecrypt-[big]{B}{% % \AEncrypted+{B}{m_1}}[m_1]} \\ % \AStepat{B}{\AEncrypt+{A}{m_2}[*]} \\ % \ASend*{B}{A}{\AEncrypted+{A}{m_2}} \\ % \AStepat{A}{\ADecrypt-[big]{A}{% % \AEncrypted+{A}{m_2}}[m_2]} % \end{ASteps} % \end{center} % The arguments specification for the commands for the \ACmd{ASteps*} and % \ACmd{step} environments: {\renewcommand{\arraystretch}{1.6}% \begin{xltabular}{\textwidth}{@{}l@{\hspace{.8em}}X@{}} \multicolumn{2}{@{}l@{}}{% \textbf{The arguments of the commands in the \ACmd{ASteps*} environment}} \\ & \cmdargs{ASend}{sBmmm}\newline \cmdargex{ASend}{\cmdsarg\cmdoarg{size}\cmdmarg{sender}% \cmdmarg{receiver}\cmdmarg{message}} \\ & \cmdargs{AStep}{sm}\newline \cmdargex{AStep}{\cmdsarg\cmdmarg{step}} \\ & \cmdargs{AStepat}{smm}\newline \cmdargex{AStepat}{\cmdsarg\cmdmarg{where}\cmdmarg{step}} \\ & \cmdargs{ARawstep}{oooom}\newline \cmdargex{ARawstep}{\cmdoarg{sender}\cmdoarg{arrow}\cmdoarg{receiver}% \cmdoarg{colon}\cmdmarg{step}} \end{xltabular}}\vspace*{-1.5\baselineskip} {\renewcommand{\arraystretch}{1.6}% \begin{xltabular}{\textwidth}{@{}l@{\hspace{.8em}}X@{}} \multicolumn{2}{@{}l@{}}{% \textbf{The arguments of the commands in the \ACmd{ASteps} environment}} \\ & \cmdargs{ASend}{sP{M}Bmmmo}\newline \cmdargex{ASend}{\cmdsarg\cmdparg{type}\cmdoarg{size}\cmdmarg{sender}% \cmdmarg{receiver}\cmdmarg{message}\cmdoarg{label}} \\ & \cmdargs{AStep}{sP{S}mo}\newline \cmdargex{AStep}{\cmdsarg\cmdparg{type}% \cmdmarg{step}\cmdoarg{label}} \\ & \cmdargs{AStepat}{sP{S}mmo}\newline \cmdargex{AStepat}{\cmdsarg\cmdparg{type}\cmdmarg{where}% \cmdmarg{step}\cmdoarg{label}} \\ & \cmdargs{Rawstep}{P{S}oooomo}\newline \cmdargex{ARawstep}{\cmdparg{type}\cmdoarg{sender}\cmdoarg{arrow}% \cmdoarg{receiver}\cmdoarg{colon}\cmdmarg{step}\cmdoarg{label}} \end{xltabular}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \clearpage \section{Notation usage examples} \label{sec:ex-notation-usage} To illustrate the usability of the notation, we provide a few examples where the notation is used to describe well-known, and not so well-known, security protocols. In the original papers referred to below, you will find the original notations used. The inconsistencies in the notations used in these papers are a major motivation behind {\Aspen}. The following examples are presented here: {\tableoflisting} The three last examples listed are from my own publications. I have included them since they represent the start of my process developing this notation. You will find that my use of notations then was a mixed bag without consistency across publications. \tol{org-ns}{Original Needham–Schroeder protocol} 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 (the \emph{Needham–Schroeder public key protocol} is presented on page~\pageref{ns-pk-ex}). \begin{ltxex}{org-ns}{Original Needham–Schroeder protocol} \begin{ASteps} \ASend{A}{S}{\APri{A}, \APri{B}, \ANonce{A}}[ons:1] \\ \ASend*{S}{A}{\AEncrypted[big]{A,S}{\ANonce{A}, \APri{B}, \AKey{A,B}, \AEncrypted{B,S}{\AKey{A,B}, \APri{A}}}}[ons:2] \\ \ASend*{A}{B}{\AEncrypted{B,S}{\AKey{A,B}, \APri{A}}}[ons:3] \\ \ASend*{B}{A}{\AEncrypted{A,B}{\ANonce{B}}}[ons:4] \\ \ASend*{A}{B}{\AEncrypted{A,B}{\ANonce{B} - 1}}[ons:5] \end{ASteps} \end{ltxex} \ANonce{A} and \ANonce{B} are nonces and the shared key \AKey{A,B} should be fresh, \BANFresh{\AKey{A,B}}. The protocol is vulnerable to a replay attack~\cite{denning1981a}. See \refltxcode{org-ns} for the {\latex} code. \tol{rev-ns}{Revised Needham–Schroeder protocol} The \emph{Revised Needham–Schroeder protocol}~\cite{needham1987a} addresses a weakness in the protocol related to its vulnerable to a replay attack. A fun fact regarding this suggested revision is its link to my home department, \href{https://en.uit.no/enhet/ifi}{Department of Computer Science} at UiT\footnote{UiT The Arctic University of Norway, formerly University of Tromsø}. From~\cite{needham1987a}: \begin{quote} \emph{In 1986 one of us (RMN) gave a lecture at the University of Tromsø which included the 1978 protocol, the criticism of it, and also a general principle about the use of nonce identifiers. This was that the identifier should always be generated by the party that sought reassurance about the time integrity of a transaction. In discussion Dr Sape J. Mullender of CWI Amsterdam pointed out that this should apply to the reassurance of B against the attack outlined.} \end{quote} The revised version adds two initial messages, \ARef{rns:1} and \ARef{rns:2}, between the two principals \APri{A} and \APri{B} and the extra nonce \ANonce{I} as an identifier of the session: \begin{ltxex}{rev-ns}{Revised Needham–Schroeder protocol} \begin{ASteps} \ASend{A}{B}{\APri{A}}[rns:1] \\ \ASend*{B}{A}{\AEncrypted{B,S}{\APri{A},\ANonce{I}}}[rns:2] \\ \ASend[big]{A}{S}{\APri{A}, \APri{B}, \ANonce{A}, \AEncrypted{B,S}{\APri{A},\ANonce{I}}}[rns:3] \\ \ASend*{S}{A}{\AEncrypted[big]{A,S}{\ANonce{A}, \APri{B}, \AKey{A,B}, \AEncrypted{B,S}{\AKey{A,B}, \APri{A}, \ANonce{I}}}}[rns:4] \\ \ASend*{A}{B}{\AEncrypted{B,S}{\AKey{A,B}, \APri{A}, \ANonce{I}}}[rns:5] \\ \ASend*{B}{A}{\AEncrypted{A,B}{\ANonce{B}}}[rns:6] \\ \ASend*{A}{B}{\AEncrypted{A,B}{\ANonce{B} - 1}}[rns:7] \end{ASteps} \end{ltxex} The inclusion of the new nonce \ANonce{I} prevents any replaying of compromised versions of message \AEncrypted{B,S}{\AKey{A,B},\APri{A}} since the revised version of the message contains \ANonce{I}: \AEncrypted{B,S}{\AKey{A,B},\APri{A},\ANonce{I}}. This can not be forged since an attacker does not have ⁠\AKey{B,S}. ⁠See \refltxcode{rev-ns} for the {\latex} code of the protocol. \tol{otway-rees}{Otway-Rees protocol} The \emph{Otway-Rees protocol}~\cite{otway1987a} is essential the same as the Revised Needham-Schroeder protocol: \begin{ltxex}{otway-rees}{Otway-Rees protocol} \begin{ASteps} \ASend[big]{A}{B}{\ACounter{A}, \APri{A}, \APri{B}, \AEncrypted{A,S}{\ANonce{A}, \ACounter{A}, \APri{A}, \APri{B}}}[or:1] \\ \ASend[big]{B}{S}{\ACounter{A}, \APri{A}, \APri{B}, \AEncrypted{A,S}{\ANonce{A}, \ACounter{A}, \APri{A}, \APri{B}}, \AEncrypted{B,S}{\ANonce{B}, \ACounter{A}, \APri{A}, \APri{B}}}[or:2] \\ \ASend[big]{S}{B}{\ACounter{A}, \AEncrypted{A,S}{\ANonce{A}, \AKey'{A,B}}, \AEncrypted{B,S}{\ANonce{B}, \AKey'{A,B}}}[or:3] \\ \ASend[big]{B}{A}{\ACounter{A}, \AEncrypted{A,S}{\ANonce{A}, \AKey'{A,B}}}[or:4] \end{ASteps} \end{ltxex} The identifier \ACounter{A} prevents the replay attack since an attacker is not able to alter \AEncrypted{A,S}{\ANonce{A}, \ACounter{A}, \APri{A}, \APri{B}} and \AEncrypted{B,S}{\ANonce{B}, \ACounter{A}, \APri{A}, \APri{B}}. See \refltxcode{otway-rees} for the {\latex} code. \tol{kerberos}{Kerberos protocol} 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 original Needham-Schroeder protocol and to reduce the number of messages needed: \begin{ltxex}{kerberos}{Kerberos protocol} \begin{ASteps} \ASend{A}{S}{\APri{A}, \APri{B}} \\ \ASend*{S}{A}{\AEncrypted[big]{A,S}{\ATS{s}, \ATTL{}, \AKey{A,B}, \APri{B}, \AEncrypted{B,S}{\ATS{s}, \ATTL{}, \AKey{A,B}, \APri{A}}}} \\ \ASend[big]{A}{B}{\AEncrypted{B,S}{\ATS{s}, \ATTL{}, \AKey{A,B}, \APri{A}}, \AEncrypted{A,B}{\APri{A}, \ATS{a}}} \\ \ASend*{B}{A}{\AEncrypted{A,B}{\ATS{a} + 1}} \end{ASteps} \end{ltxex} \ATS{s} and \ATS{a} are timestamps and \ATTL{} is a lifetime. See \refltxcode{kerberos} for the {\latex} code. \tol{dh-ke}{Diffie–Hellman key exchange} The \emph{Diffie–Hellman key exchange} protocol~\cite{diffie1976a} is used to establish a shared symmetric key between two participants over a public channel based a secret (a private key) at each participant and some shared public parameters: \begin{ltxex}{dh-ke}{Diffie–Hellman key exchange} \begin{ASteps} \ASend{A}{B}{\AVal{p}}[dh-ex:1] \\ \AStepat*{A}{\ADhpubkeyf{A}(p)[A]}[dh-ex:2] \\ \AStepat*{B}{\ADhpubkeyf{B}(p)[B]}[dh-ex:3] \\ \ASend{A}{B}{\AKey+{A}}[dh-ex:4] \\ \ASend{B}{A}{\AKey+{B}}[dh-ex:5] \\ \AStepat*{A}{\ADhkeyf{A}{B}(p)[A,B]}[dh-ex:6] \\ \AStepat*{B}{\ADhkeyf{B}{A}(p)[A,B]}[dh-ex:7] \end{ASteps} \end{ltxex} The public keys created in step \ref{dh-ex:2} and \ref{dh-ex:3} are also called Diffie-Hellman key shares. At the end of this protocol the two participants \APri{A} and \APri{B} has a shared secret key \AKey{A,B}. In BAN logic, we can state the following about the outcome \AKey{A,B}: \[ \APri{A}\BANSharedkey{\AKey{A,B}}\APri{B} \] In step \ref{dh-ex:1} above, participant \APri{A} send the public parameters \AVal{p} to participant \APri{B}. Other means of agreeing on these parameters are possible and not important for the protocol itself. See \refltxcode{dh-ke} for the {\latex} code of the \emph{Diffie–Hellman key exchange} protocol. \tol{ns-pk}{Needham–Schroeder public key protocol} The \emph{Needham–Schroeder public key protocol}~\cite{needham1978a} intends to provide mutual authentication between two parties: \begin{ltxex}{ns-pk}{Needham–Schroeder public key protocol} \begin{ASteps} \ASend{A}{S}{\APri{A}, \APri{B}}[ns-pk:1] \\ \ASend*{S}{A}{\ASigned-{S}{\AKey+{B},\APri{B}}}[ns-pk:2] \\ \ASend*{A}{B}{\AEncrypted+{B}{\ANonce{A},\APri{A}}}[ns-pk:3] \\ \ASend{B}{S}{\APri{B}, \APri{A}}[ns-pk:4] \\ \ASend*{S}{B}{\ASigned-{S}{\AKey+{A},\APri{A}}}[ns-pk:5] \\ \ASend*{B}{A}{\AEncrypted+{A}{\ANonce{A},\ANonce{B}}}[ns-pk:6] \\ \ASend*{A}{B}{\AEncrypted+{B}{\ANonce{B}}}[ns-pk:7] \end{ASteps} \end{ltxex} \label{ns-pk-ex} This protocol is vulnerable to a man-in-the-middle attack~\cite{lowe1995a}. The fix is however easy. \tol{nsl-pk}{Needham–Schroeder-Lowe public key protocol} To avoid a man-in-the-middle attack, the \emph{Needham–Schroeder-Lowe public key protocol}~\cite{lowe1995a} includes the identity of the responder in message \ref{ns-pk:6} of the protocol: \begin{ltxex}{nsl-pk}{Needham–Schroeder-Lowe public key protocol} \begin{ASteps} \ASend{A}{S}{\APri{A}, \APri{B}}[nsl-pk:1] \\ \ASend*{S}{A}{\ASigned-{S}{\AKey+{B},\APri{B}}}[nsl-pk:2] \\ \ASend*{A}{B}{\AEncrypted+{B}{\ANonce{A},\APri{A}}}[nsl-pk:3] \\ \ASend{B}{S}{\APri{B}, \APri{A}}[nsl-pk:4] \\ \ASend*{S}{B}{\ASigned-{S}{\AKey+{A},\APri{A}}}[nsl-pk:5] \\ \ASend*{B}{A}{\AEncrypted+{A}{\ANonce{A},\ANonce{B},\APri{B}}}[nsl-pk:6] \\ \ASend*{A}{B}{\AEncrypted+{B}{\ANonce{B}}}[nsl-pk:7] \end{ASteps} \end{ltxex} See \refltxcode{ns-pk} and \refltxcode{nsl-pk} for the {\latex} code of the two versions of the \emph{Needham–Schroeder public key protocol}. \tol{asw}{ASW protocol} The \emph{ASW protocol} is an optimistic fair-exchange protocol for contract signing~\cite{asokan1998a}. This is a good example for {\Aspen} since we in publications find very different (and, if I may say so, hard to read) notations used when presenting the protocol~\cite{asokan1998a,briais2007a}. This is a simplified version of the \emph{exchange} subprotocol (the main part of the protocol) of ASW is shown in {\Aspen}: \begin{ltxex}{asw}{ASW exchange protocol} \begin{ASteps} \ASend*{O}{R}{\ASigned-[big]{O}{% \AKey+{A},\AKey+{B},m,\AChash{\ANonce{O}}}}[asW:1] \\ \ASend*{R}{O}{\ASigned-[Big]{R}{% \ASigned-[big]{O}{\AKey+{A},\AKey+{B},m,\AChash{\ANonce{O}}}, \AChash{\ANonce{R}}}}[asw:2] \\ \ASend{O}{R}{\ANonce{O}}[asw:3] \\ \ASend{R}{O}{\ANonce{R}}[asw:4] \end{ASteps} \end{ltxex} Two participants \APri{O} (originator) and \APri{R} (recipient) is involved in this subprotocol. In the complete protocol two other subprotocols (\emph{abort} and \emph{resolve}) and a third participant \APri{T} (third player) is included. See \refltxcode{asw} for the {\latex} code. \tol{wmf}{Wide-mouthed-frog protocol} The \emph{Wide-mouthed-frog protocol}~\cite{burrows1990a} (Section~7, page~25) is a simple protocol that uses shared key cryptography and an authentication server. It transfers a key from \APri{A} to \APri{B} via the authentication server \APri{S} in only two messages by using synchronized clocks and by allowing \APri{A} to choose the session key: \begin{ltxex}{wmf}{Wide-mouthed-frog protocol} \begin{ASteps} \ASend[big]{A}{S}{A, \AEncrypted{A,S}{\ATS{A}, \APri{B}, \AKey'{A,B}}}[wmf:1] \\ \ASend*[big]{S}{B}{\AEncrypted{B,S}{\ATS{S}, \APri{A}, \AKey'{A,B}}}[wmf:2] \end{ASteps} \end{ltxex} \APri{A} sends a time stamp \ATS{A} and session key \AKey'{A,B} to \APri{S}. \APri{S} checks that message \ARef{wmf:1} is timely. If it is, it forwards the key \AKey'{A,B} to \APri{B} together with its own timestamp \ATS{S} in message \ARef{wmf:2}. \APri{B} then checks that the timestamp \ATS{S} from \APri{S} is later than any another it has received from \APri{S}. \tol{iwmf}{Idealized wide-mouthed-frog protocol} The \emph{Idealized wide-mouthed-frog protocol} with BAN logic is shown below: \begin{ltxex}{iwmf}{Idealized wide-mouthed-frog protocol} \begin{ASteps} \ASend*{A}{S}{\AEncrypted[big]{A,S}{\ATS{A}, \{\APri{A}\BANSharedkey{\AKey{A,B}}\APri{B}\}}}[iwmf:1] \\ \ASend*[big]{S}{B}{\AEncrypted{B,S}{\ATS{S}, \APri{A}\BANBelieves\APri{A}\BANSharedkey{\AKey{A,B}}\APri{B}}}[iwmf:2] \end{ASteps} \end{ltxex} \tol{dwmf}{Wide-mouthed-frog protocol with declarations} In \cite{briais2007a}, formal declarations as part of protocol narrations is introduced. We can do something similar with BAN logic and {\Aspen}, where we use BAN logic for the declaration part (\ARef{dwmf:1}--\ARef{dwmf:3}). The following example is similar to their version of the \emph{Wide-mouthed-frog protocol with declarations} (see \cite{briais2007a}, Table~3, page~487): \begin{ltxex}{dwmf}{Wide-mouthed-frog protocol with declarations} \begin{ASteps}[labels=D] \AStep(D){\APri{A}\BANSharedkey{\AKey{A,S}}\APri{S}; \APri{B}\BANSharedkey{\AKey{B,S}}\APri{S}}[dwmf:1] \\ \AStep(D){\APri{A}\BANSees\AKey'{A,B}; \BANFresh{\AKey'{A,B}}; \APri{A}\BANSees\AVal{m}}[dwmf:3] \\ \ASend[big]{A}{S}{A,\AEncrypted{A,S}{\ATS{A},\APri{B},\AKey'{A,B}}}[dwmf:4] \\ \ASend*[big]{S}{B}{\AEncrypted{B,S}{\ATS{S},\APri{A},\AKey'{A,B}}}[dwmf:5] \end{ASteps} \end{ltxex} See \refltxcode{wmf}, \refltxcode{iwmf} and \refltxcode{dwmf} for the {\latex} code of the \emph{Wide-mouthed-frog protocol}, the \emph{Idealized wide-mouthed-frog protocol} and the \emph{Wide-mouthed-frog protocol with declarations}. \tol{tls-hs}{TLS 1.3 Handshake} The \emph{TLS 1.3 Handshake}~\cite{rescorla2018a} has three stages. Stage one is the key exchange, stage two is the server parameters, and stage three is authentication (we only include server authentication in the example). In the steps below stage one and three are included, the key exchange algorithm used is DHE (Ephemeral Diffie-Hellman) and we ignore PSK (Pre-Shared Key): \begin{ltxex}{tls-hs}{TLS 1.3 Handshake} \begin{ASteps} \AStepat*{C}{\BANFresh{\AKey-{C_e}}; \ADhpubkeyf{C_e}[C_e]}[tls-hs:1] \\ \ASend{C}{S}{\ldots, \ANonce{C}, \AKey+{C_e}, \ldots}[tls-hs:2] \\ \AStepat*{S}{\BANFresh{\AKey-{S_e}}; \ADhpubkeyf{S_e}[S_e]}[tls-hs:3] \\ \ASend[big]{S}{C}{\ldots, \ANonce{S}, \AKey+{S_e}, \ACert-{CA}{S}, \ASigned{S}{\ANonce{C}, \ANonce{S}, \ldots}, \ldots}[tls-hs:4] \\ \AStepat*{C}{\AVerify+{CA}{\ACert-{CA}{S}}[\ATrue]; \AVerify+{S}{\ASigned{S}{\ANonce{C}, \ANonce{S}, \ldots}}[\ATrue]}[tls-hs:5a] \\ \AStepat*{C}{\ADhkeyf{C_e}{S_e}[C,S]}[tls-hs:5b] \\ \AStepat*{S}{\ADhkeyf{S_e}{C_e}[C,S]}[tls-hs:6] \\ \ASend*{C}{S}{\AEncrypted{C,S}{\ldots}}[tls-hs:7] \\ \ASend*{S}{C}{\AEncrypted{C,S}{\ldots}}[tls-hs:8] \end{ASteps} \end{ltxex} The example above is somewhat simplified to make it easier to follow (some details are hidden and some optional pathways are ignored). After message \ref{tls-hs:4} and step \ref{tls-hs:6} the client \APri{C} and the server \APri{S} share a new fresh encryption key \AKey{C,S} and the rest of the TLS handshake is encrypted. Message \ref{tls-hs:7} and message \ref{tls-hs:8} are the client handshake finished and the server handshake finished messages, respectively. \tol{smc-mean}{SMC: Calculate the mean value} In~\cite{andersen2014a}, \emph{SMC} (secure multi-party computation) algorithms for analyzing health data were discussed. The first algorithm from this paper is used to calculate the mean value of three values \AVal{V_1}, \AVal{V_2} and \AVal{V_3} from three participants \APri{P_1}, \APri{P_2} and \APri{P_3} without sharing any knowledge about the individual values. A coordinator \APri{C} coordinates the calculation. The messages between from \APri{P_{i-1}} to \APri{P_i} have the following structure (we can say that participant \APri{P_0} and \APri{P_4} is the same individual with an alias \APri{C}): \qquad \begin{ASteps*}[lmarg=0pt] \AMsg[Big]{\AEncrypted+[big]{P_i}{\ASigned-{P_{i-1}}{\AVal{V'_{i}}}}, \AEncrypted+[big]{P_i}{\ASigned-{C}{\APri{P_{i-1}},\APri{P_{i+1}}}}, \AEncrypted+[big]{P_{i+1}}{\ASigned-{C}{\APri{P_{i}},\APri{P_{i+2}}}},\ldots} \end{ASteps*} The first part of the message is the intermediate value received at participant \APri{P_i} signed by the previous participant in the calculation \APri{P_{i-1}}. The second part is each path in the calculation (where the input came from and where to send the intermediate result). The current participant \APri{P_i} can decrypt the first element that says the it should expect the input value from participant \APri{P_{i-1}} and it should forwards the intermediate result of its calculation to participant \APri{P_{i+1}}. Each such element is signed by the coordinator and encrypted with the public key of the participant that should be able to read this information. We can now write the protocol used for the calculation of the mean value \AVal{M} using the {\Aspen} notation (we ignore the signature verification steps at each participant): \begin{ltxex}{smc-mean}{SMC: Calculate the mean value} \begin{ASteps}\setcounter{counterS}{-1}% \AStepat*{C}{$\AVal{V'_0} = \ARandom'{0}$; \BANFresh{\AVal{V'_0}}}\\ \ASend[Big]{C}{P_1}{% \AEncrypted+[big]{P_1}{\ASigned-{C}{\AVal{V'_0}}}, \AEncrypted+[big]{P_1}{\ASigned-{C}{\APri{C},\APri{P_2}}}, \AEncrypted+[big]{P_2}{\ASigned-{C}{\APri{P_1},\APri{P_3}}}, \AEncrypted+[big]{P_3}{\ASigned-{C}{\APri{P_2},\APri{C}}}} \\ \AStepat*{P_1}{$\AVal{V'_1} = \AVal{V'_0} + \AVal{V_1}$} \\ \ASend[Big]{P_1}{P_2}{% \AEncrypted+[big]{P_2}{\ASigned-{P_1}{\AVal{V'_1}}}, \AEncrypted+[big]{P_2}{\ASigned-{C}{\APri{P_1},\APri{P_3}}}, \AEncrypted+[big]{P_3}{\ASigned-{C}{\APri{P_2},\APri{C}}}} \\ \AStepat*{P_2}{$\AVal{V'_2} = \AVal{V'_1} + \AVal{V_2}$} \\ \ASend[Big]{P_2}{P_3}{% \AEncrypted+[big]{P_3}{\ASigned-{P_2}{\AVal{V'_2}}}, \AEncrypted+[big]{P_3}{\ASigned-{C}{\APri{P_2},\APri{C}}}} \\ \AStepat*{P_3}{$\AVal{V'_3} = \AVal{V'_2} + \AVal{V_3}$} \\ \ASend[Big]{P_3}{C}{% \AEncrypted+[big]{C}{\ASigned-{P_3}{\AVal{V'_3}}}} \\ \AStepat*{C}{$\AVal{M} = (\AVal{V'_3}-\AVal{V'_0}) / \AVal{3}$} \end{ASteps} \end{ltxex} \begin{figure} \hspace*{\fill} \begin{mplibcode} p1:=(width,0); p2:=(0,height); p3:=(-width,0); p4:=(width,-height); p5:=(width,height); p6:=(-width,height); p7:=(-width,-height); c:=(0,-height); draw object(p1, orad); label(btex \APri{P_1} etex, p1); label.rt(btex \ALabel{S_1} etex, p1+(1.2orad,0)); draw object(p2, orad); label(btex \APri{P_2} etex, p2); label.top(btex \ALabel{S_2} etex, p2+(0,1.2orad)); draw object(p3, orad); label(btex \APri{P_3} etex, p3); label.lft(btex \ALabel{S_3} etex, p3+(-1.2orad,0)); draw object(c, orad); draw object(c, orad-2pt); label(btex \APri{C} etex, c); label.bot(btex \ALabel{S_0}, \ALabel{S_4} etex, c+(0,-1.2orad)); draw ddirarrow(c, 0, 90, p1, orad); label.lrt(btex \ALabel{M_1} etex, c+(0.5width,0)); draw ddirarrow(p1, 90, 180, p2, orad); label.urt(btex \ALabel{M_2} etex, p2+(0.5width,0)); draw ddirarrow(p2, 180, 270, p3, orad); label.ulft(btex \ALabel{M_3} etex, p2+(-0.5width,0)); draw ddirarrow(p3, 270, 0, c, orad); label.llft(btex \ALabel{M_4} etex, c+(-0.5width,0)); \end{mplibcode} \hspace*{\fill} \caption{SMC: Calculate the mean value}\label{fig:smc-mean} \end{figure} Figure \ref{fig:smc-mean} illustrates the participants and each step and message of the calculation. See \refltxcode{smc-mean} for the {\latex} code. \tol{csi-fs}{File sharing with symmetric and public key encryption} Cloud Security Infrastructure (CSI)~\cite{andersen2014c} is a scalable cloud storage architecture with focus on privacy. In \cite{andersen2014c}, a figure (Figure~3) illustrates how a user can share a file with another user using a combination of symmetric (secret) key and public key encryption. In Figure~\ref{fig:csi-fs} and in the protocol shown below, the intent of original figure in ~\cite{andersen2014c}is recreated using {\Aspen}. In the steps below, \APri{A} uploads two files \AVal{F_1} and \AVal{F_2} to a server, where file \AVal{F_1} is shared with \APri{B}: \begin{figure} \hspace*{\fill} \begin{mplibcode} d:=(0,0); p1:=(-1.3width,0); p2:=(1.3width,0); draw object(d, orad); draw object(d, orad-2pt); label(btex \APri{S} etex, d); label.bot(btex \boxed{%\small \begin{array}{@{\:}c@{\:}} \ACert!_{X509}{CA}{A} \\ \ACert!_{X509}{CA}{B} \\ \ASval[big]{\AEncrypted+{A}{\AKey{F_1}}, \AEncrypted+{B}{\AKey{F_1}}, \AEncrypted{F_1}{F_1}} \\ \ASval[big]{\AEncrypted+{A}{\AKey{F_2}}, \AEncrypted{F_2}{F_2}} \end{array}} etex, d+(0,-2.3orad)); draw object(p1, orad); label(btex $A$ etex, p1); label.lft(btex \boxed{%\small \begin{array}{@{\:}c@{\:}} \AEncrypted"_{PCKS\#12}{P_A}{\AKey-{A}} \\ \ACert!_{X.509}{CA}{A} \\ \ACert!_{X.509}{CA}{B} \\ \AVal{F_1} \\ \AVal{F_2} \end{array}} etex, p1+(-1.2orad,0)); draw ddirarrow(p1, 0+v, 0-v, d, orad); label.top(btex \ALabel{M_1} etex, (d+p1)/2+(0,1.1orad)); draw ddirarrow(p1, 0-v, 0+v, d, orad); label.bot(btex \ALabel{M_2} etex, (d+p1)/2+(0,-1.2orad)); draw object(p2, orad); label(btex \APri{B} etex, p2); label.rt(btex \boxed{%\small \begin{array}{@{\:}c@{\:}} \AEncrypted"_{PCKS\#12}{P_B}{\AKey-{B}} \\ \ACert!_{X.509}{CA}{B} \\ \ACert!_{X.509}{CA}{A} \\ \AVal{F_1} \end{array}} etex, p2+(1.2orad,0)); draw ddirarrow(d, 0, 0, p2, orad); label.top(btex \ALabel{M_3} etex, (d+p2)/2+(0,0.1orad)); \end{mplibcode} \hspace*{\fill} \caption{File sharing with symmetric and public key encryption} \label{fig:csi-fs} \end{figure} \begin{ltxex}{csi-fs}{File sharing with symmetric and public key encryption} \begin{ASteps} \AStepat*{A}{\BANFresh{\AKey{F_1}}; \BANFresh{\AKey{F_2}}} \\ \AStepat*{A}{% \AEncrypt{F_1}{F_1}[*]; \AEncrypt{F_2}{F_2}[*]} \\ \AStepat*{A}{% \AEncrypt+{A}{\AKey{F_1}}[*]; \AEncrypt+{B}{\AKey{F_1}}[*]} \\ \AStepat*{A}{\AEncrypt+{A}{\AKey{F_2}}[*]} \\ \ASend[big]{A}{S}{\AEncrypted+{A}{\AKey{F_1}}, \AEncrypted+{B}{\AKey{F_1}}, \AEncrypted{F_1}{F_1}} \\ \ASend[big]{A}{S}{\AEncrypted+{A}{\AKey{F_2}}, \AEncrypted{F_2}{F_2}} \\ \ASend[big]{S}{B}{\AEncrypted+{A}{\AKey{F_1}}, \AEncrypted+{B}{\AKey{F_1}}, \AEncrypted{F_1}{F_1}} \\ \AStepat*{B}{% \ADecrypt"{P_B}{\AEncrypted"{P_B}{\AKey-{B}}}[\AKey-{B}]; \ADecrypt-{B}{\AEncrypted+{B}{\AKey{F_1}}}[\AKey{F_1}]} \\ \AStepat*{B}{\ADecrypt{F_1}{\AEncrypted{F_1}{F_1}}[\AVal{F_1}]} \end{ASteps} \end{ltxex} In Figure~\ref{fig:csi-fs}, the boxes illustrate what is stored at each principal (data at-rest) and the arrows illustrate the messages sent between the principals (data in-transit). Each messages in the figure is labeled with the same labels used in the steps shown above. \tol{csi-ssfs}{Scalable secure file sharing} The Cloud Security Infrastructure (CSI)~\cite{andersen2014c} has come up with the concept of a \emph{store} and a \emph{share} to achieve scalable secure file sharing. Every principal has a store that is represented by a public and private key pair (\AKey+{S_A} and \AKey-{S_A} for \APri{A} in the example below). When a file is shared, a new store called a share is created. In the example below a share represented by the public and private key pair \AKey+{S_{A,B}} and \AKey-{S_{A,B}} is used to share file \AVal{F_1} between \APri{A} and \APri{B}. Each store (and share) also has a symmetric random encryption key associated with them (\AKey{S_A} and \AKey{S_{A,B}} in the example) used to encrypt the private keys of the stores: \begin{figure} \hspace*{\fill} \begin{mplibcode} d:=(0,0); p1:=(-1.3width,0); p2:=(1.3width,0); draw object(d, orad); draw object(d, orad-2pt); label(btex \APri{S} etex, d); label.bot(btex \boxed{%\small \begin{array}{@{\:}c@{\:}} \ACert!_{X509}{CA}{A} \\ \ACert!_{X509}{CA}{B} \\ \AKey+{S_A}, \AEncrypted{S_A}{\AKey-{S_A}} \\ \AEncrypted+{A}{\AKey{S_A}} \\ \AKey+{S_{A,B}}, \AEncrypted{S_{A,B}}{\AKey-{S_{A,B}}} \\ \AEncrypted+{A}{\AKey{S_{A,B}}}, \AEncrypted+{B}{\AKey{S_{A,B}}} \\ \ASval[big]{\AEncrypted+{S_{A,B}}{\AKey{F_1}}, \AEncrypted+{B}{\AKey{F_1}}, \AEncrypted{F_1}{F_1}} \\ \ASval[big]{\AEncrypted+{S_A}{\AKey{F_2}}, \AEncrypted{F_2}{F_2}} \end{array}} etex, d+(0,-2.3orad)); draw object(p1, orad); label(btex $A$ etex, p1); label.lft(btex \boxed{%\small \begin{array}{@{\:}c@{\:}} \AEncrypted"_{PCKS\#12}{P_A}{\AKey-{A}} \\ \ACert!_{X.509}{CA}{A} \\ \ACert!_{X.509}{CA}{B} \\ \AKey+{S_A}, \AEncrypted{S_A}{\AKey-{S_A}} \\ \AEncrypted+{A}{\AKey{S_A}} \\ \AKey+{S_{A,B}}, \AEncrypted{S_{A,B}}{\AKey-{S_{A,B}}} \\ \AEncrypted+{A}{\AKey{S_{A,B}}} \\ \AVal{F_1} \\ \AVal{F_2} \end{array}} etex, p1+(-1.2orad,0)); draw ddirarrow(p1, 0+v, 0-v, d, orad); label.top(btex $\ALabel{M_1},\ALabel{M_2}$ etex, (d+p1)/2+(0,1.1orad)); draw ddirarrow(p1, 0-v, 0+v, d, orad); label.bot(btex $\ALabel{M_3},\ALabel{M_4}$ etex, (d+p1)/2+(0,-1.2orad)); draw object(p2, orad); label(btex \APri{B} etex, p2); label.rt(btex \boxed{%\small \begin{array}{@{\:}c@{\:}} \AEncrypted"_{PCKS\#12}{P_B}{\AKey-{B}} \\ \ACert!_{X.509}{CA}{B} \\ \ACert!_{X.509}{CA}{A} \\ \AKey+{S_{A,B}}, \AEncrypted{S_{A,B}}{\AKey-{S_{A,B}}} \\ \AEncrypted+{B}{\AKey{S_{A,B}}} \\ \AVal{F_1} \end{array}} etex, p2+(1.2orad,0)); draw ddirarrow(d, 0+v, 0-v, p2, orad); label.top(btex \ALabel{M_5} etex, (d+p2)/2+(0,1.1orad)); draw ddirarrow(d, 0-v, 0+v, p2, orad); label.bot(btex \ALabel{M_6} etex, (d+p2)/2+(0,-1.2orad)); \end{mplibcode} \hspace*{\fill} \caption{Scalable secure file sharing} \label{fig:csi-ssfs} \end{figure} \begin{ltxex}{csi-ssfs}{Scalable secure file sharing} \begin{ASteps} \AStepat*{A}{% \BANFresh{\AKey{F_1}}; \BANFresh{\AKey{F_2}}; \BANFresh{\AKey{S_A}}; \BANFresh{\AKey{S_{A,B}}}; \BANFresh{\AKey-{S_A}}; \BANFresh{\AKey+{S_A}}; \BANFresh{\AKey-{S_{A,B}}}; \BANFresh{\AKey+{S_{A,B}}}} \\ \AStepat*{A}{% \AEncrypt{F_1}{F_1}[*]; \AEncrypt{F_2}{F_2}[*]} \\ \AStepat*{A}{% \AEncrypt+{S_{A,B}}{\AKey{F_1}}[*]; \AEncrypt+{S_A}{\AKey{F_2}}[*]} \\ \AStepat*{A}{% \AEncrypt{S_A}{\AKey-{S_A}}[*]; \AEncrypt{S_{A,B}}{\AKey-{S_{A,B}}}[*]} \\ \AStepat*{A}{% \AEncrypt+{A}{\AKey{S_A}}[*]} \\ \AStepat*{A}{% \AEncrypt+{A}{\AKey{S_{A,B}}}[*]; \AEncrypt+{B}{\AKey{S_{A,B}}}[*]} \\ \ASend[big]{A}{S}{% \AEncrypted+{A}{\AKey{S_A}}, \AEncrypted+{A}{\AKey{S_{A,B}}}, \AEncrypted+{B}{\AKey{S_{A,B}}}} \\ \ASend[big]{A}{S}{% \AEncrypted{S_A}{\AKey-{S_A}}, \AEncrypted{S_{A,B}}{\AKey-{S_{A,B}}}} \\ \ASend[big]{A}{S}{% \AEncrypted+{S_{A,B}}{\AKey{F_1}}, \AEncrypted{F_1}{F_1}} \\ \ASend[big]{A}{S}{\AEncrypted+{S_A}{\AKey{F_2}}, \AEncrypted{F_2}{F_2}} \\ \ASend[big]{S}{B}{\AEncrypted+{B}{\AKey{S_{A,B}}}, \AEncrypted{S_{A,B}}{\AKey-{S_{A,B}}}} \\ \ASend[big]{S}{B}{% \AEncrypted+{S_{A,B}}{\AKey{F_1}}, \AEncrypted{F_1}{F_1}} \\ \AStepat*{B}{% \ADecrypt"{P_B}{\AEncrypted"{P_B}{\AKey-{B}}}[\AKey-{B}]; \ADecrypt-{B}{\AEncrypted+{B}{\AKey{S_{A,B}}}}[\AKey{S_{A,B}}]} \\ \AStepat*{B}{% \ADecrypt{S_{A,B}}{\AEncrypted{S_{A,B}}{\AKey-{S_{A,B}}}}[\AKey-{S_{A,B}}]; \ADecrypt-{S_{A,B}}{\AEncrypted+{S_{A,B}}{\AKey{F_1}}}[\AKey{F_1}]} \\ \AStepat*{B}{\ADecrypt{F_1}{\AEncrypted{F_1}{F_1}}[\AVal{F_1}]} \end{ASteps} \end{ltxex} In Figure~\ref{fig:csi-ssfs} presenting the example, the boxes illustrate what is stored at each principal (data at-rest) and the arrows illustrate the messages sent between the principals (data in-transit). Each messages in the figure is labeled with the same labels used in the steps shown above. Figure~\ref{fig:csi-ssfs} is a recreation of a figure in \cite{andersen2014c} (Figure~4) illustrating the same example as the one above. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \appendix \clearpage \bibliographystyle{splncs04x} \bibliography{aspen-doc} \clearpage \section{Notes} \subsection{Notes on the 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 notation is found useful for others, it is a nice bonus. The notation is also influenced by my background as a programmer and not a mathematician or a theoretical computer scientist. 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 notation. \href{mailto:aspen@pg12.org?subject=Feedback Aspen}{Feedback} on the notation are welcome. 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 & \AKey{A} & \AKey*{K_A} & \AKey*{k_A} & \AKey*{K} & \AKey*{K_A} & C \\ Shared key & \AKey{A,B} & $-$ & \AKey*{k_{A\;B}} & $-$ & $-$ & C \\ Session key & \AKey'{A,B} & \AKey*{K_{A,\averythinspace B}} & $-$ & $-$ & $-$ & B \\ Public key & \AKey+{A} & $-$ & \AKey*{\textrm{pub}(k_A)} & \AKey*{KR} & \AKey*{+K_A} & A \\ Private key & \AKey-{A} & $-$ & \AKey*{\textrm{priv}(k_A)} & \AKey*{KR^{-1}} & \AKey*{-K_A} & A \\ Encrypted & \AEncrypted*{\AKey*{K}}{m} & $\AMsg{m}\AKey*{K}$ & $\AMsg{m}_{\AKey*{K}}$ & $\AMsg{m}_{\AKey*{K}}$ & $\AMsg{m}_{\AKey*{K}}$ & C \\ Signed with & \ASigned*{\AKey*{K}}{m} & $-$ & $-$ & \AVal{\textrm{sig}_{\AKey*{K}}\{m\}} & $-$ & A \\ Signed by & \ASigned!{A}{m} & $-$ & $-$ & $-$ & \AVal{\APri{A}\,[m]} & A \\ Send & \ACsend{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}\!\AUnpack\!\APri{B}\!:\!\AVal{m}$ & $\APri{A}\!\ACsends\!\APri{B}\!:\!\AVal{m}$ & $\APri{A}\!\ACsends\!\APri{B}\!:\!\AVal{m}$ & B \\ Hash value & \AChash{m} & $-$ & \AVal{\textrm{H}(m)} & \AVal{\textit{h}(m)} & \AVal{\textit{H}(m)} & B \\ MAC & \AMac*{\AKey*{K}}{m} & $-$ & $-$ & \AVal{\textrm{MAC}_{\AKey*{K}}(m)} & $-$ & B \\ HMAC & \AHmac*{\AKey*{K}}{m} & $-$ & $-$ & \AVal{\textrm{HMAC}_{\AKey*{K}}(m)} & $-$ & B \\ Signature & \ASig*{\AKey*{K}}{m} & $-$ & $-$ & $-$ & $-$ & A \\ Certificate & \ACertificate-{CA}{\APri{A},\AKey+{A}} & $-$ & $-$ & \AVal{\textit{Cert}_{\AKey*{KC^{-1}}}\!(A,\AKey*{KR})} & \AVal{\textit{Cert}_{\AKey*{-K_{CA}}}\!(\AKey*{+K_A})} & B \\ Certificate by & \ACertificate!{CA}{\APri{A},\AKey+{A}} & $-$ & $-$ & $-$ & \AVal{\APri{CA}\,\langle\langle\,\APri{A}\,\rangle\rangle} & A \\\Xhline{0.5pt} \end{xltabular}}\vspace*{-.5\baselineskip} 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} % 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. \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{\@Val{1}}, \PY@tc{\@True}} \\ Principle & \texttt{\small na} & {\csname #1@PY@tok@na\endcsname \PY@tc{\@Pri{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{\@Nonce{N_1}}} \\ Timestamp & \texttt{\small nt} & {\csname #1@PY@tok@nt\endcsname \PY@tc{\@TS{T_s}}} \\ String & \texttt{\small sc} & {\csname #1@PY@tok@sc\endcsname \PY@tc{\@Str{Hello}}} \\ Variable & \texttt{\small nv} & {\csname #1@PY@tok@nv\endcsname \PY@tc{\@Var{x}}, \PY@tc{\@Var{y}}, \PY@tc{\@Var{z}}} \\ Function & \texttt{\small nf} & {\csname #1@PY@tok@nf\endcsname \PY@tc{\@Function{H(\@Val{m})}}} \\ Code & \texttt{\small go} & {\csname #1@PY@tok@gp\endcsname \PY@tc{\@Cmd{\textbackslash AKey\{A\}}}} \\ Label & \texttt{\small nl} & {\csname #1@PY@tok@nl\endcsname \PY@tc{\@Label{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 \AKey+{A} and \AKey-{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} \clearpage \subsection{Notation example listing} \label{sec:ex-code} In this Section, all notation examples with their {\latex} code is listed without comments and any explanation. \immediate\closeout\locfile \IfFileExists{\jobname.loc}{\input{\jobname.loc}}{} \end{document}