Nicolas Schnepf
email: nicolas.schnepf@inria.fr

Rémi Badonnel

Abdelkader Lahmadi

Stephan Merz

Rule-Based Synthesis of Chains of Security Functions for Software-Defined Networks

Keywords: Security Management, Software-Defined Networking, Android, Rule-Based Programming

Software-defined networks (SDN) o↵er a high degree of programmability for handling and forwarding packets. In particular, they allow network administrators to combine di↵erent security functions, such as firewalls, intrusion detection systems, and external services, into security chains designed to prevent or mitigate attacks against end user applications. These chains can benefit from formal techniques for their automated construction and verification. We propose in this paper a rulebased system for automating the composition and configuration of such chains for Android applications. Given the network characterization of an application and the set of permissions it requires, our rules construct an abstract representation of a custom security chain. This representation is then translated into a concrete implementation of the chain in Pyretic, a domain-specific language for programming SDN controllers. We prove that the chains produced by our rules satisfy a number of correctness properties such as the absence of black holes or loops, and shadowing freedom, and that they are coherent with the underlying security policy.

Introduction

Software Defined Networking (SDN) is a recent paradigm in the field of network management and security that promises to improve network programability by decoupling the data and control planes. In this context, the data plane consists in virtual switches and equipment responsible for forwarding tra c across the network, whereas the control plane consists in a single or multiple controllers, responsible for dynamically adjusting the configuration of the data plane in response to network events. The communication between the two planes is supported by a dedicated protocol, typically OpenFlow. SDN is oftenly used in conjunction with Network Function Virtualization (NFV) for supporting the automated deployment of more advanced security functions running in virtual machines in addition to virtual switches. Based on these new networking paradigms, researchers proposed the concept of chains of security functions for protecting end user applications against attacks. These chains are composed of di↵erent security mechanisms such as intrusion detection systems (IDS) or firewalls in cloud infrastructures for the protection of end users. The programmability introduced by software defined networks helps greatly for automating the configuration, adjustment, and deployment of chains of security functions. Programming SDN controllers is made simpler by the introduction of domain-specific programming languages such as Pyretic designed for implementing chains of security functions at a high level of abstraction before compiling them into low-level OpenFlow configuration rules. Nevertheless, the validation of chains of security functions remains nontrivial: the complexity of their internal security functions makes it incredibly easy to introduce misconfigurations and security holes that can then be exploited by attackers targeting these networks and their users. There exist several approaches for formally verifying chains of security functions a posteriori (cf. section 2). In this paper we propose an inference system based on Horn clauses for synthesizing chains of security functions in an automated manner, ensuring that the generated chains satisfy elementary correctness requirements. We specifically target the protection of network tra c generated by Android applications, taking into account security requirements derived from the observed networking behavior of an application and the set of operating-system level requirements that the application requires. We rely on our previous work [START_REF] Schnepf | Towards generation of SDN policies for protecting android environments based on automata learning[END_REF] for characterizing the networking behavior by learning a finite Markov chain that represents the network flows observed by a dedicated network probe. Using an inference system in order to construct a high-level representation of the security chain, we obtain a declarative description of the generation process that simplifies reasoning about the properties it guarantees, such as the consistency of the deployed security rules and the absence of loops. Our contributions are threefold: (i) we design a system of Horn clauses for the inference of chains of security functions that ensure certain correctness properties and that can be translated directly into Pyretic implementations, (ii) we propose a new representation of security requirements of Android end users, (iii) we have implemented a prototype of our method in Prolog. The remainder of this paper is organized as follows. Section 2 gives an overview of existing related work. Section 3 introduces background on network security. Section 4 describes the system of Horn clauses used for synthesizing SDN based chains of security functions. Section 6 discusses the correctness properties that are guaranteed by our solution. Section 7 concludes and points out future research perspectives.

Related work

Much work has been directed towards the detection of attacks: most approaches rely on packet analysis for detecting attacks [START_REF] Ain | Rank correlation for low-rate ddos attack detection: An empirical evaluation[END_REF][START_REF] Ensafi | Idle port scanning and non-interference analysis of network protocol stacks using model checking[END_REF][START_REF] Chen | Detecting early worm propagation through packet matching[END_REF]: these methods provide good accuracy; nevertheless the increasing mass of tra c to analyze in modern network require more e cient detection methods. In her PhD thesis, Anna Sperotto proposed to base the detection of attack on flow records instead of packet traces [START_REF] Sperotto | Flow-based intrusion detection[END_REF]: the objective of her work is to configure IDS depending on observed traces of attacks. Nevertheless, she does not consider data transmitted during exchanges and does not explore the possibility of deploying other security functions than IDS. Comparing detection methods requires dedicated datasets such as the CTU 13 [START_REF] García | An empirical comparison of botnet detection methods[END_REF] which contains botnet traces, but further datasets are necessary in order to capture other types of attacks such as DOS, port scanning or worm attacks. New perspectives for the protection of end users are introduced by the SDN paradigm: one possible approach consists in composing di↵erent security functions into chains [START_REF] Hurel | Towards Cloud Based Compositions of Security Functions for Mobile Devices[END_REF][START_REF] Hurel | Behavioral and Dynamic Security Functions Chaining for Android Devices[END_REF]. There exists various work in the literature that addresses the formal verification of such chains. For instance, Vericon [START_REF] Ball | Vericon: Towards Verifying Controller Programs in Software-Defined Networks[END_REF] is a framework in which properties to be guaranteed by network policies can be expressed and verified. Al-Shaer and Hamed [START_REF] Al-Shaer | Discovery of policy anomalies in distributed firewalls[END_REF] propose another approach for the discovery of anomalies in distributed firewalls, targeting in particular contradictions in large firewall policies. Those approaches focus on the verification of the data plane of chains of security functions but do not cover the validation of aspects related to the control plane. In addition, while these approaches are useful for validating a posteriori the correctness of policies w.r.t. pre-established criteria, they do not generate a policy according to these criteria, and they may miss configuration errors that are not covered by the specified properties.

We previously [START_REF] Schnepf | Automated verification of security chains in software-defined networks with Synaptic[END_REF] introduced the Synaptic checker for the verification of both control and data plane properties of an SDN policy. This checker relies on the Pyretic programming language [START_REF] Foster | Languages for Software-Defined Networks[END_REF], part of the Frenetic family of languages for programming SDN controllers [START_REF] Foster | Frenetic, a Network Programming Language[END_REF]. Pyretic is implemented as a domain-specific language embedded in Python for describing chains of rules at a level of abstraction well above that of actual SDN protocols, but from which OpenFlow rules can be compiled. Pyretic is complemented by an extension, called Kinetic, for describing control plane policies; Kinetic also o↵ers formal verification techniques based on model checking [START_REF] Kim | Kinetic: Verifiable Dynamic Network Control[END_REF]. Synaptic extends this formalism for verifying the correctness of both the control and data planes of Pyretic policies, before their deployment in the network. We also proposed [START_REF] Schnepf | Towards generation of SDN policies for protecting android environments based on automata learning[END_REF] an extension of the Synaptic checker with features for automatically learning network behaviors, represented as a Markov chain, of Android applications using their network flow traces. Our present paper is based on this technique and exploits it for the automatic generation of SDN policies satisfying the security requirements corresponding to such an application. Most methods for the validation of chains of security functions consider their correctness a posteriori, using techniques such as model checking [START_REF] Clarke | The birth of model checking[END_REF][START_REF] Forejt | Automated verification techniques for probabilistic systems[END_REF] or SMT solving [START_REF] Biere | Handbook of satisfiability[END_REF]. In this paper, we suggest a declarative technique for the automatic synthesis of such chains, expressed at a high level of abstraction. We express our technique in terms of Horn clauses and have prototypically implemented it in Prolog. This representation makes it easy to modify the rules in order to take into account varying end-user requirements, rather than hard-coded policies defined by operators. It also helps for formally establishing a priori certain properties that the generated chains ensure.

Background on network security

We introduce some background regarding network security, with respect to the attacks we consider, network programmability, Android environments, and profiling of applications.

Network flows and considered attacks

Our work is centered on the inference of chains of security functions based on a characterization of end-user applications in terms of network flows. According to RFC 5101 [START_REF] Claise | Specification of the IP Flow Information Export (IPFIX) Protocol for the Exchange of IP Tra c Flow Information[END_REF], network flows can be defined as "collections of IP packets passing through an observation point in the network during a certain interval". They are generally described by di↵erent properties such as IP version, source and destination IP addresses (srcaddr and dstaddr ), source and destination ports (srcport and dstport), network protocol (protocol ), and the numbers of packets and bytes (packets and bytes). In our context, they are collected directly on end-user devices [START_REF] Lahmadi | A platform for the analysis and visualization of network flow data of android environments[END_REF], and are extended with a timestamp (timestamp) and the name of the source application (appname). We furthermore complement this information with the name of the organization (orgname) responsible for the network that contains the destination IP address. As highlighted in [START_REF] Sperotto | Flow-based intrusion detection[END_REF], network flows are widely used for the detection of di↵erent categories of attacks, especially denial of service, port scanning, worms and botnets. A denial of service (DoS) attack is characterized by "one or more machines targeting a victim and attempting to prevent the victim from doing useful work" [START_REF] Handley | Internet Architecture Board: Internet Denial-of-Service Considerations[END_REF]. In our context, we will consider DoS attacks that are observable from a networking point of view, such as SYN flood attacks where a high number of SYN packets are sent to the same host in order to overload the TCP stack with open connections that will never been closed. In a port scanning attack, an application initiates connections with a wide range of ports of a machine (or several machines) in order to detect which ports are open. We will consider port scanning techniques such as those generated by the nmap port scanner, available on standard Linux platforms. A worm is a program that can run independently, will consume the resources of its host in order to maintain itself, and can propagate a complete working version of itself to other machines [START_REF] Malkin | Internet Users' Glossary[END_REF]. Worms replicate by exploiting the vulnerabilities of applications and operating systems or by social engineering methods. We will consider worms that scan a certain port on many di↵erent machines in order to exploit a specific vulnerability on operating systems. A (potentially) malicious bot is a program that is installed on a system in order to enable that system to automatically (or semi-automatically) perform a task (or a set of tasks) typically under the command and control of a remote administrator, called "bot master" [START_REF] Barthel | Routing Metrics Used for Path Calculation in Low-Power and Lossy Networks[END_REF]. These bots can be detected based on the high volume of tra c they exchange with their controller or possibly by the use of network protocols that are not commonly observed in a given context.

Network programming with Pyretic

Pyretic is a domain-specific programming language embedded in Python for the configuration of SDN controllers. It is based on fundamental blocks (called policies) that can be combined for generating more complex policies. In the remainder of this paper we will consider the following primitive policies and composition operators:

identity: forward all packets; given pattern (a regular expression); sequential (p1, . . . , pn): compose the policies {p1, . . . , pn} in sequence, also written p1 p2 for n = 2; parallel (p1, . . . , pn): compose the policies {p1, . . . , pn} in parallel, also written p1 + p2 for n = 2; negate(p): forward packets that are blocked by the policy p, and block those that are forwarded by p, also written ⇠ p. This language and its primitives will serve as a support for building and composing security functions for software-defined networks.

Focus on Android environments

We will target the protection of Android devices and their applications. In particular, we will rely on the Flowoid probe [START_REF] Lahmadi | A platform for the analysis and visualization of network flow data of android environments[END_REF] dedicated to Android devices and will use it for exporting network flow records of applications running on these devices. Given its position as the market-leading operating system for smart devices and the limited e↵ectiveness of preventive methods for proactively detecting malware applications, Android is particularly exposed to security attacks. For instance in 2016, Kaspersky Lab identified more than 3.5 million malware apps on the Google market store. In addition to the network flows previously mentioned, we will take into account the permissions that an application holds for accessing resources. An Android application must explicitly state the permissions it requires in its manifest file, and the security system of Android distinguishes between normal and (potentially) dangerous permissions. The former represents accesses to resources considered as non-critical, and they are automatically granted when requested. Dangerous permissions provide access to critical information such as user contacts, and they must be granted manually, when the application is installed. An application holding such a permission could use it to leak sensitive data to remote malicious servers. Therefore, the security chains that we generate include specific checks to prevent such attacks from occurring.

Automated network profiling of Android applications

We proposed in [START_REF] Schnepf | Towards generation of SDN policies for protecting android environments based on automata learning[END_REF] an algorithm for automatically learning a Markov model of the networking behavior of Android applications: this model is based on trace logs of the flows generated by an application, collected directly on the device by using the Flowoid probe [START_REF] Lahmadi | A platform for the analysis and visualization of network flow data of android environments[END_REF] that can associate flows with applications depending on the name of the package producer. These flow records are then transmitted to a centralized platform by using the NetFlow protocol in order to learn the communication pattern of the application: the first stage of our learning algorithm consists in aggregating destination IP addresses of flows depending on common owning organizations. This information is obtained from the result of whois requests, more specifically from the orgname and netname fields of the answers to such requests. Once flows have been completed by this information we build our Markov model of the application in the following manner: states are computed as collections of flows sharing the same orgname or netname; transitions are computed depending on the successions of orgnames or netnames in the input log; finally, probabilities are computed depending on the number of flow records in the input state and on the number of occurrences of the transition in the input log. Algorithm 1 shows the pseudo-code for the learning algorithm, and Fig. 1 contains the automaton obtained for the application Pokemon Go from a flow trace containing 150 flow records. In summary, the automaton represents the connections that the application establishes to addresses associated with di↵erent organizations.

Algorithm 1 Automaton learning algorithm. acterization of an Android application in terms of its network behavior and the permissions it holds. Our approach is based on the classification of the network tra c generated by an application as described in Sect. 3.4. We then use logic programming for deriving the functional specification of the security chain to be deployed, and finally generate an instance of such a chain using the Pyretic language for programming SDN controllers. Our work is presented in the context of Android protection, although it can be extended to any systems using similar permissions for protecting user data. Similarly, it is possible to consider other formats or implementations for the generation of chains of security functions, for instance by exploiting Network Function Virtualization (NFV) facilities.

Representing flows, traces, and security functions

Recall that flows are collections of packets sharing certain properties. We summarize a flow in a record that contains the key attributes of a flow. In the following, N and R + denote the sets of natural and non-negative real numbers, Addr = {0, 1} 32 and Port = {1, . . . , 65535} the sets of IP addresses and ports, Prot = {TCP , UDP , ARP , ICMP , . . .} the set of networking protocols and String the set of (ASCII) character strings. Definition 1. A flow f is a record that contains the following attributes and maps them to values in the corresponding domains:

f.timestamp 2 R + f.srcaddr 2 Addr f.dstaddr 2 Addr f.srcport 2 Port f.dstport 2 Port f.bytes 2 N f.packets 2 N f.protocol 2 Prot f.appname 2 String f.orgname 2 String
A flow trace is a sequence of flows such that time stamps are strictly increasing along the sequence. By abuse of notation, we will write f 2 t to indicate that flow f appears as an element of the sequence t. Given two traces t1 and t2, their merge t1 t2 corresponds to the unique trace formed by the elements of t1 and t2 in increasing order of time stamps, with the proviso that whenever t1 and t2 contain flows f1 and f2 with f1.timestamp = f2.timestamp, then f1 appears in t1 t2 while f2 is dropped. For an application app we will note tapp a flow trace such that f.appname = app for all flows f in the trace, and Papp the list of permissions it requests. We let D stand for the set of Android permissions qualified as dangerous.

Our approach aims at constructing a chain of security functions for protecting a specific application. Security functions transform network traffic, i.e. sequences of packets. Packets contain header fields similar to flows, except those that contain aggregate information such as packets and bytes, but they also contain a packet payload (field payload ) that represents the actual information transmitted in a packet. We overload the merge operation to apply to sequences of packets as well as to flow traces. Security functions are built by combining in parallel basic building blocks, called security rules, and they in turn give rise to chains by applying parallel or sequential composition. Rules, security functions, and chains transform flow traces, in particular through blocking certain tra c and modifying the values of certain header fields. Definition 2. A security function s is a function from tra c (i.e., a sequence of packets) to tra c. For an integer n 2 N, the function cut(t, n) returns the prefix of tra c t consisting of at most n packets. Given a predicate pred (p) on packets, we define the function restrict (t, pred ) that returns the subsequence of tra c t consisting of those packets satisfying pred . Security functions can be composed in sequence ( ) or in parallel ( +) where (s1 s2)(t) = s2(s1(t))

(s1 + s2)(t) = s1(t) s2(t)
and these operators generalize to n-ary compositions and +.

Classifying flows for learning security requirements

Our first objective is to classify the flows observed for an application according to the attack types mentioned in section 3.1. As introduced in Sect. 3.4, the network trace tapp generated by an application is represented by a Markov chain whose locations Lapp correspond to (not necessarily contiguous) sub-traces of tapp consisting of flows with the same orgname attribute. Transitions Tapp of the Markov chain are triples (l, p, l 0 ) for locations l, l 0 2 Lapp and a probability value p 2 [0; 1]. Observe that for any flow f 2 tapp, there is a unique location l 2 Lapp (corresponding to f.orgname) such that f 2 l; we denote this location as l f . The analysis of the transition probabilities that occur in the Markov chain, and in particular those associated with self-loops, is at the basis of detecting potential attacks such as denial of service, port scanning or worm tra c. We thus classify flows, and by extension their destination addresses, based on the following metrics defined for a flow trace t of length n > 1:

avg interval (t) = P n i=2 ti.timestamp ti 1.timestamp n 1 avg size(t) = P n i=1 ti.packets n count(x , t) = |{i 2 1 .. n : ti.dstaddr = x _ ti.dstport = x}| ports(t) = {p 2 Port : 9i 2 1 .. n : ti.dstport = p} protocols(t) = {p 2 Prot : 9i 2 1 .. n : ti.protocol = p}
In addition, bgp ranking(ip) denotes a value corresponding to a trust ranking measure of the IP address ip. In practice, this value is obtained by contacting a remote service.

We associate the following thresholds to the above metrics; appropriate threshold values are defined by the network operators and administrators.

attack limit: maximum probability of self looping transitions for considering a location of the automaton as normal; min interval : minimum acceptable interval time between the arrival of packets in a flow; min size: minimum number of packets in a flow; ip limit: maximum number of occurrences of an IP address; port limit: maximum number of occurrences of a port number; port scan limit: minimum number of port numbers contacted in a trace for considering it as a port scanning trace; unsafe threshold : maximum value of bgp ranking for considering an IP address as safe.

At the core of our approach lies a classification of the destination addresses a appearing in flows in tapp according to the following predicates that indicate whether a is suspected to be the target of an attack of the various types we consider: dos(a) ⌘ f 2 tapp ^a = f.dstaddr ^(l f , p, l f ) 2 Tapp p attack limit ^count(a, l f ) ip limit âvg interval (l f )  min interval ^avg size(l f )  min size port scan(a) ⌘ f 2 tapp ^a = f.dstaddr ^(l f , p, l f ) 2 Tapp p attack limit ^count(a, l f ) ip limit âvg interval (l f )  min interval ^avg size(l f )  min size | ports(l f ) | port scan limit worm(a, pt) ⌘ f 2 tapp ^a = f.dstaddr ^(l f , p, l f ) 2 Tapp p attack limit ^pt = f.dstport ^count(pt, l f ) port limit botnet(a, pt) ⌘ f 2 tapp ^a = f.dstaddr ^count(a, l f ) ip limit ^pt = f.dstport protocols(l f ) \ {"tcp", "udp"} 6 = ; ) avg interval (l f )  min interval unsafe(a) ⌘ f 2 tapp ^a = f.dstaddr ^bgp ranking(a) unsafe threshold safe(a) ⌘ ¬dos(a) ^¬port scan(a) ^¬worm(a, pt) ^¬botnet (a, pt) ^¬unsafe(a)

danger (a, pm) ⌘ f 2 tapp ^a = f.dstaddr ^pm 2 P f.appname \ D

In words, an address is considered to be the target of a potential attack if there exists a flow in tapp for which certain threshold values are exceeded. Addresses that are not the target of an attack are considered safe. In addition, the predicate danger records addresses that receive flows from an application that holds dangerous permissions. For example, a few properties derived for the Pokemon Go application, based on its automaton are given in Listing 1.

Inferring a high-level representation of the chain

We now present a rule-based program for inferring the chain of security functions that should be deployed on the basis of the observed trace, making use of the classification of flows that occur in the trace. In a nutshell, we start by associating elementary security rules with addresses that occur in the trace. These will be composed in parallel to build security functions such as firewalls or intrusion detection systems, which in turn are composed sequentially to form the entire chain. In the present section, security functions are represented symbolically; we will explain in section 4.4 how we translate this representation into the Pyretic language.

The elementary security rules make use of the following predicates that are defined externally: regexp(s, pm): true if the string s (representing the packet payload) matches a regular expression associated with the permission pm; tcp check (t): true if the network tra c t is a valid TCP connection; udp check (t): true if the network tra c t is a valid UDP connection; http check (s): true if the string s (representing the packet payload) is a valid HTTP request; inspect payload (s): true if the string s (representing the packet payload) passes deep packet inspection. Our system is based on the following elementary security rules: forward (a, t) = restrict (t, pk : pk.dstaddr = a) block (a, pt, t) = restrict (t, pk : pk.dstaddr 6 = a ^pk.dstport 6 = pt) limit(a, n, t) = cut(forward (a, t), n) filter (a, pm, t) = restrict (t, pk : pk.dstaddr = a ^regexp(pk.payload , pm)) inspect(a, t) = restrict (t, pk : pk.dstaddr = a ^inspect payload (pk.payload )) tcp(a, pt, t) = smShould forward (and deploy forward below) take a port parameter, just like block?

The inference system below determines which security rules to deploy for addresses appearing in the given flow trace. For each of the elementary security rules r above, a corresponding predicate deploy r indicates if the rule is to be instantiated, with additional parameters corresponding to the relevant IP address, port etc.

deploy block (a, pt) worm(a, pt)

deploy block (a, pt) botnet(a, pt)
deploy forward (a) ¬worm(a, pt) ^¬botnet(a, pt)

deploy limit (a, ip limit) dos(a)

deploy limit (a, ip limit) port scan(a)

deploy tcp (a, pt) f 2 tapp ^a = f.dstaddr ^pt = f.dstport ^f.protocol = "tcp" These chains are deployed for filtering tra c generated by the target application by subjecting addresses to the chains associated with the classes to which the address belongs.

deploy udp (a,
For the Pokemon Go application, we should deploy the chain corresponding to unsafe tra c. However, given that no dangerous permission is declared in the manifest file of this application, the DLP component of that chain is trivial and can be omitted in order to reduce the overall complexity of flow evaluation.

Generation of a Pyretic implementation of the chain

The last step of our approach consists in generating the Pyretic code implementing the abstract functions that we previously computed. Below we provide rewriting rules to derive Pyretic implementations corresponding to the elementary security rules introduced in section 4.3. In these rewrites, the argument of the security rules corresponding to the tra c t remains implicit in the Pyretic translation, which is applied to the current stream of packets. The functions DPIQuery, TCPFilter , UDPFilter , and

HTTPFilter are part of our Synaptic checker [START_REF] Schnepf | Automated verification of security chains in software-defined networks with Synaptic[END_REF] using dynamic query policies that Pyretic provides. The translations of the overall chains is then obtained by composing the Pyretic code sequentially or in parallel using the combinators and + of Pyretic. The following definitions indicate the implementations of the elementary security rules; forward (a, t) ; match(dstaddr = a) block (a, pt, t) ; ⇠ match(dstaddr = a, dstport = pt) limit(a, n, t) ; LimitFilters(n, dstaddr = a) filter (a, pm, t) ; match(dstaddr = a)

RegexpQuery(regexp(pm)) inspect(a, t) ; match(dstaddr = a) DPIQuery tcp(a, pt, t) ; match(dstaddr = a, dstport = pt) TCPFilter udp(a, pt, t) ; match(dstaddr = a, dstport = pt) UDPFilter http(a, pt, t) ; match(dstaddr = a, dstport = pt) HTTPFilter

To illustrate this last step of our inference system let us consider again our running example, the Pokemon Go application.

Performance evaluation

We implemented our inference system in SWI-Prolog (version 7.6.4). We evaluated the performances of the proposed solution through an extensive set of experiments. The experimental setup was based on a MacBookPro laptop with an Intel Core i7 (2.5 GHz) processor and 16 GB of RAM.

During these experiments, we considered a set of log files (more than 7000 network flows) captured from Android applications summarized in Fig. 2. These results clearly illustrate the high heterogeneity in the number of security functions and rules generated for each application. To minimize the impact of the deployment of several chains we designed a factorization algorithm presented in [START_REF] Schnepf | Automated factorization of security chains in software-defined networks[END_REF]: this algorithm allows us to group several chains of security functions into a larger one that contains only one occurence of each security function and at most as many security rules as the original chains.

In complement to these experiments we evaluated the accuracy of the di↵erent chains of security functions. We evaluated this metric by injecting a simple port scan of 50 flows in the log file of each application, and we quantify the accuracy as the ratio of the sum of true positive and true negative results over the total number of flows. Concretely, we used 70% of the logs for generating the chains and 30% for the evaluation. We also fixed a detection rate corresponding to the number of attack flows that must be matched before blocking the tra c and we varied this rate from 0 to 10; the corresponding results appear in Fig. 3 where we present the minimum, maximum and average accuracy measured for each chain. We again observe a high heterogeneity in the results obtained for each application: for some applications, the accuracy is very close to 100% while others have a minimal accuracy lower than 50%. This is again caused by the nature of each log file: for some applications the 30% of logs used for evaluation only contain IP addresses that where already known during the learning phase and are therefore accepted by the chain while other applications have more disparities in their logs. The improvement of these results will require joint work with researchers working on attack detection to design more elaborated methods of detection. The approach proposed in this paper decouples this phase from the inference of chains through first order predicates, and this makes it easy to change the method for detecting attacks without modifying the general process.

Correctness properties of the generated chains

The construction of security chains based on a high-level representation guarantees certain correctness properties that we now discuss. Specific correctness properties of chains can be verified using formal verification techniques such as model checking or SMT solving, and our previous contribution [START_REF] Schnepf | Automated verification of security chains in software-defined networks with Synaptic[END_REF] is intended for doing so; it is thus complementary to the work presented here.

Packet routing

Two elementary desirable properties of packet routing in networks are the absence of black holes and of loops. A black hole arises if packets are sent to a link at which no actual routing function is installed. A loop refers to a cycle in routing policies, so that packets may be sent back to a security function that they have already passed. Our security functions avoid these problems by construction.

Lemma 1. The security chains generated by the approach described in section 4 are free of black holes and of loops.

Proof. In our setup, security functions are total functions on sequences of packets, and they are built up from elementary security rules using parallel and sequential composition. In particular, every constituent of our chains is fully defined before it is used, so black holes do not exist at the abstract level of the descriptions of the chains. Similarly, the highlevel definitions of chains do not involve fixpoint operators or similar looping constructs. Finally, we rely on the close correspondence between the abstract chains and their Pyretic implementation and on the correctness of the Pyretic translator in order to ensure that the latter does not introduce black holes or loops.

Shadowing freedom and coherence

The two main correctness properties of chains of security functions that we are interested in are shadowing freedom and coherence. Shadowing freedom means that whenever two rules are composed in parallel within a chain, only one of them actually applies. This property ensures that there is no confusion in the sense that two rules could be applied with potentially conflicting results. In particular, this property implies the consistency of the rules, which requires that whenever two rules apply, they result in the same decisions. Coherence means that the tra c after applying the security chains satisfies the security requirements: safe tra c passes unchanged, whereas potentially dangerous tra c is either blocked or limited within acceptable bounds.

Lemma 2. The security chains generated by the approach described in section 4 guarantee shadowing freedom.

Proof. Elementary security rules are composed in parallel in the definitions of the basic security functions stateless firewall , ids, stateful firewall , dpi, and dlp. The definition of stateless firewall composes in parallel rules forward and block , which are potentially in contradiction. However, this is possible only if both deploy forward (a) and deploy block (a, pt) are true for some address a and port pt, and this is impossible due to the definitions of these predicates. Similarly, the parallel composition of the elementary security rules tcp, udp, and http in the definition of stateful firewall is unproblematic because the definitions of the corresponding predicates deploy tcp , deploy udp , and deploy http are mutually exclusive.

We now show that our security chains are coherent with the security policy determined on the basis of the trace tapp underlying their generation.

Lemma 3. Given a trace tapp characterizing the network tra c generated by an application, the security chains generated by the approach described in section 4 transmit unchanged the tra c towards addresses considered as safe but block or limit network tra c towards other addresses.

Proof. An address is considered as potentially not safe if tapp contains some flow towards that adress classified as worm, botnet, dos, port scanning or unsafe. The stateless firewall applied as the first security function in the chain will directly block packets towards IP addresses associated with worm and botnet tra c. Concerning tra c directed to addresses associated with DoS or port scanning attacks, it will pass the stateless firewall and will subsequently be transmitted to the IDS. The tra c will then be limited to a number of packets bounded by the fixed threshold ip limit, considered to be acceptable by the security policy.

For addresses associated with unsafe flows, i.e., network tra c potentially compromising sensitive data, the security chains contain the security functions DPI and DLP that check the payload of packets. These apply the security policy by blocking packets that do not match the criteria defined by the predicates regexp (associated with Android permissions) and inspect payload . Tra c towards addresses classified as safe is only subject to the stateless firewall, which lets it pass unchanged.

Conclusions and future work

We proposed in this paper a declarative approach based on inference rules for automating the generation of chains of security functions, based on the requirements of end users. This inference system is intended to protect Android applications, by taking into account both their networking behavior and the OS-level permissions that they request. By using first-order predicates for classifying network tra c observed in the flow trace -rather than for example finite state machines -the composition and factorization of security chains to be applied for several applications becomes straightforward. Our system infers a high-level representation of the security functions, which can be translated into a concrete implementation in the Pyretic language for programming software-defined networks. We showed that the generated chains satisfy several desirable properties such as the absence of black holes and of loops, shadowing freedom, and that they are consistent with the underlying security policy.

Further correctness properties of the chains can be verified using our Synaptic checker [START_REF] Schnepf | Automated verification of security chains in software-defined networks with Synaptic[END_REF] based on symbolic model checking and SMT solving. The main assumption underlying our approach is that the networklevel behavior of Android applications can be characterized in terms of flow traces that are collected before the security chains are generated, and that are analyzed o✏ine, as described in our previous work [START_REF] Schnepf | Towards generation of SDN policies for protecting android environments based on automata learning[END_REF] on process learning. This assumption holds for many, but not all Android applications, a Web browser being a typical counter-example. In that case, network administrators must install a default security chain.

An interesting extension of our present work would be to consider which parts of the analysis are su ciently lightweight to be performed online.

As further perspectives, we are also planning to work on optimizing and improving the parameterization of the security chains that are generated by our inference system. In addition, we are interested in investigating to what extent our solution is compatible with network function virtualization techniques (NFV) to implement security functions, such as firewalls and intrusion detection systems.

  drop: block all packets; match(x1 = y1, . . . , xn = yn): forward those packets whose header fields xi contain the values yi; modify(x1 = y1, . . . , xn = yn): forward all packets but modifies their header fields xi to the values yi; count packets(x1 = y1 , . . . , xn = yn ): count the number of packets whose header fields xi contain the values yi; -LimitFilters(k, x1 = y1, . . . , xn = yn): forward a maximum of k packets whose header fields xi contain the values yi; -RegexpQuery(pattern): forward packets whose payload matches the

Fig. 1 .

 1 Fig. 1. Automaton describing the behavior of an Android application.

  States := ; Transitions := ; Flows :=List of flows. . Initialize the set of states flow := Flows[0 ] States[flow ] := 1 . Count occurrences of states and transitions for i 2 1..N do transition := (flow , Flows[i]) flow := Flows[i] if flow 2 States then States[flow ] += 1 else States[flow ] := 1 end if if transition 2 Transitions then Transitions[transition] += 1 else Transitions[transition] := 1 end if end for . Compute the probabilities of transitions for transition 2 Transitions do Transitions[transition] := Transitions[transition]/States[transition.srcState] end for

  pk : pk.dstaddr = a ^pk.dstport = pt) if tcp check (t) hi otherwise udp(a, pt, t) =

  pk : pk.dstaddr = a ^pk.dstport = pt) if udp check (t) hi otherwise http(a, pt, t) = restrict (t, pk : pk.dstaddr = a ^pk.dstport = pt ^http check (pk.payload ))

  Port } dpi(t) = +{ inspect(a, t) : deploy inspect (a), a 2 Addr } dlp(t) = +{ filter (a, pm, t) : deploy filter (a, pm), a 2 Addr, pm 2 D } Continuing our example of the Pokemon Go application, we obtain a chain containing the following security functions. (We omit the full definitions since the inference system generates too many security rules, but show the overall structure of each security function.)statelessfirewall (t) = forward (169 .45 .223 .16 , t) + forward (169 .45 .223 .20 , t) + . . . stateful firewall (t) = tcp(169 .45 .223 .16 , 80 , t) + tcp(169 .45 .223 .20 , 80 , t) + . . . http(169 .45 .223 .20 , 80 , t) + . . . dpi(t) = inspect(169 .45 .223 .16 , t) + inspect(169 .45 .223 .20 , t) + . . . These security functions are in turn composed into chains to be applied to the network tra c of the di↵erent types:

	safe chain = stateless firewall	stateful firewall
	unsafe chain = stateless firewall	stateful firewall	dpi	dlp
	dos chain = stateless firewall	ids	stateful firewall
	port scan chain = dos chain
	worm chain = stateless firewall
	botnet chain = stateless firewall

pt) f 2 tapp ^a = f.dstaddr ^pt = f.dstport pt 6 = 80 ^pt 6 = 443 ^f.protocol = "udp" deploy http (a, 80) f 2 tapp ^a = f.dstaddr ^f.dstport = 80 deploy http (a, 443) f 2 tapp ^a = f.dstaddr ^f.dstport = 443 deploy filter (a, pm) unsafe(a) ^danger (a, pm)

deploy inspect (a) unsafe(a)

Based on the predicates deploy r inferred to be true from a given trace tapp characterizing the network behavior of the application we wish to protect, we now construct security functions by composing elementary rules in parallel. stateless firewall (t) = +{ forward (a, t) : deploy forward (a), a 2 Addr } + +{ block (a, pt, t) : deploy block (a, pt), a 2 Addr, pt 2 Port } ids(t) = +{ limit(a, n, t) : deploy limit (a, n), a 2 Addr, n 2 N } stateful firewall (t) = +{ tcp(a, pt, t) : deploy tcp (a, pt), a 2 Addr, pt 2 Port } + +{ udp(a, pt, t) : deploy udp (a, pt), a 2 Addr, pt 2 Port } + +{ http(a, pt, t) : deploy http (a, pt), a 2 Addr, pt 2

  Network flows of Android applications considered during experiments, with the number of combinations of IP addresses and ports they contact, and the number of security functions (sf) and rules for the generated security chain. stateless firewall = match(dstaddr = 169 .45 .223 .16 ) + match(dstaddr = 169 .45 .223 .20 ) + . . . stateful firewall = match(dstaddr = 169 .45 .223 .16 , dstport = 80 ) TCPFilter + match(dstaddr = 169 .45 .223 .20 , dstport = 80 ) TCPFilter + . . . + match(dstaddr = 169 .45 .223 .20 , dstport = 80 ) HTTPFilter + . . .

	applications # flows # IP/ports # sf # rules
	disneyland	282	5	4	44
	dropbox	1000	17	5	311
	faceswitch	151	30	5	425
	lequipe	1000	208	4	1640
	meteo	1000	89	4	716
	ninegag	1000	124	4	930
	pokemongo	275	24	5	485
	ratp	779	3	4	28
	skype	1000	442	5	6529
	viber	1000	176	5	4163
	Fig. 2. dpi = match(dstaddr = 169 .45 .223 .16 )	DPIQuery +
	match(dstaddr = 169 .45 .223 .20 )	DPIQuery + . . .
	chain = stateless firewall	stateful firewall	dpi
					The security func-
	tions introduced previously are converted into the following chain of se-
	curity functions.

  Accuracy of the chains generated for each application.

	Application Avg. Acc. Min. Acc. Max. Acc.
	viber	0.683	0.502	0.997
	faceswitch	0.812	0.518	0.990
	dropbox	0.997	0.993	1.000
	ninegag	0.509	0.498	0.526
	disneyland	0.992	0.986	1.000
	pokemongo	0.743	0.512	0.994
	skype	0.998	0.998	0.998
	lequipe	0.518	0.496	0.537
	meteo	0.837	0.510	0.998
	ratp	0.940	0.692	0.999
	Fig. 3.

Automated synthesis of chains of security functionsWe propose in this paper a strategy based on rule-based programming for the automated inference of chains of security functions, based on a char-


Lathiful Anwar
email: l.anwar@rug.nl

Martin Goedhart

Understanding geometric proofs: scaffolding pre-service mathematics teacher students through dynamic geometry system (dgs) and flowchart proof

Keywords: Understanding, geometry, proof

The objective of this paper is to discuss the pedagogic potential that is offered by the use of a flowchart proof with open problems and a Dynamic Geometry System in understanding geometric proofs by pre-service mathematics student teachers at an Indonesian university. Based on a literature review, we discuss aspects and levels of understanding of geometric proof and how to assess students' understanding of the structure of deductive proofs, and how the use of a Digital Geometry System may support students' understanding of geometric terms and statements, including definitions, postulates, and theorems. The pedagogic focus consists of exploiting the semiotic potential of a DGS, especially the use of GeoGebra tools that may function as tools of semiotic mediation to understand the geometry statements and the scaffolding potential of flowchart proof with open problems in identifying the structure of deductive geometry proofs.

Introduction

Proof plays essential roles in mathematics and mathematics education. Proofs help mathematicians understand the meaning of statements or theorems and their validity within a framework. Through the process of proving, mathematicians discover or create new results or meanings [START_REF] Samkoff | Lessons learned from an instructional intervention on proof comprehension[END_REF][START_REF] Zaslavsky | The Need for Proof and Proving: Mathematical and Pedagogical Perspectives[END_REF]. In the context of mathematics learning, understanding proof is an essential component of mathematics competence as it offers powerful ways of developing and expressing mathematical understanding [START_REF] Nctm | Principles and Standards for School Mathematics[END_REF]. However, research has demonstrated that students at all levels have difficulties to deal with understanding and constructing proofs [START_REF] Doruk | Prospective mathematics teachers' difficulties in doing proofs and causes of their struggle with proofs[END_REF][START_REF] Güler | The Difficulties Experienced in Teaching Proof to Prospective Mathematics Teachers: Academician Views[END_REF][START_REF] Knapp | Learning To Prove in Order To Prove To Learn[END_REF][START_REF] Weber | Student Difficulty in Constructing Proofs : The Need for Strategic Knowledge[END_REF]. This paper presents some findings of the literature review we conducted aiming at developing a theoretical framework, which will underpin the design of a learning intervention. This intervention will foster understanding of Euclidean geometry proof by mathematics preservice teacher students. The students are first year students at an Indonesian university and will become teachers for secondary school. In this stage, students start to learn formal mathematical proof for the first time. This paper describes the aspects and levels of understanding of geometric proof and elaborate the use of a digital geometry system (DGS) and flow-chart proof representation as scaffolds in order to understand the structure of proof based on our literature review findings. We focus on these issues because they are relevant for our research project regarding the topic (geometric proof in undergraduate level), context and characteristics of participants, Indonesian university students, who have a little mathematical proof background.

Method

This paper presents some parts of the outcomes of our literature study which focuses on the understanding of proof and the use of DGS and flow-chart proof to support students' understanding of proof. The methodological process of the literature study is anasynthesis (coined from the words analysis and synthesis) adapted from Legendre's method (as cited in [START_REF] Jeannotte | A conceptual model of mathematical reasoning for school mathematics[END_REF]. First, we create a corpus from a search in three databases of research, namely ERIC, MathEduc, and Web of Science, and select articles/papers having mathematical proof as keywords or associated keywords by entering 'mathematic* proof' or 'mathematical prov*' and 'geometric* proof' or geometrical prov*' as keywords. It is followed by selection and un-doubling. To assure the quality of the sources, we characterized the papers regarding their relevance of method and findings for education, quality of author (the number of citations) and quality of journal (impact factor). By the end of the process, 32 English texts (books, chapters, articles, and research reports in proceedings) constituted the corpus (modified corpus).

Secondly, the resulting corpus is analyzed for relevant information, namely definitions of mathematical proof, structure of proof, learning difficulties, interventions, role of teacher, successful approaches. In order to analyze, we created a matrix of the resulting corpus consisting of four main aspects: source, research context, method, outcomes/conclusions. Thirdly, the information is then synthesized to check convergences, divergences, and to identify the theoretical gaps. Underpinned by this research, we developed a framework and prototype for a teaching intervention to foster prospective teacher's geometrical proof competence. We present this process of analysis and synthesis as linear, but the reader should consider that it is a cyclical process, see Figure 1.

Framework underpinning understanding of geometrical proof

While the ability to understand, construct and validate proofs is central to mathematics, student difficulties with understanding of proof are well-recognized internationally. In order to help students to understand, teachers need to know levels of understanding to be achieved by their students, and also potential tools and tasks scaffolding their thinking. This information is helpful for the teachers/researchers in designing their learning goals and a sequence of learning activities fostering students' understanding of proofs. As a result of our literature review, we present, in this part, our framework regarding aspects and levels of understanding as frameworks to develop an assessment model to capture students' understanding of geometrical proof, and, next to that, potential tools and methods which can be implemented in the classroom intervention to scaffold students' thinking in constructing geometric figure, emerging the meaning of geometric concepts, axioms and theorems.

Understanding of geometrical proof

Based on literature on reading comprehension of geometry proofs [START_REF] Yang | A model of reading comprehension of geometry proof[END_REF], the assessment model of proof comprehension for undergraduate students (Mejia-Ramos, Fuller, [START_REF] Mejia-Ramos | An assessment model for proof comprehension in undergraduate mathematics[END_REF], and students' understanding of the structure of deductive proof (Miyazaki, Fujita, & Jones, 2017), we distinguish three essential aspects in understanding proofs, namely a functional aspect, a structural aspect, and a communicative aspect. These three aspects are inspired by three main aspects of proof and proving proposed by Miyazaki et al. (2017): "understanding a proof as a structural object, seeing proof as intellectual activity and the role, functions, and meaning of proof and proving" (Miyazaki, Fujita, & Jones, 2017, page 225).

First of all, the functional aspect regards roles or functions of proofs. The 'function' of proof means the meaning, purpose and usefulness of a proof. In the context of learning, students should regard proof as a meaningful activity, experiencing the functionality (usefulness) of the activities, they are involved in. Second, the structural aspect refers to the deductive structure of proofs. Miyazaki et al. (2017) see the structure of a proof as a network of singular and universal propositions between premises and conclusions, connected by universal instantiation and hypothetical syllogism, see Figure 2. That means that the singular propositions are universally instantiated from universal proposition and then these singular propositions are connected by a hypothetical syllogism. Students need to know the meaning of these terms and statements (e.g. axioms, theorems) involved in a proof, recognize the status of the statements (e.g. premises, conclusions), to be able to justify the claim. The last aspect, the communicative aspect regards to students' intellectual activity to read and comprehend proofs, and to justify and persuade others about the validity of a proof. Through a validating process, students determine the truth of a proof by line-by-line checking or step-by-step checking of multi-step proofs using their understanding of the structure of deductive proofs. We interpret that this level of understanding relates to a holistic comprehension of proof where the proof is understood in terms of main ideas, methods and applications in other contexts.

Related to the level of understanding, we elaborate two models of understanding of proofs by Mejia-Ramos and colleagues (2012) and by Miyazaki and colleagues (2017). In their model of levels of structural proof understanding, Miyazaki and colleagues distinguish three levels of understanding of proof structure, namely 'Pre-structural' level, 'Partial-structural' level, and 'Holistic-structural' level. Then, they break down the second level into two sub-levels, 'Elemental' and 'Relational sub-level'. At the first level (Pre-structural), students see a proof as a collection of meaningless symbolic objects. When students start to consider the components, they are at the second level, particularly the Partial-structural Elemental sub-level. At the Partial-Structural Relational sub-level, students understand hypothetical syllogisms and universal instantiations and are able to use theorems, axioms and definitions as supporting their reasoning. At the third level of understanding (holistic-structural), students understand the components, inter-relationships between those components and how to connect them. Then, they are able to reconstruct the proof and become aware of the hierarchical relationship between theorems and will be able to construct their own proofs.

Mejia-Ramos et al.( 2012) have developed a model of assessment for proof comprehension in undergraduate mathematics. They distinguish two levels of understanding of proof, namely a local and a holistic understanding. The local understanding refers to knowing of basic terms and statements in the proof, knowing the logical status of statements in proof and the logical interrelationship between them and the statement which will be proved, and able to justify oh how the claims in the proof follows from the previous statements. Meanwhile, the holistic understanding regards being able to summarize the main idea of the proof, to identify the sub-proofs and the logical relationship between them, to adapt the idea and procedures of proof to solve other proving tasks, and to illustrate the proof regarding its relationship to specific examples.

A semiotic potential of the use of dynamic geometry system (dgs)

In terms of the structural aspects of understanding proof, several studies confirmed that the use of a Dynamic Geometry System (DGS) may help students not only solve construction problems but also helped them to understand geometrical postulates, definitions and theorems of Euclidean geometry, which are elements of the structure of proof [START_REF] Jiang | Developing Preservice Teachers' Mathematical Reasoning and Proof Abilities in the Geometer's Sketchpad Environment[END_REF][START_REF] Mariotti | Proof and proving in the classroom: Dynamic Geometry Systems as tools of semiotic mediation[END_REF][START_REF] Mariotti | Introducing students to geometric theorems: How the teacher can exploit the semiotic potential of a DGS[END_REF]. [START_REF] Mariotti | Introducing students to geometric theorems: How the teacher can exploit the semiotic potential of a DGS[END_REF] summarized that the semiotic potential of the features of DGS relates to specific mathematical meanings, namely "(1) the dragging test can be related to the theoretical validation of a geometric construction, (2) specific tools can be related to specific elements of the corresponding geometry theory: postulates, theorems; (3) actions concerning the management of the DGS's menu can be related to fundamental meta-theoretical actions concerning the construction of a theory, such as the introduction of a new theorem or a definition." (Mariotti, 2013, pp. 444-445). In the following paragraph, we elaborate two studies about the use of DGS in supporting students' ability in proving.

A study by [START_REF] Jiang | Developing Preservice Teachers' Mathematical Reasoning and Proof Abilities in the Geometer's Sketchpad Environment[END_REF] investigates learning processes of two pre-service teachers, Lisa and Fred, in exploring geometry problems using the dynamic geometry software Geometer's Sketchpad (GSP) to develop mathematical reasoning and proof abilities. They use a constant comparison approach in order to analyze participants' pre-tests, post-tests, and teaching interviews indicating that the geometer's Sketchpad can not only encourage students to make conjectures but also enhances students' mathematical reasoning and proof abilities. Particularly, the use of a Dynamic Geometry System (DGS) improves students' level of geometric thinking in terms of van Hiele levels (e.g. Lisa's level increased from level 3 to level 4) and positively changes students' conceptions of mathematics and mathematics teaching. Jiang argues that pre-service teachers' experience in using DGS to foster their mathematical reasoning and proof abilities helps them to recognize the need to improve students' knowledge of geometry, to develop their own mathematical power and their ability to develop teaching innovations.

A theoretical study by [START_REF] Mariotti | Proof and proving in the classroom: Dynamic Geometry Systems as tools of semiotic mediation[END_REF] discusses the potential offered by the use of DGS in supporting and fostering 9 th and 10 th grade student's proof competence in geometry. The theoretical framework used to support the use of DGS, Cabri Geometer, is her own Theory of Semiotic Mediation (TSM). In this context, students' personal meanings emerge and then evolve from personal meanings towards mathematical meanings, when students use an artefact for accomplishing a task through social interaction. Particularly, the specific DGS tools can also be related to geometrical axioms and theorems. Meanings emerging from the use of virtual drawing tools for solving geometry tasks can be related not only to the theoretical meaning of geometry construction but also the meaning of theorems. [START_REF] Mariotti | Proof and proving in the classroom: Dynamic Geometry Systems as tools of semiotic mediation[END_REF] argues that the DGS could support not only the conjecturing process, but also mediate the mathematical meaning of conjectures, particularly premises/singular propositions in the context of geometry proofs. Particularly, the dragging feature provided by DGS (Cabri software) supports the emergence of different meanings related to the notion of conjecture as a conditional statement relating a premise and a conclusion. Mariotti also discusses findings by Baccaglini-Frank (2010) focused on the analysis of the process of exploration that can be expected by using Maintaining Dragging (MD). Baccaglini-Frank's teaching experiment involves students from three high schools (aged 15-18), which used Cabri in the classroom. Mariotti concludes that this teaching experiment indicates that the DGS tools and dragging activities help students to solve construction tasks and to understand the notion of theorems; particularly the mathematical meaning of conditional statements such as expressing the logical dependency between premises and conclusions.

GeoGebra as another DGS is an open-source well-developed tool with a stable interface familiar to many users and works in any operating system. The software has a number of features such as dynamic geometry which can help students in steps of problem solving towards a proof [START_REF] Botana | Automated Theorem Proving in GeoGebra: Current Achievements[END_REF]. [START_REF] Botana | Automated Theorem Proving in GeoGebra: Current Achievements[END_REF] conclude that GeoGebra tools provide some useful features. Firstly, GeoGebra could not only give yes/no answers but could also show step-by-step explanations. Secondly, GeoGebra could identify properties on the construction of geometric figures. Thirdly, GeoGebra could give a counterexample to check the truth of a statement. However, research findings by [START_REF] Doruk | Pre-service elementary mathematics teachers' opinions about using GeoGebra in mathematics education with reference to "teaching practices[END_REF] show that some preservice teachers highlighted some limitations, such as difficulties in translating mathematical expressions into GeoGebra. Preservice teachers thought that GeoGebra is a complicated program and that it would take a long time and needs a big effort to become competent in GeoGebra.

A scaffolding potential of the use of flow-chart proof form with open problems

A flow-chart proof form is a means to visualize the deductive connections from premises to conclusion by identifying singular and universal propositions in the chart, see Figure 2. Flow-chart proofs show a storyline of the proof starting with premises from which the conclusion is deduced and includes the theorems or/and axioms being used, how the premises/hypotheses and conclusion are connected, and so on [START_REF] Miyazaki | Flow-chart proofs with open problems as scaffolds for learning about geometrical proofs[END_REF]. Gardiner (2004, cited in Miyazaki, Fujita, & Jones, 2017) claims that this format is a good starting point to learn other formats of proofs such as narrative proofs and two-column proofs. [START_REF] Miyazaki | Introducing the structure of proof in lower secondary school geometry: a learning progression based on flow-chart proving[END_REF] developed a learning progression based on flow-chart proving aimed at providing a basis for introducing the structure of proof in Grade 8 school geometry. Based on the theoretical underpinning of the design, researchers proposed three phases of learning progression: (1) constructing flow-chart proofs in an open problem, (2) constructing a formal proof by reference to a flow-chart proof in a closed situation, (3) refining formal proofs by placing them into a flow-chart proof format in a closed situation. The term 'open' refers to a situation where students can construct more than one suitable proof. In the open problem task, students are given a conclusion of the proof in the form of flow-chart proof format, and they are asked to determine the suitable statements to fill in the blank boxes of the flow-chart so the proof is complete. Based on three phases of learning progression, the authors designed nine lessons considering open/closed situations, varying steps of deductive reasoning, and different problems and contexts. The results from a Math test of Japanese Survey Item shows that students who followed the nine lessons are more likely to plan and construct a proof in accordance with their plan. This is due to (a) their experience with open problems that encourage them to think backward and forward to identify assumptions and conclusions in proof, (b) they could grasp the structure of proofs better through using flow-chart proofs.

Another research by [START_REF] Miyazaki | Flow-chart proofs with open problems as scaffolds for learning about geometrical proofs[END_REF], as follow-up of their previous study [START_REF] Miyazaki | Introducing the structure of proof in lower secondary school geometry: a learning progression based on flow-chart proving[END_REF], showed the role of flow-chart with open problem as scaffolding to support Grade 8 students' learning about geometrical proofs. The results of data analysis of students' activities during a classroom intervention indicates that flow-chart proof with open problems as scaffolding enhances students to understand the structure of proof by providing a visualization of both the connection between singular propositions (via hypothetical syllogism) and the connections between a singular proposition and the necessary universal proposition in the form of universal instantiation.

Concluding Remarks

We distinguish two levels of proof understanding which are proposed by Mejia-Ramos et al.: a local understanding related to knowing the definition of basic concepts/terms, knowing the logical status of statements in proof, knowing how and why each statement connects to previous statements. and a holistic understanding when students are able to summarize the main idea of the proof, to identify the sub-proofs and how these relate to the proof structure, to transfer the idea of proof to others, and instantiate the proof with examples [START_REF] Mejia-Ramos | An assessment model for proof comprehension in undergraduate mathematics[END_REF]Miyazaki et al., 2017). Classroom interventions, supporting students' activities in understanding the structure of proofs including the elements of proofs such as singular propositions (premises/geometric statements), universal proposition (geometric definition, axioms, theorems) and hypothetical syllogism (the inter-relationship of these elements), are needed to help students reach both levels of proof understanding.

Several studies confirmed that the use of a Dynamic Geometry System (DGS), such as Geometer's Sketchpad, Cabri and Geogebra, may help students not only solve construction problems but also may help them identify properties on the construction of geometric figures, understand geometrical axioms, definitions and theorems of Euclidean geometry, which are elements of the structure of proof, and universal propositions [START_REF] Botana | Automated Theorem Proving in GeoGebra: Current Achievements[END_REF][START_REF] Jiang | Developing Preservice Teachers' Mathematical Reasoning and Proof Abilities in the Geometer's Sketchpad Environment[END_REF][START_REF] Mariotti | Proof and proving in the classroom: Dynamic Geometry Systems as tools of semiotic mediation[END_REF][START_REF] Mariotti | Introducing students to geometric theorems: How the teacher can exploit the semiotic potential of a DGS[END_REF].

The use of the flow-chart proof form may provide opportunities for students to understand the structure of proof and may help students identify the components of proofs and the interrelationship among the components [START_REF] Miyazaki | Flow-chart proofs with open problems as scaffolds for learning about geometrical proofs[END_REF]Miyazaki et al., 2017). The use of open problems provides an opportunity for students to construct multiple solutions by deciding about the given statements and intermediate propositions necessary to deduce a given conclusion. This ability promotes student thinking forward and backward interactively when constructing a proof under the flow-chart proof format [START_REF] Cheng | The Effectiveness and Limitation of Reading and Coloring Strategy in Learning Geometry Proof[END_REF][START_REF] Heinze | Strategies to foster students' competencies in constructing multi-steps geometric proofs: Teaching experiments in Taiwan and Germany[END_REF].

