+ +

Trust Engineering

via

Cryptographic Protocols

Joshua D. Guttman

Jonathan C. Herzog Jonathan K. Millen John D. Ramsdell Brian T. Sniffen F. Javier Thayer

Supported by: MITRE-Sponsored Research + +

Trust Engineering

• Security in distributed systems must handle:

– Many people, organizations, machines
– Essentially different goals and policies

• Pervasive issues:

– What principal is making a request?
– If I respond, what action must I take?
– What policy do I use to decide?

• Trust engineering goal:

control global sequences of events via local decisions

– My decisions suffice to prevent harm to me,

even from actions taken elsewhere

– I can appraise source, reliability of information from others
– I can predict who might receive information I transmit

+ +

Trust in Purchasing

Electronic Purchase using a Money Order

B  C  M
γ_{c,1} goods available, for price?  \overline{▶} •
•^{‖}\underline{◀}  γ_{m,2} I will ship C goods, if paid price^{‖}
•\underline{◀}  •^{‖}
γ_{b,2} I will pay price from acc# to the bearer P, if P authorized by C^{‖}  \overline{▶} •^{‖}
γ_{c,5}

I authorize payment from acc# to M

‖ ▶ • ‖

• ‖ ◀ γ_{m,4}

I request payment and I will ship C goods

‖
B = bank  C = customer  M = merchant

+ +

EPMO Goals

• At the end of a run, C, M, B agree on identities and price

– B to transfer price from C’s acct to M’s

• C, M agree on goods

– At the end of a run, M to ship goods to C

• Protocol preserves confidentiality:

– M never learns C’s account number
– B never learns goods
– Other parties never learn C, M, B, price, goods
– B learns M’s identity only if C decides to complete transaction

Types of goal:

– Authentication of identities
– Agreement on other parameters
– Confidentiality
– Agreement on commitments
+ 2013.3.7 BiSS, Mar 2013  4

+ +

Commitments in Purchasing

Electronic Purchase using a Money Order

B  C  M
γ_{c,1} goods available, for price?  \overline{▶} •
M says γ_{m,2}  ρ_{c,2}^{‖} \underline{◀}  γ_{m,2} I will ship C goods, if paid price^{‖}
•\underline{◀}  •^{‖}
γ_{b,2} I will pay price from acc# to the bearer P, if P authorized by C^{‖}  \overline{▶} •^{‖}
γ_{c,5}

I authorize payment from acc# to M

‖

▶

ρ_{m,3} B says B will pay if authorized and C says C authorizes payment

‖

ρ_{b,3}

C says C authorizes payment from acc# to M and M says M requests

payment

‖ ◀ γ_{m,4}

I request payment and will ship C goods

‖

+ +

Trust Engineering

• Trust engineering goal:

control global sequences of events via local decisions

– My decisions suffice to prevent harm to me,

even from actions taken elsewhere

– I can appraise source, reliability of information from others
– I can predict who might receive information I transmit

• How to design new, application-specific protocols

– Craft transactions in

∘ Electronic commerce, web services, remote attestation

– “Trust engineering:” Protocol to match trust goals of participants

• Goals of this talk: Explain

– When is a protocol strong enough for its trust goals?
– CPPL, a domain specific programming language for trust eng.

+ +

EPMO Protocol Structure, 1

B  C  M

γ_{c,1} goods available, for price?

{C, N_{c}, goods, price}_{M} ▶
•
M says γ_{m,2}  ρ_{c,2}^{‖} ◀ {N_{c}, N_{m}, M}_{C}  γ_{m,2} I will ship C goods, if paid price^{‖}
•\underline{◀}  •^{‖}
γ_{b,2} I will pay price from acc# to the bearer P, if P authorized by C^{‖}  \overline{▶} •^{‖}

γ_{c,5}

I authorize payment from acc# to M

‖

… N_{m} … ▶

ρ_{m,3} B says B will pay if authorized and C says C authorizes payment

‖

ρ_{b,3}

C says C authorizes payment from acc# to M and M says M requests

payment

‖ ◀ γ_{m,4}

I request payment and will ship C goods

‖

+ +

EPMO Protocol Structure, 2

B  C  M

γ_{c,1} goods available, for price?

