Model Checking: Basics
Proof Script Generationfrom Proof Scores (1)Kazuhiro Ogata (JAIST, Japan)
i628e information processing theory

FY2019i628e information processing theory

2

Motivation
Proof tree

A proof can be regarded as a tree.
Goal (theorem to prove)

An instance of a proof rule✔

✔

✔ ✔

For example,
✔

✔

0

∀ :

⇒
∀ :1

FY2019i628e information processing theory

3Motivation∀ : NAT00∀ :⇒1∀ :0 0 0by axiomc✔

c0c ⇒0c

is used as axiom.

Note that c is an arbitrary Nat.
⇒✔

axiom
∀ : NAT 0∀ , : NAT

FY2019c0by axiom

ci628e information processing theory

4Motivation
Proof assistantA sequence of commands (or tactics),
or a proof script
Pros : it guarantees that once a proof
is done, it is correct.

✔

✔

✔

Pros : less flexible✔

✔ ✔

FY2019i628e information processing theory

5Motivation
Proof scores

Proofs (or proof plans) written in an alg. spec. lang.

Pros : flexible, can be written asprograms, etc.
Cons : subject to human errors

Only consisting of the leaf nodes ofa proof tree

FY2019i628e information processing theory

6MotivationWould like to check if proof scores are correct
One possible way to do so is to construct (or infer) proof
scripts from proof scores

✔

✔

✔

✔

✔ ✔

FY2019i628e information processing theory

7Outline
lecture 1
1. CafeOBJ, Maude & CafeInMaude
2. CafeOBJ
3. A running example
4. State machine & invariant
5. Formal specification
6. Proof scores
7. Summary
lecture 2
1.
2.
3.
4.

FY2019

Review of lecture 1
CiMPA – CafeInMaude Proof Assistant
CiMPG – CafeInMaude Proof Generator
Summary & future directionsi628e information processing theory8CafeOBJ, Maude & CafeInMaude
CafeOBJ & Maude are direct successors of OBJ3, the most
famous alg. spec. lang. & sibling langs
Joseph Goguen
PI of OBJ3

Jose Meseguer
PI of Maude

Kokichi Futatsugi
PI of CafeOBJ

Adrian Riesco
Implementer ofCafeInMaude

CafeInMaude is the world 2nd implementation of CafeOBJ
in Maude.

FY2019i628e information processing theory

9CafeOBJ
Queues are first‐in & first‐out (FIFO) data structures(collections) and defined as follows:(1) empty is a queue (the empty queue).
(2) If e is an element and q is a queue, then e | q is a queue,
where e is the top of the queue.
Let e1, e2, e3 be elements. Some examples of queues are
e1 | empty
e1 | e2 | empty
e1 | e2 | e3 | empty

FY2019i628e information processing theory

CafeOBJQueues are specified in CafeOBJ as follows:mod! QUEUE(E :: TRIVerr) {[EQueue NeQueue < Queue]
op empty : -> EQueue {constr}
op _ | _ : Elt.E Queue -> NeQueue {constr}
op enq : Queue Elt.E -> NeQueue
op deq : Queue -> Queueop top : EQueue -> ErrElt.E
op top : NeQueue -> Elt.E
op top : Queue -> Elt&Err.E
op _ \in _ : Elt.E Queue -> Bool .
var Q : Queue vars X Y : Elt.E

10

FY2019i628e information processing theory

11

CafeOBJeq enq(empty,X) = X | empty .
eq enq(Y | Q,X) = Y | enq(Q,X) .
eq deq(empty) = empty .
eq deq(X | Q) = Q .
eq top(empty) = err .
eq top(X | Q) = X .
eq X \in empty = false .
eq X \in (Y | Q) = (if X = Y then true else X \in Q fi) .
}Equations are used as left‐to‐right rewrite rules:
enq(empty,X) → X | empty
enq(Y | Q,X) → Y | enq(Q,X)

FY2019-- (enq1)-- (enq2)

i628e information processing theory

12

CafeOBJ
enq(enq(enq(empty,e1),e2),e3) is rewritten (or computed)
as follows:enq(enq(enq(empty,e1),e2),e3)→ enq(enq(e1 | empty,e2),e3)→ enq(e1 | enq(empty,e2),e3)→ enq(e1 | e2 | empty,e3)→ e1 | enq(e2 | empty,e3)→ e1 | e2 | enq(empty,e3)→ e1 | e2 | e3 | empty
enq(empty,X) → X | empty
enq(Y | Q,X) → Y | enq(Q,X)

by (enq1)by (enq2)
by (enq1)by (enq2)
by (enq2)
by (enq1)-- (enq1)-- (enq2)

FY2019i628e information processing theory

13

CafeOBJ
CafeOBJ can do symbolic execution in a sense, whichmakes it possible to do theorem proving.
Let us prove ∀ : Elt. E ∀ : Queue top.

open QUEUE . ✔
op e : -> Elt.E .
op q : -> Queue .
red top(e | q) = e .
close
e denotes an arbitrary element.
q denotes an arbitrary queue.

FY2019i628e information processing theory

CafeOBJ
Let us prove ∀ , : Elt. E ∀ : Queue∈ enq ,
ifthen true else ∈ fi
It is proved by structural induction on q + case splitting.
✔
open QUEUE .
ops x y : -> Elt.E .
red x \in enq(empty,y) = (if x = y then true else x \in empty fi) .
close
open QUEUE .
Not yetops x y z : -> Elt.E .
op q : -> Queue .
eq X:Elt.E \in enq(q,Y:Elt.E) = (if X = Y then true else X \in q fi) .
red x \in enq(z | q,y) = (if x = y then true else x \in z | q fi) .
close

14

FY2019i628e information processing theory

15

CafeOBJ✔
open QUEUE .
ops x y z : -> Elt.E .
op q : -> Queue .
eq X:Elt.E \in enq(q,Y:Elt.E) = (if X = Y then true else X \in q fi) .
eq x = z . eq y = z .
red x \in enq(z | q,y) = (if x = y then true else x \in z | q fi) .
close✔
open QUEUE .
ops x y z : -> Elt.E .
op q : -> Queue .
eq X:Elt.E \in enq(q,Y:Elt.E) = (if X = Y then true else X \in q fi) .
eq x = z . eq (y = z) = false .
red x \in enq(z | q,y) = (if x = y then true else x \in z | q fi) .
close

FY2019i628e information processing theory

CafeOBJ✔
open QUEUE .
ops x y z : -> Elt.E .
op q : -> Queue .
eq X:Elt.E \in enq(q,Y:Elt.E) = (if X = Y then true else X \in q fi) .
eq (x = z) = false . eq y = z .
red x \in enq(z | q,y) = (if x = y then true else x \in z | q fi) .
close✔
open QUEUE .
ops x y z : -> Elt.E .
op q : -> Queue .
eq X:Elt.E \in enq(q,Y:Elt.E) = (if X = Y then true else X \in q fi) .
eq (x = z) = false . eq (y = z) = false . eq x = y .
red x \in enq(z | q,y) = (if x = y then true else x \in z | q fi) .
close

16

FY2019i628e information processing theory

17

CafeOBJ✔
open QUEUE .
ops x y z : -> Elt.E .
op q : -> Queue .
eq X:Elt.E \in enq(q,Y:Elt.E) = (if X = Y then true else X \in q fi) .
eq (x = z) = false . eq (y = z) = false . eq (x = y) = false .
red x \in enq(z | q,y) = (if x = y then true else x \in z | q fi) .
close

Each open-close fragment used in a proof score
corresponds to one leaf node in a proof tree.
Even if some open-close fragments are missing, CafeOBJ
complains at all.

FY2019i628e information processing theory

A running example
A mutual exclusion protocol called Qlock, an abstract
version of the Dijkstra binary semaphore.
Pseudo code for process p:
Loop “Remainder Section”
rs: enqueue(queue,p);
ws: repeat until top(queue) = p;
“Critical Section”
cs: dequeue(queue);
Each process p is located at rs, ws or cs.
Initially, p is located at rs & queue is empty.

18

FY2019i628e information processing theory

19

State machine & invariant
The set ⊆ of initial states≜State machine, ,A set of states

A binary relation
over states

⊆S

…
…
…

FY2019i628e information processing theory

State machine & invariant
The set(1) ⊆of reachable states wrt(2) If ∈&,∈ , then ′ ∈ .
…
…
…
…
…

20

FY2019i628e information processing theory

21

State machine & invariant
A state predicate ∶iff ∀ ∈.

→ Bool is invariant wrt∶ → Bool can be interpreted as the setstates s.t. ∈and vice versa.
…
…
…
…

of…
…
…
…
…

FY2019i628e information processing theory

State machine & invariant
An inductive invariant is a state predicate∶ → Bool that satisfies the following:(1) ∀ ∈(2) ∀ ,∈
⇒
…
…
…
…
…
…
…
…
…

22

FY2019i628e information processing theory

23

State machine & invariant
To prove that ∶ → Bool is invariant wrt , we needto find an inductive invariant ∶ → Bool s.t.
∀ ∈⇒.
Such

or part of suchis called a lemma of the proof.
…
…
…
…
…
…
…
…
…

FY2019i628e information processing theory

Formal specification
Treating states as black boxes but possible to observe
values from them. Given a state & a process ID ,queue

the content ofpc ,the location where process is locatedused in Qlock

queue & pc are called observer functions.
Let init be an arbitrary initial state.
empty .
eq queue init
eq pc init,
rs .

24

FY2019i628e information processing theory

25

Formal specification
ceq pc(want(S,I),J)= (if I = J then ws else pc(S,J) fi)
if c-want(S,I) .
ceq queue(want(S,I)) = enq(queue(S),I) if c-want(S,I) .
ceq want(S,I)=S
if not c-want(S,I) .
where c-want(S,I) = (pc(S,I) = rs)
spc(s,i)) = rs
Loop “Remainder Section”
rs: enqueue(queue);ws: repeat until top(queue) = p;
“Critical Section”
cs: dequeue(queue);

FY2019s' = want(s,i)

pc(s',i)) = ws
pc(s',j) = pc(s,j) if i jqueue(s') = enq(queue(s),i)want is called a transition functions.

i628e information processing theory

26

Formal specification
ceq pc(try(S,I),J)= (if I = J then cs else pc(S,J) fi)eq queue(try(S,I)) = queue(S) .
ceq try(S,I)=S

if c-try(S,I) .
if not c-try(S,I) .

where c-try(S,I) = (pc(S,I) = ws) and top(queue(S)) = I)
ss' = try(s,i)
pc(s,i)) = ws
top(queue(s)) = i
Loop “Remainder Section”
rs: enqueue(queue);ws: repeat until top(queue) = p;
“Critical Section”
cs: dequeue(queue);pc(s',i)) = cs
pc(s',j) = pc(s,j) if iqueue(s') = queue(s)try is called a transition functions.

jFY2019i628e information processing theory

27

Formal specification
ceq pc(exit(S,I),J)= (if I = J then rs else pc(S,J) fi)
if c-exit(S,I) .
ceq queue(exit(S,I)) = deq(queue(S)) if c-exit(S,I) .
ceq exit(S,I)=S
if not c-exit(S,I) .
where c-exit(S,I) = (pc(S,I) = cs)
spc(s,i)) = cs
Loop “Remainder Section”
rs: enqueue(queue);ws: repeat until top(queue) = p;
“Critical Section”
cs: dequeue(queue);

FY2019s' = exit(s,i)
pc(s',i)) = rspc(s',j) = pc(s,j) if i jqueue(s') = deq(queue(s))

exit is called a transition functions.

i628e information processing theory

Formal specification
Mutual exclusion property: there is always at most one
process in the critical section.
eq inv1(S:Sys,I:Pid,J:Pid)= (((pc(S,I) = cs) and pc(S,J) = cs) implies I = J) .
To verify that Qlock enjoys the property, it suffices toprove ∀ ∶ Sys ∀i, j: Pid inv1 s, i, j .
Sys is a sort (or type) of the reachable states of the statemachine formalizing Qlock & Pid is a sort (or a type) ofprocess IDs.

28

FY2019i628e information processing theory

29

Proof score
To prove ∀ ∶ Sys ∀i, j: Pid inv1 s, i, j , we first use
structural induction on s, Theorem of Constants and (aninstance of) the induction hypothesis.
✔
open QLOCK .
ops i j : -> Pid .
red inv1(init,i,j) .
close

FY2019open QLOCK .
Not yetop s : -> Sys .
ops i j k : -> Pid .
eq [:nonexec] : inv1(s,I:Pid,J:Pid) = true .
red inv1(s,i,j) implies inv1(want(s,k),i,j) .
close

i628e information processing theory

Proof score
open QLOCK .
Not yetop s : -> Sys .
ops i j k : -> Pid .
eq [:nonexec] : inv1(s,I:Pid,J:Pid) = true .
red inv1(s,i,j) implies inv1(try(s,k),i,j) .
close
open QLOCK .
Not yetop s : -> Sys .
ops i j k : -> Pid .
eq [:nonexec] : inv1(s,I:Pid,J:Pid) = true .
red inv1(s,i,j) implies inv1(exit(s,k),i,j) .
close30

FY2019i628e information processing theory

31

Proof score
To discharge the three cases (try, want & exit), we usecase splitting by adding some equations.
Based on the condition of each transition function, theresult returned by CafeOBJ for each open-close fragment,etc., we find equations to do case splitting.

FY2019i628e information processing theory

Proof score
open QLOCK .
Not yetop s : -> Sys .
ops i j k : -> Pid .
eq [:nonexec] : inv1(s,I:Pid,J:Pid) = true .
eq pc(s,k) = rs .
red inv1(s,i,j) implies inv1(want(s,k),i,j) .
close
open QLOCK .
✔
op s : -> Sys .
ops i j k : -> Pid .
eq [:nonexec] : inv1(s,I:Pid,J:Pid) = true .
eq (pc(s,k) = rs) = false .
red inv1(s,i,j) implies inv1(want(s,k),i,j) .
close

32

FY2019i628e information processing theory

33

Proof score
open QLOCK .
✔
op s : -> Sys .
ops i j k : -> Pid .
eq [:nonexec] : inv1(s,I:Pid,J:Pid) = true .
eq pc(s,k) = rs . eq i = k .
red inv1(s,i,j) implies inv1(want(s,k),i,j) .
closeopen QLOCK .
Not yetop s : -> Sys .
ops i j k : -> Pid .
eq [:nonexec] : inv1(s,I:Pid,J:Pid) = true .
eq pc(s,k) = rs . eq (i = k) = false .
red inv1(s,i,j) implies inv1(want(s,k),i,j) .
close

FY2019i628e information processing theory

Proof score
open QLOCK .
op s : -> Sys .
ops i j k : -> Pid .
eq [:nonexec] : inv1(s,I:Pid,J:Pid) = true .
eq pc(s,k) = rs . eq (i = k) = false .
red inv1(s,i,j) implies inv1(want(s,k),i,j) .
close

CafeOBJ returns the following for the open-close fragment:((((if (k = j) then ws else pc(s,j) fi) = cs) and ((i = j) and (pc(s,i) =cs))) xor (((pc(s,j) = cs) and ((pc(s,i) = cs) and ((i = j) and ((if (k = j)then ws else pc(s,j) fi) = cs)))) xor (true xor (((pc(s,j) = cs) and((pc(s,i) = cs) and ((if (k = j) then ws else pc(s,j) fi) = cs))) xor((pc(s,i) = cs) and ((if (k = j) then ws else pc(s,j) fi) = cs))))))

34

FY2019i628e information processing theory

35

Proof score
open QLOCK .
✔
op s : -> Sys .
ops i j k : -> Pid .
eq [:nonexec] : inv1(s,I:Pid,J:Pid) = true .
eq pc(s,k) = rs . eq (i = k) = false . eq j = k .
red inv1(s,i,j) implies inv1(want(s,k),i,j) .
close
open QLOCK .
✔
op s : -> Sys .
ops i j k : -> Pid .
eq [:nonexec] : inv1(s,I:Pid,J:Pid) = true .
eq pc(s,k) = rs . eq (i = k) = false . eq (j = k) = false .
red inv1(s,i,j) implies inv1(want(s,k),i,j) .
close

FY2019i628e information processing theory

Proof score
open QLOCK .
Not yetop s : -> Sys .
ops i j k : -> Pid .
eq [:nonexec] : inv1(s,I:Pid,J:Pid) = true .
eq pc(s,k) = ws . eq top(queue(s)) = k .
eq i = k . eq (j = k) = false . eq pc(s,j) = cs .
red inv1(s,i,j) implies inv1(try(s,k),i,j) .
close

Based on the three equations, we can conjecture thelemma:
eq inv2(S:Sys,I:Pid) = (pc(S,I) = cs implies top(queue(S)) = I) .

36

FY2019i628e information processing theory

37

Proof score
open QLOCK .
✔
op s : -> Sys .
ops i j k : -> Pid .
eq [:nonexec] : inv1(s,I:Pid,J:Pid) = true .
eq [:nonexec] : inv2(s,I:Pid) = true .
eq pc(s,k) = ws . eq top(queue(s)) = k .
eq i = k . eq (j = k) = false . eq pc(s,j) = cs .
red inv2(s,j) implies inv1(s,i,j) implies inv1(try(s,k),i,j) .
close

FY2019i628e information processing theory

Proof score
open QLOCK .
✔
op s : -> Sys .
ops i k : -> Pid .
eq [:nonexec] : inv1(s,I:Pid,J:Pid) = true .
eq [:nonexec] : inv2(s,I:Pid) = true .
eq pc(s,k) = cs . eq (i = k) = false . eq pc(s,i) = cs .
red inv1(s,i,k) implies inv2(s,i) implies inv2(exit(s,k),i) .
close∀ ∶ Sys ∀i, j: Pid inv1 s, i, j &∀ ∶ Sys ∀i: Pid inv2 s, i are proved bysimultaneous (structural) induction on s.

38

FY2019i628e information processing theory

39

SummaryQueues have been used as an example to describe formal(data) specifications in CafeOBJ and proof scores for data.
Qlock has been used as an example to describe formal(systems) specifications in CafeOBJ and proof scores forsystems.
Even if some open-close fragments, leaf nodes in a prooftree, are missing, CafeOBJ complains at all.
Thus, proof scores are subject to human errors.

FY2019i628e information processing theory

40SummarySome case studies have been done in which some security
protocols are formally verified with CafeOBJ and poof scores.
e‐commerce protocols, such as iKP and SET
Kazuhiro Ogata, Kokichi Futatsugi: Proof Score Approach to Analysis ofElectronic Commerce Protocols. International Journal of Software
Engineering and Knowledge Engineering 20(2): 253‐287 (2010)

authentication protocols, such as NSLPK and TESLA
Kazuhiro Ogata, Kokichi Futatsugi:Proof Scores in the OTS/CafeOBJ Method.
FMOODS 2003: 170‐184
Iakovos Ouranos, Kazuhiro Ogata, Petros S. Stefaneas: TESLA Source
Authentication Protocol Verification Experiment in the Timed OTS/CafeOBJ
Method: Experiences and Lessons Learned. IEICE Transactions 97‐D(5): 1160‐
1170 (2014)