Key Pair Security in Imandra

In this notebook we introduce a simple implementation of a key pair exchange protocol in ReasonML. Messages can either be key requests, unencrypted responses to key requests with a public key or encrypted messages with a private key. In addition to this we introduce the concept of a "listener" - an agent who can intercept other messagers.

In [1]:
type person =
  | Mallory
  | Bob
  | Alice;

type public_key =
  | Public(person);
type private_key =
  | Private(person);

/* identifier person (purporting from) + payload */
type full_unencrypted_payload = (person, public_key);
type full_encrypted_payload = (person, int);

type data =
  | UnEncrypted(full_unencrypted_payload)
  /* where it's believed to be being sent and the actual public key used */
  | Encrypted((person, public_key), full_encrypted_payload);

/* actual people */
type channel = {
  from: person,
  to_: person,
};

let swap = (c: channel): channel => {from: c.to_, to_: c.from};

type known = {
  asker: person,
  ident: person,
  actual: person,
};

type msg = {
  channel,
  data,
};

type action =
  | Listen(person, channel)
  | KeyRequest(person, person)
  | Send(msg);

type state = {
  /* fst arg believes 2nd arg to be that person */
  believed_identities: list((person, person)),
  /* can learn a key */
  can_learn_keys: list((person, person)),
  /* person knows a given key */
  known_keys: list(known),
  /* a 'listener' / spy on a channel */
  listeners: list((person, channel)),
  /* msg was decrypted and read by person */
  decrypted: list((person, full_encrypted_payload)),
  /* actual encrypted channel messages sent */
  msgs: list((channel, full_encrypted_payload)),
};

let believed_identity = (s: state, a: person, b: person) =>
  List.mem((a, b), s.believed_identities);

/* Has person A requested person B's key? */

let can_learn_key = (s: state, a: person, b: person) =>
  List.mem((a, b), s.can_learn_keys);

/* Does person A know person B's key? */

let knows_key = (s: state, asker: person, ident: person, actual: person) =>
  asker == actual || List.mem({asker, ident, actual}, s.known_keys);

/* Is person A listening to channel C? Partially reflexive and symmetric! */

let listening = (s: state, a: person, c: channel) =>
  c.to_ == a
  || List.exists(
       ((p, c2)) => a == p && (c == c2 || c == swap(c2)),
       s.listeners,
     );

/* For all appropriate listeners on a given channel, do something */

let map_listeners =
    (s: state, c: channel, guard: person => bool, f: person => 'b) => {
  let doit = ((l_p, l_c)) =>
    if (listening(s, l_p, c) && guard(l_p)) {
      Some(f(l_p));
    } else {
      None;
    };
  List.filter_map(x => doit(x), s.listeners);
};

let step = (s: state, a: action) =>
  switch (a) {
  /* We can only listen in on messages between distinct people */
  | Listen(p, c) when c.from != c.to_ && c.from != p && c.to_ != p => {
      ...s,
      listeners: [(p, c), ...s.listeners],
    }
  | KeyRequest(asker, key_owner) =>
    /* filter out self requests */
    if (asker == key_owner) {
      s;
    } else {
      let ks =
        map_listeners(
          s,
          {from: asker, to_: key_owner},
          l => true,
          l => (l, key_owner),
        );
      /* once asker asks key_owner for his key, he believes this person's identity */
      {
        ...s,
        can_learn_keys: [(asker, key_owner), ...ks] @ s.can_learn_keys,
        believed_identities: [(key_owner, asker), ...s.believed_identities],
      };
    }
  | Send({channel, data: UnEncrypted((person, Public(key_owner)))}) =>
    /* filter out self sends */
    if (channel.from == channel.to_ || person == channel.to_) {
      s;
    } else if
      /* if the asker already believes he knows a key belonging to person then don't accept the key */
      (List.exists(
         ({asker, ident, actual}) => asker == channel.to_ && ident == person,
         s.known_keys,
       )) {
      s;
    } else if
      /* the recipent must be able to learn the key and the sender must know the key of key_owner believing it to be of person */
      (can_learn_key(s, channel.to_, person)
       && knows_key(s, channel.from, person, key_owner)) {
      /* The sink of the channel now knows the sent key */
      let r = {asker: channel.to_, ident: person, actual: key_owner};
      /* All listeners on the channel now know p's key */
      let ks =
        map_listeners(
          s,
          channel,
          l => can_learn_key(s, l, person),
          l => {asker: l, ident: person, actual: key_owner},
        );
      {...s, known_keys: [r, ...ks] @ s.known_keys};
    } else {
      s;
    }
  | Send({
      channel,
      data: Encrypted((recipient_ident, Public(t)), (p, msg)),
    }) =>
    /* filter out self sends */
    if (channel.from == channel.to_
        || recipient_ident == channel.from
        || p == channel.to_
        || recipient_ident == p) {
      s;
    } else if
      /* if channel.from asked for the key and the identity is different don't accept the message */
      (believed_identity(s, channel.to_, channel.from) && p != channel.from) {
      s;
    } else if
      /* if public key is known by sender and the key matches the channel.to_ */
      (knows_key(s, channel.from, recipient_ident, channel.to_)
       && t == channel.to_) {
      {
        ...s,
        decrypted: [(channel.to_, (p, msg)), ...s.decrypted],
        msgs: [(channel, (p, msg)), ...s.msgs],
      };
    } else {
      s;
    }
  | _ => s
  };

let init: state = {
  believed_identities: [],
  can_learn_keys: [],
  known_keys: [],
  listeners: [],
  decrypted: [],
  msgs: [],
};
Out[1]:
type person = Mallory | Bob | Alice
type public_key = Public of person
type private_key = Private of person
type full_unencrypted_payload = person * public_key
type full_encrypted_payload = person * Z.t
type data =
    UnEncrypted of full_unencrypted_payload
  | Encrypted of (person * public_key) * full_encrypted_payload
type channel = { from : person; to_ : person; }
val swap : channel -> channel = <fun>
type known = { asker : person; ident : person; actual : person; }
type msg = { channel : channel; data : data; }
type action =
    Listen of person * channel
  | KeyRequest of person * person
  | Send of msg
type state = {
  believed_identities : (person * person) list;
  can_learn_keys : (person * person) list;
  known_keys : known list;
  listeners : (person * channel) list;
  decrypted : (person * full_encrypted_payload) list;
  msgs : (channel * full_encrypted_payload) list;
}
val believed_identity : state -> person -> person -> bool = <fun>
val can_learn_key : state -> person -> person -> bool = <fun>
val knows_key : state -> person -> person -> person -> bool = <fun>
val listening : state -> person -> channel -> bool = <fun>
val map_listeners :
  state -> channel -> (person -> bool) -> (person -> 'b) -> 'b list = <fun>
val step : state -> action -> state = <fun>
val init : state =
  {believed_identities = []; can_learn_keys = []; known_keys = [];
   listeners = []; decrypted = []; msgs = []}

We can introduce some printing functions so that any traces produced can be visually interpreted.

In [2]:
let person_to_string = (p) =>
  switch (p) {
    | Alice => "Alice"
    | Mallory => "Mallory"
    | Bob => "Bob"
  };
Out[2]:
val person_to_string : person -> string = <fun>

This step allows us to depict message transitions between agents.

In [3]:
let graph_step = (s: action) =>
  switch (s) {
  | Listen(p, c) =>
    person_to_string(p)
    ++ "->"
    ++ person_to_string(c.from)
    ++ "[style=dotted];\n"
    ++ person_to_string(p)
    ++ "->"
    ++ person_to_string(c.to_)
    ++ "[style=dotted];\n"
  | KeyRequest(a, k) =>
    "edge [color=yellow];\n"
    ++ person_to_string(a)
    ++ "->"
    ++ person_to_string(k)
    ++ ";\n"
  | Send({channel, data: UnEncrypted((person, Public(key_owner)))}) =>
    person_to_string(channel.from)
    ++ "->"
    ++ person_to_string(channel.to_)
    ++ "[label=\""
    ++ person_to_string(key_owner)
    ++ "\",color=blue];\n"
  | Send({
      channel,
      data: Encrypted((recipient_ident, Public(t)), (p, msg)),
    }) =>
    person_to_string(channel.from)
    ++ "->"
    ++ person_to_string(channel.to_)
    ++ "[label=\""
    ++ person_to_string(t)
    ++ "\",color=black];\n"
  };
Out[3]:
val graph_step : action -> string = <fun>
In [4]:
let rec graph_inner = (xs:list(action)) =>
  switch (xs)
  {
    | [] => ""
    | [h, ...t] =>
      graph_step(h)++graph_inner(t)
  };
Out[4]:
val graph_inner : action list -> string = <fun>
termination proof

Termination proof

call `graph_inner (List.tl xs)` from `graph_inner xs`
original:graph_inner xs
sub:graph_inner (List.tl xs)
original ordinal:Ordinal.Int (_cnt xs)
sub ordinal:Ordinal.Int (_cnt (List.tl xs))
path:[xs <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.017s
details:
Expand
smt_stats:
num checks:8
arith assert lower:27
arith tableau max rows:17
arith tableau max columns:39
arith pivots:20
rlimit count:7273
mk clause:123
datatype occurs check:24
mk bool var:631
arith assert upper:32
datatype splits:188
decisions:74
arith row summations:52
propagations:162
conflicts:19
arith fixed eqs:14
datatype accessor ax:95
arith conflicts:5
arith num rows:17
arith assert diseq:14
datatype constructor ax:160
num allocs:8519943
final checks:5
added eqs:705
del clause:26
arith eq adapter:28
memory:19.120000
max memory:19.120000
Expand
  • start[0.017s]
      let (_x_0 : int) = count.list count.action xs in
      let (_x_1 : action list) = List.tl xs in
      let (_x_2 : int) = count.list count.action _x_1 in
      xs <> [] && ((_x_0 >= 0) && (_x_2 >= 0))
      ==> not (_x_1 <> [])
          || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
  • simplify
    into:
    let (_x_0 : action list) = List.tl xs in
    let (_x_1 : int) = count.list count.action _x_0 in
    let (_x_2 : int) = count.list count.action xs in
    not (_x_0 <> []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
    || not (xs <> [] && (_x_2 >= 0) && (_x_1 >= 0))
    expansions:
    []
    rewrite_steps:
      forward_chaining:
      • unroll
        expr:
        (|Ordinal.<<| (|Ordinal.Int_79/boot|
                        (|count.list_992/server| (|get.::.1_980/server|…
        expansions:
        • unroll
          expr:
          (|count.list_992/server| (|get.::.1_980/server| xs_981/server))
          expansions:
          • unroll
            expr:
            (|count.list_992/server| xs_981/server)
            expansions:
            • Unsat

            In the final printer function, we depict encrypted messages with black transition lines, key requests with yellow lines, and unencrypted messages with blue transition lines. Listeners to other parties are depicted with dashed lines.

            In [5]:
            [@program] let graph = (xs:list(action)) =>
              Document.graphviz("digraph G {\nAlice [color=blue];\nMallory [color=red];\nBob [color=green];\n"++graph_inner(xs)++"\n}\n");
            [@install_doc graph];
            
            Out[5]:
            val graph : action list -> Document.t = <fun>
            

            We can now ask imandra to prove correctness properties about the protocol. For example, is it possible for a message to be decrypted by someone who is not the intended recipient. Click on the Load graph button to visually interpret the counterexample found by imandra.

            In [6]:
            /* Can xq decrypt a message saying it's from xw, but actually it's been sent by another party? */
            [@blast]
            verify((x1, x2, m, xs) => {
              let s = List.fold_left(step, init, xs);
              List.mem((x1, (x2, m)), s.decrypted)
              ==> List.mem(({from: x2, to_: x1}, (x2, m)), s.msgs);
            });
            CX.xs;
            
            Out[6]:
            - : person -> person -> Z.t -> action list -> bool = <fun>
            module CX :
              sig val x1 : person val x2 : person val m : Z.t val xs : action list end
            - : action list = <document>
            
            Counterexample (after 66 steps, 0.060s):
            let x1 : person = Alice
            let x2 : person = Mallory
            let m : int = 0
            let xs : action list =
              let (_x_0 : channel) = {from = Alice; to_ = Mallory} in
              let (_x_1 : (person * public_key)) = (Alice, Public Alice) in
              [Listen (Bob, _x_0); KeyRequest (Mallory, Alice);
               Send {channel = _x_0; data = UnEncrypted _x_1};
               Send
               {channel = {from = Bob; to_ = Alice};
                data = Encrypted (_x_1, (Mallory, 0))}]
            
            Refuted

            We see that imandra, and in particular the [@blast] capability finds a counterexample very quickly. We can further ask whether if a particpant decodes a message then it must have been sent by the original sender of the message.

            In [7]:
            /* if a message has been sent by x2 and x1 decodes that message then they must be the same message */
            [@blast]
            verify((x1, x2, x3, m, xs) => {
              let s = List.fold_left(step, init, xs);
              (
                List.mem(({from: x2, to_: x3}, (x2, m)), s.msgs)
                && List.mem((x1, (x2, m)), s.decrypted)
              )
              ==> x1 == x3;
            });
            CX.xs;
            
            Out[7]:
            - : person -> person -> person -> Z.t -> action list -> bool = <fun>
            module CX :
              sig
                val x1 : person
                val x2 : person
                val x3 : person
                val m : Z.t
                val xs : action list
              end
            - : action list = <document>
            
            Counterexample (after 93 steps, 0.179s):
            let x1 : person = Mallory
            let x2 : person = Bob
            let x3 : person = Alice
            let m : int = 0
            let xs : action list =
              let (_x_0 : (person * public_key)) = (Alice, Public Mallory) in
              let (_x_1 : (person * int)) = (Bob, 0) in
              let (_x_2 : (person * public_key)) = (Mallory, Public Alice) in
              [KeyRequest (Bob, Alice);
               Send {channel = {from = Mallory; to_ = Bob}; data = UnEncrypted _x_0};
               Send
               {channel = {from = Bob; to_ = Mallory}; data = Encrypted (_x_0, _x_1)};
               KeyRequest (Bob, Mallory);
               Send {channel = {from = Alice; to_ = Bob}; data = UnEncrypted _x_2};
               Send {channel = {from = Bob; to_ = Alice}; data = Encrypted (_x_2, _x_1)}]
            
            Refuted

            Here imandra very quickly finds a counter-example which corresponds to the well-known "man in the middle attack" - where Mallory listens to the conversation between Alice and Bob and can intercept and forward messages, potentially tampering with the content. Again - click on the Load graph button to visually interpret the counterexample found by imandra.