{C, N_{c}, goods, price}_{M} ▶
•
M says γ_{m,2}  ρ_{c,2}^{‖} ◀ {N_{c}, N_{m}, M}_{C}  γ_{m,2} I will ship C goods, if paid price^{‖}
•\underline{◀}  •^{‖}
γ_{b,2} I will pay price from acc# to the bearer P, if P authorized by C^{‖}  \overline{mo, \{N_{c}, N_{b}\}_{C}  ▶} •^{‖}

γ_{c,5}

I authorize payment from acc# to M

‖

mo, N_{b} ▶

ρ_{m,3} B says B will pay if authorized and C says C authorizes payment

‖

ρ_{b,3}

C says C authorizes payment from acc# to M and M says M requests

payment

‖ ◀ hash(M, B, N_{b}, N_{m}) γ_{m,4}

I request payment and will ship C goods

‖
mo = [[ hash(C, N_{c}, N_{b}, N_{m}, price) ]]_{B}

+ +

EPMO Weakened

B  C  M

• {C, N_{c}, goods, price}_{M} ▶ •

ρ_{c,2}  M says γ_{m,2}^{‖} ◀ {N_{c}, N_{m}, M}_{C}  γ_{m,2} I will ship C goods, if paid^{‖}
•◀{C, N_{c}, N_{m}, acc# , price}_{B} •^{‖}

γ_{b,2}

I will pay price to the bearer P,

if P authorized by C

‖ mo, {N_{c}, N_{b}}_{C} ▶ • ‖

γ_{c,5}  I authorize payment to M^{‖}  \overline{mo, N_{b}  ▶} ρ_{m,3} B says γ_{b,2} and C authorizes payment to M^{‖}
ρ_{b,3} C says C authorizes payment to M and M says M requests payment^{‖} ◀  hash(M, B, N_{b}, N_{m}) I request payment and will ship C goods γ_{m,4}^{‖}

mo = [[ hash(C, N_{c}, N_{b}, N_{m}, price) ]]_{B}

+ +

Lowe-style attack

B  C  M′  M

• {C, N_{c}, goods, price}_{M′} ▶ •

•^{‖}◀  {N_{c}, N_{m}}_{C}  • I will ship C goods, if paid^{‖}
•◀{C, N_{c}, N_{m}, price}_{B} •^{‖}

•

I will pay price to the bearer P,

if P authorized by C

‖ mo, {N_{c}, N_{b}}_{C} ▶ • ‖

•  I authorize payment to M′^{‖}  \overline{mo, N_{b}  ▶}  ρ_{m,3} B says γ_{b,2} and C authorizes payment to M^{‖}
ρ_{b,3} C says C authorizes payment to M and M says M requests payment^{‖} ◀  hash(M, B, N_{b}, N_{m}) I, M, request payment and will ship C goods•^{‖}

+ +

Authentication Protocols: A Coordination Mechanism

• Causes principals to agree on certain parameters

• After a run, participant knows:

– There is a protocol run by another principal
– Some parameters match across runs
– Some shared values are secrets
– Other principal’s run overlaps mine temporally

• Protocol design now tractable, based on a few theorems

– “Authentication tests” determine extent of agreement
– Formalize reasoning of previous slides via strands and bundles

• Formulas γ, ρ clarify real-world consequences of protocol run

– When is customer committed to paying?
– When is merchant committed to shipping?
– Whose word did you depend on when deciding?

• Trust decisions constrain protocol runs (“business logic”)

+ +

Trust management and protocols

• Each principal P

– Reasons locally in initial theory Th_{P}, e.g. a theory in Datalog
– Derives guarantee before transmitting message
– Relies on assertions of others as premises

• Premises: formulas associated with message receptions

– Specifies what recipient may rely on, e.g.

“B says B will transfer funds if authorized”

– Provides local representation of remote guarantee
– Th_{P} determines whether ϕ follows from P′ says ϕ — — Relevant notion of “trust”

• Role of protocol

– When I rely on you having asserted a formula,

then you did guarantee that assertion

– Coordination mechanism for rely/guarantees
– Sound protocol: “relies” always backed by “guarantees”

even with malicious adversary M′

+ 2013.3.7 BiSS, Mar 2013  12

+ +

Soundness

• Protocol Π is sound if:

for all executions B of Π, and message receptions n ∈ B

{prin(m) says γ_{m}: m ≺_{B} n} ⟶_{L} ρ_{n}

where

⟶_{L} is the consequence relation of the underlying logic
≺_{B} is the partial order generated by

m → n implies m ≺ n (msg trans)

m ⇒ n implies m ≺ n (next step on strand, i.e. local run )

• Soundness follows from authentication properties

– Strand space authentication methods work fine
– Recency easy to incorporate

• Soundness:

Criterion for Π to be strong enough for its trust interpretation

+ +

A Domain Specific Language

• CPPL, a Cryptographic Protocol Programming Language

– Expresses cryptographic protocols
– Programmer treats crypto primitives as black boxes
– Controls behavior via trust queries
– Equipped with a useful semantics — — In the strand space framework  — — spi or applied pi would also work

∘ Useful for proving protocol security ∘ Useful in structuring compiler we wrote

+ +

Coding the Merchant

let  chan = accept in

receive chan
 {c, n c, goods, price} km
-->
let n m = new nonce in
send
  --> chan {n c, n m, m} kc
receive chan
    [[hash(c, n c, n b, n m, price)]] skb, n b
  -->
send
  --> chan [[hash(B, n b, n m)]] skm
return

M
\overline{\{C, N_{c}, g, p\}_{M} ▶} •
◀ {N_{c}, N_{m}, M}_{C}  • γ_{m,2} ∧ pubkey(c, kc)
\overline{mo, N_{b}  ▶} • ρ_{m,3}
◀ [[ h(M, B, N_{b}, N_{m}) ]]_{M} • γ_{m,4}

+ +

Coding the Merchant: Trust Formulas

let  chan = accept in

receive chan
 {c, n c, goods, price} km
--> true
let n m = new nonce in
send γ_{m,2} and pubkey(c,kc)
  --> chan {n c, n m, m} kc
receive chan
    [[hash(c, n c, n b, n m, price)]] skb, n b, b
  --> if sigkey(b,skb) then ρ_{m,3}
send sigkey(b,skb) and γ_{m,4}
  --> chan [[hash(B, n b, n m)]] skm
return

M
\overline{\{C, N_{c}, g, p\}_{M} ▶} •
◀ {N_{c}, N_{m}, M}_{C}  • γ_{m,2} ∧ pubkey(c, kc)
\overline{mo, N_{b}  ▶} • ρ_{m,3}
◀ [[ h(M, B, N_{b}, N_{m}) ]]_{M} • γ_{m,4}

+ +

Semantics of CPPL

• A structured operational semantics • Judgment:

σ ; Δ ⊢ c : s

• Means:

In environment σ, — — partial map from identifiers to values

a principal holding theory Δ, executing code c, may unleash strand s — —

“strand:” purely local sequence of sends, receives

+ +

Semantics of receive

\frac{σ_{1} = σ ⊕ σ′ σ_{1} ; Δ, ϕ σ_{1} ⊢ c : s}{σ ; Δ ⊢ (x recv m ϕ c) : − (x, m) σ_{1} , ϕ σ_{1} ⇒ s}

— — dom(σ′) ⊆ vars(m) vars(x, m, ϕ) ⊆ dom(σ_{1})

⊕ means disjoint union of fns

−(x, m), ϕ ⇒ s: receive m from channel x, relying on ϕ; then do rest of strand s

+ +

Semantics of send

\frac{σ_{1} = σ ⊕ σ′  Δ ∥− ϕ σ_{1}  σ_{1} ; Δ ⊢ c : s}{σ ; Δ ⊢ (send ϕ x m c) : + (x, m) σ_{1} , ϕ σ_{1} ⇒ s}
— —dom(σ′) ⊆ vars(ϕ)  vars(x, m, ϕ) ⊆ dom(σ^{1})

+(x, m), ϕ ⇒ s:

transmit m on channel x, guaranteeing ϕ; then do rest of strand s

+ +

CPPL Principles

• Principal maintains an environment during run

– Variables progressively become bound, never change value after
– Values are atomic (nonce, name, key, etc)

• Message transmission, reception:

– Reception:

∘ Branch on form of message

∘ New variables bound from msg components ∘ Rely on assertion of sender

– Transmission:

∘ Branch on successful guarantee

∘ New variables bound from successful guarantee

(as in logic programming)

• Derive guarantees using:

– Th_{P}, your initial theory
– Values of variables bound up to this point
– Rely formulas for earlier msg receptions

+ +

Subprotocols

• Subprotocols encapsulated by rely/guarantee

– Callee relies on assertion of caller

∘ Property of input parameters

– Callee guarantees result for caller

∘ Relation on input, output parameters

– Caller and callee are same principal P (same theory Th_{P})

• Subprotocol call, return: local message transmissions

– Call: Message from caller to callee
– Return: Message from callee to caller
– RPC-like mechanism (“LPC”)

• Flow of information on subprotocol call, return matches convention

– Guarantee before transmitting
– Rely when receiving

+ +

Protocol Headers

epmo_merchant_role(m, km, skm): (c, b, goods, price)
    rely pubkey(m, km) and sigkey(m, skm)
    guarantee supplied(c, goods, price, b)
in ... end

+ +

Subprotocol Headers

retrieve_pubkey (b, a, c, cver, d, kd) : (a, ka)
rely      certifying_authority(c, a)
and directory_service(d, c)
and pubkey(d, kd)
and sign_verification_key_of(c, cver)
guarantee pubkey(a, ka)
in
...
end

Precondition/postcondition specifies effect of successful run of subprotocol

+ +

Subprotocol call site

call with
pubkey(a, ka)
--> null_protocol () ()
true

use key ka …

|
certifying_authority(c, a)
and directory_service(d, c)
and pubkey(d, kd)
and sign_verification_key_of(c, cver)
  --> retrieve_pubkey (b, a, c, cver, d, kd) (a, ka)
pubkey(a, ka)

use key ka …

+ +

Subprotocol Semantics

Invocation

\frac{σ_{1} = σ_{orig} ⊕ σ′ dom(σ′) ⊆ ide(pr, n, ai, x^{∗}) σ_{1} ; Γ_{0}, (Ψ σ) ⊢ c : s, υ}{σ_{orig} ; Γ_{0} ⊢ proc n Ψ x^{∗} c : − call pr, n, ai, x^{∗} σ_{1}, Ψ σ_{1} ⇒ s, υ}

Return

\frac{σ_{1} = σ ⊕ σ′  dom(σ′) ⊆ ide(Φ)  Γ ∥− Φ σ_{1}}{σ ; Γ ⊢ return Φ x^{∗} : ⟨+ret (ai, x^{∗}) σ_{1}, Φ σ_{1}⟩, ∅}

+ +

Trust and Protocols

• Crypto protocols coordinate principals

– Agree on parameter values
– Agree on assertions made

• Trust decisions at runtime can control protocol behavior

– Stop protocol run if trust constraints fail
– Choose branch conditional on successful trust constraint
– Message transmissions and subprotocol calls

• Strand-based semantics

– Provides good protocol verification methods, design heuristics
– Motivated language design and implementation

• Status: Second version of compiler now complete

– Datalog trust engine, Crypto library

• Trust engineering using cryptographic protocols

+ +

Contrast: Earlier Work

• The BAN tradition

– Messages are formulas or formulas idealize messages
– Who asserted the formulas?
– Who drew consequences from formulas?

• Embedding formulas explicitly inside messages

– Main view of logical trust mgt starts with LAWB
– Formulas parsed out of certificates
– Problem of partial information?

• Our view: Formulas part of transmission/reception, not msg

– Compatible with many insights of earlier views
– Independent method to determine what events happened
– Clarity about who makes assertions, who infers consequences
– Partial information easy to handle
– Rigorous notion of soundness

+ +

A Signed Alternate: SEPMO

B  C  M

n_{c,1} {C, N_{c}, goods, price}_{M} ▶ n_{m,1}

n_{c,2} ‖ ◀ {[[ N_{c}, N_{m}, M, goods, price ]]_{M}}_{C} n_{m,2} ‖

n_{b,1} ◀ {C, N_{c}, N_{m}, price}_{B} n_{c,3}^{‖}
n_{b,2}^{‖}  \overline{mo, \{N_{c}, N_{b}\}_{C} ▶} n_{c,4}^{‖}
n_{c,5}^{‖}  \overline{mo, N_{b}  ▶} n_{m,3}^{‖}
n_{b,3}^{‖} ◀  hash(M, B, N_{b}, N_{m})  n_{m,4}^{‖}

Signed Electronic Purchase using Money Order mo = [[ hash(C, N_{c}, N_{b}, N_{m}, price) ]]_{B}