abstract ok : message
abstract ko : message

name skP : message
name skS : message

channel cP
channel cS.

SIGNED DDH

The signed DDH protocol as described in [G] features two roles, P and S. Each role is associated to a secret key (skP and skS).

  • P -> S : <pk(skP), g^a>
  • S -> P : <pk(skS),gb>,sign(<<ga,g^b>,pk(skP)>,skS)
  • P -> S : sign(<<gb,ga>,pk(skS)>,skP)

We consider multiple sessions but two agents only (one agent for the role P and one agent for the role S) and show the strong secrecy of the shared key.

  • In this file signed-ddh-P.sp, we show that the key gab as computed by P is indistinguishable from g^k with k fresh (system secretP).
  • In another file signed-ddh-S.sp, we show that the key gab as computed by S is indistinguishable from g^k with k fresh (system secretS).

[G] ISO/IEC 9798-3:2019, IT Security techniques – Entity authentication – Part 3: Mechanisms using digital signature techniques.

We first declare some public constants, the secret keys for roles P and S, the channels used by these two roles.

 name a : index -> message
name b : index -> message.

Names a and b represent the random numbers used by roles P and S. They are indexed so that each new session uses a new random name.

 name k : index -> index -> message.

The name k represents the random number used in the strong secrecy property. It has 2 as index arity to model the fact that each interaction between session i of role P and session j of role S uses a new random name.

 ddh g, (^) where group:message exponents:message.

We declare a DDH context, using g for the generator element and ^ for the power operator.

 signature sign,checksign,pk.

We also declare a signature scheme by specifying 3 function symbols.

 process Pchall(i:index) =
out(cP, <pk(skP),g^a(i)>);
in(cP, x2);
let gS = snd(fst(x2)) in
let pkS = fst(fst(x2)) in
if checksign(snd(x2),pkS) = <<g^a(i),gS>,pk(skP)> && pkS = pk(skS) then
out(cP,sign(<<gS,g^a(i)>,pkS>,skP));
in(cP, challenge);
try find j such that gS = g^b(j) in
out(cP, diff(g^a(i)^b(j),g^k(i,j)))
else

out(cP, diff(ok,ko))

process S(j:index) =
in(cS, x1);
let gP = snd(x1) in
let pkP = fst(x1) in
if pkP = pk(skP) then
out(cS, < <pk(skS),g^b(j)>, sign(<<gP,g^b(j)>,pkP>,skS)>);
in(cS, x3);
if checksign(x3,pkP) = <<g^b(j),gP>,pk(skS)> then
out(cS,ok)

system (!_i Pchall(i) | !_j S(j)). System before processing:

(!_i Pchall i) | (!_j S j)

System after processing:

(!_i
Pchall:
out(cP,pair(pk(skP),(g ^ a(i))));
in(cP,x2);
let gS = snd(fst(x2)) in
let pkS = fst(fst(x2)) in
if ((checksign(snd(x2),pkS(i)) = pair(pair((g ^ a(i)),gS(i)),pk(skP)))
&& (pkS(i) = pk(skS))) then
Pchall1:
out(cP,sign(pair(pair(gS(i),(g ^ a(i))),pkS(i)),skP));
in(cP,challenge);
find (j) such that (gS(i) = (g ^ b(j))) in
Pchall2: out(cP,diff(((g ^ a(i)) ^ b(j)),(g ^ k(i,j)))); null else
Pchall3: out(cP,diff(ok,ko)); null else Pchall4: null) |
(!_j
in(cS,x1);
let gP = snd(x1) in
let pkP = fst(x1) in
if (pkP(j) = pk(skP)) then
S:
out(cS,
pair(pair(pk(skS),(g ^ b(j))),
sign(pair(pair(gP(j),(g ^ b(j))),pkP(j)),skS)));
in(cS,x3);
if (checksign(x3,pkP(j)) = pair(pair((g ^ b(j)),gP(j)),pk(skS))) then
S1: out(cS,ok); null else S2: null else S3: null)

