PRIVATE AUTHENTICATION

The Private Authentication protocol as described in [F] involves an initiator A and a responder B.

The initiator A sends a message enc(<pkA,n0>,r0,pkB) to the responder B, where pkA (respectively pkB) is the public key of A (respectively B). The responder B checks that the first projection of the decryption of the received message is equal to pkA and that the second projection of the decryption of the received message has a correct length. In that case, B sends back enc(<n0,n>,r,pkA).

The protocol is as follows:

  • A -> B : enc(<pkA,n0>,r0,pkB)
  • B -> A : enc(<n0,n>,r,pkA)

This is a “light” model without the last check of A.

In this file, we prove anonymity, i.e. that an attacker cannot tell whether a session is initiated by an identity A or by an identity Abis.

[F] G. Bana and H. Comon-Lundh. A computationally complete symbolic attacker for equivalence properties. In 2014 ACM Conference on Computer and Communications Security, CCS ’14, pages 609–620. ACM, 2014

When this option is set to true, Squirrel checks whether each tactic invoked for the proof is also sound for quantum attackers.

We first declare the communication channels, the function symbols for the public encryption scheme as well as the several names used in the protocol’s messages.

We also declare a public function symbol plus, which we will use to model the addition of lengths of messages.

The initiator A is indexed by i to represent an unbounded number of sessions and is defined by a single output.

We define a similar process for the initiator Abis.

The responder B is indexed by j to represent an unbounded number of sessions.

In order to express anonymity using an equivalence property, we model two systems using the diff operator. On the left side, the key kA is used while the right side uses the key kAbis.

 System before processing:

O:
out(cO,pair(pair(pk(kA),pk(kAbis)),pk(kB)));
(!_i A i) | ((!_ibis Abis ibis) | (!_j B j))

System after processing:

O:
out(cO,pair(pair(pk(kA),pk(kAbis)),pk(kB)));
(!_i A: out(cA,enc(pair(pk(kA),n0(i)),r0(i),pk(kB))); null) |
((!_ibis
Abis:
out(cAbis,enc(pair(pk(kAbis),n0bis(ibis)),r0bis(ibis),pk(kB))); null) |
(!_j
in(cB,mess);
let dmess = dec(mess,kB) in
B:
out(cB,
enc(if
((fst(dmess(j)) = diff(pk(kA),pk(kAbis))) &&
(len(snd(dmess(j))) = len(n(j))))
then pair(snd(dmess(j)),n(j)) else pair(n(j),n(j)),r(j),
pk(diff(kA,kAbis)))); null))

System default registered with actions (init,O,A,Abis,B).

The protocol is finally defined by a system where an unbounded number of sessions for A, Abis and B play in parallel, after having outputted the public keys of A, Abis and B.

 Goal eq_sym :
(x = y) = (y = x)
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: x,y:'a
----------------------------------------
(x = y) = (y = x)

[> Line 11: by (rewrite ...)
[goal> Goal eq_sym is proved
Exiting proof mode.


Goal neq_sym :
(x <> y) = (y <> x)
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: x,y:'a
----------------------------------------
(x <> y) = (y <> x)

[> Line 14: by (rewrite ...)
[goal> Goal neq_sym is proved
Exiting proof mode.


Goal eq_refl :
(x = x) = true
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: x:'a
----------------------------------------
(x = x) = true

[> Line 18: by (rewrite ...)
[goal> Goal eq_refl is proved
Exiting proof mode.


Goal false_true :
(false = true) = false
[goal> Focused goal (1/1):
System: any
----------------------------------------
(false = true) = false

[> Line 30: by (rewrite ...)
[goal> Goal false_true is proved
Exiting proof mode.


Goal eq_true :
(b = true) = b
[goal> Focused goal (1/1):
System: any
Variables: b:bool
----------------------------------------
(b = true) = b

[> Line 35: by (case b)
[goal> Goal eq_true is proved
Exiting proof mode.


Goal eq_true2 :
(true = b) = b
[goal> Focused goal (1/1):
System: any
Variables: b:bool
----------------------------------------
(true = b) = b

[> Line 39: by (case b)
[goal> Goal eq_true2 is proved
Exiting proof mode.


Goal not_not :
not(not(b)) = b
[goal> Focused goal (1/1):
System: any
Variables: b:bool
----------------------------------------
not(not(b)) = b

[> Line 54: by (case b)
[goal> Goal not_not is proved
Exiting proof mode.


Goal not_eq :
not(x = y) = (x <> y)
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: x,y:'a
----------------------------------------
not(x = y) = (x <> y)

[> Line 60: by (rewrite ...)
[goal> Goal not_eq is proved
Exiting proof mode.


Goal not_neq :
not(x <> y) = (x = y)
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: x,y:'a
----------------------------------------
not(x <> y) = (x = y)

[> Line 66: by (rewrite ...)
[goal> Goal not_neq is proved
Exiting proof mode.


Goal not_eqfalse :
(b = false) = not(b)
[goal> Focused goal (1/1):
System: any
Variables: b:bool
----------------------------------------
(b = false) = not(b)

[> Line 72: by (case b)
[goal> Goal not_eqfalse is proved
Exiting proof mode.


Goal eq_false :
((x = y) = false) = (x <> y)
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: x,y:'a
----------------------------------------
((x = y) = false) = (x <> y)

[> Line 80: (rewrite ...)
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: x,y:'a
----------------------------------------
((x = y) = false) = not(x = y)

[> Line 80: ((case (x = y));(intro _))
[goal> Focused goal (1/2):
System: any
Type variables: 'a
Variables: x,y:'a
_: x = y
----------------------------------------
(true = false) = not(true)

[> Line 80: simpl
[goal> Focused goal (1/2):
System: any
Type variables: 'a
Variables: x,y:'a
_: x = y
----------------------------------------
true

[> Line 80: auto
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: x,y:'a
_: not(x = y)
----------------------------------------
(false = false) = not(false)

[> Line 81: by (rewrite ...)
[goal> Goal eq_false is proved
Exiting proof mode.


Goal and_true_r :
(b && true) = b
[goal> Focused goal (1/1):
System: any
Variables: b:bool
----------------------------------------
(b && true) = b

[> Line 94: by (rewrite ... ...)
[goal> Goal and_true_r is proved
Exiting proof mode.


Goal and_false_r :
(b && false) = false
[goal> Focused goal (1/1):
System: any
Variables: b:bool
----------------------------------------
(b && false) = false

[> Line 101: by (rewrite ... ...)
[goal> Goal and_false_r is proved
Exiting proof mode.


Goal or_false_r :
(b || false) = b
[goal> Focused goal (1/1):
System: any
Variables: b:bool
----------------------------------------
(b || false) = b

[> Line 112: by (rewrite ... ...)
[goal> Goal or_false_r is proved
Exiting proof mode.


Goal or_true_r :
(b || true) = true
[goal> Focused goal (1/1):
System: any
Variables: b:bool
----------------------------------------
(b || true) = true

[> Line 119: by (rewrite ... ...)
[goal> Goal or_true_r is proved
Exiting proof mode.


Goal not_and :
not((a && b)) = (not(a) || not(b))
[goal> Focused goal (1/1):
System: any
Variables: a,b:bool
----------------------------------------
not((a && b)) = (not(a) || not(b))

[> Line 128: (rewrite ...)
[goal> Focused goal (1/1):
System: any
Variables: a,b:bool
----------------------------------------
not((a && b)) <=> not(a) || not(b)

[> Line 129: (((case a);(case b));(intro //=))
[goal> Goal not_and is proved
Exiting proof mode.


Goal not_or :
not((a || b)) = (not(a) && not(b))
[goal> Focused goal (1/1):
System: any
Variables: a,b:bool
----------------------------------------
not((a || b)) = (not(a) && not(b))

[> Line 134: (rewrite ...)
[goal> Focused goal (1/1):
System: any
Variables: a,b:bool
----------------------------------------
not((a || b)) <=> not(a) && not(b)

[> Line 135: (((case a);(case b));(intro //=))
[goal> Goal not_or is proved
Exiting proof mode.


Goal if_true :
b => if b then x else y = x
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b:bool,x,y:'a
----------------------------------------
b => if b then x else y = x

[> Line 144: (intro *)
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b:bool,x,y:'a
H: b
----------------------------------------
if b then x else y = x

[> Line 145: (case if b then x else y)
[goal> Focused goal (1/2):
System: any
Type variables: 'a
Variables: b:bool,x,y:'a
H: b
----------------------------------------
b && if b then x else y = x => x = x

[> Line 146: auto
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b:bool,x,y:'a
H: b
----------------------------------------
not(b) && if b then x else y = y => y = x

[> Line 147: (intro [HH _])
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b:bool,x,y:'a
H: b
HH: not(b)
_: if b then x else y = y
----------------------------------------
y = x

[> Line 147: by (have ... as )
[goal> Goal if_true is proved
Exiting proof mode.


Goal if_true0 :
if true then x else y = x
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: x,y:'a
----------------------------------------
if true then x else y = x

[> Line 153: by (rewrite ...)
[goal> Goal if_true0 is proved
Exiting proof mode.


Goal if_false :
not(b) => if b then x else y = y
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b:bool,x,y:'a
----------------------------------------
not(b) => if b then x else y = y

[> Line 160: ((intro *);(case if b then x else y))
[goal> Focused goal (1/2):
System: any
Type variables: 'a
Variables: b:bool,x,y:'a
H: not(b)
----------------------------------------
b && if b then x else y = x => x = y

[> Line 161: (intro [HH _])
[goal> Focused goal (1/2):
System: any
Type variables: 'a
Variables: b:bool,x,y:'a
H: not(b)
HH: b
_: if b then x else y = x
----------------------------------------
x = y

[> Line 161: by (have ... as )
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b:bool,x,y:'a
H: not(b)
----------------------------------------
not(b) && if b then x else y = y => y = y

[> Line 162: auto
[goal> Goal if_false is proved
Exiting proof mode.


Goal if_false0 :
if false then x else y = y
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: x,y:'a
----------------------------------------
if false then x else y = y

[> Line 168: by (rewrite ...)
[goal> Goal if_false0 is proved
Exiting proof mode.


Goal if_then_then :
if b then if b' then x else y else y = if (b && b') then x else y
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b,b':bool,x,y:'a
----------------------------------------
if b then if b' then x else y else y = if (b && b') then x else y

[> Line 175: by ((case b);(case b'))
[goal> Goal if_then_then is proved
Exiting proof mode.


Goal if_then_implies :
if b then if b' then x else y else z =
if b then if (b => b') then x else y else z
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b,b':bool,x,y,z:'a
----------------------------------------
if b then if b' then x else y else z =
if b then if (b => b') then x else y else z

[> Line 182: ((case b);
((intro H);((case b');((intro H');(simpl;(try auto))))))

[goal> Focused goal (1/2):
System: any
Type variables: 'a
Variables: b,b':bool,x,y,z:'a
H: b
H': b'
----------------------------------------
x = if (true => true) then x else y

[> Line 183: by (rewrite ...)
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b,b':bool,x,y,z:'a
H: b
H': not(b')
----------------------------------------
y = if (true => false) then x else y

[> Line 184: (rewrite ...)
[goal> Focused goal (1/2):
System: any
Type variables: 'a
Variables: b,b':bool,x,y,z:'a
H: b
H': not(b')
----------------------------------------
not((true => false))

[> Line 185: ((intro Habs);by (have ... as ))
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b,b':bool,x,y,z:'a
H: b
H': not(b')
----------------------------------------
y = y

[> Line 186: auto
[goal> Goal if_then_implies is proved
Exiting proof mode.


Goal if_same :
if b then x else x = x
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b:bool,x:'a
----------------------------------------
if b then x else x = x

[> Line 192: by (case b)
[goal> Goal if_same is proved
Exiting proof mode.


Goal if_then :
b = b' => if b then if b' then x else y else z = if b then x else z
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b,b':bool,x,y,z:'a
----------------------------------------
b = b' => if b then if b' then x else y else z = if b then x else z

[> Line 201: by ((intro ->);(case b'))
[goal> Goal if_then is proved
Exiting proof mode.


Goal if_else :
b = b' => if b then x else if b' then y else z = if b then x else z
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b,b':bool,x,y,z:'a
----------------------------------------
b = b' => if b then x else if b' then y else z = if b then x else z

[> Line 210: by ((intro ->);(case b'))
[goal> Goal if_else is proved
Exiting proof mode.


Goal if_then_not :
b = not(b') => if b then if b' then x else y else z = if b then y else z
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b,b':bool,x,y,z:'a
----------------------------------------
b = not(b') => if b then if b' then x else y else z = if b then y else z

[> Line 219: by ((intro ->);(case b'))
[goal> Goal if_then_not is proved
Exiting proof mode.


Goal if_else_not :
b = not(b') => if b then x else if b' then y else z = if b then x else y
[goal> Focused goal (1/1):
System: any
Type variables: 'a
Variables: b,b':bool,x,y,z:'a
----------------------------------------
b = not(b') => if b then x else if b' then y else z = if b then x else y

[> Line 228: by ((intro ->);(case b'))
[goal> Goal if_else_not is proved
Exiting proof mode.


Goal fst_pair :
fst(<x,y>) = x
[goal> Focused goal (1/1):
System: any
Variables: x,y:message
----------------------------------------
fst(<x,y>) = x

[> Line 236: auto
[goal> Goal fst_pair is proved
Exiting proof mode.


Goal snd_pair :
snd(<x,y>) = y
[goal> Focused goal (1/1):
System: any
Variables: x,y:message
----------------------------------------
snd(<x,y>) = y

[> Line 240: auto
[goal> Goal snd_pair is proved
Exiting proof mode.


Goal iff_refl :
(x <=> x) = true
[goal> Focused goal (1/1):
System: any
Variables: x:bool
----------------------------------------
(x <=> x) = true

[> Line 248: by (rewrite ...)
[goal> Goal iff_refl is proved
Exiting proof mode.


Goal iff_sym :
(x <=> y) = (y <=> x)
[goal> Focused goal (1/1):
System: any
Variables: x,y:bool
----------------------------------------
(x <=> y) = (y <=> x)

[> Line 254: by (rewrite ...)
[goal> Goal iff_sym is proved
Exiting proof mode.


Goal true_iff_false :
(true <=> false) = false
[goal> Focused goal (1/1):
System: any
----------------------------------------
(true <=> false) = false

[> Line 259: by (rewrite ...)
[goal> Goal true_iff_false is proved
Exiting proof mode.


Goal false_iff_true :
(false <=> true) = false
[goal> Focused goal (1/1):
System: any
----------------------------------------
(false <=> true) = false

[> Line 265: by (rewrite ...)
[goal> Goal false_iff_true is proved
Exiting proof mode.


Goal exists_false1 :
(exists (a:'a), false) = false
[goal> Focused goal (1/1):
System: any
Type variables: 'a
----------------------------------------
(exists (a:'a), false) = false

[> Line 277: by (rewrite ...)
[goal> Goal exists_false1 is proved
Exiting proof mode.


Goal exists_false2 :
(exists (a:'a,b:'b), false) = false
[goal> Focused goal (1/1):
System: any
Type variables: 'a, 'b
----------------------------------------
(exists (a:'a,b:'b), false) = false

[> Line 281: by (rewrite ...)
[goal> Goal exists_false2 is proved
Exiting proof mode.


Goal exists_false3 :
(exists (a:'a,b:'b,c:'c), false) = false
[goal> Focused goal (1/1):
System: any
Type variables: 'a, 'b, 'c
----------------------------------------
(exists (a:'a,b:'b,c:'c), false) = false

[> Line 285: by (rewrite ...)
[goal> Goal exists_false3 is proved
Exiting proof mode.


Goal exists_false4 :
(exists (a:'a,b:'b,c:'c,d:'d), false) = false
[goal> Focused goal (1/1):
System: any
Type variables: 'a, 'b, 'c, 'd
----------------------------------------
(exists (a:'a,b:'b,c:'c,d:'d), false) = false

[> Line 289: by (rewrite ...)
[goal> Goal exists_false4 is proved
Exiting proof mode.


Goal exists_false5 :
(exists (a:'a,b:'b,c:'c,d:'d,e:'e), false) = false
[goal> Focused goal (1/1):
System: any
Type variables: 'a, 'b, 'c, 'd, 'e
----------------------------------------
(exists (a:'a,b:'b,c:'c,d:'d,e:'e), false) = false

[> Line 293: by (rewrite ...)
[goal> Goal exists_false5 is proved
Exiting proof mode.


Goal exists_false6 :
(exists (a:'a,b:'b,c:'c,d:'d,e:'e,f:'f), false) = false
[goal> Focused goal (1/1):
System: any
Type variables: 'a, 'b, 'c, 'd, 'e, 'f
----------------------------------------
(exists (a:'a,b:'b,c:'c,d:'d,e:'e,f:'f), false) = false

[> Line 297: by (rewrite ...)
[goal> Goal exists_false6 is proved
Exiting proof mode.


Goal forall_true1 :
(forall (a:'a), true) = true
[goal> Focused goal (1/1):
System: any
Type variables: 'a
----------------------------------------
(forall (a:'a), true) = true

[> Line 307: auto
[goal> Goal forall_true1 is proved
Exiting proof mode.


Goal forall_true2 :
(forall (a:'a,b:'b), true) = true
[goal> Focused goal (1/1):
System: any
Type variables: 'a, 'b
----------------------------------------
(forall (a:'a,b:'b), true) = true

[> Line 311: auto
[goal> Goal forall_true2 is proved
Exiting proof mode.


Goal forall_true3 :
(forall (a:'a,b:'b,c:'c), true) = true
[goal> Focused goal (1/1):
System: any
Type variables: 'a, 'b, 'c
----------------------------------------
(forall (a:'a,b:'b,c:'c), true) = true

[> Line 315: auto
[goal> Goal forall_true3 is proved
Exiting proof mode.


Goal forall_true4 :
(forall (a:'a,b:'b,c:'c,d:'d), true) = true
[goal> Focused goal (1/1):
System: any
Type variables: 'a, 'b, 'c, 'd
----------------------------------------
(forall (a:'a,b:'b,c:'c,d:'d), true) = true

[> Line 319: auto
[goal> Goal forall_true4 is proved
Exiting proof mode.


Goal forall_true5 :
(forall (a:'a,b:'b,c:'c,d:'d,e:'e), true) = true
[goal> Focused goal (1/1):
System: any
Type variables: 'a, 'b, 'c, 'd, 'e
----------------------------------------
(forall (a:'a,b:'b,c:'c,d:'d,e:'e), true) = true

[> Line 323: auto
[goal> Goal forall_true5 is proved
Exiting proof mode.


Goal forall_true6 :
(forall (a:'a,b:'b,c:'c,d:'d,e:'e,f:'f), true) = true
[goal> Focused goal (1/1):
System: any
Type variables: 'a, 'b, 'c, 'd, 'e, 'f
----------------------------------------
(forall (a:'a,b:'b,c:'c,d:'d,e:'e,f:'f), true) = true

[> Line 327: auto
[goal> Goal forall_true6 is proved
Exiting proof mode.


[warning> loaded: Basic.sp <]

This axiom states that the length of a pair is equal to the sum of the lengths of each component of the pair.

 Goal if_len :
len(if b then y else z) = if b then len(y) else len(z)

Helper lemma for pushing conditionals under the len(_) function.

 [goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: b:bool,y,z:message
----------------------------------------
len(if b then y else z) = if b then len(y) else len(z)

 [> Line 124: by (case b)
[goal> Goal if_len is proved
Exiting proof mode.


 Goal if_same_branch :
(b => y = x) => (not(b) => z = x) => if b then y else z = x
 [goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: b:bool,x,y,z:message
----------------------------------------
(b => y = x) => (not(b) => z = x) => if b then y else z = x

 [> Line 133: by ((intro *);(case b))
[goal> Goal if_same_branch is proved
Exiting proof mode.


 Goal anonymity :
forall t:timestamp, equiv(frame@t)

The anonymity property is expressed as an equivalence between the left side (the one using kA and the right side (the one using kAbis) of the system. This property is expressed by the logic formula forall t:timestamp, frame@t where frame@t is a bi-frame.

 [goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: t:timestamp
H: [happens(t)]
----------------------------------------
0: frame@t

The high-level idea of the proof is as follows: we show that the message outputted by the role B does not give any element to the attacker to distinguish the left side from the right side, relying on the fact that encryption satisfies key privacy and IND-CCA1 assumptions.

 [> Line 155: (enrich pk(kA), pk(kAbis), pk(kB))
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: t:timestamp
H: [happens(t)]
----------------------------------------
0: pk(kB)
1: pk(kAbis)
2: pk(kA)
3: frame@t

We start by adding to the frame the two public keys pk(kA), pk(kAbis) and pk(kB) since any execution starts by the action O outputting them. This allows to simplify some cases in the proof below.

 [> Line 157: (induction t)
[goal> Focused goal (1/5):
Systems: left:default/left, right:default/right (same for equivalences)
H: [happens(init)]
----------------------------------------
0: pk(kB)
1: pk(kAbis)
2: pk(kA)
3: frame@init


 [> Line 163: auto
[goal> Focused goal (1/4):
Systems: left:default/left, right:default/right (same for equivalences)
H: [happens(O)]
IH: equiv(pk(kB), pk(kAbis), pk(kA), frame@pred(O))
----------------------------------------
0: pk(kB)
1: pk(kAbis)
2: pk(kA)
3: frame@O

Case where t = 0:
This case is trivial thanks to the addition of pk(kA), pk(kAbis) and pk(kB) in the frame.

 [> Line 165: (rewrite ...)
[goal> Focused goal (1/4):
Systems: left:default/left, right:default/right (same for equivalences)
H: [happens(O)]
IH: equiv(pk(kB), pk(kAbis), pk(kA), frame@pred(O))
----------------------------------------
0: pk(kB)
1: pk(kAbis)
2: pk(kA)
3: <frame@pred(O),
<of_bool(exec@pred(O) && true),
if (exec@pred(O) && true) then <<pk(kA),pk(kAbis)>,pk(kB)>>>


 [> Line 166: by (apply ... )
[goal> Focused goal (1/3):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: i:index
H: [happens(A(i))]
IH: equiv(pk(kB), pk(kAbis), pk(kA), frame@pred(A(i)))
----------------------------------------
0: pk(kB)
1: pk(kAbis)
2: pk(kA)
3: frame@A(i)


 [> Line 178: expandall
[goal> Focused goal (1/3):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: i:index
H: [happens(A(i))]
IH: equiv(pk(kB), pk(kAbis), pk(kA), frame@pred(A(i)))
----------------------------------------
0: pk(kB)
1: pk(kAbis)
2: pk(kA)
3: <frame@pred(A(i)),
<of_bool(exec@pred(A(i)) && true),
if (exec@pred(A(i)) && true) then enc(<pk(kA),n0(i)>,r0(i),pk(kB))>>

Case where t = A(i):
The output of this action is the same on both sides. We show that this output can be removed from the frame so that we can conclude by induction hypothesis. We start by expanding all macros and splitting the pairs and function applications. We are then left with the two names n0(i) and r0(i) used for the encryption. These names are fresh (i.e. does not appear anywhere else in the frame) so we are able to remove them with the fresh tactic.

 [> Line 179: ((fa 3);((fa 4);((fa 4);((fa 4);(fa 4)))))
[goal> Focused goal (1/3):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: i:index
H: [happens(A(i))]
IH: equiv(pk(kB), pk(kAbis), pk(kA), frame@pred(A(i)))
----------------------------------------
0: pk(kB)
1: pk(kAbis)
2: pk(kA)
3: frame@pred(A(i))
4: n0(i)
5: r0(i)


 [> Line 180: ((fresh 5);(rewrite ... //))
[goal> Focused goal (1/3):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: i:index
H: [happens(A(i))]
IH: equiv(pk(kB), pk(kAbis), pk(kA), frame@pred(A(i)))
----------------------------------------
0: pk(kB)
1: pk(kAbis)
2: pk(kA)
3: frame@pred(A(i))
4: n0(i)


 [> Line 181: by ((fresh 4);(rewrite ... //))
[goal> Focused goal (1/2):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: ibis:index
H: [happens(Abis(ibis))]
IH: equiv(pk(kB), pk(kAbis), pk(kA), frame@pred(Abis(ibis)))
----------------------------------------
0: pk(kB)
1: pk(kAbis)
2: pk(kA)
3: frame@Abis(ibis)


 [> Line 186: expandall
[goal> Focused goal (1/2):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: ibis:index
H: [happens(Abis(ibis))]
IH: equiv(pk(kB), pk(kAbis), pk(kA), frame@pred(Abis(ibis)))
----------------------------------------
0: pk(kB)
1: pk(kAbis)
2: pk(kA)
3: <frame@pred(Abis(ibis)),
<of_bool(exec@pred(Abis(ibis)) && true),
if (exec@pred(Abis(ibis)) && true) then
enc(<pk(kAbis),n0bis(ibis)>,r0bis(ibis),pk(kB))>>

Case where t = Abis(ibis):
Similar to the previous case.

 [> Line 187: ((fa 3);((fa 4);((fa 4);((fa 4);(fa 4)))))
[goal> Focused goal (1/2):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: ibis:index
H: [happens(Abis(ibis))]
IH: equiv(pk(kB), pk(kAbis), pk(kA), frame@pred(Abis(ibis)))
----------------------------------------
0: pk(kB)
1: pk(kAbis)
2: pk(kA)
3: frame@pred(Abis(ibis))
4: n0bis(ibis)
5: r0bis(ibis)


 [> Line 188: ((fresh 5);(rewrite ... //))
[goal> Focused goal (1/2):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: ibis:index
H: [happens(Abis(ibis))]
IH: equiv(pk(kB), pk(kAbis), pk(kA), frame@pred(Abis(ibis)))
----------------------------------------
0: pk(kB)
1: pk(kAbis)
2: pk(kA)
3: frame@pred(Abis(ibis))
4: n0bis(ibis)


 [> Line 189: by ((fresh 4);(rewrite ... //))
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: j:index
H: [happens(B(j))]
IH: equiv(pk(kB), pk(kAbis), pk(kA), frame@pred(B(j)))
----------------------------------------
0: pk(kB)
1: pk(kAbis)
2: pk(kA)
3: frame@B(j)


 [> Line 195: (expand frame, output, exec, cond, dmess)
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: j:index
H: [happens(B(j))]
IH: equiv(pk(kB), pk(kAbis), pk(kA), frame@pred(B(j)))
----------------------------------------
0: pk(kB)
1: pk(kAbis)
2: pk(kA)
3: <frame@pred(B(j)),
<of_bool(exec@pred(B(j)) && true),
if (exec@pred(B(j)) && true) then
enc(if (fst(dec(input@B(j),kB)) = pk(diff(kA, kAbis)) &&
len(snd(dec(input@B(j),kB))) = len(n(j))) then
<snd(dec(input@B(j),kB)),n(j)>
else <n(j),n(j)>,r(j),pk(diff(kA, kAbis)))>>

Case where t = B(j):
We have to show that the output message does not give any information to the attacker to distinguish the left side from the right side.

 [> Line 196: ((fa 3);((fa 4);(fa 4)))
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: j:index
H: [happens(B(j))]
IH: equiv(pk(kB), pk(kAbis), pk(kA), frame@pred(B(j)))
----------------------------------------
0: pk(kB)
1: pk(kAbis)
2: pk(kA)
3: frame@pred(B(j))
4: enc(if (fst(dec(input@B(j),kB)) = pk(diff(kA, kAbis)) &&
len(snd(dec(input@B(j),kB))) = len(n(j))) then
<snd(dec(input@B(j),kB)),n(j)>
else <n(j),n(j)>,r(j),pk(diff(kA, kAbis)))


 [> Line 204: ((enckp 4); 1: auto)
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: j:index
H: [happens(B(j))]
IH: equiv(pk(kB), pk(kAbis), pk(kA), frame@pred(B(j)))
----------------------------------------
0: pk(kB)
1: pk(kAbis)
2: pk(kA)
3: frame@pred(B(j))
4: enc(if (fst(dec(input@B(j),kB)) = pk(diff(kA, kAbis)) &&
len(snd(dec(input@B(j),kB))) = len(n(j))) then
<snd(dec(input@B(j),kB)),n(j)>
else <n(j),n(j)>,r(j),pk(kA))

We first use the key privacy assumption: knowing only a cipertext, it should not be possible to know which specific key was used. The corresponding enckp tactic allows here to replace kAbis by kA on the right side.

 [> Line 211: ((cca1 4); 2: auto)
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: j:index
H: [happens(B(j))]
IH: equiv(pk(kB), pk(kAbis), pk(kA), frame@pred(B(j)))
----------------------------------------
0: pk(kB)
1: pk(kAbis)
2: pk(kA)
3: frame@pred(B(j))
4: len(
if (fst(dec(input@B(j),kB)) = pk(diff(kA, kAbis)) &&
len(snd(dec(input@B(j),kB))) = len(n(j))) then
<snd(dec(input@B(j),kB)),n(j)>
else <n(j),n(j)>)

We now use the ciphertext indistinguishability (IND-CCA1) assumption, which requires to show that the lengths of the plaintexts on both sides are equal.

 [> Line 214: (rewrite ...)
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: j:index
H: [happens(B(j))]
IH: equiv(pk(kB), pk(kAbis), pk(kA), frame@pred(B(j)))
----------------------------------------
0: pk(kB)
1: pk(kAbis)
2: pk(kA)
3: frame@pred(B(j))
4: if (fst(dec(input@B(j),kB)) = pk(diff(kA, kAbis)) &&
len(snd(dec(input@B(j),kB))) = len(n(j))) then
len(<snd(dec(input@B(j),kB)),n(j)>)
else len(<n(j),n(j)>)

We use the lemma if_len to push the conditional under len(_).

 [> Line 217: (rewrite ...)
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: j:index
H: [happens(B(j))]
IH: equiv(pk(kB), pk(kAbis), pk(kA), frame@pred(B(j)))
----------------------------------------
0: pk(kB)
1: pk(kAbis)
2: pk(kA)
3: frame@pred(B(j))
4: if (fst(dec(input@B(j),kB)) = pk(diff(kA, kAbis)) &&
len(snd(dec(input@B(j),kB))) = len(n(j))) then
len(snd(dec(input@B(j),kB))) ++ len(n(j))
else len(n(j)) ++ len(n(j))


 [> Line 221: (rewrite ... //)
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: j:index
H: [happens(B(j))]
IH: equiv(pk(kB), pk(kAbis), pk(kA), frame@pred(B(j)))
----------------------------------------
0: pk(kB)
1: pk(kAbis)
2: pk(kA)
3: frame@pred(B(j))
4: len(n(j)) ++ len(n(j))


 [> Line 224: ((fa 4);(fa 4))
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: j:index
H: [happens(B(j))]
IH: equiv(pk(kB), pk(kAbis), pk(kA), frame@pred(B(j)))
----------------------------------------
0: pk(kB)
1: pk(kAbis)
2: pk(kA)
3: frame@pred(B(j))
4: n(j)

We use the if_same_branch helper lemma to simplify the conditional using the fact that both branches are identical.

 [> Line 225: by ((fresh 4);(rewrite ... //))
[goal> Goal anonymity is proved

We conclude using the fact that n(j) is fresh.

 Exiting proof mode.

Squirrel Prover

Press the left and right arrows to do and undo an instruction.

Alternatively, you can double-click on an instruction.

This zone shows a Squirrel file. You can double-click on a comment to collapse it for better readabilility.

This zone shows the output given by Squirrel.

This zone shows the output of the previous instruction, to help identifying the change caused by the instruction.

PRIVATE AUTHENTICATION

The Private Authentication protocol as described in [F] involves an initiator A and a responder B.

The initiator A sends a message enc(<pkA,n0>,r0,pkB) to the responder B, where pkA (respectively pkB) is the public key of A (respectively B). The responder B checks that the first projection of the decryption of the received message is equal to pkA and that the second projection of the decryption of the received message has a correct length. In that case, B sends back enc(<n0,n>,r,pkA).

The protocol is as follows:

  • A -> B : enc(<pkA,n0>,r0,pkB)
  • B -> A : enc(<n0,n>,r,pkA)

This is a “light” model without the last check of A.

In this file, we prove anonymity, i.e. that an attacker cannot tell whether a session is initiated by an identity A or by an identity Abis.

[F] G. Bana and H. Comon-Lundh. A computationally complete symbolic attacker for equivalence properties. In 2014 ACM Conference on Computer and Communications Security, CCS ’14, pages 609–620. ACM, 2014

When this option is set to true, Squirrel checks whether each tactic invoked for the proof is also sound for quantum attackers.

set postQuantumSound=true.

We first declare the communication channels, the function symbols for the public encryption scheme as well as the several names used in the protocol’s messages.

channel cA
channel cAbis
channel cB
channel cO

aenc enc,dec,pk

name kA : message
name kAbis : message
name kB : message

name n0 : index -> message
name r0 : index -> message
name n0bis : index -> message
name r0bis : index -> message

name n : index -> message
name r : index -> message.

We also declare a public function symbol plus, which we will use to model the addition of lengths of messages.

abstract (++) : message -> message -> message.

The initiator A is indexed by i to represent an unbounded number of sessions and is defined by a single output.

process A(i:index) =
out(cA, enc(<pk(kA),n0(i)>,r0(i),pk(kB))).

We define a similar process for the initiator Abis.

process Abis(i:index) =
out(cAbis, enc(<pk(kAbis),n0bis(i)>,r0bis(i),pk(kB))).

The responder B is indexed by j to represent an unbounded number of sessions.

In order to express anonymity using an equivalence property, we model two systems using the diff operator. On the left side, the key kA is used while the right side uses the key kAbis.

process B(j:index) =
in(cB, mess);
let dmess = dec(mess, kB) in
out(cB,
enc(
(if fst(dmess) = diff(pk(kA),pk(kAbis)) && len(snd(dmess)) = len(n(j)) then
<snd(dmess), n(j)>
else
<n(j), n(j)>),
r(j), pk(diff(kA,kAbis)))
).

The protocol is finally defined by a system where an unbounded number of sessions for A, Abis and B play in parallel, after having outputted the public keys of A, Abis and B.

system O:
out(cO,<<pk(kA),pk(kAbis)>,pk(kB)>);
(!_i A(i) | !_ibis Abis(ibis) | !_j B(j)).

This axiom states that the length of a pair is equal to the sum of the lengths of each component of the pair.

include Basic.

axiom length_pair (m1:message, m2:message): len(<m1,m2>) = len(m1) ++ len(m2).

Helper lemma for pushing conditionals under the len(_) function.

goal if_len (b : boolean, y,z:message):
len(if b then y else z) =
(if b then len(y) else len(z)).
Proof.
by case b.
Qed.

(* Helper lemma *)
goal if_same_branch (x,y,z : message, b : boolean):
(b => y = x) =>
(not b => z = x) =>
(if b then y else z) = x.
Proof.
by intro *; case b.
Qed.

The anonymity property is expressed as an equivalence between the left side (the one using kA and the right side (the one using kAbis) of the system. This property is expressed by the logic formula forall t:timestamp, frame@t where frame@t is a bi-frame.

equiv anonymity.

The high-level idea of the proof is as follows: we show that the message outputted by the role B does not give any element to the attacker to distinguish the left side from the right side, relying on the fact that encryption satisfies key privacy and IND-CCA1 assumptions.

Proof.

We start by adding to the frame the two public keys pk(kA), pk(kAbis) and pk(kB) since any execution starts by the action O outputting them. This allows to simplify some cases in the proof below.

enrich pk(kA), pk(kAbis), pk(kB).

induction t.

Case where t = 0:
This case is trivial thanks to the addition of pk(kA), pk(kAbis) and pk(kB) in the frame.

auto.

rewrite /*.
by apply IH.

Case where t = A(i):
The output of this action is the same on both sides. We show that this output can be removed from the frame so that we can conclude by induction hypothesis. We start by expanding all macros and splitting the pairs and function applications. We are then left with the two names n0(i) and r0(i) used for the encryption. These names are fresh (i.e. does not appear anywhere else in the frame) so we are able to remove them with the fresh tactic.

expandall.
fa 3; fa 4; fa 4; fa 4; fa 4.
fresh 5; rewrite if_true //.
by fresh 4; rewrite if_true //.

Case where t = Abis(ibis):
Similar to the previous case.

expandall.
fa 3; fa 4; fa 4; fa 4; fa 4.
fresh 5; rewrite if_true //.
by fresh 4; rewrite if_true //.

Case where t = B(j):
We have to show that the output message does not give any information to the attacker to distinguish the left side from the right side.

expand frame, output, exec, cond, dmess.
fa 3; fa 4; fa 4.

We first use the key privacy assumption: knowing only a cipertext, it should not be possible to know which specific key was used. The corresponding enckp tactic allows here to replace kAbis by kA on the right side.

enckp 4; 1: auto.

We now use the ciphertext indistinguishability (IND-CCA1) assumption, which requires to show that the lengths of the plaintexts on both sides are equal.

cca1 4; 2: auto.

We use the lemma if_len to push the conditional under len(_).

rewrite if_len.

(* We use our axiom on the length of a pair. *)
rewrite !length_pair.

We use the if_same_branch helper lemma to simplify the conditional using the fact that both branches are identical.

rewrite (if_same_branch (len(n(j)) ++ len(n(j)))) //.

We conclude using the fact that n(j) is fresh.

fa 4; fa 4.
by fresh 4; rewrite if_true //.

Previously: