(*
BASIC HASH
The Basic Hash protocol as described in [Brusò et al., 2010]
is an RFID protocol involving:
- a tag associated to a secret key;
- generic readers having access to a database containing all these keys.
The protocol is as follows:
T --> R : <nT, h(nT,kT)>
R --> T : ok
kT is the key of T, stored in the readers' database.
nT is a session nonce.
This file is an introductory example. It does NOT correspond to
how we would normally model Basic Hash in Squirrel. Proof scripts
use a minimum of ingredients and are thus unnecessarily tedious.
*)
(* Declare a hash function h that satisfies PRF, hence EUF. *)
hash h.
(* Keys for tags T1 and T2. *)
name k1 : message.
name k2 : message.
(* Session nonces *)
name nt : message.
name nt' : message.
(* Please ignore the next lines... *)
system null.
System before processing:
null
System after processing:
null
System default registered with actions (init).
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 <]
(* Declaring a goal phi as done next means that we are
going to prove (phi ~ true). Logical connectives in phi
are thus the dotted connectives, i.e. function symbols
representing boolean operations. *)
goal authentication :
(* Assume tag T1 has run a session with nonce nt,
and T2 with nonce nt'. *)
(
(* if reader accepts att(..) *)
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>))
= h(fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)),k1)
||
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>))
= h(fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)),k2)
) => (
(* then att(..) is an honest input *)
(fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = nt &&
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = h(nt,k1))
||
(fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = nt' &&
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = h(nt',k2))
).
Goal authentication :
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) =
h(fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)),k1) ||
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) =
h(fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)),k2) =>
fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = nt &&
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = h(nt,k1) ||
fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = nt' &&
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = h(nt',k2)
Proof.
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
----------------------------------------
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) =
h(fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)),k1) ||
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) =
h(fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)),k2) =>
fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = nt &&
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = h(nt,k1) ||
fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = nt' &&
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = h(nt',k2)
intro H.
[> Line 61: (intro H)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
H: snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) =
h(fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)),k1) ||
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) =
h(fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)),k2)
----------------------------------------
fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = nt &&
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = h(nt,k1) ||
fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = nt' &&
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = h(nt',k2)
(* the inference ---- is as still a dotted implication *)
case H.
[> Line 62: (case H)
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
H: snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) =
h(fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)),k1)
----------------------------------------
fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = nt &&
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = h(nt,k1) ||
fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = nt' &&
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = h(nt',k2)
(* Reader recognizes valid input from T1. *)
+ euf H => _.
[> Line 64: ((euf H);(intro _))
[goal> Focused goal (1/3):
System: left:default/left, right:default/right
H: snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) =
h(fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)),k1)
_: nt = fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>))
----------------------------------------
fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = nt &&
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = h(nt,k1) ||
fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = nt' &&
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = h(nt',k2)
- left.
[> Line 65: left
[goal> Focused goal (1/3):
System: left:default/left, right:default/right
H: snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) =
h(fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)),k1)
_: nt = fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>))
----------------------------------------
fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = nt &&
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = h(nt,k1)
auto.
[> Line 65: auto
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
H: snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) =
h(fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)),k1)
_: nt = fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>))
----------------------------------------
fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = nt &&
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = h(nt,k1) ||
fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = nt' &&
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = h(nt',k2)
- left.
[> Line 66: left
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
H: snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) =
h(fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)),k1)
_: nt = fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>))
----------------------------------------
fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = nt &&
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = h(nt,k1)
auto.
[> Line 66: auto
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
H: snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) =
h(fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)),k2)
----------------------------------------
fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = nt &&
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = h(nt,k1) ||
fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = nt' &&
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = h(nt',k2)
(* Reader recognizes valid input from T2. *)
+ euf H => _.
[> Line 68: ((euf H);(intro _))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
H: snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) =
h(fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)),k2)
_: nt' = fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>))
----------------------------------------
fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = nt &&
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = h(nt,k1) ||
fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = nt' &&
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = h(nt',k2)
- right.
[> Line 69: right
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
H: snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) =
h(fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)),k2)
_: nt' = fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>))
----------------------------------------
fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = nt' &&
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = h(nt',k2)
auto.
[> Line 69: auto
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
H: snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) =
h(fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)),k2)
_: nt' = fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>))
----------------------------------------
fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = nt &&
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = h(nt,k1) ||
fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = nt' &&
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = h(nt',k2)
- right.
[> Line 70: right
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
H: snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) =
h(fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)),k2)
_: nt' = fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>))
----------------------------------------
fst(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = nt' &&
snd(att(<<nt,h(nt,k1)>,<nt',h(nt',k2)>>)) = h(nt',k2)
auto.
[> Line 70: auto
[goal> Goal authentication is proved
Qed.
Exiting proof mode.
(* To prove an equivalence we use a global goal.
The two sides of the equivalence are given at once,
using diff(_,_) when the left and right sides differ. *)
global goal privacy (i1,i2,j1,j2:index) :
equiv(<nt,h(nt,k1)>,
diff(<nt',h(nt',k1)>,
<nt',h(nt',k2)>)).
Goal privacy :
forall i1,i2,j1,j2:index,
equiv(<nt,h(nt,k1)>, diff(<nt',h(nt',k1)>, <nt',h(nt',k2)>))
Proof.
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: i1,i2,j1,j2:index
----------------------------------------
0: <nt,h(nt,k1)>
1: diff(<nt',h(nt',k1)>, <nt',h(nt',k2)>)
(* First break the pairs. *)
fa 0.
[> Line 82: (fa 0)
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: i1,i2,j1,j2:index
----------------------------------------
0: nt
1: h(nt,k1)
2: diff(<nt',h(nt',k1)>, <nt',h(nt',k2)>)
fa 2.
[> Line 83: (fa 2)
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: i1,i2,j1,j2:index
----------------------------------------
0: nt
1: h(nt,k1)
2: nt'
3: diff(h(nt',k1), h(nt',k2))
(* Then show that the second hashes look like randomness. *)
prf 3.
[> Line 85: (prf 3)
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: i1,i2,j1,j2:index
----------------------------------------
0: nt
1: h(nt,k1)
2: nt'
3: if (diff(nt' <> nt, true) && true) then n_PRF else h(nt',diff(k1, k2))
rewrite if_true.
[> Line 86: (rewrite ...)
[goal> Focused goal (1/2):
System: left:default/left, right:default/right (same for equivalences)
Variables: i1,i2,j1,j2:index
----------------------------------------
diff(nt' <> nt, true) && true
project.
[> Line 87: project
[goal> Focused goal (1/3):
System: left:default/left
(equivalences: left:default/left, right:default/right)
Variables: i1,i2,j1,j2:index
----------------------------------------
nt' <> nt && true
+ auto.
[> Line 88: auto
[goal> Focused goal (1/2):
System: right:default/right
(equivalences: left:default/left, right:default/right)
Variables: i1,i2,j1,j2:index
----------------------------------------
true && true
+ auto.
[> Line 89: auto
[goal> Focused goal (1/1):
Systems: left:default/left, right:default/right (same for equivalences)
Variables: i1,i2,j1,j2:index
----------------------------------------
0: nt
1: h(nt,k1)
2: nt'
3: n_PRF
(* Conclude by reflexivity -- fresh may also be used. *)
refl.
[> Line 91: refl
[goal> Goal privacy is proved
Qed.
Exiting proof mode.
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.
