An Introduction to Proof Equivalence

Teachers: Matteo Acclavio and Paolo Pistone

Classes are evey morning from 11h to 13h

Online resurces:

---

Course schedule

Day 1, 7 August: Overview and Motivations

• What is a proof?
• Two approaches to the problem of Proof Identity
• What is a proof system?
• Natural Deduction, Sequent Calculus and rule permutations.

In this class we discuss the notion of proof and how they can be formalized. After underlying the importance of defining a notion of proof equivalence, we provide the two main approaches to this problem we will explore during the course. We recall the definition of proof system by Cook-Reckhow and the sequent calculi and natural deduction systems for both classical and intuitionistic logic. We then analyze the standard rules permutations we can perform on sequent calculus derivations.

Slides and Notes

Bibliografy:

• Ideas and Results in Proof Theory
• Hilbert's Twenty-Fourth Problem
• The Problem of Proof Identity, and why computer scientists should care about Hilbert’s 24th problem

---

Day 2, 8 August: The Paradise of Syllogism and the Forbidden Fruit

• How much information is needed?
• Multiplicative Linear Logic, Proof nets, and units
• Are structural rules canonical?
• Canonicity of structural rules

We show the Multiplicative Linear Logic and how we can represent proofs using proof nets. We show their canonicity w.r.t. sequent calculus derivations. We show then show that as soon as units or structural behaviors are included in a system, then canonicity may become impossible to achieve.

Notes

Bibliografy:

• Proof nets for MLL
• Proof nets for MLL (linear time correctness criterion)
• No proof nets for MLL with units
• Slice nets (MALL)
• Conflic nets (MALL)

---

Day 3, 9 August: Normalization LJ and Denotationional Semantics

• Is natural deduction canonical?
• Natural deduction, normalization and canonicity
• What is a Denotational Semantics?
• Game semantics for Intiotionistic Propositional Logic

Notes Part 1

Slides Part 2

Bibliografy:

• Deciding equivalence in LJ (with conjunction)
• Game Semantic (introduction)
• Game Semantic (as presented, forget about modalities)

We show the canonicity of disjuntion-free fragment natural deduction with respect normalization and generality. Moreover, in presence of disjunction we can make obtain canonicity with respect to normalization but not with respect to generality. We then define the notion of denotational semantics. We show how a denotational semantics can be easily defined in term of quotient, we show how Game Semantics provides a concrete model for such a semantics.

---

Day 4, 10 August: Overview

• Why normalization is not suitable for proof equivalence in classical logic?
• Reducing non-determinism via Focusing
• How much non-determinism can we get rid of?
• Combinatorial Proofs for Classical Logic

Slides

Bibliografy:

• Focusing Gentzen's LK proof system (recorded talk)
• Towards Hilbert's 24th Problem: Combinatorial Proof Invariants
• ESSLLI 2021 course on Combinatorial Proof

We show the impossibility of having a non-trivial denotational semantics for classical logic by presenting Lafont critical pairs and Joyal's argument. We then present some refinement of sequent calculi allowing to reintroduce canonicity by reducing the non-determinism in proof search. We conclude by introducing the syntax of combinatorial proofs for classical logic, a graphical syntax suitable to provide a canonical representation of proofs. We discuss which rule permutations are captured by this syntax and we discuss the extension of this syntax to other logic.

---

Day 5, 11 August: Overview

• What about quantifiers?
• Proof equivalence in first and second order logic
• Why computer scientist should care about proof equivalence?
• Applications to real world problems

We introduce first and second order quantifiers, and the calculi for first and second order classical and intuitionistic logic. We show the additional challenges in proof equivalence for these logics, and the partial results in the literature. We conclude the course by illustrating applications of proof equivalence to verification, interoperability of theorem provers and suggests the current trends in proof theoretical approaches to programming language theory.

Slides

Bibliografy:

• System F

---

Security 2

Courses classes are Thursday form 9h45 to 11h15 online (the link is available on the moodle)

Online resurces

• Security Engineering (Ross Anderson): only for chapters 1, 8 and 9;
• notes on attack and attack-defence trees
• notes on access control
• Other notes on access control

Evaluation:

• Attack trees presentations (30%)
• Evaluation on information flows (20%)
• Homeworks on Proverif (50%)

---

Course schedule

Week 1, 18 February: Overview

• What does security mean?
• Secure systems need good design:
  • Evaluate potential risks
  • Risk assessment and cost models
  • Risk prevention/incentives

Suggested reading:

What Is Security Engineering

---

Week 2, 25 February: Attack Trees

• Risk management

  • security risk = possible damage
    • Identify risks
    • Reduce risks
    • Keep other risks under control during this operation
    • Repete...
  • Glossary:
    • Asset = something of Evaluate
    • Vulnerability = a weakeness of the system which can be exploited to harm the asset
    • Threat = exploitation of a vulnerability by a threat agent
    • Risk = quantification of a threat
    • Control = measure to reduce a risk
  • How to do risk analysis?
    • identify context
    • identify assets
    • assess risks
    • treat risks
  • Classify threats (impact vs likelihood)
  • Possible controls:
    • acceptance
    • avoidance
    • transfer
    • possible treatments: accept risks, reduce impact, reduce likelihood
  • Controls have costs or may not be 100% effective

• Attack Trees

  • free lunch tree example
  • threat Trees
  • fault Trees
  • Tree nodes are AND, OR, SAND, KofN ...

• Attack Trees semantics

  • Why semantics? (distinguis equivalent trees)
  • propositional/set semantics
  • multiset semantics

• Computing Attributes

  • possible attribute domains: cost, probability, possibility, time, ...
  • possibility = boolean circuits
  • cost = OR -> minimum of children values / AND -> sum of children values
  • probability = OR -> probability of union / AND -> probability of intersection

Suggested reading:

• Risk Analysis: Attack Trees & Other Tricks
• Original paper introducing attack trees
• Formalisation of attack trees semantics

---

Week 3, 4 March: free meal case study

• Attack trees Evaluation:
  • case analysis of the free-meal attack tree
    • loss
    • time
    • probability
• focus on nodes refinements types

---

Week 4, 11 March: Students presentations

During this class students will give short presentations of some attack trees they produce. Each presentation must include

• Presentation of the problem:

  • identify the attack
  • identify the context
  • cite if any source has been used to construct the tree (students are authorised to use public available material by citing it)
  • provide the attack tree of the chosen attack by justifying some design choices, e.g.:
    • why a conjunctive/disjunctive refinement
    • why only considering some refinements/node children and not others
    • ...
  • Minimal Tree Size:
    • minimal height = 2 , that is, there must be a path of lenght 2 from the root to a leaf
    • minimal width = 5 , that is, the tree must have at least 5 leaves

• Evaluations using the tree:

  • chose (at least) two attributes
  • explicit attribute domains. E.g., probabilities may be expressed in percentage, or using real numbers in the interval [0,1], or using some meta-attribute like impossible/unlikely/likely/surely
  • explicit how the attributes have been assigned to the leaves of the tree as public available statistics, experts evaluations... or as arbitrary decision of the student
  • chose who estimates the attributes (attacker or defender)
  • fix an evaluation method. By means of example, the cost value of a disjunctive node may be the minimum of the value of its children, while for the loss value of a disjunctive node we may be the maximum of the value of its children.

---

Suggested reading

• notes on attack and attack-defence trees
• if you are interested in fault-trees and other refinement node types: Parametric analyses of attack-fault trees

---

Week 5, 15 March (Matteo): Control Access Models

• Access control policies: determine who has access to what (and when) in a system
• Discretionary Access Control (DAC): users decide
  • each resource has an owner
  • each owner decides who has access to a resource
  • Troyan horse information leak: Alice owns a file Info which cannot be accessed by Bob. A Troyan-horse (executed as Alice) may read Info and copy on a file Stole owned by Bob, allowing Bob to read the content of Info.
• Mandatory Access Control (MAC): system decides
  • each user and security has a security Labels
  • if labels match some conditions, then access is guaranteed
  • resource access must not change during import/export of datas
• Role Based Access Control (RBAC): roles decides
  • each user has a role
  • roles determine access rights
• Principles:
  • least privilege: each user should have the minimal access privileges to accomplish its tasks
  • separating duties: avoid to have users with too much power
  • policies combination: combine policies for finer access control
• Terminology:
  • Users: active in the system.
  • Objects: passive in the system.
  • Access rights: read, write, execute, delede, create, switch, move, ...
  • System description: (S, O, A, M: S x O -> P(A)) where
    • S = set of subjects
    • O = set of Objects
    • A = set of access rights
    • M: S x O -> P(A) = matrix associating to every subject and object a set of access rights in A
  • in MAC there is also:
    • (L,>) = partially ordered set of labels
    • l: S U O -> L = labeling function associating a label to each object and subject

Bell LaPadula Model (MAC)

[The model preserves confidentiality but not integrity of data!]

• Simple security rule [or ss-rule] (no read up): a subject s can read an object o only if l(s)=l(o) or l(s)>l(o)
• *-Property (no write down): a subject s can write an object o only if l(s)=l(o) or l(s)<l(o)
• Discretionary security property [or ds-property]: users can grant access to objects according with ss-rule and *-property

State of a system

• (C, M, l) where
  • C = configuration / current access status: it is given by a set of triple of the form (s,o,a) in S x O x A
  • M and l are respectively the access matrix and the label function (which may be updated)
• Possible evolutions (operational semantic rules):
• add (s,o,a) to C when s get the access right a to o
• remove (s,o,a) from C when s release the access right a to o
• change l(s) when the security label of s is changed
• change l(o) when the security label of o is changed
• add a to M(s,o) to give s the access right a on o
• remove a from M(s,o) to rescind s the access right a on o
• a subset C of S x O x A may evolve to C' if C' may be obtained by applying operational semantic rules to C

Suggested reading

• Access Control: Policies, Models, and Mechanisms (skip sections 6->8)
• Multilevel Security
• Security Policies and Security Models

---

Week 6, 22 March (Matteo): Chinese Wall

• In the Bell-LaPadula model if a configuration C satisfies the ss-rule, *-property and ds-property, then any confuguration C' which may be obtained by applying operational semantic rules to C does.
• Troyan-horse example in Bell-LaPadula:
  • S:={Alice, Bob}
  • O:={Info, Stole}
  • M:=

    	Alice	Bob
    Info	Read, Write	None
    Stole	Read, Write	Read

  • (L,<):= ({top,bot} , top<bot)
  • l: S U O -> L:=
    l(Alice)=l(Info)=top and l(Bob)=l(Stole)=bot
  • the initial configuration is the empty one, the final configuration should be
    {(Alice, Info, Read), (Alice, Stole, Write), (Bob ,Stole , Read)}

Chinese Wall or Brewer-Nash (DAC + Mandatory access)

• objects have owners (companies databases)
• each company belongs to a conflic of interest class
• you can think that every object has a label (owner, owner's conflict of interest class)

• SS-rule: a subject s can read an object o belonging to a company x only if
  • s had no access to any object in a different company x' in the same conflict of interest class
• *-Property: a subject s can write an object o belonging to a company x only if
  • s have read access to o
  • s had read access only to objects in x's database

Suggested reading

• Access Control: Policies, Models, and Mechanisms (skip sections 6->8)
• Multilateral Security

---

Week 7, 1 April (Ross Horne): Hardware security:

---

Spring break (week of the 5th of April)

---

Week 8, 15 April (Sjouke Mauw): Intro to protocols

---

Week 9, 22 April (Ross Horne): students presentations on access control models

---

Week 10, 29 April (Sergiu Bursuc): Protocol verification inProverif

---

Week 11, 6 May (Semyon Yurkov): ePayment protocol proof in Proverif

---

Week 12, 13 May (Reynaldo Gil Pons): Mafia fraud proof in Proverif

---

Week 13, 20 May (Sergiu Bursuc): Advanced

---

Week 14, 27 May (Sergiu Bursuc): Advanced

CS2040 - Spring course 2020

Courses classes are on Monday, Wednesday and Thursday form 1h45 to 3h05 in room PL-5 (2bis, Passage Landrieu).

Textbook

INTRODUCTION TO. JAVA. PROGRAMMING (10th Edition) by Daniel Jiang

Tutor: Gavin Goerke

Online resurces

Java

• W3shool: usefull website with tutorial and explainations;
• geekforgeek: another usefull website;
• stackoverflow: if you have a really weird code problem, it probably has already be solved here;

Base 2 integer conversion

From base 10 to base 2 and

Linear Feedback Shift Register

• Wikipedia
• LFSR Introduction
• a simple tecnique to compute the feedback value

The "De Brujin" magic trick

!! their card encoding may not corresponds to the one proposed in this exercise!!

• the math behind;
• the trick in action 1
• the trick in action 2

Exceptions

Exceptions have to be excaptional!
Some in-depth articles on When and How to use or avoid exceptions:

• a general overview on exceptions in Java
• When and How to Use Exceptions
• How and When (Not) to Use Exceptions

JavaFX

If you have problems with JavaFX and eclipse on your laptop (like me), you can download IntelliJ (community version) and follow these instructions;

Program of the course

Date	Content	Assignments
Week 1: Gen 13	Introduction Introduction to the course and the course Web site Peergrade Compilers and IDE Introduction Slides !! Class only on Monday 13 !!	Ex1 Part1 try Part 2
Week 2: Gen 20 at 13h45 Gen 23 at 13h45 and at 15h20	Types Data type Program type Type casting An elementary encryption method: Caesar cipher Encrypting via LFSR No class on Wednesday 22, double class on Thursday 23	Write a Caesar cipher encripting program Finish Ex1 and upload the solution on peergrade. Revise course CS1040 topics: Chapters 1-8 of the book (see also myProgrammingLab exercises)
Week 3: Gen 27 at 13h45 Gen 29 at 13h45 Gen 30 at 13h45 and at 15h20	Objects and Classes What is a class? Unified Modeling Language this What is an object? Differences between objects and classes Why to use OOP? Programming paradigms (procedural vs OOP) here our zoo classes ! Double class on Thursday 30 !	Book chapter 9 Give feedback to at least 2 peergrade submissions myProgrammingLab exercises on book chapter 9 (at least the two projects at the end of the chapter)
Week 4 Feb 3 at 13:55 Feb 5 at 13:45 Feb 6 at 13:45	OOP thinking & Inheritance & Abstract Classes Why to use OOP? Data access Association Subclasses Inheritance super Override VS Overload Polymorphism here our new zoo ArrayList Excercise: social network (the code we wrote in class)	Book chapter 10 & 11 & 13 myProgrammingLab exercises on chapter 10 myProgrammingLab projects of chapter 11
Week 5 Feb 10 at 13:55 Feb 12 at 13:45 Feb 13 at 13:45	Excercises Some exercises on the point of the plane (solution w.i.p.) Solution of assignement 2	Assignement 2 Revise Book chapters 9-11 & 13 myProgrammingLab exercises on chapter 10 myProgrammingLab projects of chapter 11
17.2 - 28.2	Spring Break Revise Chapters form 1 to 11 and 13, focussing on 9-11 and 13. Pay attention to the following key concept summarized in the Chapters Summary (at the end of each Chapter): Chapter 2: 9-12, 17; Chapter 3: 1, 4-6; Chapter 4: 2, 8-11; Chapter 6: all; Chapter 7: 1-9; Chapter 9: all; Chapter 10: 1, 2, 3; Chapter 11: all; Chapter 13: 1-6, 9, 10;	Keep in practice with coding
Week 6 2.3	Midterm Exam Theory Test Programming Test ! No class on Wednesday 4 !	Book chapters 1-11 & 13
Week 7 9.3	Exception handling and Text I/O exceptions and exception handling Try-Catch File class create/rename/delede files write data to a file read data from a file Excercises ! No class on Monday 9 !	Book chapter 12.1-12.11 myProgrammingLab exercises on book chapter 12
Week 8 16.3	Excercises on File Exercises (folder zip download) ! No class on Monday 16 !	Book chapter 12.10-12.11 myProgrammingLab exercises on book chapter 12
Week 9 23.3	JavaFX the Application class and the method launch Scene,Stage and Pane Working with layouts Property binding Color and Font Solutions to File Exercises Scene Builder and Gluon are visual layout tools design GUI. First steps using scene builder. More details on using scene builder. With and without scene builder.	Book chapter 14, suggested order: from 14.1 to 14.4 -> 14.10 -> from 14.5 to the end First step tutorial: How to create a new windows A more detailed tutorial on JavaFX Send me your final project proposal [What kind of application you want to develop?]
Week 10 30.3	Event Driven Programming and some more JavaFX Event source MouseEvent KeyEvent Animations: Animation, PathTransition, FadeTransition, and Timeline Label and Buttons	Book chapter 15 untill 16.4 HW3 on peergrade Try to make run the boinching ball example a the end of chapter 15
Week 11 6.4	JavaFX and I/O Radio Button TextField PasswordField ComboBox and ListView To view and play video and audio	Book chapter 15 Start to implement the GUI of your final project Try to make this Connection Four look like this.
Week 12 13.4	Recursion Recursion in programming Factorial Fibonacci numbers Fractals	book chapters 17 and 18 Send me at least a static (does not change by user interaction) but working (that is compiling and showing all the components) graphical interface for your final project before Thursday the 16th.
Week 13 20.4	Recursion and Complexity Last project revision Recursion vs Iteration Complexity: O(n) notation What is the complexity of an algorythm? Complexity of sorting algorithms Complexity: 1000000$ Problems	Chapter 22-23 Send me your first version of the final project before Thursday the 23th
Week 14 27.4	class only on Monday: course recap and project revision. PROJECT DEADLINE THURSDAY 30th AOE
7.5	Final Exam, h12, room: PL-5

---

Course Syllabus

download