A study by Miyazaki et al. (2017) suggests that the level of understanding of the structure of proof as a part of local understanding should be taken into consideration in designing an effective learning intervention. [START_REF] Mariotti | Proof and proving in the classroom: Dynamic Geometry Systems as tools of semiotic mediation[END_REF] also recommends future research to better describe how the complex web of meanings emerging from activities with the DGS may be transformed into mathematical meanings such as geometric definitions, axioms and theorems. Hence, the findings presented in this paper indicate our future promising research direction for the study on designing a learning intervention which implements the use of DGS, GeoGebra, as semiotic tools and flow-chart proof format as a scaffolding tool to support a local and holistic understanding of prospective mathematics teachers who have little mathematical proof background.

Figure 1 :

 1 Figure 1: Cyclic process of an Anasynthesis (adapted from Jeannotte & Kieran, 2017)

Figure 2 :

 2 Figure 2: An example of flow-chart of proof visualizing the structure of proof (adapted from Miyazaki, Fujita, & Jones, 2015)


Kristin Krogh Arnesen

Ole Enge

Kirsti Rø

Anita Valenta
email: anita.valenta@ntnu.no

Initial participation in a reasoning-and-proving discourse in elementary school teacher education

Keywords: mathematical discourse, reasoning and proving, elementary school teacher education

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Reasoning and proving are central aspects of mathematics as a discipline, and many researchers have argued that they should be a central part of school mathematics at all grades and in all topics. In this paper, we use a broad definition of the word proof [START_REF] Reid | Proof in Mathematics Education[END_REF], to denote mathematical reasoning involved in the process of making sense of and establishing mathematical knowledge. Hence, we follow [START_REF] Stylianides | An analytic framework of reasoning and proving[END_REF], who used the term 'reasoning-and-proving' to denote the activities involved in this process: identifying patterns, making conjectures and providing arguments.

The reasoning-and-proving process is difficult to learn and difficult to teach. In exploring ways to teach proof, a number of studies have shown the crucial role that a teacher plays in helping students identifying the structure of a proof, presenting arguments and distinguishing between correct and incorrect arguments (see e.g. [START_REF] Stylianides | Proof and proving in school mathematics[END_REF]. Researchers have found that elementary school teachers tend to rely on external authorities, such as textbooks, college instructors or more capable peers, as the basis of their conviction. They also believe it is possible to affirm the validity of a mathematical generalisation using a few examples (see [START_REF] Martin | Proof frames of preservice elementary teachers[END_REF]. Similarly, [START_REF] Stylianides | Preservice teachers' knowledge of proof by mathematical induction[END_REF] revealed that pre-service teachers had two main types of difficulties with proof: the lack of understanding of the logic mathematical underpinnings of different modes of argumentation and the inability to use different modes of representations appropriately.

As exemplified above, research in mathematics education has shed light on different aspects of preservice teachers' work on reasoning-and-proving, such as their beliefs related to proofs and proving, the challenges they face when deducing proofs and their use of modes of reasoning. However, more knowledge is needed about how pre-service teachers learn to teach reasoning-and-proving, as well as how teacher education can support their learning. A vital part of teachers' learning how to teach reasoning-and-proving is learning how to reason and prove in school-relevant mathematical areas (e.g. multiplicative reasoning). That learning is the topic of our study.

We examine two elementary school teachers' work on a reasoning-and-proving task during a professional development course. Like [START_REF] Remillard | Identifying discursive entry points in paired-novice discourse as a first step in penetrating the paradox of learning mathematical proof[END_REF], we consider mathematics to be a specific type of discourse where reasoning-and-proving is essential. Thus, mathematics learning is seen as participation in the discourse [START_REF] Sfard | Thinking as communicating: Human development, the growth of discourses, and mathematizing[END_REF]. The two teachers whose work we analyse have limited experience of reasoning-and-proving in mathematics, and we are interested in their initiation into that discourse. Our research question is: What characterises two in-service teachers' initial participation in a mathematical discourse on reasoning-and-proving in elementary school teacher education?

Theoretical framework

Within a commognitive framework1 , [START_REF] Sfard | Thinking as communicating: Human development, the growth of discourses, and mathematizing[END_REF] take the position that learning mathematics is learning to participate in a specific discourse. Here, discourse is a special type of communication within a specific community that is made mathematical by that community's use of words, visual mediators, narratives and routines. The use of words in mathematics includes the use of ordinary words that have a special meaning in mathematics, like function and proof, and mathematical words, like fraction and axiom. Furthermore, people participating in mathematical communication use visual mediators to identify the object about which they are talking. These visual mediators are often symbolic, but they also include graphs, illustrations and physical artefacts. Within a discourse, any sequence of utterances, spoken or written, that describes the properties of objects or the relationships between objects is called a narrative. Mathematical narratives can be numerical, e.g. "½ is equivalent to 2/4", or more general, e.g. "addition is commutative". Narratives are subject to endorsement or rejection, that is, being labelled as true or false, based on specific rules defined by the community. Endorsement of narratives is the main goal of the mathematics discourse; this includes the processes of constructing new endorsable narratives, substantiating them and recalling them in new situations.

Routines are well-defined practices that a given community regularly employs in a discourse. [START_REF] Sfard | Thinking as communicating: Human development, the growth of discourses, and mathematizing[END_REF] describe routines as patterns that are guided by two sets of rules: those telling the participants how to act, and those indicating when to do the given action. In contrast to rules on the object-level, which describe regularities on actions on and relations of objects, routines describe the participants' patterns of actions in a given discourse, and they can be considered to be rules on a meta-level. [START_REF] Lavie | Routines we live by: From ritual to exploration[END_REF] emphasise the role of routines when participating in a specific discourse, and they suggest that learning routines can be seen as the routinisation of actions in a given discourse. Thus, on their way to new routines, learners must pass, if only briefly, through the stage of ritualised performance or imitation [START_REF] Sfard | Thinking as communicating: Human development, the growth of discourses, and mathematizing[END_REF]. Here, rituals are understood to be socially oriented; they are acts of solidarity with co-performers. At this transitory stage, learners may become very familiar with the how of the new routine, but they will be much less aware of when it is used.

Our research question focuses on participation in a mathematical discourse on reasoning-andproving, involving the processes of identifying patterns, making conjectures and providing arguments for whether or not conjectures are true. Hence, from a discursive stance, we are primarily interested in the routines associated with the construction and substantiation of narratives. New narratives are constructed mainly through operations on previously endorsed narratives. To substantiate a constructed mathematical narrative, one produces a proof-a sequence of endorsed narratives, each of which is deductively inferred from previous ones, the last of which is the narrative that is being endorsed. Thus, learning to reason and prove in mathematics is about individualising both the when and the how of the construction and substantiation routines. In this paper, we focus on substantiation routines as framed by a task in which a hypothesis is already given.

To obtain insight into how individuals learn about reasoning-and-proving, it is useful to delineate the possible patterns of the processes and actions involved in constructing and substantiating narratives. Applying a commognitive perspective, [START_REF] Jeannotte | A conceptual model of mathematical reasoning for school mathematics[END_REF] have developed a conceptual model of mathematical reasoning based on exhaustive analyses of mathematics education research. They propose the following definition of mathematical reasoning through commognition lenses: "Mathematical reasoning processes are commognitive processes that are meta-discursive, that is, that derive narratives about objects or relations by exploring the relations between objects" (Jeannotte & Kieran 2017, p. 9). Because their notion of mathematical reasoning involves proving, it coincides with our use of reasoning-and-proving. However, we use the latter to indicate that we look at a special kind of reasoning that is used when validating mathematical hypotheses, as mathematical reasoning per se does not necessarily include proving. Furthermore, [START_REF] Jeannotte | A conceptual model of mathematical reasoning for school mathematics[END_REF] distinguishbetween processes related to the search for similarities and differences and processes related to validating. Searching for similarities and differences includes generalising, conjecturing, identifying a pattern, comparing and classifying. All these processes infer narratives about mathematical objects or relations (although on a partly different basis); thus, they are related to the routine of constructing narratives [START_REF] Sfard | Thinking as communicating: Human development, the growth of discourses, and mathematizing[END_REF]. The processes related to validating include validating, justifying, proving and formal proving (defined inclusively, with an increasing degree of deductive structure and stringency). These processes aim to change the epistemic value (e.g. true, false) of a given narrative; therefore, they are related to substantiation routines [START_REF] Sfard | Thinking as communicating: Human development, the growth of discourses, and mathematizing[END_REF].

This study investigated two teachers' initial participation based on their utterances and actions in a mathematical discourse on reasoning-and-proving in elementary school teacher education. We aim to illustrate how key concepts from the commognitive framework proposed by [START_REF] Sfard | Thinking as communicating: Human development, the growth of discourses, and mathematizing[END_REF] can provide insight into how mathematics teachers learn about the process of reasoning-and-proving.

Method

The two elementary school teachers, Sandra and Nora (pseudonyms), who participated in the research study, were part of a professional developmental course in mathematics for teachers in grades 1-7 in Norway that was held by two of the authors of this paper. Both teachers are 45-50year-old females, and both completed general teacher education with less than 15 ECST credits in mathematics education. Sandra and Nora represent typical teachers attending the course, due to their age, educational background, gender and having more than 10 years of experience as general teachers.

The course contained materials on mathematics and mathematics education, and it was organised as six, three-day seminars distributed over one year, in addition to the teachers' individual work on literature and assignments. The topics were sense-making in mathematics, pattern seeking and exploration, use of different representations (e.g. the array model for multiplication) and reasoningand-proving (in particular, representation-based proofs). The participants noted that the coursework invited them to use new ways of thinking about and working with mathematics. This paper presents an analysis of the data collected through video recordings (in total 24 minutes) of Sandra and Nora working on a task (Teddy's hypothesis, see Figure 1) on the second day of the fourth seminar of the course. The day before data collection, the topic was multiplication: different properties, strategies, models and reasoning-and-proving.

The task was chosen for the purpose of reasoning-and-proving, starting with a hypothesis proposed by Teddy, an imaginary student (Figure 1). The first step of the task (part a) involves validation of the hypothesis; the second step of the task (part b) entails both stating and validating the new hypotheses. In our analysis, we study validation processes, as exemplified by Sandra and Nora's work on the first step of the task (part a).

Teddy is a grade 5 student. He and his classmates are working on square and cubic numbers. After completing some tasks, Teddy says to the teacher: "Look here, if you multiply … take two numbers and multiply… and both numbers end with 5… then the result also will end with 5". a) Give a proof that shows that Teddy's observation is correct for all such numbers. b) The situation can be used to propose and solve other problems, for instance:

1. Is it only when both numbers end with 5 that the result ends with 5? 2. Does the result hold only for 5, or when two numbers ending with the same digit are multiplied, does the product also end with that same digit? 3. Which digits can square numbers end with? Teddy's hypothesis can be proved by using a generic example and array model of multiplication. Given any two numbers, both ending with 5, say 125 and 35, one can use the array model for multiplication to represent the multiplication 125x35, as shown in Figure 2. Every cell in this array, except the cell with 5x5, is a multiple of 10. Thus, these cells do not contribute to the ones in the product. Only the cell with 5x5 does, and since 5x5 equals 25, we find that the product ends with 5. There is nothing special about the two numbers (35 and 125) in the example. The product of any two numbers both ending with 5 will have the same structure; thus, the number resulting from such a multiplication will end with 5.

Data analysis

The video recordings of Sandra and Nora's work on the task were transcribed, and then coded. The coding was guided by the research question. The aim was to describe the actions and utterances in the teachers' work, rather than to evaluate the mathematical and logical correctness of their arguments. Four researchers made a descriptive coding of the collected data, individually [START_REF] Miles | Qualitative data analysis: An expanded sourcebook[END_REF]. Next, the researchers compared and contrasted their coding and grouped the codes into six categories describing the two teachers' reasoning-and-proving efforts. The following categories were agreed upon: confirming; proposing hypotheses; questioning validity; warranting; searching for patterns; and making drawings.

To illustrate the categories and our findings, we present the teachers' work from part a of the hypothesis task. However, the above-mentioned categories apply to the teachers' discussions on all the given tasks. The teachers' utterances are sometimes imprecise and difficult to interpret, and we tried to preserve this in the translation. In the analysis presented below, we use italics to emphasise the categories. Because, eh, when you, right, in the 5 times table [S: Yeah], when you multiply with an odd number, you'll always end with 5, [S: Yeah] the answer will, the sum will always end, the answer will always be 5, thus … 18 N:

Sandra and

And, anything that ends with 5 is an odd number, so if you multiply… 35 is an odd number, right.

S:

Yes, yes, because of the 5.

N:

Yes, so because of the 5 there it will be an odd number. 21 S:

Yeah. And five is an odd number. 34 S:

Yeah, … Shall we drop this now, and try the next question?

While drawing the arrays, the teachers are searching for patterns. The patterns they discuss concern even and odd numbers in the 5 times table [32]. After turn [34], the teachers leave the task in step a, and proceed to step b. It is not clear if they are dissatisfied with the pattern discovered or if they are finding it difficult to identify a way to use the pattern to prove the hypothesis in turn [17] or Teddy's hypothesis, when they choose to leave the task.

Results and discussion

Our analysis shows that Sandra and Nora use several actions related to construction and substantiation routines. According to [START_REF] Sfard | Thinking as communicating: Human development, the growth of discourses, and mathematizing[END_REF], one of the distinct characteristics of discourses is the keywords that are used. In a mathematical reasoning-and-proving discourse, these keywords relate to deductive reasoning, which is "the only form of reasoning that can change the epistemic value of mathematical knowledge from likely to true" (Jeannotte & Kieran, 2017, p. 8). Sandra and Nora use words that are distinctive of a reasoning-and-proving discourse, namely their warranting of statements by their use of the word "because" followed by "then" or "therefore", as seen in excerpts [18][19][20][21][START_REF] Valenta | And, therefore[END_REF][START_REF] Yeah | [END_REF]. Moreover, the teachers question the validity of the arguments they provide, and they make drawings and search for patterns. In general, the use of drawings as visual mediators is one of the main aspects of mathematical discourse, and its role in reasoning-and-proving was emphasised in the professional development course. Sandra and Nora's drawings and their search for patterns is initiated by their act of questioning the validity of the arguments, which is part of the process of convincing (oneself or another) and is fundamental to mathematical reasoning [START_REF] Jeannotte | A conceptual model of mathematical reasoning for school mathematics[END_REF].

At the same time, Sandra and Nora's explicit reference to representation-based proving (as seen in statement [24]), within the framework of [START_REF] Sfard | Thinking as communicating: Human development, the growth of discourses, and mathematizing[END_REF] and [START_REF] Lavie | Routines we live by: From ritual to exploration[END_REF], indicate that the teachers' participation is ritualised. As previously explained, rituals are understood to be socially oriented; they are acts of solidarity with co-performers or authorities. With their questioning of validity, Sandra and Nora express what they assume to be expected by the community, i.e. the teacher educators, regarding substantiation routines ("is that what they want?"

[24]). The making of drawings and the search for patterns emerge in the teachers' work as a result of stating this question. This stands in contrast to questioning validity on the basis of the given hypothesis and a discussion of what narratives can be considered to already be endorsed by the community. Apart from the question referring to the teacher educators, Sandra and Nora also frequently confirm each other's contributions. Because their questioning of the validity and confirming each other's statements appears to be an attempt to gain social acceptance rather than their need to support and strengthen their substantiation of Teddy's hypothesis, their initial participation in the reasoning-and-proving discourse appears to be ritualised.

Our analysis also reveals ritualised participation in terms of how to act, in particular, how to use drawings. As shown in Figure 3, Sandra has made a drawing based on her own request for a representation-based proof of Teddy's hypothesis. The drawing and the following search for a pattern are related to the teachers' hypothesis (as seen in [17]), and not Teddy's hypothesis. Nevertheless, the chosen drawing does not advance the teachers 'reasoning-and-proving process.

Sandra and Nora's actions related to construction and substantiation of narratives also indicate ritualised participation in terms of when to do a given action. As previously discussed, metadiscursive processes of reasoning-and-proving can be divided into processes of searching for similarities and differences (constructing narratives) and validating processes (substantiation of narratives). Throughout Sandra and Nora's conversation, these processes seem to intersect: several actions that they use, e.g. proposing hypotheses and searching for patterns, are mainly related to the processes of construction of narratives, and they are not appropriate for modifying the epistemic value of a narrative from likely to true. In a substantiation routine, a sequence of endorsed narratives is used, each of which is deductively inferred from previous narratives. Sandra and Nora propose several new hypotheses during their work (e.g. in [17]), and they are not explicit about whether the new narratives are (or can be seen to be) endorsed by the community and how they connect to Teddy's hypothesis. Moreover, Sandra and Nora search for patterns related to even and odd numbers, and it seems that the aim of this action is proving a hypothesis given in [17]. However, their search for patterns does not help them validate the hypothesis, and they leave the task. It is worth noting that the teachers' use of actions related to the construction of narratives happens, even though the Teddy's hypothesis task was designed to direct the teachers to participate in the validating process.

Conclusions and implications

Ritualised participation and challenges in knowing how and when a given action can be used are not surprising results when studying novices' initial participation in a given discourse [START_REF] Sfard | Thinking as communicating: Human development, the growth of discourses, and mathematizing[END_REF]). Yet, within the frames of commognition, we have highlighted that some reasoning-and-proving actions seem to be more visible and applicable for novice participants than other actions; thus, they are easier to imitate. teachers in this study employed several actions that are not directly related to substantiation but are regularly applied in a mathematical discourse. They search for patterns, propose a hypothesis and make drawings. They also perform actions related to substantiation routines, such as warranting and questioning validity. Yet, other actions related to substantiation of narratives seem to be more hidden. For example, being critical is central to substantiation routines; however, Sandra and Nora continuously confirmed each other's contributions.

Moreover, the analysis discloses the two teachers' tendency to use construction-related actions (searching for patterns, proposing hypotheses) in what was designed to be a validating activity. Thus, the findings imply a need in teacher education to be more explicit about what actions are specific for reasoning-and-proving, and also, to be explicit about changes in actions when moving from construction to substantiation of narratives.

In this paper, we have reported on the characteristics of two in-service teachers' learning of reasoning-and-proving in a professional development context in the field of elementary education. Nevertheless, our study is limited by the number of participants, and further research from a commognitive standpoint is needed to shed more light on elementary education teachers' learning of reasoning-and-proving. For example, longitudinal studies are needed to learn more about teachers' evolving routines. Another topic for further research is the role of visual mediators in a reasoning-and-proving context, and how participants can routinise the use of visual mediators in the discourse.

Figure 1 .

 1 Figure 1. Teddy's hypothesis task (adapted from Skott, Jess, & Hansen, 2008, pp. 223-224)

Figure 2 .

 2 Figure 2. The array model for multiplication used in a representation-based proof of the hypothesis

Figure

  Figure 3. Sandra's drawings for part a of the hypothesis task 31 N: Odd number. 32 S: Yeah. But it's a … eh, even number (writes e below the 1x5 array). No, (corrects to the letter o below the 1x5 array) odd number. Odd number plus odd number is always … even number [N: even number, yeah] (writes o+o=e below the 2x5 array. And here it's [N: odd number] odd number plus odd number plus odd number, equals odd number (writes o+o+o=o below the 3x5 array, then o+o+o+o=e below the 4x5 array) 33 N:And five is an odd number. 34 S:Yeah, … Shall we drop this now, and try the next question?

  Nora start their work by reading the hypothesis proposed by Teddy. Both hypotheses are related to Teddy's, but they are partly different, as[4] is more general than Teddy's hypothesis and [7] concerns properties of the 5 times table. In turn [9], the teachers warrant the hypothesis stated in turn[7]; in turn [10], they question the validity of Teddy's hypothesis. A few turns later, the discussion continues, as follows:

	1	N:	It is true, what he says.
	2	S:	Yeah.
	3	N:	So, the argument is correct.
	4	S:	Yes, it is, eh; but it's more. It works for all odd numbers; so, the answer is 5.
	5	N:	Yes, exactly.
	6	S:	As long as one is a 5, one of …
	7	N:	Yes, in the 5 times table, no matter what you multiply with something with
			a 5 in, then you'll get a 5 at the end of the answer.
	8	S:	Yes, ehm …
	9	N:	But, that's also because 5 is an odd number.
	10 S:
	17 N:

Yeah, but do you have an argument that shows that Teddy is correct? Yes, it is, but is it ... is it enough? Now, we have actually, sort of gone further.

The category confirming in our analysis is a social act of support. Examples of this are seen in turns [2] and

[5]

. Furthermore, two new hypotheses are proposed in this excerpt of the discussion, one in turn [4] and another in

[7]

.

The term "commognition" is a combination of the words "communication" and "cognitive", and it stresses that thinking is a way of communicating with oneself and others.