Definition

Communication protocol

rules for data transmission in a network. i.e. HTTP

Cryptographic protocol

communication protocol for encrypted messages.

used in: e-banking, e-commerce, file sharing, online messengers

Cryptography is not enough: the attacker can circumvent cryptography and break the protocol.

Possible flaws can be in the:

Automated Protocol Analysis

Protocols are complicated and attacks are difficult to find. We need Automatation, formal proofs.

Requirements:

Attacks

Interleaving Attack

Message from one protocol-session is used in other ones.

Reflection Attack

(Subtype of Interleaving attack)

Message sent back to the person that generated it (in a different session).

Problem: (If we are using symmetric encryption) the sender can not verify who sent the message.

Solution: Identifier (sender / receivers name)

$A -\{\textcolor{pink}A,\text{Give } E \text{ 1000€}\}_k \rarr B$

Replay Attack

(Subtype of Interleaving attack)

Duplicate of message re-sent at a different time.

Problem: we cant verify the freshness of the received message.

Solution 1: timestamp$t$(issues with time zones, synchronization)

$A -\{A,\text{Give } E \text{ 1000€},\textcolor{pink}t\}_k \rarr B$

Solution 2: nonce$n$

$A \longleftarrow \textcolor{pink}{n_B} -B$ Challenge / Request

$A -\{A,\text{Give } E \text{ 1000€},\textcolor{pink}{n_B}\}_k \rarr B$ Response

Man-in-the-middle Attack

Needham-Shroeder Protocol

Uses nonces $n$ , Asymmetric encryption to exchange symmetric keys.

Because public keys / nonces are for specific sessions, we don't need identifiers (except for the first message or else someone could respond faster than$B$using$pk_A$from that session).

$A \larr \{B, n_B\}_{pk_A} - B$

$A - \{n_B, n_A\}_{pk_B} \rarr B$

$A \larr \{n_A\}_{pk_A} - B$

Man-in-the-middle Attack

The victim $B$ then thinks he is communicating with $\bigcirc$ but he is actually communicating with $A$ .

The attacker has access to $n_A,n_B$ and can decrypt all messages from $B$ .

$A \larr \{B, n_B\}_{pk_A} - \bigcirc \larr \{B, n_B\}_{pk_\bigcirc} - B$Attacker reads Bobs messages, has his$n_B$.

$A - \{n_B, n_A\}_{pk_B}\rarr B$

$A \larr \{n_A\}_{pk_A} - \bigcirc \larr \{n_A\}_{pk_\bigcirc} - B$Attacker gets$n_A$from Bob.

Solution: Needham-Schroeder-Lowe Protocol

$A \larr \{B, n_B\}_{pk_A} - B$

$A - \{\textcolor{pink}A,n_B, n_A\}_{pk_B} \rarr B$(new identifier!)

$A \larr \{n_A\}_{pk_A} - B$

Then the attack is not possible because bob does not think he is talking to $\bigcirc$ anymore.

Applied Pi-Calculus

Highly abstracted mathematical descriptions for concurrent computation.

Very simple, only based on functions, no side-effects, only focused on communication.

Considers cryptography as flawless.

Example: Digital Signature

We want to model $A$ using a digital signature that can be verified with a $pk$ .

We can express the entire digital signature encryption as

$\operatorname{ver}(\operatorname{sign}(x, s k(k)), v k(k)) \rarr x$

Below we used$k_A$for$k$.

And model the process the following way

$System \triangleq\text{new }k_A. (Init \mid Resp)$

$Init\triangleq \text {new } n_B. \operatorname{out}(c, n_B) . \operatorname{in}(c, x).\text{let} (=B,=n_B, z)=\text{ver}(x, \text{vk}(k_{A})) \text { in } P$

$Resp \triangleq \text{in}(c,x).\text{new }n_A. \operatorname{out}(c, \textcolor{pink}{\text{sign}((B, x, n_A), \text{sk}(k_{A}))})$

• In depth explaination

  $System \triangleq$

  $\text{new }k_A.$create new$k_A$and then

  $(Init \mid Resp)$run$Init$and$Resp$concurrently.

  $Resp \triangleq$

  $\text{in}(c,x).$receive ($n_B$) on channel$c$, bind result to$x$then

  $\text{new }n_A.$create new$n_B$then

  $\operatorname{out}(c, ~\textcolor{pink}{\text{sign}((B, x, n_A), \text{sk}(k_{A}))}~) = \operatorname{out}(c, ~\textcolor{pink}{(B_{sk_A}, x_{sk_A}, {n_A}_{sk_A})}~)$

  Send value of$\text{sign}((B, x, n_A), \text{sk}(k_{A}))$to channel$c$.

  Where$\text{sign}((B, x, n_A), \text{sk}(k_{A})) = \text{sign}((B, x, n_A), sk_A)$

  $Init\triangleq$

  $\text {new } n_B.$create new$n_B$then

  $\operatorname{out}(c, n_B) .$send value of$n_B$to channel$c$then

  $\operatorname{in}(c, x).$receive on channel$c$, bind result to$x$in process$P$.

  $\text{let} \bigg((=B,=n_B, z)=\text{ver}(x, \text{vk}(k_{A})) \bigg)\text { in } P$

  Only if$x$(see above) could be verified, pattern match

  the received decrypted triplet with$(B, n_B, \dots)$, bind$n_A$to$z$.

Example: Pairs

We have the following process:

$\text{new }s.(\text { out}(a, \operatorname{pair}(M, s)) \mid \operatorname{in}(a, x) \text {.if } \operatorname{snd}(x)=s \text { then out}(b, \operatorname{fst}(x)))$

We have an attacker:

$\operatorname{in}(a, x) . \text { out}(a, \operatorname{pair}(N, \operatorname{snd}(x)))$

Question: Can our process output anything different than $M$ with / without the attacker?

Answer: Without the attacker only $M$ is put out , but with the attacker also$N$.

Example: Hashes

$h(M)$ hashes data and outputs a bit string.

We have a modified hash function:

$\text { new } s .\left(\begin{array}{l}\text {out}(a, \operatorname{pair}(M, h(\operatorname{pair}(s, M)))) \mid \\\operatorname{in}(a, x) . \text { if } h(\operatorname{pair}(s, \operatorname{fst}(x)))=\operatorname{snd}(x) \text { then out }(b, \operatorname{fst}(x))\end{array}\right)$

Question: Is this function secure?

Answer: Yes - $s$ is kept a secret and the attacker can not forge $h(pair(s,N))$

Basic Security Goals

There are many more properties, but we only focus on these.

Secrecy

Only authorized end-points should be able to read messages.

Secrecy is undecidable - infinite number of opponents $O$ . (automatized proofs with tools possible).

Protocol $P$ preserves secercy of $M \Lrarr$

Integrity

The recipient of a message should be able to determine changes during transmission.

Sender and receiver should agree on their roles.

Authenticity

For authentication we have to introduce a new process:

We use these events to log authentication / acceptance of requests :

• Example

  $A \longleftarrow n_B \text{ -----} B$

  $A \text{ --- } \{B, n_B, n_A\}_{sk_A}\rarr B$

  where$sk_A := sk(k_A)$

  ---

  $System \triangleq$

  $\text{new }k_A.$

  $(Init \mid Resp)$

  $Resp \triangleq$

  $\text{in}(c,x).$

  $\text{new }n_B.$

  $\textcolor{pink}{\text{event} ~ {begin}(A, B, M)}$

  $\operatorname{out}(c, ~{\text{sign}((B, x, n_A), \text{sk}(k_{A}))}~)$

  $Init\triangleq$

  $\text {new } n_B.$

  $\operatorname{out}(c, n_B) .$

  $\operatorname{in}(c, x).$

  $\text{let} \bigg((=B,=n_B, z)=\text{ver}(x, \text{vk}(k_{A})) \bigg)\text { in } P$

  $\textcolor{pink}{\text{event} ~ { end }(A, B, M)}$

Non-Injective Agreement

• Identity: The recipient should be able to verify the requesters identity.

• Order: In all execution traces, if we reach the $end$ we must have also reached a $begin$ .

Formally

$P$ guarantees noninjective agreement iff:

• In depth explaination

  $P$is the process we want to analyse that runs parallel to any opponent$O$.

  $Q$is the process left after$P$and$Q'$is the process left after$Q$.

  $\rarr^*$stands for n-step reductions.

  $\widetilde a$stands for a sequence of variables that are bounded in the following process.

  This is a recursive definition:

  It means that in our closed process $P$ for any opponent $O$ that we run in parallel, after n-reductions and binding arbitrary many variables to our process (which we simply refer to as $\widetilde a$ - we must always reach two processes running in parallel from which both fulfill the non-injective agreement.

  Because these processes can run concurrently we can have any arbitrary ordering as long as an end event always follows after a begin event.

  Therefore these orderings would both be valid although the required end event does not follow immediately after the begin event:

  Begin1 $\rightarrow$ Begin2 $\rightarrow$ End1 $\rightarrow$ End2

  Begin1 $\rightarrow$ Begin2 $\rightarrow$ End2 $\rightarrow$ End1

Injective Agreement

• Freshness: same as above but recipient should be able to verify the freshness of the authentication request.

Formally

$P$ guarantees noninjective agreement iff:

Challenge-Response Nonce Handshakes

Handshake Implementations: (Challenge/Request - Response)

• Plain-Cipher PC

• Cipher-Plain CP

• Cipher-Cipher CC

Reminder: we place loggers before and after each authentication / acceptance of requests.

When a direction is mentioned in which an injective agreement is given that means that the freshness of the received nonce can be verified by the receiver.

PC Handshake

Symmetric version

Asymmetric version

Identifier was changed - else the message could be sent to anyone.

CP Handshake

The second message is an acknowledgement.

There are 2 authentications happening.

Symmetric version

Asymmetric version

Here the request is encrypted with $pk_A$ - Then the identifier must be changed to $B$ .

The request might come from an attacker.

CC Handshake

Symmetric version

The first agreement property ( $A \larr B$ ) only holds if the endpoints can not swap roles (we must add tags for the messages).

We can not change the identifiers in the messages since it would make the protocol vulnerable to a reflection attack.

Asymmetric version

Combination of Handshakes

All the other protocols are only made out of the ones mentioned above.

Example: Mutual Authentication

Combination of PC and CC handshake.

We can not remove the identifier $B$ or else a reflection attack would be possible.

Example: SAML-based single sign-on

Protocol to allow client $C$ to authenticate with a service provider $SP$ via an identity provider $IdP$ .

The client wants to request some resource from the service provider. (Instagram in example.)

The Service provider then allows the client to log in with a third party. (Google in example.)

Using automated techniques, people found an attack:

The $IdP$ then (if this protocol would ever be used) have access to the clients $C$ google account data (Gmail, google calendar, ...).

ProVerif

Cryptographic protocol verifier based on Horn clause resolution.

Input notation: applied pi-calculus.

Outcomes

Possible outcomes after modelling a protocol:

Translation

Is what ProVerif does:

The horn clauses are then sent to a theorem prover.

The translations are sound (= error free) but incomplete:

Horn Clauses

Are a special type of logical formulas.

For all $x$ (all the messages):

$(\forall \tilde{x})\left(p_{1}(\widetilde M_{1}) \wedge \ldots \wedge p_{n}(\widetilde{M}_{n}) \Rightarrow q(\widetilde{N})\right)$

Resolution provers take a set of Horn clauses and a specified goal: $\exists \tilde x.p(\widetilde M)$

Translation: Applied Pi-Calculus → Logic Formulas

Translating the predicates from the pi-calculus into logical formulas.

Facts (a type of horn clause)

We only have 2 predicates.

$F::=$

Input

$P \dots$ process

$S \dots$ free public names in $P$

Output

set of Horn-Clauses:

$B(P,S) =$

Initial Attacker Knowlege

All free public names in $P$ that the attacker knows.

$\text{InitialAttackerKnowledge}(S) = \{attacker(n) \mid n \in S\}$

Attacker Rules

We model all the constructors and destructors in terms of the attackers knowledge.

$\text{AttackerRules} =$

For each constructor$f$

For each destructor$g$with$g(M_1,...,M_n)=M$

For each Input and output

Protocol Rules

$\text{ProtocolRules}(P) =$

Each output $out(c,N)$ generates a Horn-Clause with the form:

Examples of protocol rules

Example 1:

Example 2: