Mayank Agarwal
email: agarwalm@post.bgu.ac.il

Rami Puzis
email: puzis@bgu.ac.il

Jawad Haj-Yahya

Polina Zilberman
email: polinaz@post.bgu.ac.il

Yuval Elovici
email: elovici@bgu.ac.il

Anti-forensic = Suspicious: Detection of Stealthy Malware that Hides its Network Traffic

Keywords: Stealthy, Malware, Command & Control, Trusted Network Monitor, Security

Stealthy malware hides its presence from the users of a system by hooking the relevant libraries, drivers, system calls or manipulating the services commonly used to monitor system behaviour. Tampering the network sensors of host-based intrusion detection systems (HIDS) may impair their ability to detect malware and significantly hinders subsequent forensic investigations. Nevertheless, the mere attempt to hide the traffic indicates malicious intentions. In this paper we show how comparison of the data collected by multiple sensors at different levels of resilience may reveal these intentions. At the lowest level of resilience, information from untrusted sensors such as netstat and process lists are used. At the highest resilience level, we analyse mirrored traffic using a secured hardware device. This technique can be considered as fully trusted. The detection of a discrepancy between what is reported by these common tools and what is observed on a trusted system operating at a different level is a good way to force a dilemma on malware writers: either apply hiding techniques, with the risk that the discrepancy is detected, or keep the status of network connections untouched, with a greater ability for the administrator to recognize the presence and to understand the behaviour of malware. The proposed method was implemented on an evaluation testbed and is able to detect stealthy malware that hides its communication from the HIDS. The false positive rate is 0.01% of the total traffic analysed, and barring a few exceptions that can easily be white-listed, there are no legitimate processes which raise false alerts.

Introduction

In the recent years, there has been an increase in the amount of malware related security incidents resulting in leakage of personal and corporate information, DDoS attacks, data loss, etc. [START_REF] Kalita | WannaCry Ransomware Attack: Protect Yourself from WannaCry Ransomware Cyber Risk and Cyber War[END_REF][START_REF]Cloudflare Bug -Cloudbleed May Have Leaked Data From Millions of Sites[END_REF][START_REF]DDoS attacks in Q4 2017 -Securelist[END_REF]. Malware poses a serious security threat to organizations, computer networks, and end users. As the sophistication of malware has advanced, its detection has become more complex. Malware developers employ various anti-forensic techniques in order to evade the detection mechanisms deployed on the targeted systems. Prominent anti-forensic techniques include: file and directory hiding, process hiding, anti-VM, anti-debug, hiding sockets and connections, etc. Examples of malwares that employ antiforensic techniques include: vlany, azazel, enyelkm [START_REF]vlany is a Linux LD-PRELOAD rootkit[END_REF][START_REF]Azazel is a userland rootkit[END_REF][START_REF]enyelkm -LKM rootkit for Linux x86 with the 2.6 kernel[END_REF] etc.

A host-based intrusion detection system (HIDS) usually consists of various sensors (e.g., the process sensor, CPU sensor, memory sensor, network sensor, etc.) in order to monitor the various components of the host. There are stealthy malwares 3 that employ network hiding 4 anti-forensic feature [START_REF]vlany is a Linux LD-PRELOAD rootkit[END_REF][START_REF]Azazel is a userland rootkit[END_REF]. Malware equipped with such anti-forensic features are harder to detect using HIDS, because their network communication data is not available. A network intrusion detection system (NIDS) may be able to flag network packets if they are sent to suspicious domains or if the traffic patterns resemble an anomalous behavior (e.g., ping sweep). However, neither rules nor machine learning algorithms commonly employed by NIDS are 100% accurate. Irrespective of whether the NIDS flags such packets or not, a NIDS cannot determine if a malware tried to hide its network communication from the HIDS. Furthermore, the technique used by the malware to hide its network communication from the HIDS cannot be ascertained. Notwithstanding any other malicious activities performed by a malware, the fact that a stealthy malware attempts to hide its network communication is itself an indication that the target system is compromised. However, this information (hiding network communication) is crucial for efficient forensic investigation.

The use of HIDS or NIDS alone are insufficient to detect the presence of stealthy malwares that hide their network communication. In order to detect stealthy malware, we employ a detection philosophy that combines from both the observations from host and network sensors in order to ascertain whether an adversary attempts to hide its traffic from HIDS.

The main contributions of this research are: [START_REF]AbuseIPDB -IP address abuse reports[END_REF] We propose a multi-level monitoring method which combines resilient trusted network monitor with multiple untrusted host-based sensors. By untrusted we mean that they can be circumvented by attackers with various skill levels. [START_REF]Azazel is a userland rootkit[END_REF] The proposed multi-level monitoring method detects stealthy malware that attempts to hide its network traffic and also determines the technique adopted by the attacker. (3) The proposed method has been evaluated using stealthy malwares obtained from Internet sources. The evaluation results confirm that all the stealthy malwares that were tested are detected successfully while the false positive rate stands at a mere 0.01% of the total packets analyzed.

The rest of this paper is organized as follows. Section 2 describes the multilevel monitoring method which is the core of the detection method proposed for the identification of stealthy malware. The experimental setup, information regarding malware dataset, and the results obtained using the proposed method are presented in Section 3. In Section 4 we present the existing approaches used for stealthy malware detection, and Section 5 concludes the work. The proposed multi-level monitoring method consists of the host sensors (HS) and a trusted network monitor (TNM) as shown in Fig. 1. The HS are deployed on the host and consist of packet hashing and netstat sensors. In addition to these, there is a heartbeat generator that runs on the host which informs about the running status of the HS. The HS are considered untrusted as they can be subverted by a malware. The TNM is deployed on a dedicated machine and is connected to the network via the port mirroring interface. Due to the port mirror configuration, the TNM receives a copy of all of the packets sent by the host which traverse the switch.

Ideally, in the absence of stealthy malware, for a fixed time interval in which the network communication is measured using HS and TNM, there should be no discrepancy between the measurements obtained by them. A benign application will never hide its network communication from the host sensors, as it does not have any malicious intentions. However, if a discrepancy arises when the traffic measured by the host sensors and the TNM is compared, it provides an evidence of suspicious activity on the host. Not all discrepancies are considered instances of stealthy malwares as explained below:

1. Discrepancy arising out of localhost traffic: Localhost traffic generated on the host is captured by the host sensors, but since the traffic is destined for localhost, it does not reach the switch interface. Consequently, it is not mirrored on the TNM. Such a discrepancy is not considered malicious in the current research and is ignored. 2. Discrepancy arising from packet losses: Packets that are observed on the host sensors but are not seen on the TNM are ignored. Such a scenario might occur as packets seen on host sensors might not be mirrored correctly possibly due to too many packets being mirrored on the TNM at a given time. Also, because the host sensors observe the network communication, the malware is not hidden from the host sensors and does not fall into the category of the stealthy malware being considered. 3. Discrepancies arising due to the presence of malware: Packets sent from the host that were observed on the TNM but were hidden from the host sensors). Such communication definitely points out the presence of malware on the host which evades the host sensors. A malware can hide its network communication in various ways like patching the HS deployed, exploiting bugs that may exist in the libraries used by the HS deployed, detecting their execution and disabling them etc. The goal of a malware developer is to eventually hide its traces in order to escape detection.

Thus, by capturing the network communication at different levels of resilience (by HS and the TNM in our case), and comparing this data, different types of discrepancies can be identified, and the presence of stealthy malware can be ascertained. As the stealthy malware has no control over the TNM, it cannot hide its network communication from the TNM. The various components of the host sensors and TNM are shown in Fig. 1 and described below.

Packet Hashing Sensor: This sensor is a part of host sensors as well as the TNM. The packet hashing sensor is a network packet sniffer deployed in promiscuous mode. It must be noted that host sensors only capture the traffic pertaining to the host on which they are deployed, while the TNM can capture traffic from multiple hosts simultaneously. The packet hashing sensor ignores packets having broadcast and multicast address. The reason for ignoring broadcast and multicast communication is that a stealthy malware aims to minimize its footprints in order to evade detection mechanisms. If it sends broadcast or multicast communication, the respective frame is received by many hosts in the network. This leads to an increase in the footprint of the malicious communication which might eventually aid the detection mechanisms.

The packet hashing sensor only records information relating to transmitted (Tx) packets from the host and does not record the packets received (Rx) by the host. The motivation behind this philosophy is twofold: a) the stealthy malware on the host usually initiates the connection (Tx traffic) with the C&C (or some other host) and would attempt to hide this communication from the host sensors, and b) monitoring Rx leads to additional load on the TNM.

The packet hashing sensor saves the following information for every transmitted packet (src-ip, dst-ip, src-port, dst-port, seq-num, and ack-num), where src-ip (dst-ip) is the source (destination) IP address of the connection, src-port (dst-port) is the source (destination) port address of the connection, and seqnum (ack-num) represents the sequence (acknowledgment) number of a TCP connection. For UDP packets, the seq-num and ack-num fields are set to null. In addition, this module computes and stores the hash of the above tuple for every transmitted packet which is later used for comparison purposes.

Netstat Sensor: This sensor is only a host sensor component. The netstat sensor records all of the information obtained from the netstat utility. It stores the unique connections (src-ip, dst-ip, src-port, dst-port) as seen on the host.

Analysis Module: The analysis module is only present on the TNM. The packet hashing sensor on the host and the TNM, along with the netstat sensor on the host send their information to the analysis module. On examining the information received from these sensors, the analysis module determines if there exists a stealthy malware that is trying to communicate with its C&C server or any other compromised machine in the network.

Heartbeat Generator and Heartbeat Sensor: In addition to the host sensors the multi-level monitoring method also makes use of a heartbeat generator on the host and a heartbeat sensor on the TNM. The main task of the heartbeat generator is to ensure that the host sensors are running and have not been terminated or disabled by the stealthy malware. In order to accomplish this, the heartbeat generator running on the host sends periodic keep-alive messages to the heartbeat sensor running in the TNM.

Customized Secure Processor

As described above, the TNM may need to monitor multiple hosts which may be infected by stealthy malware. It is imperative in such cases to ensure that the TNM's operations are carried out in a trusted environment. Specifically, a malware should not be able to manipulate operations of the TNM and its communication with the switch. To ensure this, the TNM software is running as a trusted application on a customized secure processor. The secure processor implements various features to protect against known attacks on the computing system hardware and the software that is running on it. The features include:

1. Secure IO and Secure Debug -protect against various hardware threats such as key extraction, illicit debugging, probing, and side-channel at tacks (SCA). 2. Secure Boot -protects against attacks such as: image hacking, botnet enrolling, and cold boot attacks. 3. Trusted Execution Environment (TEE) -guarantees an isolated execution environment for the trusted application. This feature is essential for protecting against attacks such as: software exploitation, privilege escalation, and botnet enrolling. 4. Secure Storage -an important feature that exists in secure processors in order to protect against SCAs, probing, and key extraction. In addition, it is used by the TEE to load and execute the trusted applications, while protecting the code and data of the applications running. 5. Secure Disk Storage -for recording and analyzing network packets and sending statistics to the Splunk server.

6. Customizable Crypto Primitives -these include ECC, ECDSA, AES. 7. Dual Ethernet Ports -the first of these ports is used for the local area network (LAN), and the second is used for streaming the mirrored data from the switch to the TNM.

All of the features above ensure that the TNM is unaffected by the presence of malware running on a host monitored by the TNM. Hence, the network communication performed by the stealthy malware eventually appears on the TNM (if they are destined for the switch), even if the malware succeeds in hiding itself from the host sensors.

Evaluation of the Proposed Method

In this section, we provide a detailed explanation of the experimental setup and attack model. The description of the attack model covers the various sophistication levels of the malware and their detection likelihood under distinct detection approaches. This is followed by subsections that discuss the malware dataset characteristics chosen for this research, the false positives obtained, and the runtime performance of the host sensors and the analysis module.

Experimental Setup

The experimental setup is similar to the one shown in Fig. 1 except that we used five machines to execute the malware. On each of the five machines executing the malware, different operating systems (OSs) were installed depending on malware requirements; the host sensors are deployed on each of the five machines. The switch port on which the TNM is connected is configured as a mirror port, so that it can sniff the traffic sent by the five machines.

Attack Model

We assume that a stealthy malware possesses at least one the following features (ordered based on the level of sophistication, from the least to the highest) as shown in Table 1. It shows the features detectable by different detection mechanisms for the malwares that possesses feature A, B, and C. A good detection system is the one which can detect all of the features possessed by the stealthy malware. For explanation, we consider a malware having feature C (malware hiding from netstat and packet hiding sensor) and look at the features detectable by the different detection mechanisms shown in Table 1: i) Host sensor with only the netstat sensor deployed: Since the malware hides itself from netstat, 'only netstat' monitoring would not help to detect the feature C. ii) Host sensor with only the packet hashing sensor deployed: As the malware hides itself from the packet hashing sensor, it fails to detect feature C. iii) Host sensor with both the netstat and packet hashing sensors deployed:

The malware still remains undetected as it hides itself from both of them. iv)

Only NIDS deployed: The malware traffic may be flagged depending on the traffic generated by the malware and the NIDS configuration, however NIDS alone cannot determine if the malware hides its network communication from host sensors. v) Both host sensors and the TNM are deployed (proposed approach): The proposed multi-level monitoring method not only detects the stealthy malware, but it also identifies the network hiding anti-forensic techniques it adopted.

Malware Dataset Characteristics and Evaluation

We used the virussign.com dataset [START_REF]Virus Free Downloads[END_REF] for evaluating the malware samples. A total of five machines were used to execute malwares. A set of sixty malwares were executed on a single machine with the host sensors deployed. Thus five machines could execute 300 malware samples. The network activities generated by these (300) malwares is collected over a period of twenty minutes and the statistics from the various sensors are collected and analyzed. The whole setup of executing 300 malwares and recording the activities for a period of twenty minutes constitutes a single run. We execute 10 such runs.

Ideally, without the presence of malwares, the number of connections observed on the host sensors and the TNM must be identical. A connection implies a tuple consisting of (src-ip, dst-ip, src-port, dst-port). Figure 2 depicts the connections made by the network hiding stealthy malware that were observed by netstat, packet hashing sensor (PHS), or TNM while the Table 2 shows the individual statistics per run. It can be concluded from Fig. 2 that circumventing connections from netsat is the easiest. Netstat observed the least number of hidden connections in comparison to the other senors. There are a large number of connections which are observed by the packet hashing sensor which are missed by netstat. The netstat utility being a part of the operating system is widely used for checking network connection management. Hiding network communication from netstat is one of the most basic anti-forensics mechanism an attacker would employ while developing a stealthy malware that performs network communication. There are connections which are invisible to the packet hashing sensor but are recorded in netstat. However, there are relatively few connections of such type as can be observed in Fig. 2.

Next, we observe that a large number of connections were hidden from the packet hashing sensor that were eventually captured by the TNM. If we compare the connections that were hidden from netstat but visible in packet hashing sensor to those that were hidden from packet hashing sensor but seen on TNM, it can be concluded that hiding network communication from packet hashing sensors is relatively more complicated as compared to hiding from netstat. But, seeing the number of connections that were hidden from the packet hashing sensor, which were visible on the TNM, shows that many malwares are equipped with network hiding anti-forensic mechanism.

Finally, we inspect the number of connections that were hidden from both netstat and packet hashing sensor but were visible on the TNM. Such malwares possess the most sophisticated anti-forensic mechanism that cannot be detected by an HIDS deployed on the host as the network data is unavailable. We see that the number of such connections are almost the same as the number of connections that were hidden from packet hashing sensor but seen on TNM. A malware developer who writes sophisticated malware to hide from the packet hashing sensor would mostly include the intelligence to hide itself from netstat.

In Fig. 2, some runs (e.g., Run 9) have a large number of connections that were hidden from the host sensors. As we mentioned earlier, malwares employ various mechanism to hide their presence. Some attackers write sophisticated programs to circumvent the host sensors while others just terminate or disable the host sensors. As a result, the host sensors are unable to capture statistics and in the meantime the malware performs its desired activity which eventually gets logged on the TNM. On the other hand, the run 10 of Fig. 2 does not have any packets seen on TNM that were hidden from the host sensors. This shows that the said run did not include malware with network hiding anti-forensic mechanism. So, depending on the nature of the anti-forensic mechanism built into the malware, different sets of observations are obtained.

Irrespective of whether the malware hides its communication from netstat, packet hashing sensor or both, its communication is eventually captured by the TNM due to multi-level monitoring. As the TNM is unaffected by the presence of malwares, it identifies all those connections that the malware attempted to hide from the host sensors. The proposed method not only detects the IPs and ports contacted by stealthy malware, but also determines the level of stealthiness adopted by the malware.

Port 53 49%

Port 80 37%

Port 443 4% Port 25 2%

Other Ports 8% Fig. 3. Distribution of ports that were contacted by the stealthy malware

Figure 3 shows the distribution of top 5 port numbers that were used by the stealthy malware for communication. The ports 53, 80, 443, 25 constitutes a total of the total 93% of the ports communicated by stealthy malwares. The port 53 is used by the DNS server and constitutes a majority 49% of the ports communicate by the stealthy malware. It is obvious that a stealthy malware would want to hide its DNS resolution in order to conceal its activity. Similarly ports 80, 443 are http and https ports that may be used by the malware in order to exfiltrate information to C&Cs. Table 3 shows the top five IP addresses contacted by the stealthy malwares. In total, the proposed method observed connections to 899 unique IPs that were not captured by the HS but seen on the TNM due to multi-level monitoring approach. The threat intelligence websites [START_REF]AbuseIPDB -IP address abuse reports[END_REF][START_REF]Data Mining for Threat Intelligence[END_REF]7,[START_REF]Open Threat Intelligence[END_REF][START_REF]Ransomware Tracker[END_REF] reports all these IPs into various categories like malware, phishing, botnet, ransomware, blacklisted, malicious etc. Not of the threat intelligence websites report all of the IPs as suspicious. As most of the threat intelligence websites are community driven, the threat information depends on its update frequency. We believe that the proposed method can also be used in order to enhance the information available on the threat intelligence websites. The proposed method is capable to detect the newer IPs that a stealthy malware may contact, and also report its stealthiness sophistication. Additionally the proposed scheme can also report on those malwares that subvert the HIDS in-order to contact the C&Cs.

False Positives and Runtime Performance

As the proposed system involves deep packet inspection of the packets seen on the host sensors and the TNM, the system must be resistant to false positives (FPs). In order to test for the FPs, we deployed our host sensors on various systems that did not contain any malware and monitored them by the TNM. The users were instructed to perform their routine activities. On a few of the systems, some dedicated tasks were assigned like opening random websites, HD video playback, downloading large files, rate limited large file download and uploading data. The goal was to obtain a good mix of the traffic patterns seen during a normal user's day-to-day browsing. Table 4 summarizes the the false positive results obtained for the various users. We observed few false positives (905 packets out of 6.9M packets analyzed, representing 0.01311% of all of the traffic). The 905 packets were distributed in the following fashion: AS15169 Google: 489, Ben Gurion University Internal traffic: 399, AS36351 SoftLayer Technologies: 12, AS16625 Akamai Technologies: 2, AS54113 Fastly: 2, AS8068 Microsoft Corporation: 1. A major chunk of the FPs observed belonged to Google and internal Ben Gurion University traffic(the place where we conducted our experiments) and they could easily be avoided by putting them in a whitelist. By configuring a whitelist of the genuine hosts, the FPs can be further reduced. Now we look into the performance metrics of the packet hashing sensor and the analysis module.

We use the dumpcap utility for the packet hashing sensor. The packet hashing sensor consumes an average of 6.329 Mb per run and has a standard deviation of 0.0164 Mb. The analysis module consumes an average of 45.46 Mb per run and has a standard deviation of 13.73 Mb. Both the packet hashing sensor and analysis modules have plausible memory consumption and would not impact the performance of a system on which they are running. Our assumption is that a subset of the machines need to be monitored at a given instance for the presence of stealthy malwares. This helps us to address the scalability issues associated with our approach. Although we use per packet capture analysis for identifying stealthy malwares, we envision to use aggregation based analysis (like traffic flow statistics etc.) as a part of our future work to make it more cost efficient in terms of large scale deployment.

Related Work

Analysis of malware can either be static, dynamic or hybrid [START_REF] Damodaran | A comparison of static, dynamic, and hybrid analysis for malware detection[END_REF]. In static analysis, the malware is not executed at all. Information regarding the malware is gathered via the file hashes, file type, header details, embedded sources etc. Under dynamic analysis, the malware is executed in a controlled environment; e.g., sandbox, Virtualbox, or an isolated environment etc. In hybrid analysis, a combination of static and dynamic analysis is used. We describe the major approaches currently used to detect stealthy malware.

Intrusion Detection Systems: As mentioned earlier, the use of an HIDS or NIDS alone would be insufficient for detecting the presence of stealthy malware. Malware developers usually employ various techniques, including polymorphic/metamorphic code mutation, entry point obscuration [START_REF] Alam | A framework for metamorphic malware analysis and real-time detection[END_REF][START_REF] Szor | The art of computer virus research and defense[END_REF] etc., which leads to the generation of equivalent code (e.g., the addition of NOPs) or the distribution of malicious code in a benign program in order to evade detection from signature based IDSs. Anomaly based IDSs have the ability to detect newer threats, however building the normal network profile required by these systems is a challenge. In addition, stealthy malware may not leave significant traces that would enable a signature or anomaly-based IDS to detect its presence.

Emulation based techniques: These became popular because they provided the means for analyzing the behavior of a malicious program in an emulated environment, allowing anti-malware developers to study the behavior of malware and use the observations from the emulated environment to detect malware in real systems. However, malware developers created techniques that enabled them to determine whether they were operating under emulated or real environments, e.g., volume identifiers, network interfaces, special strings [START_REF] Musavi | Back to Static Analysis for Kernel-Level Rootkit Detection[END_REF] etc. Since we deal with stealthy malware, we assume that it has built-in antiemulation forensics, so that it can evade analysis in an emulated environment.

System hook detection methods: Many stealthy malwares use process hijacking, divert the normal code flow, or modify the function pointers in order to execute the malicious code prior to or after the execution of system calls. Such techniques are known as hooking and they can be performed in a variety of ways. Various malware detection techniques are used to identify the presence of malware by detecting the hooks [START_REF] Hoglund | Rootkits: subverting the Windows kernel[END_REF][START_REF] Butler | VICE-catch the hookers[END_REF][START_REF] Rutkowska | Detecting windows server compromises with patchfinder 2[END_REF], however not all hooks are inherently malicious, and as a result, malware detection techniques that simply reply on the detection of hooks can lead to a large number of false positives.

Visualization based techniques: These techniques employ various visualization techniques in order to depict the various connections between the clients and servers [START_REF] Chen | Oceans: Online collaborative explorative analysis on network security[END_REF]. Visualization methods often require manual intervention once its tags anything suspicious, making the process cumbersome.

Noninvasive Techniques: Authors in [START_REF] Guri | Noninvasive detection of anti-forensic malware[END_REF] propose a noninvasive method to detect the malwares possessing anti-forensic mechanisms. Their method requires tracing flow of instructions (Opcode) and the flow of input-output operations (IO) of a malware under multiple execution environments (forensic vs non-forensic) and comparing the traces for suspected vulnerabilities. Although it is a promising approach being noninvasive, executing malwares under multiple execution environments and recording traces is challenging.

Cross view detection techniques: These techniques employ a number of measures to determine the system state, for example, by obtaining the number of files in a directory using system API calls and via actual traversal using a non-API call. Under normal conditions, the results of such operations should yield the same result. If a discrepancy is found, it indicates the presence of malware that hides files from the system. Several detection tools, including Rootkit [START_REF] Cogswell | Rootkit detection tool by Microsoft[END_REF], Strider Ghostbuster etc. make use of cross view detection technique in order to detect the presence of stealthy malware. Cross view detection methods often offer high detection rates. For the detection of stealthy malware that hides its traffic from HIDS, our method makes use of the cross-view detection principle via the host sensors and trusted network monitoring.

Existing techniques make use of a variety of methods in order to detect stealthy malware and often require non-trivial changes at the operating system level or are limited in terms of detecting the sophistication level of the malware hiding technique etc., making malware detection relatively complex and prone to false positives. In contrast, the proposed multi-level monitoring method is not limited by such constraints and has the potential to effectively detect even newer stealthy malware.

Conclusion & Discussion

In this paper, we propose a method to detect the presence of stealthy malware that hides its traffic from HIDSs. In order to escape detection by HIDSs, state of the art malware is equipped with various anti-forensic mechanisms like antidebug, anti-VM, hiding network connections and network communication. Our proposed method aims to enhance security of the existing malware detection infrastructure, and we believe it should be integrated with threat detection mechanisms in place in order to increase the robustness and resilience of the existing threat detection mechanisms. If the proposed multi-level monitoring technique will be widely adopted, malware developers would have to identify other means of hiding their network traces. The proposed method not only overcomes the drawbacks associated with the existing approaches for detecting stealthy malware, but also possesses the ability to detect newer malware with network hiding anti-forensic capabilities.

The approach has been tested with real malwares and was shown to be effective against anti-forensic techniques that circumvent host-based traffic sensors. Evaluation was carried out on a testbed with hardware PCs, as opposed to a Virtualbox, sandbox, etc. Thus, we can be confident that stealthy malware that has a built-in anti-VM or anti-sandboxing or anti-emulation technologies, etc. is also executed and detected. Had this research been conducted on a VM or in a sandbox or hypervisor environment, stealthy malware that is able to detect its execution environment would not have been detected.

Detecting malware that performs stealthy communication is crucial as such malware can effectively hide itself from HIDSs. The proposed method not only detects the traffic that was hidden but also identifies the technique used by the attacker to hide its network traffic. Employment of the proposed method leads to a catch 22 situation for the malware developers that need to conceal outgoing traffic -If they do, their presence will be detected using our method. If they don't, their detection using standard measures will be easier. As a result of the proposed method, a malware developer is left with a choice either not to hide its communication from HIDS or rely on steganography, covert channels etc. to conceal their communication. The latter requires much more advanced attack infrastructure (e.g. presence on the organization gateway, man in the middle, etc.) than hooking some libraries on the host machine. Many organizations employ traffic monitoring on their premises in order to detect the presence of malware or identify suspicious traffic. For such organizations, the proposed method can easily be augmented in order to detect malware that hides its traffic from HIDS.

Fig. 1 .

 1 Fig. 1. Multi-level monitoring method: Uses host sensors (HS) and the Trusted Network Monitor (TNM)

Fig. 2 .

 2 Fig. 2. Statistical observations of the connections made by the network hiding stealthy malware that were observed by netstat, packet hashing sensor (PHS), or TNM.

Table 1 .

 1 Anti-forensic mechanisms of stealthy malware and features detectable by the different detection mechanisms

				Detection Mechanism
			Host Sensor (Only Netstat Sensor)	Host,Sensor (Only Packet Hashing Sensor)	Host,Sensor (Netstat + Packet Hashing Sensor)	Only NIDS	Host Sensors + TNM (Proposed Method)
	Feature	Sophistication Level		Features Detected
		Hidden: Netstat sensor				None, but may
	A	Visible: Packet hashing	None	None	A	flag suspicious	A
		sensor				communication
		Hidden: Packet hashing				None, but may
	B	sensor	None	None	B	flag suspicious	B
		Visible: Netstat sensor				communication
	C	Hidden:netstat and packet hashing sensor	None	None	None	None, but may communication flag suspicious	C

Table 2 .

 2 Connections observed by netstat, packet hashing sensor (PHS), or TNM.

		Seen on netstat	Seen on PHS	Seen on TNM	Seen on TNM
	Run #	but hidden		but hidden	but not	but neither on
			from PHS		from netstat	on PHS	PHS & netstat
		1	16				147		1317	1305
		2	148				259		264	127
		3	3				4350		1588	1588
		4	120				453		10	10
		5	472				1039		1281	811
		6	1174				2619		2102	1666
		7	170				3368		55	55
		8	291				8881		261	221
		9	355				10687		5407	5407
	10	6				1850		0	0
	Total	2755				33653		12285	11190
	Number of Unique Connections	2000 4000 6000 8000 10000	Seen on netstat hidden from PHS Seen on PHS hidden from netstat Seen on TNM but not on PHS Seen on TNM but neither on PHS & netstat
		0
			#1	#2	#3	#4	#5	#6	#7	#8	#9 #10
							Run Number

Table 3 .

 3 Top 5 IPs contacted by stealthy malwares.

	IP	Unique Hits	Threat Intelligence Reports [1,4,7,8,9]
	68.178.213.61	224	Malware, Phishing, Spam, Botnet, Ransomware.
	194.58.56.172	97	Malware, Phishing.
	23.253.126.58	49	Malware, Phishing, Botnet.
	104.239.157.210	46	Malware, Phishing, Botnet, Ransomware.
	199.2.137.20	44	Malware, Botnet, Blacklisted.

Table 4 .

 4 False positives observed.

	Total Users	Packets Captured by TNM	FPs	FP %
	11	6,904,567	905	905 6, 904, 567	= 0.0131 %

In this manuscript, the term stealthy malware is used to refer to malware that has network hiding anti-forensic capability. A stealthy malware can possess other antiforensic mechanisms in addition to network hiding.

[START_REF]Data Mining for Threat Intelligence[END_REF] By network hiding, we refer to communication in which the malware hides its network communication from network sensors (e.g., Wireshark, dumpcap, netstat, etc.) that a HIDS may employ in order to hide its network activity.


Stefano Berardi
email: stefano@di.unito.it

Makoto Tatsuta
email: tatsuta@nii.ac.jp

Intuitionistic Podelski-Rybalchenko Theorem and Equivalence between Inductive Definitions and Cyclic Proofs

A cyclic proof system gives us another way of representing inductive and coinductive definitions and efficient proof search. Podelski-Rybalchenko termination theorem is important for program termination analysis. This paper first shows that Heyting arithmetic HA proves Kleene-Brouwer theorem for induction and Podelski-Rybalchenko theorem for induction. Then by using this theorem this paper proves the equivalence between the provability of the intuitionistic cyclic proof system and that of the intuitionistic system of Martin-Lof's inductive definitions when both systems contain HA.

Introduction

This paper studies two subjects: intuitionistic Podelski-Rybalchenko theorem for induction, and equivalence between intuitionistic system of Martin-Löf's inductive definitions and an intuitionistic cyclic proof system.

Podelski-Rybalchenko theorem [START_REF] Podelski | Transition Invariants[END_REF] states that if a transition invariant is a finite union of well-founded relations then the transition invariant is also wellfounded. This gives us good sufficient conditions for analysis of program termination [START_REF] Podelski | Transition Invariants[END_REF]. Intuitionistic provability of this theorem is also interesting; if we can show this theorem is provable in some intuitionistic logical system, the theorem also gives us not only termination but also an upper bound of computation steps of a given program. For this purpose, we have to replace wellfoundedness in the theorem by induction principle, since well-foundedness is a property of negation of existence and induction principle can show a property of existence. We say Podelski-Rybalchenko theorem for induction when we replace well-foundedness by induction principle in Podelski-Rybalchenko theorem. [START_REF] Berardi | An intuitionistic version of Ramseys Theorem and its use in Program Termination[END_REF] shows Podelski-Rybalchenko theorem for induction is provable in intuitionistic second-order logic. [START_REF] Berardi | Equivalence of Inductive Definitions and Cyclic Proofs under Arithmetic[END_REF] shows that this theorem for induction is provable in Peano arithmetic, by using the fact that Peano arithmetic can formalize Ramsey theorem. However until now it was not known whether Podelski-Rybalchenko theorem for induction is provable in some intuitionistic first-order logic. This paper will show this theorem for induction is provable in Heyting arithmetic and answer this question.

An inductive/coinductive definition is a way to define a predicate by an expression which may contain the predicate itself. The predicate is interpreted by the least/greatest fixed point of the defining equation. Inductive/coinductive definitions are important in computer science, since they can define useful recursive data structures such as lists, trees, and streams, and useful notions such as bisimulations. Inductive definitions are important also in mathematical logic, since they increase the proof theoretic strength. Martin-Löf's system of inductive definitions given in [START_REF] Martin-Löf | Haupstatz for the intuitionistic theory of iterated inductive definitions[END_REF] is one of the most popular systems of inductive definitions. This system has production rules for an inductive predicate, and the production rule determines the introduction rules and the elimination rules for the predicate. [START_REF] Brotherston | Sequent calculus proof systems for inductive definitions[END_REF][START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF] proposed an alternative formalization of inductive definitions, called a cyclic proof system. A proof, called a cyclic proof, is defined by proof search, going upwardly in a proof figure. If we encounter the same sequent (called a bud) as some sequent we already passed (called a companion) we can stop. The induction rule is replaced by a case rule, for this purpose. The soundness is guaranteed by some additional condition, called a global trace condition, which can show the case rule decreases some measure of a bud from that of the companion. In general, for proof search, a cyclic proof system can find an induction formula in a more efficient way than Martin-Löf's system, since a cyclic proof system does not have to choose fixed induction formulas in advance. A cyclic proof system enables us to get efficient implementation of theorem provers with inductive definitions [START_REF] Brotherston | Cyclic Proofs for First-Order Logic with Inductive Definitions[END_REF][START_REF] Brotherston | Cyclic Proofs of Program Termination in Separation Logic[END_REF][START_REF] Brotherston | Automated Cyclic Entailment Proofs in Separation Logic[END_REF][START_REF] Brotherston | A Generic Cyclic Theorem Prover[END_REF]. A cyclic proof system can also give us another logical system for coinductive predicates, since a coinductive predicate is a dual of an inductive predicate, and sequent calculus is symmetric for this dual. [START_REF] Brotherston | Sequent calculus proof systems for inductive definitions[END_REF][START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF] investigated Martin-Löf's system LKID of inductive definitions in classical logic for the first-order language, and the cyclic proof system CLKID ω for the same language, showed the provability of CLKID ω includes that of LKID, and conjectured the equivalence.

As the second subject, this paper studies the equivalence for intuitionistic logic, namely, the provability of the intuitionistic cyclic proof system, called CLJID ω , is the same as that of the intuitionistic system of Martin-Lof's inductive definitions, called LJID. This question is theoretically interesting, and answers will potentially give new techniques of theorem proving by cyclic proofs to type theories with inductive/coinductive types and program extraction by constructive proofs. This paper first points out that the countermodel of [START_REF] Berardi | Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proof System[END_REF] also shows the equivalence is false in general. Then this paper shows the equivalence is true under arithmetic, namely, the provability of CLJID ω is the same as that of LJID, when both systems contain Heyting arithmetic HA.

There are not papers that study the equivalence for intuitionistic logic or Kleene-Brouwer theorem for induction in intuitionistic first-order logic. For Podelski-Rybalchenko theorem for induction, [START_REF] Berardi | An intuitionistic version of Ramseys Theorem and its use in Program Termination[END_REF] intuitionistically showed it but the paper used second-order logic.

Section 2 proves Kleene-Brouwer theorem for induction and Podelski-Rybalchenko theorem for induction. Section 3 defines LJID and CLJID ω and discuss a cyclic proof system for streams. Section 4 discusses the countermodel, defines CLJID ω + HA and LJID + HA, states the equivalence theorem, and explains ideas of the equivalence proof. Section 5 discusses proof transformation and proves the equivalence theorem. Section 6 discusses related work. We conclude in Section 7.

HA-Provable Podelski-Rybalchenko Theorem for Induction

This section will prove Podelski-Rybalchenko theorem for induction, inside Heyting arithmetic HA. First we will prove Kleene-Brouwer theorem for induction, inside HA. This is done by carefully using some double induction. This theorem is new. Next we will show induction for the set MS of monotonically-colored subsequences. Monotonically-colored subsequences are used in ordinary proof of Ramsey theorem and we will show some intuitionistic property of them. Then by applying Kleene-Brouwer theorem to a part of MS and some orders > u,Left and > u,Right , we will obtain two Kleene-Brouwer relations > KB1,r and > KB2,r and show their induction principle. These two relations are simple but necessary preparation for the next relation. Then by applying Kleene-Brouwer theorem to some lifted tree determined by > KB2,r and the relation > KB1,r , we will obtain a Kleene-Brouwer relation > KB,r and show its induction principle. This relation is a key of the proof. Then we will show that induction for decreasing transitive sequences is reduced to induction for Erdös trees with the relation > KB,r . An Erdös tree is some set of monotonically-colored sequences and implicitly used in ordinary proof of Ramsey theorem. Since Erdös trees are in the lifted tree, by combining them, finally we will prove Podelski-Rybalchenko theorem for induction.

Kleene-Brouwer Theorem

We will show Kleene-Brouwer theorem for induction, which states that if we have both induction principle for a lifted tree (namely u * T for some tree T ) with respect to the one-step extension relation and induction principle for relations on children, then we have induction principle for the Kleene-Brouwer relation. We can prove it by refining an ordinary proof of Kleene-Brouwer theorem for orders.

We assume Heyting arithmetic HA is defined in an ordinary way with constants and function symbols 0, s, +, ×. We define x < y by ∃z.x + sz = y and x ≤ y by x = y ∨ x < y. We can assume some coding of a sequence of numbers by a number in Heyting arithmetic, because the definitions on pages 115-117 of [START_REF] Shoenfield | Mathematical Logic[END_REF] work also in HA. We write t 0 , . . . , t n for the sequence of t 0 , . . . , t n . We also write |t|, and (t) u for the length of the sequence t, and the u-th element of the sequence t respectively. We write * for the concatenation operation of sequences.

We write > R or > for a binary relation. We write < R for the binary relation of the inverse of > R . For notational simplicity, we say X is a set in order to say there is some first-order formula F x such that x ∈ X ↔ F x. Then we also say t ∈ X in order to say F t. We write y < R x ∈ X for y < R x ∧ y ∈ X. We write x ∈ σ when x is an element of the sequence σ. We write U <ω for the set of finite sequences of elements in U . For a set S of sequences, we write u * S for { u * σ | σ ∈ S}. For a set U and a binary relation > R for U , the induction principle for (U, > R ) is defined as

Ind(U, > R , F ) ≡ ∀x ∈ U ((∀y < R x ∈ U.F y) → F x) → ∀x ∈ U.F x, Ind(U, > R ) ≡ Ind(U, > R , F ) (for every formula F x).
For a set U a set T is called a tree of U if T ⊆ U <ω and T is nonempty and closed under prefix operations. Note that the empty sequence is a prefix of any sequence. As a graph, the set of nodes is T and the set of edges is {(x, y) ∈ T 2 | y = x * u }. We call a set T ⊆ U <ω a lifted tree of U when there are a tree T ⊆ U <ω and r ∈ U such that T = r * T . We define LiftedTree(T, U ) as a first-order formula that means T is a lifted tree of U .

For x, y ∈ U <ω we define the one-step extension relation x > ext y if y = x * u for some u. For a set T ⊆ U <ω and σ ∈ U <ω , we define T σ as {ρ ∈ T | ρ = σ * ρ }. Note that T σ is a subset of T . For a nonempty sequence σ, we define first(σ) and last(σ) as the first and the last element of σ respectively.

The next lemma shows induction implies x > x. The proof is in [START_REF] Berardi | Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic[END_REF].

Lemma 2.1 If HA Ind(U, >), then HA ∀x, y ∈ U (y < x → y = x).

Definition 2.2 (Kleene-Brouwer Relation) For a set U , a lifted tree T of U , and a set of binary relations > u on U for every u ∈ U , we define the Kleene-Brouwer relation > KB for T and {(> u ) | u ∈ U } as follows: for x, y ∈ T , x > KB y if (1) x = z * u, u 1 * w 1 , y = z * u, u 2 * w 2 , and u 1 > u u 2 for some z, u, u 1 , w 1 , u 2 , w 2 , or (2) y = x * z for some z = .

When (> u ) is some fixed (>) for all u, for simplicity we call the relation (> KB ) the Kleene-Brouwer relation for T and >.

Note that (> KB ) is a relation on T . This Kleene-Brouwer relation is slightly different from ordinary Kleene-Brouwer order for the following points: it creates a relation instead of an order, it uses a set of relations indexed by an element, and it is defined for a lifted tree instead of a tree (in order to use indexed relations).

The next theorem shows induction principle for the Kleene-Brouwer relation.

Theorem 2.3 (Kleene-Brouwer Theorem for Induction) If HA LiftedTree(T, U ), HA Ind(T, > ext ) and HA ∀u ∈ U.Ind(U, > u ), then HA Ind(T, > KB ).

Proof. By induction on (T, > ext ) with the induction principle Ind(T, > ext ), we will show ∀σ ∈ T.Ind(T σ , > KB ). After we prove it, we can take σ to be to show the theorem, since T = T .

Fix σ ∈ T in order to show Ind(T σ , > KB ). Note that we can use induction hypothesis for every σ * u ∈ T :

Ind(T σ * u , > KB ). (1)
Assume ∀x ∈ T σ ((∀y

< KB x ∈ T σ .F y) → F x) (2)
in order to show ∀x ∈ T σ .F x. For simplicity we write F (X) for ∀x ∈ X.F x. Let Gu ≡ F (T σ * u ). By Ind(U, > last(σ) ) we will show the following claim. Claim: ∀u ∈ U.Gu. Fix u ∈ U in order to show Gu.

By IH for v with > last(σ) we have

v < last(σ) u → F (T σ * v ). (3)
We can show

∀x ∈ T σ * u ((∀y < KB x ∈ T σ * u .F y) → (∀y < KB x ∈ T σ .F y)) (4)
as follows. Fix x ∈ T σ * u , assume

∀y < KB x ∈ T σ * u .F y (5)
and assume y < KB x ∈ T σ in order to show F y. By definition of > KB , we have y ∈ T σ * v for some v < last(σ) u, or y ∈ T σ * u . In the first case, F y by (3). In the second case, F y by ( 5). Hence we have shown [START_REF] Berardi | Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proof System[END_REF]. Combining ( 4) with (2), we have

∀x ∈ T σ * u ((∀y < KB x ∈ T σ * u .F y) → F (x)). (6)
By IH (1) for σ * u , we have Ind(T σ * u , > KB ), namely,

∀x ∈ T σ * u ((∀y < KB x ∈ T σ * u .F y) → F x) → ∀x ∈ T σ * u .F x. (7)
By (7)(6), F (T σ * u ). Hence we have shown the claim. If y < KB σ ∈ T σ , we have y ∈ T σ * u for some u, since y < KB σ implies y = σ by definition of KB and Lemma 2.1 for > u . By the claim, F y. Hence

∀y < KB σ ∈ T σ .F y. (8)
By letting x := σ in (2), we have (∀y

< KB σ ∈ T σ .F y) → F σ. By (8), F σ. Combining it with the claim, ∀x ∈ T σ .F x. 2

Proof Ideas for Podelski-Rybalchenko Theorem for Induction

In this subsection we will explain proof ideas of Theorem 2.15.

A sequence

u 1 > R u 2 > R u 3 > R .
. . is called transitive when u i > R u j for any i < j. We say the edge from u to v is of color R when u > R v. A sequence is called monotonically-colored when for any element there is a color such that the edge from the element to any element after it in the sequence has the same color.

Definition 2.4 For a set U and a relation > for U , we define the set DS(U, >) of decreasing sequences as { x 0 , . . . ,

x n-1 | n ≥ 0, x i ∈ U, ∀i < n -1.(x i > x i+1 )}.
We define the set DT(U, >) of decreasing transitive sequences by

{ x 0 , . . . , x n-1 | n ≥ 0, x i ∈ U, ∀i(∀j ≤ n -1.(i < j → x i > x j ))}.
We define > R1∪...∪R k as the union of > Ri for all 1 ≤ i ≤ k. We define > R1+...+R k as the disjoint union of > Ri for all 1 ≤ i ≤ k. (Whenever we use it, we implicitly assume the disjointness is provable in HA.)

We define Monoseq R1,...,R k (x) to hold when

x = x 0 , . . . , x n-1 ∈ DT(U, > R1+...+R k ) and ∀i < n -1.(∀j ≤ n -1.(i < j → 1≤l≤k (x i > R l x i+1 → x i > R l x j ))
). Note that n may be 0. We define MS as {x ∈ DT(U,

> R1+...+R k ) | Monoseq R1,...,R k (x)}.
MS is the set of monotonically-colored finite sequences. Note that MS r is a subset of MS (by taking T and σ to be MS and r in our notation T σ ) and a lifted tree of U for any r ∈ U . We will show Podelski-Rybalchenko theorem for induction stating that if a transition invariant > Π is a finite union of relations > π such that each Ind(> n π ) is provable for some n, and each (> π ) is decidable, then Ind(> Π ) is provable.

First each Ind(> π ) is obtained by Ind(> n π ). Next by the decidability of each (> π ), we can assume all of (> π ) are disjoint to each other. For simplicity, we explain the idea of our proof for well-foundedness instead of induction principle.

Assume the relation > Π has some infinite decreasing transitive sequence

u 1 > Π u 2 > Π u 3 > Π . . .
in order to show contradiction.

The set MS will be shown to be well-founded with the one-step extension relation. For a decreasing transitive sequence x of U , a lifted tree T ∈ U <ω is called an Erdös tree of x when the elements of x are the same as elements of elements of T , every element of T is monotonically-colored, and the edges from a parent to its children have different colors. Let ET be a function that returns an Erdös tree of a given decreasing transitive sequence. Then we consider ET( u 1 ), ET( u 1 , u 2 ), ET( u 1 , u 2 , u 3 ), . . . . Define MS r as the set of sequences beginning with r in MS. Define > KB1,r as the Kleene-Brouwer relation for the lifted tree MS r and some left-to-rightdecreasing relation on children of the lifted tree. Define > KB2,r as the Kleene-Brouwer relation for the lifted tree MS r and some right-to-left-decreasing relation on children of the lifted tree. By Kleene-Brouwer theorem, (> KB1,r ) and (> KB2,r ) are well-founded. Define ET2( u 1 , . . . , u n ) as the (> KB2,u1 )-sorted sequence of elements in ET( u 1 , . . . , u n ). Then consider ET2( u 1 ), ET2( u 1 , u 2 ), ET2( u 1 , u 2 , u 3 ), . . . . Define > KB,r as the Kleene-Brouwer relation for > KB1,r and the set of (> KB2,r )-sorted finite sequences of elements in MS r . This definition is a key idea. By this definition, we can show the most difficult step in this proof:

ET2( u 1 ) > KB,u1 ET2( u 1 , u 2 ) > KB,u1 ET2( u 1 , u 2 , u 3 ) > KB,u1 . . . .

Since (> KB,u1

) is well-founded by Kleene-Brouwer theorem, we have contradiction. Hence we have shown

u 1 > Π u 2 > Π u 3 > Π . . . terminates.
In general we need classical logic to derive induction principle from wellfoundedness, but the idea we have explained will work well for showing induction principle in intuitionistic logic.

Proof of Podelski-Rybalchenko Theorem for Induction

This subsection gives a proof of Podelski-Rybalchenko Theorem for Induction.

The next lemma shows that induction principle for each relation implies induction principle for monotonically-colored sequences. This lemma can be proved by refining Lemma 6.4 (1) of [START_REF] Berardi | An intuitionistic version of Ramseys Theorem and its use in Program Termination[END_REF] from second-order logic to first-order logic. The proof is given in [START_REF] Berardi | Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic[END_REF].

Lemma 2.5 If HA Ind(DT(U, > Ri ), > ext ) for all 1 ≤ i ≤ k, then HA ∀r ∈ U.Ind(MS r , > ext ).
Next we create Kleene-Brouwer relations > KB1,r and > KB2,r for monotonically-colored sequences beginning with r. Then we consider the set of (> KB2,r )-sorted finite sequences of monotonically-colored finite sequences beginning with r. It is a lifted tree. Then, by induction principle for MS, the lifted tree is well-founded with the one-step extension relation. The Kleene-Brouwer relation for the lifted tree and > KB1,r gives us > KB,r for the lifted tree. Since an Erdös tree is in the lifted tree, this will later show induction principle for Erdös trees.

Definition 2.6 For u ∈ U , we define > u,Left for U by:

u 1 > u,Left u 2 if u > Rj u 1 , u > R l u 2 ,
and j < l for some j, l.

We define > KB1,r for MS r as the KB relation for MS r ⊆ U <ω and (> u,Left ) ⊆ U 2 for all u ∈ U .

For u ∈ U , we define > u,Right for U by:

u 1 > u,Right u 2 if u 1 < u,Left u 2 .
We define > KB2,r for MS r as the KB relation for MS r ⊆ U <ω and (> u,Right ) ⊆ U 2 for all u ∈ U .

We define > KB,r for DS(MS r , > KB2,r ) r as the KB relation for DS(MS r , > KB2,r ) r ⊆ MS <ω r and > KB1,r .

> u,Left is the left-to-right-decreasing order of children of u in some ordered tree of U in which the edge label R i is put to an edge (x, y) such that x > Ri y, each parent has at most one child of the same edge label, and children are ordered by their edge labels with R 1 < . . . < R k . Similarly > u,Right is the right-to-leftdecreasing order of children of u in the ordered tree.

Definition 2.7 For u ∈ U ⊆ N , finite T ⊆ MS such that ∀ρ ∈ T.∀v ∈ ρ.(v > R1+...+R k u), and for σ ∈ T , we define the function insert by:

insert(u, T, σ) = insert(u, T, σ * v ) if last(σ) > Ri u, v = µv.(σ * v ∈ T ∧ last(σ) > Ri v), T ∪ {σ * u } otherwise,
where µv.F (v) denotes the least element v with the natural number order such that F (v). Formally insert(u, T, σ) = T is an abbreviation of some HA-formula G(u, T, σ, T ). It is the same for ET below.

For x ∈ DT(U, > R1+...+R k ) -{ }, we define ET(x) ⊆ MS by ET( u ) = { u }, ET(x * u ) = insert(u, ET(x), first(x) ) if x = .
Note that insert(u, T, σ) adds a new element u to the set T at some position below σ to obtain a new set. ET(x) is an Erdös tree obtained from the decreasing transitive sequence x.

The next lemma (1) states a new element is inserted at a leaf. It is proved by induction on the number of elements in T . The claim [START_REF] Baelde | Infinitary Proof Theory: the Multiplicative Additive Case[END_REF] states that edges from a parent to its children have different colors. It is proved by induction on the length of x. ∈ ρ for all ρ ∈ T , σ = x 0 , . . . , x n-1 , x i > Rj x i+1 implies x i > Rj u for all i < n -1, and insert(u, T, σ) = T , then there is some ρ ∈ T σ such that ρ * u ∈ MS, T = T + {ρ * u }, and ρ * u is a maximal sequence in T .

(

) If σ * u, u 1 * ρ 1 , σ * u, u 2 * ρ 2 ∈ ET(x), u > Ri u 1 , and u > Ri u 2 , then u 1 = u 2 . 2
Definition 2.9 For x ∈ DT(U, > R1+...+R k ) -{ }, we define ET2(x) ≡ x 0 , . . . , x n-1 where {x 0 , . . . , x n-1 } = ET(x) and ∀i < n -1.(x i > KB2,first(x) x i+1 ).

Note that > KB2,first(x) is a total order on ET(x) by Lemma 2.8 (2). ET2(x) is the decreasing sequence of all nodes in the Erdös tree ET(x) ordered by > KB2,first(x) .

The next lemma shows ET2 is monotone. It is the key property of reduction in Lemma 2.11. The next lemma shows that induction for decreasing transitive sequences is reduced to induction for Erdös trees with > KB,r .

Lemma 2.11 HA ∀r ∈ U.Ind(ET2(DT(U, > R1+...+R k ) r ), > KB,r ) implies HA Ind(DT(U, > R1+...+R k ), > ext ).
Proof Sketch. In order to show Ind(DT(U, > R1+...+R k ), > ext ) for F , define Gy ≡ ∀z ∈ DT(z = → ET2(z) = y → F z) and use Ind(ET2(DT(U, > R1+...+R k ) r ), > KB,r ) for G and Lemma 2.10. The proof is in [START_REF] Berardi | Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic[END_REF]. 2

The next lemma shows induction holds when we restrict the universe. The proof is in [START_REF] Berardi | Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic[END_REF].

Lemma 2.12 HA Ind(U, >) and HA V ⊆ U imply HA Ind(V, >).

The next lemma shows induction is implied from induction for decreasing sequences. The proof is in [START_REF] Berardi | Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic[END_REF]. Lemma 2.13 HA Ind(DS(U, >), > ext ) implies HA Ind(U, >).

The next lemma shows induction for a power of a relation implies induction for the relation. The proof is in [START_REF] Berardi | Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic[END_REF].

Lemma 2.14 HA Ind(U, > n ) implies HA Ind(U, >).

Define

Trans(U, > R ) ≡ ∀xyz ∈ U (x > R y ∧ y > R z → x > R z), Decide(U, > R ) ≡ ∀xy ∈ U (x > R y ∨ ¬(x > R y)).
The next theorem states that if some powers of relations > Ri have induction principle, > Ri are decidable and their union is transitive, then the union has induction principle. This theorem is the same as Theorem 6.1 in [START_REF] Berardi | Equivalence of Inductive Definitions and Cyclic Proofs under Arithmetic[END_REF] except HA and the decidability condition Decide(U, > Ri ). Proof. We will discuss in HA. By Lemma 2.14, we can replace n i by 1 and obtain Ind(U, > Ri ). In order to obtain disjoint relations, we define > R 1 as

> R1 and > R i+1 as (> Ri+1 ) -(> R 1 ) -. . . -(> R i ). Then (> R 1 ), . . . , (> R k ) are disjoint and ∀xy ∈ U (x > R1∪...∪R k y → x > R 1 +...+R k y) by Decide(U, > Ri ) for 1 ≤ i ≤ k. Since (> R i ) ⊆ (> Ri ), Ind(U, > R i ).
For simplicity, from now on we write > Ri for > R i in this proof. We will show Ind(U, > R1+...+R k ).

From Ind(U, > Ri ), by replacing induction on elements by induction on sequences, we have Ind(DT(U, > Ri ), > ext ) for 1 ≤ i ≤ k. By Lemma 2.5, we have ∀r ∈ U.Ind(MS r , > ext ). Apparently ∀u ∈ U.Ind(U, > u,Left ). By taking U to be U , T to be MS r , and > u to be > u,Left in Theorem 2.3 for > KB1,r , we have ∀r ∈ U.Ind(MS r , > KB1,r ). By Theorem 2.3 for > KB2,r , we have ∀r ∈ U.Ind(MS r , > KB2,r ) similarly. By replacing induction on elements by induction on sequences, we have ∀r ∈ U.Ind(DS(MS r , > KB2,r ), > ext ). Since DS(MS r , > KB2,r ) r is a subset of DS(MS r , > KB2,r ), from Lemma 2.12, we have ∀r ∈ U.Ind(DS(MS r , > KB2,r ) r , > ext ). By taking T to be DS(MS r , > KB2,r ) r , U to be MS r , and (> u ) to be (> KB1,r ) in Theorem 2.3 for > KB,r , we have ∀r ∈ U.Ind(DS(MS r , > KB2,r ) r , > KB,r ). This is a key step of this proof. Since ET2(DT(U, > R1+...+R k ) r ) ⊆ DS(MS r , > KB2,r ) r , by Lemma 2.12, we have ∀r ∈ U.Ind(ET2(DT(U, > R1+...+R k ) r ), > KB,r ). By Lemma 2.11, Ind(DT(U, > R1+...+R k ), > ext ). By Trans(U, > R1+...+R k ), DT(U, > R1+...+R k ) is DS(U, > R1+...+R k ). Hence we have Ind(DS(U, > R1+...+R k ), > ext ). From Lemma 2.13, by replacing induction on sequences by induction on elements, we have Ind(U, > R1+...+R k ). 2 3 Cyclic Proofs

Intuitionistic Martin-Löf 's Inductive Definition System LJID

We define an intuitionistic Martin-Löf's inductive definition system, called LJID.

The language of LJID is determined by a first-order language with inductive predicate symbols. The logical system LJID is determined by production rules for inductive predicate symbols. These production rules mean that the inductive predicate denotes the least fixed point defined by these production rules.

We assume the first order terms t, u, . . .. We assume ∀x and ∃y are less tightly connected than other logical connectives. To save space, we sometimes write P xy and F xy for P (x, y) and F (x, y).

For example, the production rules of the inductive predicate symbol N are

N 0 N x N sx Γ, A A (Axiom) Γ ∆ Γ ∆ (Wk) (Γ ⊆ Γ, ∆ ⊆ ∆) Γ F Γ, F ∆ Γ ∆ (Cut) Γ ∆ Γ θ ∆θ (Subst) Γ F Γ, ¬F (
Γ F 0 Γ, F x F sx Γ, N t F t
This elimination rule describes mathematical induction principle. The inference rules are given in Figure 1 where for (P i R) we assume the production rule

Q 1 - → u 1 . . . Q n - → u n P 1 - → t 1 . . . P m - → t m P - → t
and for (Ind P j ) we assume a predicate F i for each P i and the minor premises are defined as

Γ, Q i1 - → u i1 , . . . , Q ini - → u ini , F 1 - → t i1 , . . . , F imi - → t imi F i - → t i
for each production rule

Q i1 - → u i1 . . . Q ini - → u ini P 1 - → t i1 . . . P imi - → t imi P i - → t i
Note that the antecedents and the succedents are sets and the succedent is empty or a formula. The system LJID is the same as the system obtained from classical Martin-Löf's inductive definition system LKID defined in [START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF] by restricting every sequent to intuitionistic sequents and replacing (→L), (∨R), and (Ind P j ) accordingly. The provability of the system LJID is the same as that of the natural deduction system given in [START_REF] Martin-Löf | Haupstatz for the intuitionistic theory of iterated inductive definitions[END_REF].

Cyclic Proof System CLJID ω

An intuitionistic cyclic proof system, called CLJID ω , is defined as the system obtained from classical cyclic proof system CLKID ω defined in [START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF] by restricting every sequent to intuitionistic sequents and replacing (→L) and (∨R) in the same way as LJID. Note that the global trace condition in CLJID ω is the same as that in CLKID ω (Definition 5.5 of [START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF]).

Namely, the inference rules of CLJID ω are obtained from LJID by replacing (IndP j ) by case distinctions

Γ, P - → u ∆ (CaseP )
where the case distinctions are

Γ, - → u = - → t , Q 1 - → u 1 , . . . , Q n - → u n , P 1 - → t 1 , . . . , P m - → t m ∆
for each production rule

Q 1 - → u 1 . . . Q n - → u n P 1 - → t 1 . . . P m - → t m P - → t
A cyclic proof in CLJID ω is defined by (1) allowing a bud as an open assumption and requiring a companion for each bud, (2) requiring the global trace condition.

The global trace condition [START_REF] Brotherston | Automated Cyclic Entailment Proofs in Separation Logic[END_REF][START_REF] Brotherston | Sequent calculus proof systems for inductive definitions[END_REF] is the condition that for every infinite path in the infinite unfolding of a given cyclic proof, there is a trace that passes main formulas of case rules infinitely many times. The global trace condition ensures that when we think some measure by counting case rules, the measure of a bud is smaller than that of the companion. For example, in the next example the companion (a) uses P x0y, but the bud (a) uses P x0y where x is x and x < x, so their actual meanings are different even though they are of the same form. The global trace condition guarantees the soundness of a cyclic proof system.

An example of a cyclic proof (trivial steps are omitted) is as follows: where the mark (a) denotes the bud-companion relation, and the production rules are P 0yy

0 = 0 x = 0,

P xyz P (sx)y(sz)

Note that the predicate P is addition on natural numbers and the proof is, essentially, deriving the arithmetic identity x + 0 = x.

We call an atomic formula an inductive atomic formula when its predicate symbol is an inductive predicate symbol.

Cyclic Proofs for Coinductive Predicates

This subsection shows how we can use a cyclic proof system to formalize coinductive predicates. Since a coinductive predicate is a dual of an inductive predicate, and sequent calculus is symmetric for this dual, we can construct a cyclic proof system for coinductive predicates. For example, for stream predicates we can define a cyclic proof system µνLK from CLKID ω as follows:

(1) Add function symbols head, tail, and the pair , with the axioms x, y = x , y → x = x ∧ y = y and x = head x, tail x , and a coinductive predicate symbol P with its coproduction rule Qyx P x P y, x co which means P is defined coinductively by this rule. Note that P represents the set of streams x 0 , x 1 , x 2 , . . . such that Q(x i , x i+1 , x i+2 , . . . ) for all i. (2) Add the inference rules (P R) and (Case P ) in the same way as CLKID ω , namely,

Γ, t = y, x , Qyx, P x ∆ Γ, P t ∆ (Case P ) Γ Qyx, ∆ Γ P x, ∆ Γ P y, x , ∆ (P R) (3)
We call an atomic formula a coinductive atomic formula when its predicate symbol is a coinductive predicate symbol. We define a cotrace as a sequence of coinductive atomic formulas in the succedents of a path such that two atomic formulas are related by an inference rule in a similar way to a trace defined in [START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF]. The global trace and cotrace condition is the condition that for every infinite path in the infinite unfolding of a given cyclic proof, the path contains either a trace that passes main formulas of case rules infinitely many times, or a cotrace that passes main formulas of rules (P R) infinitely many times.

(4) A cyclic proof is a preproof that satisfies the global trace and cotrace condition.

Example. We define the bit stream predicate BS by the following coproduction rules:

Bit y BS x BS y, x co where Bit is an ordinary predicate symbol with the axiom Bit x ↔ x = 0∨x = 1.

The inference rules from this production rule are:

Γ Bit y, ∆ Γ BS x, ∆ Γ BS y, x , ∆ (BS R) Γ, t = y, x , Bit y, BS x ∆ Γ, BS t ∆ (Case BS)
Then we can show x = 0, x BS x, namely, the zero stream is a bit stream, as follows (trivial steps are omitted):

x = 0, x Bit 0 (a) x = 0, x BS x x = 0, x BS 0, x (BS R) (a) x = 0, x BS x
where (a) denotes the bud-companion relation. The cyclic proof system µνLK is sound for the standard model.

Theorem 3.1 If a sequent is provable in µνLK, then it is true in the standard model where a coinductive predicate is interpreted as the greatest fixed point that satisfies the coproduction rules.

Proof sketch. We add an ordinary predicate symbol Q with the axiom Qyx ↔ ¬Qyx and add an inductive predicate symbols P with the production rules Q(head x)(tail x)

P x P (tail x) P x
In the standard model, P is the greatest solution of the equation

P x ↔ ∃yx (x = y, x ∧ Qyx ∧ P x )
and P is the least solution of the equation

P x ↔ Q(head x)(tail x) ∨ P (tail x).
By putting ¬ on both sides of the equation for P and taking y and x to be head x and tail x, we can show ¬P is a solution of the equation for P . Hence P x→¬P x is true. In the same say by putting ¬ on both sides of the equation for P , and using x = headx, tailx , we can show ¬ P is a solution of the equation for P . Hence ¬ P x → P x is true. Therefore P x ↔ ¬P x is true.

We define a transformation ( ) -for a sequent and a proof, in order to replace P by P . For a sequent J, we define J -by replacing P by ¬ P and then moving an atomic formula ¬ P t of the antecedent to P t of the succedent and moving an atomic formula ¬ P t of the succedent to P t of the antecedent.

Given a cyclic proof π, we define π -by replacing each sequent J by J -and then replacing (P R) by

Γ -Qyx , ∆ - Γ -, Qyx ∆ -Γ -, P x ∆ - Γ -, P y, x ∆ - (Case P ) (trivial steps are omitted)
and replacing (CaseP ) by

Γ -, x = y, x , Qyx P x , ∆ - Γ -, x = y, x Qyx , P x , ∆ - Γ -, x = y, x Qyx , P x, ∆ -( P R) Γ -, x = y, x P x, ∆ - ( P R) Γ -P x, ∆ - (trivial steps are omitted)
Then a cotrace in π corresponds to a trace in π -. Hence π -is a cyclic proof of J -in CLKID ω when π is a cyclic proof of J in µνLK. By the soundness of CLKID ω , J -is true in the standard model. Since P x ↔ ¬P x is true, J is true in the standard model where P is interpreted as the greatest fixed point. 2

Equivalence between LJID and CLJID ω

This section studies the equivalence between CLJID ω and LJID.

Countermodel and Addition of Heyting Arithmetic

This subsection gives a countermodel and adds arithmetic to the logical systems. The counterexample given in [START_REF] Berardi | Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proof System[END_REF] also shows that the equivalence between CLJID ω and LJID does not hold in general, because the proof of the statement H in [START_REF] Berardi | Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proof System[END_REF] is actually in CLJID ω , and LJID does not prove H since LKID does not prove H. This gives us the following theorem (it is not new in the sense [START_REF] Berardi | Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proof System[END_REF] immediately implies it). Theorem 4.1 There are some signature and some set of production rules for which the provability of CLJID ω is not the same as that of LJID.

There is a possibility of the equivalence under some conditions. We will show the equivalence holds by adding arithmetic to both systems.

We add arithmetic to both LJID and CLJID ω . Definition 4.2 CLJID ω + HA and LJID + HA are defined to be obtained from CLJID ω and LJID by adding Heyting arithmetic. Namely, we add constants and function symbols 0, s, +, ×, the inductive predicate symbol N , the productions for N , and Heyting axioms:

N 0 N x N sx N x → sx = 0, N x ∧ N y → sx = sy → x = y, N x → x + 0 = x, N x ∧ N y → x + sy = s(x + y), N x → x × 0 = 0, N x ∧ N y → x × sy = x × y + x.

Equivalence Theorem

In this subsection we state the equivalence theorem and explains proof ideas. First we assume a new inductive predicate symbol P for each inductive predicate symbol P and define the production rules of P in the same way as [START_REF] Berardi | Equivalence of Inductive Definitions and Cyclic Proofs under Arithmetic[END_REF].

Definition 4.3 We define the production rule of

P Q 1 - → u 1 . . . Q n - → u n v > v 1 P 1 - → t 1 v 1 . . . v > v m P m - → t m v m N v P - → t v
for each production rule of

P Q 1 - → u 1 . . . Q n - → u n P 1 - → t 1 . . . P m - → t m P - → t
where v, v 1 , . . . , v m are fresh variables.

We write LJID + HA + (Σ, Φ) for the system LJID + HA with the signature Σ and the set Φ of production rules. Similarly we write CLJID ω + HA + (Σ, Φ). For simplicity, in Φ we write only P for the set of production rules for P . We define Σ N = {0, s, +, ×, <, N } and Φ N = {N }. We write P for (P ) .

The next theorem shows the equivalence of LJID + HA and CLJID ω + HA with signatures.

) Let Σ = Σ N ∪ { - → Q , - → P , - → P } and Φ = Φ N ∪ { - → P , - → P }.
Then the provability of CLJID ω + HA + (Σ, Φ) is the same as that of LJID + HA + (Σ, Φ).

We explain our ideas of proofs of this theorem. [START_REF] Berardi | Equivalence of Inductive Definitions and Cyclic Proofs under Arithmetic[END_REF] shows the equivalence between classical systems by using classical Podelski-Rybalchenko theorem for induction. This proof goes well even if we replace classical systems by intuitionistic systems except that we have to replace classical Podelski-Rybalchenko theorem for induction by intuitionistic Podelski-Rybalchenko theorem for induction. Since we proved intuitionistic Podelski-Rybalchenko theorem for induction in Theorem 2.15, by combining them, we can show the equivalence between LJID and CLJID ω .

Proof Transformation

This section gives the proof of the equivalence. More detailed discussions are given in [START_REF] Berardi | Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic[END_REF]. We define proof transformation from CLJID ω + HA to LJID + HA. First we will define stage numbers and path relations, and then define proof transformation using them.

For notational convenience, we assume a cyclic proof Π in this section. Let the buds in Π be J 1i (i ∈ I) and the companions be J 2j (j ∈ K). Assume f : I → K such that the companion of a bud J 1i is J 2,f (i) .

Stage Numbers for Inductive Definitions

In this subsection, we define and discuss stage transformation.

We introduce a stage number to each inductive atomic formula so that the argument of the formula comes into the inductive predicate at the stage of the stage number. This stage number will decrease by a progressing trace. A proof in LJID + HA will be constructed by using the induction on stage numbers.

First we give stage transformation of an inductive atomic formula. We assume a fresh inductive predicate symbol P for each inductive predicate symbol P and we call it a stage-number inductive predicate symbol.

(Γ ∆) • - → v by (Γ ) • - → v ∆ • .
We write (a i ) i∈I for the sequence of elements a i where i varies in I. We extend the notion of proofs by allowing open assumptions. We write Γ CLJID ω +HA ∆ with assumptions (J i ) i∈I when there is a proof with assumptions (J i ) i∈I and the conclusion Γ ∆ in CLJID ω + HA. Definition 5.1 In a path π in a proof, we define Ineq(π) as the set of the forms v > v and v = v for any stage numbers v, v eliminated by every case distinction in π.

The proof of the next proposition gives stage transformation of a proof into a proof of the stage transformation of the conclusion of the original proof. We write Π • for the stage transformation of Π. Γ CLJID ω +HA ∆ with assumptions (Γ i ∆ i ) i∈I without any buds, then for some fresh variables ( -

→ v i ) i∈I we have (Γ ) • - → v CLJID ω +HA ∆ • with assumptions (Ineq(π i ), (Γ i ) • - → v i ∆ • i
) i∈I without any buds, where π i is the path from the conclusion to the assumption

(Γ i ) • - → v i ∆ • i .

Path Relation

In this section, we will introduce path relations and discuss them. We assume a subproof Π j of Π such that it does not have buds, its conclusion is J 2j and its assumptions are J 1i (i ∈ I j ).

For J in Π • j , we define J as v 1 , . . . , v k where J is Γ

• v1...v k ∆ • .
For a path π from the conclusion to an assumption in Π • j , we write π for the corresponding path in Π. We extend this notation to a finite composition of π's. By the correspondence (ˇ), a stage-number inductive atomic formula in Π • j corresponds to an inductive atomic formula in Π, and a path, a trace, and a progressing trace in Π • j correspond to the same kind of objects in Π. where J 1 and J 2 are the top and bottom sequents of π respectively, J1 and J2 are those of the path π, F (q 1 , q 2 ) is that there is some progressing trace from the q 2 -th atomic formula in J2 to the q 1 -th atomic formula in J1 , G(q 1 , q 2 ) is that there is some non-progressing trace from the q 2 -th atomic formula in J2 to the q 1 -th atomic formula in J1 .

We define B 1 as the set of paths from conclusions to assumptions in Π • j (j ∈ K). We define B as the set of finite compositions of elements in B 1 such that if π ∈ B then π is a path in the infinite unfolding of Π. Definition 5.4 For π ∈ B, define x > π y by x > π y ≡ (x) 0 = j ∧ (y) 0 = f (i) ∧ (x) 1 >π (y) 1 , where J 1i is the top sequent of π, and J 2j is the bottom sequent of π.

Note that ( ) 0 and ( ) 1 are operations for a number that represents a sequence of numbers defined in Section 3. The first element is a companion number. The next lemma is the only lemma that uses the global trace condition.

Lemma 5.6 For all π ∈ B, there is n > 0 such that HA Ind(U, > n π ).

We define > Π as {> π | π ∈ B}. Note that > Π is transitive, since the top sequent of π 1 is the bottom sequent of π 2 by the first element, and ((> π1 ) • (> π2 )) ⊆ (> π1π2 ).

Proof Transformation

This section gives proof transformation.

The next lemma shows we can replace (Case) rules of CLJID ω + HA by (Ind) rules of LJID + HA. Lemma 5.7 If there is a proof with some assumptions and without any buds in CLJID ω + HA, then there is a proof of the same conclusions with the same assumptions in LJID + HA.

The next is a key lemma and shows each bud in a cyclic proof is provable in LJID + HA, which is proved by using Theorem 2.15.

Lemma 5.8 For every bud J of a proof in CLJID ω + HA and fresh variables -→ v , (J) • -→ v is provable in LJID + HA.

The next is the main proposition stating that a cyclic proof is transformed into an (LJID + HA)-proof with stage-number inductive predicates.

Conclusion

We have first shown intuitionistic Podelski-Rybalchenko theorem for induction in HA, and we have secondly shown the provability of the intuitionistic cyclic proof system is the same as that of the intuitionistic system of Martin-Lof's inductive definitions when both systems contain HA. We have also constructed a cyclic proof system µνLK for stream predicates.

One future work would be to construct a cyclic proof system for coinductive predicates in a general way and show the equivalence between the cyclic proof system and other logical systems for coinductive predicates.

Lemma 2 . 8 ( 1 )

 281 For u ∈ U , T ⊆ MS, and σ ∈ T , if u /

Lemma 2 .

 2 [START_REF] Brotherston | Automated Cyclic Entailment Proofs in Separation Logic[END_REF] HA ∀r ∈ U.∀x, y ∈ DT(U, > R1+...+R k ) r .(x > ext y → ET2(x) > KB,r ET2(y)).Proof. Fix r ∈ U and x, y ∈ DT(U, > R1+...+R k ) r and assume x > ext y. Let y = x * u . Then ET(y) = insert(u, ET(x), r ). By Lemma 2.8 (1), we have σ such that ET(y) = ET(x) + {σ * u }. Then we have two cases: Case 1. last(ET2(x)) > KB2,r σ * u .Then ET2(y) = ET2(x) * σ * u . By definition, ET2(x) > KB,r ET2(y). Case 2. σ * u > KB2,r τ for some τ ∈ ET2(x). Let ρ be the next element of σ * u in ET2(y). Then ET2(x) = α * ρ * β and ET2(y) = α * σ * u , ρ * β. By definition of ET2, σ * u > KB2,r ρ. Since σ * u is maximal in ET(y) by Lemma 2.8 (1), there is no α = such that σ * u * α = ρ. Hence σ * u < KB1,r ρ. Hence ET2(x) > KB,r ET2(y). 2

Theorem 2 . 15 (

 215 Podelski-Rybalchenko Theorem for Induction) If HA Ind(U, > n1 R1 ), HA Decide(U, > R1 ), . . . , HA Ind(U, > n k R k ), HA Decide(U, > R k ),and HA Trans(U, > R1+...+R k ), then Ind(U, > R1+...+R k ).

Fig. 1 .

 1 Fig. 1. Inference Rules

  y = 0, P x0y x = y (a)P x0y x = y P x 0y x = y (Subst) P x 0y , x = sx , y = sy x = y (Wk) P x 0y , x = sx , y = sy sx = sy P x 0y , x = sx , y = sy x = y (a)P x0y x = y (Case P )

Theorem 4 . 4 (

 44 Equivalence of LJID + HA and CLJID ω + HA

Proposition 5 . 2 (

 52 Stage Transformation) For any fresh variables -→ v , if

Definition 5 . 3

 53 For a finite composition π of paths in {Π • j | j ∈ K} such that π is a path in the infinite unfolding of Π, we define the path relation >π byx >π y ≡ |x| = | J 2 | ∧ |y| = | J 1 | ∧ F (q1,q2) (x) q2 > (y) q1 ∧ G(q1,q2) (x) q2 = (y) q1

Lemma 5 . 5

 55 {> π | π ∈ B} is finite. Proof. Define C n as {> π1...πm | m ≤ n, π i ∈ B 1 }. Since > π is a relation on N × N ≤pwhere p is the maximum number of inductive atomic formulas in the antecedents of Π, there is L such that |C n | ≤ L for all n. Then we have the leastn such that C n+1 = C n . Then |{> π | π ∈ B}| = |C n |. 2

  Secondly we give stage transformation of a production rule. We transform the production of P into the production of P given in Definition 4.3.Next we give the stage transformation of a sequent. For given fresh variables -→ v , we transform a sequent J into J • -→ v defined as follows. We define Γ • as the set obtained from Γ by replacing P (

	-→ t ) by ∃vP ( -→ t , v). For fresh variables -→ v ,
	we define (Γ ) • -→ v as the sequent obtained from Γ • by replacing the i-th element of the form ∃vP ( -→ t , v) in the sequent Γ • by P ( -→ t , v i ). We define (Γ ∆) • by
	Γ • ∆ • , and define
	P ( → -t , v) means that the t comes into P at the stage v. We transform P ( -→ -→ t ) into ∃vP ( -→ t , v). We call a variable v a stage number of element -→ t when P ( -→ t , v). P ( -→ t ) and ∃vP ( -→ t , v)
	will become equivalent by inference rules introduced by the transformation of production rules. We call P ( -→ t , v) a stage-number inductive atomic formula.

These production rules mean that N denotes the smallest set closed under 0 and s, namely the set of natural numbers.The inference rules of LJID contains the introduction rules and the elimination rules for inductive predicates, determined by the production rules. These rules describe that the predicate actually denotes the least fixed point. In particular, the elimination rule describes the induction principle.For example, the above production rules give the introduction rulesΓ N 0 Γ N x Γ N sx

Γ ¬F (¬R) Γ, F ∆ Γ, G ∆ Γ, F ∨ G ∆ (∨L) Γ F Γ F ∨ G (∨R l ) Γ G Γ F ∨ G (∨Rr) Γ, F, G ∆ Γ, F ∧ G ∆ (∧L) Γ F Γ G Γ F ∧ G (∧R) Γ F Γ, G ∆ Γ, F → G ∆ (→L) Γ, F G Γ F → G (→R) Γ, F [x := t] ∆ Γ, ∀xF ∆ (∀L) Γ F Γ ∀xF (∀R) (x / ∈ FV(Γ )) Γ, F ∆ Γ, ∃xF ∆ (∃L) (x / ∈ FV(Γ, ∆)) Γ F [x := t] Γ ∃xF (∃R) Γ [x := t] ∆[x := t] Γ [x := u], t = u ∆[x := u] (= L) Γ t = t (= R) minor premises Γ, Pj -→ u Fj -→ u (Ind Pj) Γ Q1 -→ u 1 . . . Γ Qn -→ u n Γ P1 -→ t 1 . . . Γ Pm -→ t m Γ P -→ t (P R)

The next shows conservativity for stage-number inductive predicates.

Proposition 5.10 (Conservativity of N and

Proof of Theorem 4.4. (1) LJID + HA + (Σ, Φ) to CLJID ω + HA + (Σ, Φ).

For this claim, we can obtain a proof from the proof of Lemma 7.5 in [START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF] by restricting every sequent into intuitionistic sequents and replacing LKID+(Σ, Φ) and CLKID ω + (Σ, Φ) by LJID + (Σ, Φ) and CLJID ω + (Σ, Φ) respectively.

(

. By Proposition 5.9, J is provable in LJID + HA + (Σ , Φ ). By Proposition 5.10, J is provable in LJID + HA + (Σ, Φ). 2

Related Work

The conjecture 7.7 in [START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF] (also in [START_REF] Brotherston | Sequent calculus proof systems for inductive definitions[END_REF]) is that the provability of LKID is the same as that of CLKID ω . In general, the equivalence was proved to be false in [START_REF] Berardi | Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proof System[END_REF], by showing a counterexample. However, if we restrict both systems to only the natural number inductive predicate and add Peano arithmetic to both systems, the equivalence was proved to be true in [START_REF] Simpson | Cyclic Arithmetic is Equivalent to Peano Arithmetic[END_REF], by internalizing a cyclic proof in ACA 0 and using some results in reverse mathematics. [START_REF] Berardi | Equivalence of Inductive Definitions and Cyclic Proofs under Arithmetic[END_REF] proved that if we add Peano arithmetic to both systems, CLKID ω and LKID are equivalent, namely the equivalence is true under arithmetic, by showing arithmetical Ramsey theorem and Podelski-Rybalchenko theorem for induction.

This paper shows that similar results as shown in [START_REF] Berardi | Equivalence of Inductive Definitions and Cyclic Proofs under Arithmetic[END_REF] hold for intuitionistic logic, namely, the provability of LJID is the same as that of CLJID ω if we add Heyting arithmetic to both systems.

The results of this paper immediately give another proof to the equivalence under arithmetic for classical logic shown in [START_REF] Berardi | Equivalence of Inductive Definitions and Cyclic Proofs under Arithmetic[END_REF] by using the fact Γ CLKID ω +PA ∆ implies E, Γ, ¬∆ CLJID ω +HA for some finite set E of excluded middles.

By taking -→ Q and -→ P to be empty in Theorem 4.4, we have conservativity of CLJID ω + HA over LJID + HA with only the inductive predicate N , which answers the question (iv) in Section 7 of [START_REF] Simpson | Cyclic Arithmetic is Equivalent to Peano Arithmetic[END_REF].

[17] presented the first logical system for inductive/coinductive predicates. [START_REF] Niwiński | Games for the µ-calculus[END_REF] also gave a similar system. They are both based on a finite system with unfold and fold, and limited to propositional logic. [START_REF] Walukiewicz | Completeness of Kozens axiomatisation of the propositional µcalculus[END_REF] showed the completeness of the system by using a cyclic proof system but it is also limited to propositional logic. [START_REF] Fortier | Cuts for circular proofs: semantics and cutelimination[END_REF][START_REF] Baelde | Infinitary Proof Theory: the Multiplicative Additive Case[END_REF] investigated cyclic proof systems for inductive/coinductive predicates. [START_REF] Doumane | Constructive completeness for the linear-time µ-calculus[END_REF][START_REF] Afshari | Cut-free Completeness for Modal Mu-Calculus[END_REF] also used cyclic proof systems for inductive/coinductive predicates to show some completeness results. But these systems are all limited to propositional logic.