System default registered with actions (init,Pchall,Pchall1,Pchall2,Pchall3,
Pchall4,S,S1,S2,S3).

In the system secretP, we add an output at the end of the role of P. This output is actually a bi-term:

  • the left side of the system outputs the shared key as computed by P,
  • the right side of the system outputs g^k(i,j) where k(i,j) is fresh.

The goal will be to prove that these two sides are indistinguishable.

The try find construct is needed to retrieve the index j, but this else branch should never be reachable. We thus output a bi-term with distinct public constants so that the equivalence for the strong secrecy could not hold if this else branch is reached.

include Basic. 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 <]
 goal P_charac (i:index):
happens(Pchall1(i)) =>
cond@Pchall1(i) =>
exists (j:index), snd(fst(input@Pchall1(i))) = g^b(j). Goal P_charac :
happens(Pchall1(i)) =>
cond@Pchall1(i) => exists (j:index), snd(fst(input@Pchall1(i))) = g ^ b(j)

In the proof of strong secrecy for the system secretP, we will use the following property, stating that whenever P accepts a message from S, this message is of the form <<_,x>,_> where x = g^b(j).

 Proof. [goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i:index
----------------------------------------
happens(Pchall1(i)) =>
cond@Pchall1(i) => exists (j:index), snd(fst(input@Pchall1(i))) = g ^ b(j)

The high-level idea of the proof is to use the EUF cryptographic axiom: only S can forge a correct signature that will be accepted by P since the secret key is not known by the attacker.

 intro Hap Hcond. [> Line 118: (intro Hap Hcond)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i:index
Hap: happens(Pchall1(i))
Hcond: cond@Pchall1(i)
----------------------------------------
exists (j:index), snd(fst(input@Pchall1(i))) = g ^ b(j)

We start by introducing the hypotheses and expanding the macros.
expand cond, pkS(i)@Pchall1(i). [> Line 119: (expand cond, pkS(i)@Pchall1(i))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i:index
Hap: happens(Pchall1(i))
Hcond: checksign(snd(input@Pchall1(i)),fst(fst(input@Pchall1(i)))) =
<<g ^ a(i),gS(i)@Pchall1(i)>,pk(skP)> &&
fst(fst(input@Pchall1(i))) = pk(skS)
----------------------------------------
exists (j:index), snd(fst(input@Pchall1(i))) = g ^ b(j)
destruct Hcond as [Meq Meq0]. [> Line 120: (destruct Hcond, [Meq Meq0])
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i:index
Hap: happens(Pchall1(i))
Meq: checksign(snd(input@Pchall1(i)),fst(fst(input@Pchall1(i)))) =
<<g ^ a(i),gS(i)@Pchall1(i)>,pk(skP)>
Meq0: fst(fst(input@Pchall1(i))) = pk(skS)
----------------------------------------
exists (j:index), snd(fst(input@Pchall1(i))) = g ^ b(j)

 rewrite Meq0 in Meq. [> Line 123: (rewrite ... in Meq)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i:index
Hap: happens(Pchall1(i))
Meq: checksign(snd(input@Pchall1(i)),pk(skS)) =
<<g ^ a(i),gS(i)@Pchall1(i)>,pk(skP)>
Meq0: fst(fst(input@Pchall1(i))) = pk(skS)
----------------------------------------
exists (j:index), snd(fst(input@Pchall1(i))) = g ^ b(j)

We then rewrite Meq using the message equality Meq0.

 euf Meq. [> Line 127: (euf Meq)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j:index
Hap: happens(Pchall1(i))
Meq: checksign(snd(input@Pchall1(i)),pk(skS)) =
<<g ^ a(i),gS(i)@Pchall1(i)>,pk(skP)>
Meq0: fst(fst(input@Pchall1(i))) = pk(skS)
----------------------------------------
S(j) <= Pchall1(i) || S(j) < Pchall1(i) =>
<<gP(j)@S(j),g ^ b(j)>,pkP(j)@S(j)> = <<g ^ a(i),gS(i)@Pchall1(i)>,pk(skP)> =>
exists (j:index), snd(fst(input@Pchall1(i))) = g ^ b(j)

We are now able to apply the euf tactic, which will search for occurences of signatures with skS: the only possibility is the output of an action S(j).

 intro *. [> Line 129: (intro *)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j:index
H: S(j) <= Pchall1(i) || S(j) < Pchall1(i)
Hap: happens(Pchall1(i))
Meq: checksign(snd(input@Pchall1(i)),pk(skS)) =
<<g ^ a(i),gS(i)@Pchall1(i)>,pk(skP)>
Meq0: fst(fst(input@Pchall1(i))) = pk(skS)
Meq1: <<gP(j)@S(j),g ^ b(j)>,pkP(j)@S(j)> =
<<g ^ a(i),gS(i)@Pchall1(i)>,pk(skP)>
----------------------------------------
exists (j:index), snd(fst(input@Pchall1(i))) = g ^ b(j)

The conclusion is now trivial from the Meq1 and D1 hypotheses.
by exists j. [> Line 130: by (exists j)
[goal> Goal P_charac is proved

Qed. Exiting proof mode.


 equiv strongSecP. Goal strongSecP :
forall t:timestamp, equiv(frame@t)

We now show the strong secrecy of the shared key for the system secretP, expressed by the logic formula forall t:timestamp, frame@t where frame@t is actually a bi-frame. We will prove that the left projection of frame@t (i.e. where the shared key g^a^b is outputted) is indistinguishable from the right projection of frame@t (i.e. where g^k is outputted).

 Proof. [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 proof is done by induction, after having enriched the frame with some additional (bi-)terms. Intuitively, the idea of enriching the frame is to simplify the cases that are contexts built using applications of public function symbols and terms added in the enriched frame. It then remains to prove:

  • the base case, i.e. prove that the enriched bi-frame is indistinguishable;
  • the case corresponding to the output diff(ok,ko), i.e. prove that this output is never reached using the previous P_charac property.
 enrich
skP, skS,
seq(i:index ->g^a(i)),
seq(j:index ->g^b(j)),
seq(i,j:index ->diff( g ^ a(i), g) ^ diff( b(j), k(i,j))). [> Line 158: (enrich skP, skS, seq(i:index->(g ^ a(i))),
seq(j:index->(g ^ b(j))),
seq(i,j:index->(diff((g ^ a(i)),g) ^ diff(b(j),k(i,j)))))

[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: t:timestamp
H: [happens(t)]
----------------------------------------
0: seq(i,j:index->(diff(g ^ a(i), g) ^ diff(b(j), k(i,j))))
1: seq(j:index->(g ^ b(j)))
2: seq(i:index->(g ^ a(i)))
3: skS
4: skP
5: frame@t

We start by enriching the frame.

 induction t; try (by expandall; apply IH). [> Line 166: ((induction t);(try by (expandall;(apply ... ))))
[goal> Focused goal (1/2):
Systems: left:default/left, right:default/right (same for equivalences)
H: [happens(init)]
----------------------------------------
0: seq(i,j:index->(diff(g ^ a(i), g) ^ diff(b(j), k(i,j))))
1: seq(j:index->(g ^ b(j)))
2: seq(i:index->(g ^ a(i)))
3: skS
4: skP
5: frame@init

We now apply the induction tactic, which generates several cases, one for each possible value that can be taken by the timestamp t.

For most cases, applying the induction hypothesis IH allows to conclude because frame@t can be built from frame@pred(t) and elements added to the frame by the tactic enrich.

 + expandall. [> Line 170: expandall
[goal> Focused goal (1/2):
Systems: left:default/left, right:default/right (same for equivalences)
H: [happens(init)]
----------------------------------------
0: seq(i,j:index->(diff(g ^ a(i), g) ^ diff(b(j), k(i,j))))
1: seq(j:index->(g ^ b(j)))
2: seq(i:index->(g ^ a(i)))
3: skS
4: skP

Case where t = init. We use here the DDH assumption.
by ddh g,a,b,k. [> Line 171: by (ddh g, a, b, k)
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: i:index
H: [happens(Pchall3(i))]
IH: equiv(seq(i,j:index->(diff(g ^ a(i), g) ^ diff(b(j), k(i,j)))),
seq(j:index->(g ^ b(j))), seq(i:index->(g ^ a(i))), skS, skP,
frame@pred(Pchall3(i)))
----------------------------------------
0: seq(i,j:index->(diff(g ^ a(i), g) ^ diff(b(j), k(i,j))))
1: seq(j:index->(g ^ b(j)))
2: seq(i:index->(g ^ a(i)))
3: skS
4: skP
5: frame@Pchall3(i)


 + expand frame, exec, output. [> Line 177: (expand frame, exec, output)
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: i:index
H: [happens(Pchall3(i))]
IH: equiv(seq(i,j:index->(diff(g ^ a(i), g) ^ diff(b(j), k(i,j)))),
seq(j:index->(g ^ b(j))), seq(i:index->(g ^ a(i))), skS, skP,
frame@pred(Pchall3(i)))
----------------------------------------
0: seq(i,j:index->(diff(g ^ a(i), g) ^ diff(b(j), k(i,j))))
1: seq(j:index->(g ^ b(j)))
2: seq(i:index->(g ^ a(i)))
3: skS
4: skP
5: <frame@pred(Pchall3(i)),
<of_bool(exec@pred(Pchall3(i)) && cond@Pchall3(i)),
if (exec@pred(Pchall3(i)) && cond@Pchall3(i)) then diff(ok, ko)>>

Case where t = Pchall3(i). We will show that this case is not possible, by showing that the formula exec@pred(Pchall3(i)) && cond@Pchall3(i) is equivalent to False, relying on the previous property P_charac.
have ->: (exec@pred(Pchall3(i)) && cond@Pchall3(i)) <=> false. [> Line 178: (have ((exec@pred(Pchall3(i)) && cond@Pchall3(i)) <=> False),
->)

[goal> Focused goal (1/2):
System: left:default/left, right:default/right (same for equivalences)
Variables: i:index
H: [happens(Pchall3(i))]
IH: equiv(seq(i,j:index->(diff(g ^ a(i), g) ^ diff(b(j), k(i,j)))),
seq(j:index->(g ^ b(j))), seq(i:index->(g ^ a(i))), skS, skP,
frame@pred(Pchall3(i)))
----------------------------------------
exec@pred(Pchall3(i)) && cond@Pchall3(i) <=> false

 {
split => //. [> Line 179: (split;(intro //))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right (same for equivalences)
Variables: i:index
H: [happens(Pchall3(i))]
IH: equiv(seq(i,j:index->(diff(g ^ a(i), g) ^ diff(b(j), k(i,j)))),
seq(j:index->(g ^ b(j))), seq(i:index->(g ^ a(i))), skS, skP,
frame@pred(Pchall3(i)))
----------------------------------------
exec@pred(Pchall3(i)) && cond@Pchall3(i) => false
intro [Hexec Hcond]. [> Line 180: (intro [Hexec Hcond])
[goal> Focused goal (1/2):
System: left:default/left, right:default/right (same for equivalences)
Variables: i:index
H: [happens(Pchall3(i))]
Hcond: cond@Pchall3(i)
Hexec: exec@pred(Pchall3(i))
IH: equiv(seq(i,j:index->(diff(g ^ a(i), g) ^ diff(b(j), k(i,j)))),
seq(j:index->(g ^ b(j))), seq(i:index->(g ^ a(i))), skS, skP,
frame@pred(Pchall3(i)))
----------------------------------------
false
expand cond. [> Line 181: (expand cond)
[goal> Focused goal (1/2):
System: left:default/left, right:default/right (same for equivalences)
Variables: i:index
H: [happens(Pchall3(i))]
Hcond: forall (j:index), not(gS(i)@Pchall3(i) = g ^ b(j))
Hexec: exec@pred(Pchall3(i))
IH: equiv(seq(i,j:index->(diff(g ^ a(i), g) ^ diff(b(j), k(i,j)))),
seq(j:index->(g ^ b(j))), seq(i:index->(g ^ a(i))), skS, skP,
frame@pred(Pchall3(i)))
----------------------------------------
false
depends Pchall1(i), Pchall3(i) => //. [> Line 182: ((depends Pchall1(i), Pchall3(i));(intro //))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right (same for equivalences)
Variables: i:index
H: [happens(Pchall3(i))]
Hcond: forall (j:index), not(gS(i)@Pchall3(i) = g ^ b(j))
Hexec: exec@pred(Pchall3(i))
IH: equiv(seq(i,j:index->(diff(g ^ a(i), g) ^ diff(b(j), k(i,j)))),
seq(j:index->(g ^ b(j))), seq(i:index->(g ^ a(i))), skS, skP,
frame@pred(Pchall3(i)))
----------------------------------------
Pchall1(i) < Pchall3(i) => false
intro Ord. [> Line 183: (intro Ord)
[goal> Focused goal (1/2):
System: left:default/left, right:default/right (same for equivalences)
Variables: i:index
H: [happens(Pchall3(i))]
Hcond: forall (j:index), not(gS(i)@Pchall3(i) = g ^ b(j))
Hexec: exec@pred(Pchall3(i))
IH: equiv(seq(i,j:index->(diff(g ^ a(i), g) ^ diff(b(j), k(i,j)))),
seq(j:index->(g ^ b(j))), seq(i:index->(g ^ a(i))), skS, skP,
frame@pred(Pchall3(i)))
Ord: Pchall1(i) < Pchall3(i)
----------------------------------------
false
executable pred(Pchall3(i)) => //. [> Line 184: ((executable pred(Pchall3(i)));(intro //))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right (same for equivalences)
Variables: i:index
H: [happens(Pchall3(i))]
Hcond: forall (j:index), not(gS(i)@Pchall3(i) = g ^ b(j))
Hexec: exec@pred(Pchall3(i))
IH: equiv(seq(i,j:index->(diff(g ^ a(i), g) ^ diff(b(j), k(i,j)))),
seq(j:index->(g ^ b(j))), seq(i:index->(g ^ a(i))), skS, skP,
frame@pred(Pchall3(i)))
Ord: Pchall1(i) < Pchall3(i)
----------------------------------------
(forall (t:timestamp), t < Pchall3(i) => exec@t) => false
intro Hexec'. [> Line 185: (intro Hexec')
[goal> Focused goal (1/2):
System: left:default/left, right:default/right (same for equivalences)
Variables: i:index
H: [happens(Pchall3(i))]
Hcond: forall (j:index), not(gS(i)@Pchall3(i) = g ^ b(j))
Hexec: exec@pred(Pchall3(i))
Hexec': forall (t:timestamp), t < Pchall3(i) => exec@t
IH: equiv(seq(i,j:index->(diff(g ^ a(i), g) ^ diff(b(j), k(i,j)))),
seq(j:index->(g ^ b(j))), seq(i:index->(g ^ a(i))), skS, skP,
frame@pred(Pchall3(i)))
Ord: Pchall1(i) < Pchall3(i)
----------------------------------------
false
use Hexec' with Pchall1(i) as Hexec1 => //. [> Line 186: ((have ... as Hexec1);(intro //))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right (same for equivalences)
Variables: i:index
H: [happens(Pchall3(i))]
Hcond: forall (j:index), not(gS(i)@Pchall3(i) = g ^ b(j))
Hexec: exec@pred(Pchall3(i))
Hexec': forall (t:timestamp), t < Pchall3(i) => exec@t
Hexec1: exec@Pchall1(i)
IH: equiv(seq(i,j:index->(diff(g ^ a(i), g) ^ diff(b(j), k(i,j)))),
seq(j:index->(g ^ b(j))), seq(i:index->(g ^ a(i))), skS, skP,
frame@pred(Pchall3(i)))
Ord: Pchall1(i) < Pchall3(i)
----------------------------------------
false
expand exec. [> Line 187: (expand exec)
[goal> Focused goal (1/2):
System: left:default/left, right:default/right (same for equivalences)
Variables: i:index
H: [happens(Pchall3(i))]
Hcond: forall (j:index), not(gS(i)@Pchall3(i) = g ^ b(j))
Hexec: exec@pred(Pchall3(i))
Hexec': forall (t:timestamp), t < Pchall3(i) => exec@t
Hexec1: exec@pred(Pchall1(i)) && cond@Pchall1(i)
IH: equiv(seq(i,j:index->(diff(g ^ a(i), g) ^ diff(b(j), k(i,j)))),
seq(j:index->(g ^ b(j))), seq(i:index->(g ^ a(i))), skS, skP,
frame@pred(Pchall3(i)))
Ord: Pchall1(i) < Pchall3(i)
----------------------------------------
false
use P_charac with i as [j0 Hyp] => //. [> Line 188: ((have ... as [j0 Hyp]);(intro //))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right (same for equivalences)
Variables: i,j0:index
H: [happens(Pchall3(i))]
Hcond: forall (j:index), not(gS(i)@Pchall3(i) = g ^ b(j))
Hexec: exec@pred(Pchall3(i))
Hexec': forall (t:timestamp), t < Pchall3(i) => exec@t
Hexec1: exec@pred(Pchall1(i)) && cond@Pchall1(i)
Hyp: snd(fst(input@Pchall1(i))) = g ^ b(j0)
IH: equiv(seq(i,j:index->(diff(g ^ a(i), g) ^ diff(b(j), k(i,j)))),
seq(j:index->(g ^ b(j))), seq(i:index->(g ^ a(i))), skS, skP,
frame@pred(Pchall3(i)))
Ord: Pchall1(i) < Pchall3(i)
----------------------------------------
false
by use Hcond with j0. [> Line 189: by (have ... as )
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: i:index
H: [happens(Pchall3(i))]
IH: equiv(seq(i,j:index->(diff(g ^ a(i), g) ^ diff(b(j), k(i,j)))),
seq(j:index->(g ^ b(j))), seq(i:index->(g ^ a(i))), skS, skP,
frame@pred(Pchall3(i)))
----------------------------------------
0: seq(i,j:index->(diff(g ^ a(i), g) ^ diff(b(j), k(i,j))))
1: seq(j:index->(g ^ b(j)))
2: seq(i:index->(g ^ a(i)))
3: skS
4: skP
5: <frame@pred(Pchall3(i)),<of_bool(false),if false then diff(ok, ko)>>
}

fa 5. [> Line 192: (fa 5)
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: i:index
H: [happens(Pchall3(i))]
IH: equiv(seq(i,j:index->(diff(g ^ a(i), g) ^ diff(b(j), k(i,j)))),
seq(j:index->(g ^ b(j))), seq(i:index->(g ^ a(i))), skS, skP,
frame@pred(Pchall3(i)))
----------------------------------------
0: seq(i,j:index->(diff(g ^ a(i), g) ^ diff(b(j), k(i,j))))
1: seq(j:index->(g ^ b(j)))
2: seq(i:index->(g ^ a(i)))
3: skS
4: skP
5: frame@pred(Pchall3(i))
6: <of_bool(false),if false then diff(ok, ko)>


 fa 6. [> Line 192: (fa 6)
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: i:index
H: [happens(Pchall3(i))]
IH: equiv(seq(i,j:index->(diff(g ^ a(i), g) ^ diff(b(j), k(i,j)))),
seq(j:index->(g ^ b(j))), seq(i:index->(g ^ a(i))), skS, skP,
frame@pred(Pchall3(i)))
----------------------------------------
0: seq(i,j:index->(diff(g ^ a(i), g) ^ diff(b(j), k(i,j))))
1: seq(j:index->(g ^ b(j)))
2: seq(i:index->(g ^ a(i)))
3: skS
4: skP
5: frame@pred(Pchall3(i))
6: if false then diff(ok, ko)


 by rewrite if_false. [> Line 194: by (rewrite ...)
[goal> Goal strongSecP is proved

It now remains to simplify if false then diff(ok,ko).
Qed. 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.

Previously: